나는 공식 유도로 정의 COQ

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) 

나는 induction 유형을 world 유형으로 시도했지만 유도 성 ty가 아니기 때문에 실패했습니다. 체육.

Coq에서 증명할 수 있나요? 그렇다면 어떻게 제안 할 수 있습니까?

Answer 1

당신은 유형 R_ends의 용어에 구조 유도를 사용할 수 있습니다

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

: 인덱스 대신 매개 변수를 사용하여, 덧붙여

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을 정의 할 수

이렇게 작성하면 R_ends은 표준 라이브러리 (Coq.Init.Wf)에 정의 된 접근성 조건부 Acc과 유사하다는 것을 쉽게 알 수 있습니다.

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

잘 알려진 인덕션을 사용하는 데 사용됩니다.