使用 Coq 的 Lob 定理的特例

Question

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

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 中可证明吗？如果是，你能建议如何吗？

Answer 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.

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

使用 Coq 的 Lob 定理的特例

A special case of Lob's theorem using Coq

coq

lob

coq-tactic