2

在 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 关闭它，它不会检测到错误。

那么，基本上，有没有共同归纳的公式可以尽早发现这个错误，而不是等待整个证明完成并检查警戒性？

4

1 回答 1

1

使用paco 库。它提供了一个最大的定点算子来定义共归纳谓词，并且符合合理的推理原则，因此目标看起来不像A -> A. 该库附带一个教程（在此处呈现）。

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.
于 2019-12-25T11:57:04.833 回答