Coq : 응용 프로그램 증명

Question

이것은 약간 이론적 인 질문입니다. 하나는 f 및 f가있다 (또는 예정) 것을 x에서 증명할 수 등의 방법으로

Function fx {A} (x:A) (f:A->Type) (g:Type->f x): f x := g (f x). 
Definition fx' {A} (x:A) (f:A->Type): f x. 

, 이것은 의미가 x에 적용 : 우리는 겉으로하지 fx'fx하지만를 정의 할 수 있습니다.

assert (h := f x). 

이 수수께끼 같다 : 그러나 우리는 유형 Type의 무언가를 얻을 수 x에 f을 적용 할 수 있습니다 하나는 그가 그렇게 한 증인 y: f x를 얻을 수 없습니다 fx에 여전히 을 적용 할 수 있습니다.

내가 생각할 수있는 유일한 설명은 다음과 같습니다. 유형으로 f x은 용어로, 단지 유형입니다. 우리는 한 유형에서 과거의 응용 프로그램을 추론 할 수 없습니다. 유사하게, 우리는 함수와 그 잠재적 인 논증으로부터 미래의 응용을 추론 할 수 없다. 스스로 적용하는 (예를 들면) 증거의 단계가 아니기 때문에 증거를 얻을 수 없습니다. 그러나 나는 단지 짐작하고있다. 질문 :

fx'을 정의 할 수 있습니까? 그렇다면 어떻게? 아니, 왜

Answer 1

첫째, 귀하의 질문에 직접 대답 (이론적 설명 해주세요) 경우 : 없는를, fx'을 정의 할 수 없습니다. 당신의 조각에 따르면, fx' 다음 스크립트와 같이, fx'의 존재는 모순을 의미 있는지 어렵지 않다 유형

forall (A : Type) (x : A) (f : A -> Type), f x. 

해야한다.

Section Contra. 

Variable fx' : forall (A : Type) (x : A) (f : A -> Type), f x. 

Lemma contra : False. 
Proof. 
    exact (fx' unit tt (fun x => False)). 
Qed. 

End Contra. 

여기에 무슨 일이 일어 났습니까? fx' 유형은 유형이 A 인 모든 유형의 가족에 대해 f x의 요소를 생성 할 수 있으며, x은 임의의 값을 나타낼 수 있습니다. 특히 f을 (fun x => False) 유형의 상수 패밀리로 사용할 수 있습니다.이 경우 f x은 False과 동일합니다. (False는, Prop의 구성원이 외에 또한 Type의 구성원합니다.)

지금, 당신의 질문 주어, 나는 당신이 약간 COQ의 유형과 명제의 의미가 혼동 생각합니다. 당신은 말했다 :

이 수수께끼 같다 하나는 그가 그렇게 한 증인 y: f x를 얻을 수 없습니다 여전히 x에 f을 적용 할 수 있지만.

우리는 fx에 적용 할 수 있다는 사실은 단순히 표현 f x가,이 경우, Type이다 유효한 유형을 가지고 있다는 것을 의미한다. 즉, Coq는 f x : Type을 표시합니다.그러나 유형이있는 것은 과 다른 점입니다. : f과 x이 임의 인 경우 y이라는 문구를 y : f x과 같이 만들 수 없습니다. 특히, 우리는 False : Type을 가지고 있지만, p을 p : False으로 만들 수있는 방법이 없습니다. 그 이유는 Coq의 논리가 일관성이 없다는 것을 의미하기 때문입니다.