不是 A 形式的共归纳 -> A?
Coinduction not of form A -> A?
在 Coq 中,协同归纳采用证明 A -> 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. It provides a greatest fixpoint operator to define coinductive predicates, and that goes with sound reasoning principles, so that the goal doesn't look like A -> A
. The library comes with a tutorial (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.
在 Coq 中,协同归纳采用证明 A -> 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. It provides a greatest fixpoint operator to define coinductive predicates, and that goes with sound reasoning principles, so that the goal doesn't look like A -> A
. The library comes with a tutorial (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.