我试图证明"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 自动扩展值 - 更好!
最佳答案
你的证明的一个问题是,在引入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
只要生成的应用程序受到保护,就可以轻松应用于我们的流的尾部。
关于coq - 在 Coq 中证明共归纳性质(词法顺序是传递性的),我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/29135051/