Streicher_K_ Axiom을 사용하는 방법

Question

누군가가 간단한 예제를 보여줄 수 있습니다 Streicher_K_ 공리를 Coq.Logic.EqdepFacts에서 사용하는 방법?

은 어쩌면 단순한 사실을 보여주는 : 나는 또한 인 Streicher_K_으로 그것을 증명하는 방법을 찾아 시행 착오

Variable A:Type. 
Variable x:A. 
Axiom SK:Streicher_K_on_ A x (fun p:x=x => (eq_refl x) = p). 

Lemma single_proof : forall (y:A)(u v:x = y), u = v. 
intros. 
destruct u. 
apply (SK). 
reflexivity. 
Qed. 

:

Lemma single_proof : forall (A:Type)(x y:A) (u v:x = y), u = v. 

나는 Streicher_K_on_ 그것을 증명하기 위해 관리 훨씬 더 간단하다 :

Axiom SK:Streicher_K_ A. 

그러나 문제는 나는 왜 이것이 작동하는지 전혀 모른다. 기본 유형 검사를 이해하지 못합니다.

Answer 1

K와 많은 동등한 문

공리 K의 문은 첫 눈에 이해하기 조금 어렵다. 추가 매개 변수 때문에 표준 라이브러리에서 이해하기가 더 어렵습니다. 다행히, 당신이 증명하려고 한 일을 일반화 다음과 같은 대안에 해당하고, 우리가 실제로 필요 종종 : (". 신분 증명의 유니시티" "UIP는"의 약자)

이

UIP : forall (T : Type) (x y : T) (p q : x = y), p = q 

Coq 표준 라이브러리에는이 두 문장과 이와 유사한 몇 가지 유사어가 표시된 EqdepTheory 모듈이 있습니다. 그것은 하나가 그들 중 하나, eq_rect_eq 가정 동안 우리가 자유롭게 이러한 문 중 하나를 사용할 수 있습니다 :이 조각 한

Require Import Coq.Logic.EqdepFacts. 

Module Ax : EqdepElimination. 

Axiom eq_rect_eq : 
    forall (U:Type) (p:U) (Q:U -> Type) (x:Q p) (h:p = p), 
     x = eq_rect p Q x p h. 

End Ax. 

Module Export UIPM := EqdepTheory Ax. 

을, 우리는, 예를 들어,

Check UIP. 

를 실행할 수 있습니다하지만 어떻게 우리가 물건을 입증 할 K?

UIP를 증명하기 위해 K를 사용하는 방법에 대해서도 당황 스러웠습니다. 대답은 다음 진술에 있습니다.

Definition J (A : Type) (x : A) (P : forall y, x = y -> Prop) : 
    P x eq_refl -> forall y (p : x = y), P y p := 
    fun H y p => 
    match p with 
    | eq_refl => H 
    end. 

첫눈에, K와 J는 상당히 유사합니다. 의 자신의 유형을 비교해 보자

J : forall (A : Type) (x : A) (P : forall y : A, x = y -> Prop), 
    P x eq_refl -> forall (y : A) (p : x = y), P y p 

K : forall (A : Type) (x : A) (P :    x = x -> Prop), 
    P eq_refl -> forall   (p : x = x), P p 

가 (. 난 그냥 가독성 대신 Streicher_K의 K을 썼다) 한 가지 차이점은 J는 술어에 의해 매개 변수화되어 있다는 점이다 오른쪽 y에 대한 포괄적 인 평등 x = y의 P . K도 술어 P을 갖지만 동등성은 x = x 만 고려합니다.

또 다른 차이점은 K은 Coq의 이론에서 입증 될 수 있지만 K은 이론에 추가 공리를 추가하는 것으로 만 입증 될 수 있다는 것입니다. K에 사용 된 술어 P이 J에 사용 된 것보다 더 구체적이지만, match 문이 Coq에 어떻게 입력되었는지에 따라 이것은 놀랄 것 같습니다.

K과 J을 합치면 UIP 증명에 도달 할 수 있습니다. 의 처음에만 재귀 평등을 위해 작동하는지, 그것의 전문 버전을 증명하자 J의 정의 패턴을 사용하는

가

Definition UIP (A : Type) (x y : A) (p q : x = y) : p = q := 
    J A x (fun y p => forall q : x = y, p = q) (UIP_refl A x) y p q. 

주의 사항 : 다음

Definition UIP_refl (A : Type) (x : A) (p : x = x) : eq_refl = p := 
    Streicher_K A x (fun q => eq_refl = q) eq_refl p. 

, J은 우리가 임의의 등식이 일반화 할 수 있습니다 어울리는. 후드 아래 Coq는 destruct (SK).을 호출했을 때도 귀하의 증명에서 패턴 일치를 사용하고있었습니다.