1

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

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)

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

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

4

1 回答 1

3

您可以对类型的术语使用结构归纳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.

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

于 2017-03-24T07:34:31.543 回答