Coq HoTT - 정리를 올바르게 정리하는 방법은 무엇입니까?

Question

HoTT의 책에서 정리 2.8.1에 대한 증명을 완료했습니다 (아래 참조). 그것은 그러나 나는이 경고

Toplevel input, characters 0-4: 
<warning> 
Warning: Nested proofs are deprecated and will stop working in a future Coq 
version [deprecated-nested-proofs,deprecated]</warning> 

내가 그들을 둘 때, 경고가 사라 때문에 때문에 정리 내부의 정의로 알고를 얻을 작동합니다. 그러나 제가 글로벌 이길 원하는 유일한 정의는 J입니다.

정리를 정의 안에 보관하는 동안 어떻게 경고를 제거 할 수 있습니까? 작동해야 용어를 정의하는 pose를 사용

Require Export HoTT. 

Definition J (A:Type) (P : forall (x y:A), x = y -> Type) 
      (h : forall x:A, P x x idpath) : 
    forall (x y:A) (p:x=y), P x y p 
    := 
    fun x y p => match p with idpath => h x end. 

Theorem th_2_8_1 : 
    forall (x y:Unit), Unit <~> x=y. 
Proof. 

    Definition g (x y:Unit)(p:x=y) : Unit := 
    match p with idpath => tt end. 

    Definition f (x y:Unit)(s:Unit) : x=y := 
    match x,y,s with tt,tt,tt => idpath end. 

    Definition alpha1 (x y:Unit)(s:Unit) : ((g x y) o (f x y))s = s 
    := 
     match x,y,s with tt,tt,tt => idpath end. 

    Definition P (f : forall (x y:Unit)(s:Unit), x=y) 
       (g : forall (x y:Unit)(p:x=y), Unit) 
       (x y:Unit) (p:x=y) : Type 
    := 
     ((f x y) o (g x y)) p = p. 

    Definition h (x:Unit) : P f g x x idpath 
    := 
     match x with tt => idpath idpath end. 

    Definition alpha2 (x y:Unit)(p:x=y): ((f x y) o (g x y)) p = p := 
    (J Unit (P f g) h) x y p. 


    intros x y. 
    exists (f x y). 
    apply(BuildIsEquiv Unit (x=y) (f x y) (g x y) (alpha2 x y) (alpha1 x y)). 

    induction x0. 
    rewrite <- (f x y). 
    induction x. 
    simpl. 
    apply(idpath idpath). 
    apply(tt). 
Defined 

Answer 1

: (다른 방법이있을 수 있지만)

Require Export HoTT. 

Theorem th_2_8_1 : 
    forall (x y:Unit), Unit <~> x=y. 
Proof. 

    pose(g:=fun (x y:Unit)(p:x=y) => match p with idpath => tt end). 

    pose(f := fun (x y:Unit)(s:Unit) => 
       match x,y,s return (x=y) with tt,tt,tt => idpath end). 

    pose(alpha1 := fun (x y:Unit)(s:Unit) => 
     match x,y,s return ((g x y) o (f x y))s = s 
     with tt,tt,tt => idpath end). 

    pose(P := fun 
      (f : forall (x y:Unit)(s:Unit), x=y) 
      (g : forall (x y:Unit)(p:x=y), Unit) 
      (x y:Unit) 
      (p:x=y) 
    => 
     ((f x y) o (g x y)) p = p). 

    pose(h := fun (x:Unit) => 
     match x return P f g x x idpath 
     with tt => idpath idpath end). 

    pose(alpha2 := fun (x y:Unit)(p:x=y) => (J Unit (P f g) h) x y p). 


    intros x y. 
    exists (f x y). 
    apply(BuildIsEquiv Unit (x=y) (f x y) (g x y) (alpha2 x y) (alpha1 x y)). 

    induction x0. 
    rewrite <- (f x y). 
    induction x. 
    simpl. 
    apply(idpath idpath). 
    apply(tt). 
Defined.  

나는 그 경고에 대해 너무 많이 걱정하지 말 것