Un cas particulier du théorème de Lob en utilisant Coq

Question

je une formule définie inductivement comme suit:

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

Et hypothèse:

Hypothesis W : forall w, R_ends w. 

Je voudrais prouver:

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

J'ai essayé d'utiliser la tactique induction sur le type world mais j'ai échoué car ce n'est pas un ty inductif pe.

Est-il prouvé en Coq et si oui, pouvez-vous suggérer comment?

Answer 1

Vous pouvez utiliser induction sur un terme de 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. 

Soit dit en passant, vous pourriez avoir défini R_ends d'une manière légèrement différente, en utilisant un paramètre au lieu d'un index:

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

Lorsqu'il est écrit de cette façon, il est facile de voir que R_ends est analogue au prédicat d'accessibilité Acc, défini dans la bibliothèque standard (Coq.Init.Wf):

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

Il est utilisé pour travailler avec une induction bien fondée.