在Coq中證明Co-Inductive屬性（詞彙順序是傳遞性的）

Question

我試圖證明Coq中的"Practical Coinduction"中的第一個示例。第一個例子是證明無限流整數上的詞典排序是可傳遞的。

我一直沒能制定的證明，以繞過Guardedness condition

這裏是我發展至今。首先是無限流的通常定義。然後定義稱爲lex的詞典順序。最後，傳遞性定理的失敗證明。

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. 

這裏是我想證明的引理。我首先準備目標，以便我可以應用構造函數，希望最終能夠使用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. 

我該怎麼做？感謝任何提示！

• 編輯

感謝亞瑟（一如既往！）有益和有啓發答案，我也能完成的證明。我給我的版本以供參考。

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. 

我用cons_ht引理 「擴大」 的s1和s3值。這裏的lex（與head和tail）的定義更接近Practical Coinduction中的逐字制定。 Arthur使用更優雅的技術，讓Coq自動擴展值 - 更好！

Answer 1

您的證據存在的一個問題是，在推出s1 s2 s3之後，您致電cofix太晚了。因此，你得到的合作假設lex s1 s2並不是非常有用：爲了在守護時應用它，正如你所提到的，我們需要在之後應用已經應用了lex的構造函數。但是，在這樣做之後，我們需要在某個點顯示lex (tail s1) (tail s3)成立，其中由cofix引入的假設不能起到任何作用。

爲了解決這個問題，我們需要在之前執行cofix的調用，以便它產生的假設足夠一般。我把重整你的lex定義的自由，使之變得更容易在這樣的證據來操作：

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. 

現在，假設的形式

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

它可以很容易地應用到我們的流的尾巴，只要最終的應用程序被守衛。