使用 Coq 的 Lob 定理的一个特例答案

【问题标题】：A special case of Lob's theorem using Coq使用 Coq 的 Lob 定理的一个特例
【发布时间】：2017-03-24 06:49:39
【问题描述】：

我有一个归纳定义如下的公式：

Parameter world : Type.
Parameter R : world -> world -> Prop.
Definition Proposition : Type := world -> Prop

(* This says that R has only a finite number of steps it can take *)
Inductive R_ends : world -> Prop :=
 | re : forall w, (forall w', R w w' -> R_ends w') -> R_ends w.
 (*  if every reachable state will end then this state will end *)

和假设：

Hypothesis W : forall w, R_ends w.

我想证明：

forall P: Proposition, (forall w, (forall w0, R w w0 -> P w0) -> P w)) -> (forall w, P w)

我尝试在 world 类型上使用 induction 策略，但失败了，因为它不是归纳类型。

在 Coq 中是否可以证明，如果可以，您能建议如何证明吗？

【问题讨论】：

标签： coq lob coq-tactic

【解决方案1】：

您可以对R_ends 类型的术语使用结构归纳：

Lemma lob (P : Proposition) (W : forall w, R_ends w) :
    (forall w, (forall w0, R w w0 -> P w0) -> P w) -> (forall w, P w).
Proof.
  intros H w.
  specialize (W w).
  induction W.
  apply H.
  intros w' Hr.
  apply H1.
  assumption.
Qed.

顺便说一句，您可以用稍微不同的方式定义R_ends，使用参数而不是索引：

Inductive R_ends (w : world) : Prop :=
 | re : (forall w', R w w' -> R_ends w') -> R_ends w.

这样编写时，很容易看出R_ends 类似于标准库中定义的可访问性谓词Acc (Coq.Init.Wf)：

Inductive Acc (x: A) : Prop :=
     Acc_intro : (forall y:A, R y x -> Acc y) -> Acc x.

它用于有充分根据的归纳。

【讨论】：