共归纳不是A形式的-> A？
共归纳不是A形式的-> A？
提问于 2019-12-25 08:14:29
在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关闭它，它不会检测到错误。
所以，基本上，有没有协同归纳的公式可以在早期捕捉到这个错误，而不是等待整个证明完成并检查警戒性？
Stack Overflow用户
回答已采纳
发布于 2019-12-25 19:57:05
使用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.页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/59474310
复制相关文章
相似问题
腾讯云开发者
