使用勒柯克

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策略，但由於它不是歸納型PE。

它是否可以在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類似於標準庫（Coq.Init.Wf）中定義的可訪問性謂詞Acc：

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

它被用來與有根有據的感應工作。