A special case of Lob's theorem using Coq

Question

I have a formula inductively defined as follows:

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 *)

And hypothesis:

Hypothesis W : forall w, R_ends w.

I would like to prove:

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

I tried using the induction tactic on the type world but failed since it is not an inductive type.

Is it provable in Coq and if yes, can you suggest how?

Answer 1

You can use structural induction on a term of type 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.

Incidentally, you could have defined R_ends in a slightly different manner, using a parameter instead of an index:

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

When written this way, it's easy to see that R_ends is analogous to the accessibility predicate Acc, defined in the standard library (Coq.Init.Wf):

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

It's used to work with well-founded induction.