Prouver une propriété co-inductive (l'ordre lexical est transitif) dans Coq

Question

J'essaye de prouver le premier exemple dans "Practical Coinduction" dans Coq. Le premier exemple est de prouver que l'ordre lexicographique sur les flux infinis d'entiers est transitif.

Je n'ai pas été en mesure de formuler la preuve pour contourner le Guardedness condition

Voici mon développement jusqu'à présent. D'abord juste la définition habituelle des flux infinis. Puis définition de l'ordre lexicographique appelé lex. Et à la fin la preuve ratée du théorème de transitivité.

Require Import Omega. 

Section stream. 
    Variable A:Set. 

    CoInductive Stream : Set := 
    | Cons : A -> Stream -> Stream. 

    Definition head (s : Stream) := 
    match s with Cons a s' => a end. 

    Definition tail (s : Stream) := 
    match s with Cons a s' => s' end. 

    Lemma cons_ht: forall s, Cons (head s) (tail s) = s. 
    intros. destruct s. reflexivity. Qed. 

End stream. 

Implicit Arguments Cons [A]. 
Implicit Arguments head [A]. 
Implicit Arguments tail [A]. 
Implicit Arguments cons_ht [A]. 

CoInductive lex s1 s2 : Prop := 
    is_le : head s1 <= head s2 -> 
      (head s1 = head s2 -> lex (tail s1) (tail s2)) -> 
      lex s1 s2. 


Lemma lex_helper: forall s1 s2, 
     head s1 = head s2 -> 
     lex (Cons (head s1) (tail s1)) (Cons (head s2) (tail s2)) -> 
     lex (tail s1) (tail s2). 
Proof. intros; inversion H0; auto. Qed. 

Voici le lemme que je veux prouver. Je commence par préparer l'objectif afin que je puisse appliquer un constructeur, espérant pouvoir éventuellement utiliser l'hypothèse du cofix.

Lemma lex_lemma : forall s1 s2 s3, lex s1 s2 -> lex s2 s3 -> lex s1 s3. 
    intros s1 s2 s3 lex12 lex23. 
    cofix. 
    rewrite <- (cons_ht s1). 
    rewrite <- (cons_ht s3). 
    assert (head s1 <= head s3) by (inversion lex12; inversion lex23; omega). 
    apply is_le; auto. 

    simpl; intros. inversion lex12; inversion lex23. 
    assert (head s2 = head s1) by omega. 

    rewrite <- H0, H5 in *. 
    assert (lex (tail s1) (tail s2)) by (auto). 
    assert (lex (tail s2) (tail s3)) by (auto). 

    apply lex_helper. 
    auto. 
    repeat rewrite cons_ht. 
    Guarded. 

Comment procéder à partir de là? Merci pour vos conseils!

• EDIT

Merci à Arthur (comme toujours!) Réponse utile et instructif que je pourrais aussi compléter la preuve. Je donne ma version ci-dessous pour référence.

Lemma lex_lemma : forall s1 s2 s3, lex s1 s2 -> lex s2 s3 -> lex s1 s3. 
    cofix. 
    intros s1 s2 s3 lex12 lex23. 
    inversion lex12; inversion lex23. 
    rewrite <- (cons_ht s1). 
    rewrite <- (cons_ht s3). 
    constructor; simpl. 
    inversion lex12; inversion lex23; omega. 
    intros; eapply lex_lemma; [apply H0 | apply H2]; omega. 
Qed. 

J'utilise le lemme cons_ht pour "développer" la valeur de s1 et s3. La définition de lex ici (avec head et tail) est plus proche de la formulation verbatim dans Practical Coinduction. Arthur utilise une technique plus élégante qui permet à Coq d'augmenter automatiquement les valeurs - beaucoup mieux!

Answer 1

Un problème avec votre preuve est que vous avez fait l'appel à cofix trop tard, après s1 s2 s3 avait été introduit. En conséquence, l'hypothèse coinductive que vous obtenez, lex s1 s2, n'est pas très utile: afin de l'appliquer tout en restant prudent, comme vous l'avez mentionné, nous devons le faire après ayant appliqué le constructeur de lex. Cependant, après avoir fait cela, nous aurions besoin de montrer à un certain point que lex (tail s1) (tail s3) tient, où l'hypothèse introduite par cofix ne peut pas faire de bien.

Afin de résoudre ce problème, nous devons effectuer l'appel à cofixavant en introduisant les variables, de sorte que l'hypothèse qu'il produit soit suffisamment générale. Je pris la liberté de reformuler votre définition de lex, de sorte qu'il devient plus facile à manipuler dans une telle preuve:

CoInductive lex : Stream nat -> Stream nat -> Prop := 
| le_head n1 n2 s1 s2 : n1 < n2 -> lex (Cons n1 s1) (Cons n2 s2) 
| le_tail n s1 s2 : lex s1 s2 -> lex (Cons n s1) (Cons n s2). 

Lemma lex_trans : forall s1 s2 s3, lex s1 s2 -> lex s2 s3 -> lex s1 s3. 
Proof. 
    cofix. 
    intros s1 s2 s3 lex12 lex23. 
    inversion lex12; subst; clear lex12; 
    inversion lex23; subst; clear lex23; 
    try (apply le_head; omega). 
    apply le_tail; eauto. 
Qed. 

Maintenant, l'hypothèse a la forme

forall s1 s2 s3, lex s1 s2 -> lex s2 s3 -> lex s1 s3

qui peut facilement être appliqué à la queue de nos cours d'eau, tant que l'application qui en résulte est gardée.