CODEWITHSUNDEEP
coqtype-theory
Carlos Pinzón
Carlos Pinzón

Reputation: 1427

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

I have completed a proof in coq (shown below) for Theorem 2.8.1 from HoTT's book. It works, however I get this warning 

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>

I know it's because of the definitions inside the theorem because when I put them out, the warning disappeared. But the only definition I want to be global is J.

How can I remove the warnings while keeping the definitions inside the theorem?

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

Upvotes: 1

Views: 186

Answers (1)

Carlos Pinz&#243;n
Carlos Pinz&#243;n

Reputation: 1427

Using pose for defining the terms should work: (although there may be another way)

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.

Upvotes: 1

Related Questions