Coq: destruct (co) hypothèse inductive sans perte d'information

Question

Considérer le développement suivant:

Require Import Relation RelationClasses. 

Set Implicit Arguments. 

CoInductive stream (A : Type) : Type := 
| scons : A -> stream A -> stream A. 

CoInductive stream_le (A : Type) {eqA R : relation A} 
         `{PO : PartialOrder A eqA R} : 
         stream A -> stream A -> Prop := 
| le_step : forall h1 h2 t1 t2, R h1 h2 -> 
      (eqA h1 h2 -> stream_le t1 t2) -> 
      stream_le (scons h1 t1) (scons h2 t2). 

Si j'ai une hypothèse stream_le (scons h1 t1) (scons h2 t2), il serait raisonnable que la tactique destruct pour le transformer en une paire d'hypothèses R h1 h2 et eqA h1 h2 -> stream_le t1 t2. Mais ce n'est pas ce qui se passe, car destruct perd des informations chaque fois que vous faites quelque chose de non-trivial. Au lieu de cela, de nouveaux termes h0, h3, t0, t3 sont introduits dans le contexte, sans rappel qu'ils sont respectivement égaux à h1, h2, t1, t2.

Je voudrais savoir s'il existe un moyen rapide et facile de faire ce genre de "smart destruct". Voici ce que j'ai en ce moment:

Theorem stream_le_destruct : forall (A : Type) eqA R 
    `{PO : PartialOrder A eqA R} (h1 h2 : A) (t1 t2 : stream A), 
    stream_le (scons h1 t1) (scons h2 t2) -> 
    R h1 h2 /\ (eqA h1 h2 -> stream_le t1 t2). 
Proof. 
    intros. 
    destruct H eqn:Heq. 
    remember (scons h1 t1) as s1 eqn:Heqs1; 
    remember (scons h2 t2) as s2 eqn:Heqs2; 
    destruct H; 
    inversion Heqs1; subst; clear Heqs1; 
    inversion Heqs2; subst; clear Heqs2. 
    split; assumption. 
Qed. 

Answer 1

En effet, inversion fait fondamentalement ce que vous voulez, mais comme Arthur l'a souligné, c'est un peu instable, principalement en raison des différentes étapes de congruence.

Sous le capot, inversion appelle simplement une version de destruct, mais en gardant en tête quelques égalités. Comme vous l'avez bien découvert, la correspondance de pattern dans Coq va "oublier" les arguments des constructeurs, sauf si ce sont des variables, alors toutes les variables sous la portée seront instanciées.

Qu'est-ce que cela signifie? Cela signifie que, afin de détruire correctement un I : Idx -> Prop inductif, vous voulez obtenir votre objectif de la forme: I x -> Q x, de sorte que la destruction du I x permettra également d'affiner le x en Q. Ainsi, une transformation standard pour un I term inductif et l'objectif Q (f term) consiste à le réécrire à I x -> x = term -> Q (f x). Ensuite, en détruisant I x, vous obtiendrez instancié à l'index approprié. Dans cet esprit, il peut être judicieux de mettre en œuvre l'inversion manuellement en utilisant la tactique case: de Coq 8.7;

From Coq Require Import ssreflect. 
Theorem stream_le_destruct A eqA R `{PO : PartialOrder A eqA R} (h1 h2 : A) (t1 t2 : stream A) : 
    stream_le (scons h1 t1) (scons h2 t2) -> 
    R h1 h2 /\ (eqA h1 h2 -> stream_le t1 t2). 
Proof. 
move E1: (scons h1 t1) => sc1; move E2: (scons h2 t2) => sc2 H. 
by case: sc1 sc2/H E1 E2 => h1' h2' t1' t2' hr ih [? ?] [? ?]; subst. 
Qed. 

Vous pouvez lire le manuel pour plus de détails, mais essentiellement avec la première ligne, nous créons les égalités dont nous avons besoin; ensuite, dans la seconde nous pouvons détruire le terme et obtenir les instantiations appropriées pour résoudre le but. Un bon effet de la tactique case: est que, contrairement à la destruction, elle va essayer de nous empêcher de détruire un terme sans d'abord mettre ses dépendances dans la portée.

Answer 2

appel destruct ne sera pas directement vous donner ce que vous voulez. Vous devez utiliser inversion à la place.

Theorem stream_le_destruct : forall h1 h2 t1 t2, 
    stream_le (scons h1 t1) (scons h2 t2) -> 
    h1 <= h2 /\ (h1 = h2 -> stream_le t1 t2). 
Proof. 
    intros. 
    inversion H; subst; clear H. 
    split; assumption. 
Qed. 

Malheureusement, la tactique inversion est assez mal comportés, car il a tendance à générer beaucoup d'hypothèses d'égalité fausses, ce qui rend difficile de les nommer de manière cohérente. Une alternative (un peu lourde, certes) consiste à utiliser inversion uniquement pour prouver un lemme comme celui que vous avez fait, et appliquer ce lemme dans des preuves au lieu d'appeler inversion.