在Coq中,共归采用证明A的形式->受警戒性约束的对象,以确保进度。这种表述很容易出错,因为它看起来像您一开始就到达了目的地,并且根据证明中的当前状态不容易看到保护性。是否有其他公式更接近通常的归纳法,您必须得出与前提不同的结论?
示例:
CoInductive stream A : Type :=
| SCons : A -> stream A -> stream A
.
Arguments SCons [A] _ _.
CoInductive sEq A : stream A -> stream A -> Prop :=
| StreamEq x s0 s1 : sEq A s0 s1 -> sEq A (SCons x s0) (SCons x s1)
.
Arguments sEq [A].
Arguments StreamEq [A].
Theorem sEq_refl {A} (s : stream A) : sEq s s.
revert s; cofix f; intros.
destruct s.
apply StreamEq.
apply f.
Qed.
cofix之后,您得到这个奇怪的状态:
A : Type
f : forall s : stream A, sEq s s
s : stream A
============================
sEq s s
更糟糕的是,如果您尝试使用apply f
直到用Qed关闭它,它都不会检测到该错误。
因此,从根本上讲,是否存在共鸣的表述可以早日捕获此错误,而不是等待整个证明完成并检查保护性?
使用paco library。它提供了一个最大的定点运算符来定义共归谓词,并且遵循合理的推理原理,因此目标看起来不像A -> A
。该库带有一个教程(rendered here)。
From Paco Require Import paco.
Set Implicit Arguments.
CoInductive stream A : Type := SCons
{ head : A;
tail : stream A
}.
Arguments SCons [A] _ _.
Definition seq_ {A} (r : stream A -> stream A -> Prop) (s1 s2 : stream A) : Prop
:= head s1 = head s2 /\ r (tail s1) (tail s2).
Definition seq {A} : stream A -> stream A -> Prop := paco2 (seq_ (A := A)) bot2.
Theorem seq_refl {A} (s : stream A) : seq s s.
Proof.
revert s; pcofix self; intros.
pfold.
split.
- reflexivity.
- right. apply self.
Qed.