Coq HoTT - 如何正确地将定义放入定理中？

Question

我已经完成了 HoTT 书中定理 2.8.1 的 coq 证明（如下所示）。它有效，但我收到此警告

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.

如何在将定义保留在定理内的同时删除警告？

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

使用 pose 来定义术语应该可行：（尽管可能还有其他方法）

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.

Coq HoTT - 如何正确地将定义放入定理中？

Coq HoTT - How to correctly put a definition inside a theorem?

coq

type-theory