Coq에서 HoTT 경로 유도를 사용하는 방법? COQ에서

Question

나는

Definition f (s:Unit) : tt=tt := match s with tt => idpath end. 
Definition g (p:tt=tt) : Unit := match p with idpath => tt end. 

을하고 난 forall (p:tt=tt), (f o g) p = p을 증명하고 싶습니다.

HoTT의 책에서 1.12.1에 설명 된 경로 유도를 사용하여 수행하고 싶습니다.

그것은 p이 idpath되는 경우, 우리는

assert((f o g) idpath = idpath). 
simpl. 
reflexivity. 

을 증명할 수하지만 어떻게 모든 증거 함께 패키지로 COQ에서 경로 유도를 사용 않는 것이 분명하다?

지금까지 전체 증거 (? admit 대신 넣어 무엇)

Require Import HoTT. 
Definition f (s:Unit) : tt=tt := match s with tt => idpath end. 
Definition g (p:tt=tt) : Unit := match p with idpath => tt end. 
Theorem myTheorem : forall (p:tt=tt), (f o g) p = p. 
    assert((f o g) idpath = idpath). 
    simpl. 
    reflexivity. 
admit. 

Answer 1

COQ에서 경로 유도의 아날로그은 match 구조입니다. 다음은 HoTT 서적에 설명 된대로 경로 유도를 정의하는 데이 방법을 사용할 수있는 방법입니다.

Set Implicit Arguments. 

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

이 정의의 유형은 우리가

• y : A,
• p : x = y 및
• P : forall y, x = y -> Type는

이 충분 P y p을 입증 할 때마다 말한다 표시하려면 P x eq_refl이 성립한다. J을 사용하면 g 기능이 일정하다는 것을 알 수 있습니다. (필자는 COQ 표준 라이브러리에 의해 주어진 것들에 맞게 정의를 고쳐있다.)

Definition f (s : unit) : tt = tt := match s with tt => eq_refl end. 
Definition g (p : tt = tt) : unit := match p return unit with eq_refl => tt end. 

Definition g_tt p : g p = tt := 
    J (fun y q => match q return unit with eq_refl => tt end = tt) 
    eq_refl p. 

이 증거의 까다로운 부분은 J의 P 파라미터가 다른 경우 인해야한다 무엇을 찾는 것입니다 경로 유도에 의해 진행되는 증거. 여기서는 유형의 인수가 필요하기 때문에 g의 정의를 펼쳐야합니다. 반면 위에 사용 된 q 유형은 tt = y입니다. 어쨌든 P tt p은 정의 상으로는 g p = tt과 같음을 알 수 있습니다. 이는 우리가 증명하고자하는 것입니다.

p : tt = tt에 대해 p = eq_refl을 표시하는 트릭을 사용할 수 있습니다. 이전 결과와 결합하면 원하는 결과를 정확하게 얻을 수 있습니다.

Definition result (p : tt = tt) : p = eq_refl := 
    J (fun y q => 
     unit_rect (fun z => tt = z -> Prop) 
       (fun u => u = eq_refl) 
       y q) 
    eq_refl p. 

다시 한 번 요점은 P 매개 변수입니다. unit에 대한 유도 원리를 사용하여 요소를 찾을 때마다 T x (T : unit -> Type 및 x : tt) 유형을 정의 할 수 있다고합니다.J의 애플리케이션의 결과는이 경우 단지

unit_rect (fun z => tt = z -> Prop) 
      (fun u => u = eq_refl) 
      tt p 
= (p = eq_refl) 

unit_rect위한 연산 규칙에 따라 어떤 타입을

P tt p 

있어야 리콜.

불행히도 이런 종류의 증거는 CoD의 전술 언어로 복제하기가 어렵습니다. 종종 P이 무엇이되어야 하는지를 추측하기가 어렵 기 때문입니다. 이 값이 무엇인지 알아 내고 증명 용어를 명시 적으로 적는 것이 더 쉽습니다.

이유를 잘 모르겠지만, match으로 교정 기간을 적어두면이 주석을 알아내는 데 Coq도 훨씬 좋습니다. 비교 :

Definition result' (p : tt = tt) : p = eq_refl := 
    match p with eq_refl => eq_refl end. 

를이 훨씬 간단 보이지만, 당신은 당신이 그것을 인쇄하려고하면 COQ에 의해 추론 실제 용어는 훨씬 더 복잡 것을 볼 수 있습니다. 시도 해봐!

편집

아, 난 그냥 당신이 COQ의 HOTT 버전을 사용하려고했던 것을 깨달았다. 나는 그 버전을 설치하지 않았지만 내 솔루션을 적용하기가 너무 어렵지 않아야한다고 생각한다.