在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

它可以很容易地应用到我们的流的尾巴，只要最终的应用程序被守卫。