在 Coq 中证明 Co-Inductive 属性（词法排序是传递的）

Question

我正在尝试用 Coq 证明 "Practical Coinduction" 中的第一个例子。第一个例子是为了证明无限整数流的字典顺序是可传递的。

这是我到目前为止的发展。首先只是无限流的通常定义。然后定义字典顺序叫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.

中的 "hypothesis"

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.

我该如何从这里开始？感谢您的任何提示！

编辑

感谢 Arthur（一如既往！）的帮助和启发性回答，我也可以完成证明。我在下面给出我的版本以供参考。

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 引理 "expand" s1 和 s3 的值。这里 lex 的定义（head 和 tail）更接近 Practical Coinduction 中的逐字表述。 Arthur 使用了一种更优雅的技术，使 Coq 自动扩展值 - 更好！

Answer 1

你的证明有一个问题是你调用 cofix 太晚了，在 s1 s2 s3 被引入之后。因此，您得到的余归假设 lex s1 s2 不是很有用：为了在保持警惕的情况下应用它，正如您提到的，我们需要在 [=32= 之后] ] 应用了 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

它可以很容易地应用到我们流的尾部，只要生成的应用程序受到保护。

在 Coq 中证明 Co-Inductive 属性（词法排序是传递的）

Proving a Co-Inductive property (lexical ordering is transitive) in Coq

coq

coinduction