HITs-Examples/Integers.v

Require Import HoTT.
Require Export HoTT.

Module Export Ints.

Private Inductive Z : Type0 :=
| nul : Z
| succ : Z -> Z
| pred : Z -> Z.

Axiom inv1 : forall n : Z, n = pred(succ n).
Axiom inv2 : forall n : Z, n = succ(pred n).

Fixpoint Z_rec
  (P : Type)
  (a : P)
  (s : P -> P)
  (p : P -> P)
  (i1 : forall (m : P), m = p(s m))
  (i2 : forall (m : P), m = s(p m))
  (x : Z)
  {struct x}
  : P
  := 
    (match x return _ -> _ -> P with
      | nul => fun _ => fun _ => a
      | succ n => fun _ => fun _ => s ((Z_rec P a s p i1 i2) n)
      | pred n => fun _ => fun _ => p ((Z_rec P a s p i1 i2) n)
    end) i1 i2.

Axiom Z_rec_beta_inv1 : forall
  (P : Type)
  (a : P)
  (s : P -> P)
  (p : P -> P)
  (i1 : forall (m : P), m = p(s m))
  (i2 : forall (m : P), m = s(p m))
  (n : Z)
  , ap (Z_rec P a s p i1 i2) (inv1 n) = i1 (Z_rec P a s p i1 i2 n).

Axiom Z_rec_beta_inv2 : forall
  (P : Type)
  (a : P)
  (s : P -> P)
  (p : P -> P)
  (i1 : forall (m : P), m = p(s m))
  (i2 : forall (m : P), m = s(p m))
  (n : Z)
  , ap (Z_rec P a s p i1 i2) (inv2 n) = i2 (Z_rec P a s p i1 i2 n).

Fixpoint Z_ind
  (P : Z -> Type)
  (a : P nul)
  (s : forall (n : Z), P n -> P (succ n))
  (p : forall (n : Z), P n -> P (pred n))
  (i1 : forall (n : Z) (m : P n), (inv1 n) # m = p (succ n) (s (n) m))
  (i2 : forall (n : Z) (m : P n), (inv2 n) # m = s (pred n) (p (n) m))
  (x : Z)
  {struct x}
  : P x
  := 
    (match x return _ -> _ -> P x with
      | nul => fun _ => fun _ => a
      | succ n => fun _ => fun _ => s n ((Z_ind P a s p i1 i2) n)
      | pred n => fun _ => fun _ => p n ((Z_ind P a s p i1 i2) n)
    end) i1 i2.

Axiom Z_ind_beta_inv1 : forall
  (P : Z -> Type)
  (a : P nul)
  (s : forall (n : Z), P n -> P (succ n))
  (p : forall (n : Z), P n -> P (pred n))
  (i1 : forall (n : Z) (m : P n), (inv1 n) # m = p (succ n) (s (n) m))
  (i2 : forall (n : Z) (m : P n), (inv2 n) # m = s (pred n) (p (n) m))
  (n : Z)
  , apD (Z_ind P a s p i1 i2) (inv1 n) = i1 n (Z_ind P a s p i1 i2 n).

Axiom Z_ind_beta_inv2 : forall
  (P : Z -> Type)
  (a : P nul)
  (s : forall (n : Z), P n -> P (succ n))
  (p : forall (n : Z), P n -> P (pred n))
  (i1 : forall (n : Z) (m : P n), (inv1 n) # m = p (succ n) (s (n) m))
  (i2 : forall (n : Z) (m : P n), (inv2 n) # m = s (pred n) (p (n) m))
  (n : Z)
  , apD (Z_ind P a s p i1 i2) (inv2 n) = i2 n (Z_ind P a s p i1 i2 n).

End Ints.

Definition negate : Z -> Z.
Proof.
intro x.
refine (Z_rec _ _ _ _ _ _ x).
 Unshelve.
 Focus 1.
 apply nul.

 Focus 3.
 apply pred.

 Focus 3.
 apply succ.

 Focus 2.
 apply inv1.

 apply inv2.
Defined.

Definition plus : Z -> Z -> Z.
Proof.
intro x.
refine (Z_rec _ _ _ _ _ _).
 Unshelve.
 Focus 1.
 apply x.

 Focus 3.
 apply succ.

 Focus 3.
 apply pred.

 Focus 1.
 apply inv1.

 apply inv2.
Defined.

Definition minus (x : Z) (y : Z) := plus x (negate y).

Definition Z_to_S : Z -> S1.
Proof.
refine (Z_rec _ _ _ _ _ _).
  Unshelve. 

  Focus 1.
  apply base.

  Focus 3.
  intro x.
  apply x.

  Focus 3.
  intro x.
  apply x.

  Focus 1.
  intro m.
  compute.
  reflexivity.

  refine (S1_ind _ _ _).
  Unshelve.

  Focus 2.
  apply loop.

  rewrite @HoTT.Types.Paths.transport_paths_FlFr.
  rewrite ap_idmap.
  rewrite concat_Vp.
  rewrite concat_1p.
  reflexivity.
Defined.

Lemma eq1 : ap Z_to_S (inv1 (pred (succ (pred nul)))) = reflexivity base.
Proof.
rewrite Z_rec_beta_inv1.
reflexivity.
Qed.


Lemma eq2 : ap Z_to_S (ap pred (inv2 (succ (pred nul)))) = loop.
Proof.
rewrite <- ap_compose.
enough (forall (n m : Z) (p : n = m), ap Z_to_S p = ap (fun n : Z => Z_to_S(pred n)) p).
  Focus 2.
  compute.
  reflexivity.

  rewrite Z_rec_beta_inv2.
  compute.
  reflexivity.
Qed.

Module Export AltInts.

Private Inductive Z' : Type0 :=
| positive : nat -> Z'
| negative : nat -> Z'.

Axiom path : positive 0 = negative 0.

Fixpoint Z'_ind
  (P : Z' -> Type)
  (po : forall (x : nat), P (positive x))
  (ne : forall (x : nat), P (negative x))
  (i : path # (po 0) = ne 0)
  (x : Z')
  {struct x}
  : P x
  := 
    (match x return _ -> P x with
      | positive n => fun _ => po n
      | negative n => fun _ => ne n
    end) i.

Axiom Z'_ind_beta_inv1 : forall
  (P : Z' -> Type)
  (po : forall (x : nat), P (positive x))
  (ne : forall (x : nat), P (negative x))
  (i : path # (po 0) = ne 0)
  , apD (Z'_ind P po ne i) path = i.
End AltInts.

Definition succ_Z' : Z' -> Z'.
Proof.
refine (Z'_ind _ _ _ _).
 Unshelve.
 Focus 2.
 intro n.
 apply (positive (S n)).

 Focus 2.
 intro n.
 induction n.
  apply (positive 1).

  apply (negative n).

 simpl.
 rewrite transport_const.
 reflexivity.
Defined.

Definition pred_Z' : Z' -> Z'.
Proof.
refine (Z'_ind _ _ _ _).
 Unshelve.
 Focus 2.
 intro n.
 induction n.
  apply (negative 1).

  apply (positive n).

 Focus 2.
 intro n.
 apply (negative (S n)).

 simpl.
 rewrite transport_const.
 reflexivity.
Defined.


Fixpoint Nat_to_Pos (n : nat) : Pos :=
  match n with
  | 0 => Int.one
  | S k => succ_pos (Nat_to_Pos k)
  end.

Definition Z'_to_Int : Z' -> Int.
Proof.
refine (Z'_ind _ _ _ _).
  Unshelve.

  Focus 2.
  intro x.
  induction x.
  apply (Int.zero).
  apply (succ_int IHx).

  Focus 2.
  intro x.
  induction x.
  apply (Int.zero).
  apply (pred_int IHx).

  simpl.
  rewrite transport_const.
  reflexivity.
Defined.

Definition Pos_to_Nat : Pos -> nat.
Proof.
intro x.
induction x.
apply 1.
apply (S IHx).
Defined.


Definition Int_to_Z' (x : Int) : Z'.
Proof.
induction x.
apply (negative (Pos_to_Nat p)).
apply (positive 0).
apply (positive (Pos_to_Nat p)).
Defined.

Lemma Z'_to_int_pos_homomorphism : 
  forall n : nat, Z'_to_Int (positive (S n)) = succ_int (Z'_to_Int (positive n)).
Proof.
intro n.
reflexivity.
Qed.

Lemma Z'_to_int_neg_homomorphism : 
  forall n : nat, Z'_to_Int (negative (S n)) = pred_int (Z'_to_Int (negative n)).
Proof.
intro n.
reflexivity.
Qed.

Theorem isoEq1 : forall x : Int, Z'_to_Int(Int_to_Z' x) = x.
Proof.
intro x.
induction x.
induction p.
reflexivity.

rewrite Z'_to_int_neg_homomorphism.
rewrite IHp.
reflexivity.

reflexivity.

induction p.
reflexivity.

rewrite Z'_to_int_pos_homomorphism.
rewrite IHp.
reflexivity.
Defined.

Lemma Int_to_Z'_succ_homomorphism :
  forall x : Int, Int_to_Z' (succ_int x) = succ_Z' (Int_to_Z' x).
Proof.
simpl.
intro x.
simpl.
induction x.
 induction p.
  compute.
  apply path.

  reflexivity.

 reflexivity.

 induction p.
  reflexivity.

  reflexivity.
Qed.

Lemma Int_to_Z'_pred_homomorphism :
  forall x : Int, Int_to_Z' (pred_int x) = pred_Z' (Int_to_Z' x).
Proof.
intro x.
induction x.
 induction p.
  reflexivity.

  reflexivity.

 reflexivity.

 induction p.
  reflexivity.

  reflexivity.

Qed.

Theorem isoEq2 : forall x : Z', Int_to_Z'(Z'_to_Int x) = x.
Proof.
refine (Z'_ind _ _ _ _).
  Unshelve.

  Focus 2.
  intro x.
  induction x.
  reflexivity.
  rewrite Z'_to_int_pos_homomorphism.
  rewrite Int_to_Z'_succ_homomorphism.
  rewrite IHx.
  reflexivity.

  Focus 2.
  intro x.
  induction x.
  apply path.
  rewrite Z'_to_int_neg_homomorphism.
  rewrite Int_to_Z'_pred_homomorphism.
  rewrite IHx.
  reflexivity.

  simpl.
  rewrite @HoTT.Types.Paths.transport_paths_FlFr.
  rewrite concat_p1.
  rewrite ap_idmap.

  enough (ap (fun x : Z' => Z'_to_Int x) path = reflexivity Int.zero).
  rewrite ap_compose.
  rewrite X.
  apply concat_1p.

  apply axiomK_hset.
  apply hset_int.
Defined.

Theorem adj : 
  forall x : Z', isoEq1 (Z'_to_Int x) = ap Z'_to_Int (isoEq2 x).
Proof.
intro x.
apply hset_int.
Defined.

Definition isomorphism : IsEquiv Z'_to_Int.
Proof.
apply (BuildIsEquiv Z' Int Z'_to_Int Int_to_Z' isoEq1 isoEq2 adj).
Qed.

Axiom everythingSet : forall T : Type, IsHSet T.

Definition Z_to_Z' : Z -> Z'.
Proof.
refine (Z_rec _ _ _ _ _ _).
 Unshelve.
 Focus 1.
 apply (positive 0).

 Focus 3.
 apply succ_Z'.

 Focus 3.
 apply pred_Z'.

 Focus 1.
 refine (Z'_ind _ _ _ _).
  Unshelve.
  Focus 2.
  intros.
  reflexivity.

  Focus 2.
  intros.
  induction x.
   Focus 1.
   compute.
   apply path^.

   reflexivity.

  apply everythingSet.

 refine (Z'_ind _ _ _ _).
  Unshelve.
  Focus 2.
  intros.
  induction x.
   Focus 1.
   compute.
   apply path.

   reflexivity.

  Focus 2.
  intros.
  reflexivity.

  apply everythingSet.

Defined.

Definition Z'_to_Z : Z' -> Z.
Proof.
refine (Z'_ind _ _ _ _).
 Unshelve.
 Focus 2.
 induction 1.
  apply nul.

  apply (succ IHx).

 Focus 2.
 induction 1.
  Focus 1.
  apply nul.

  apply (pred IHx).

 simpl.
 rewrite transport_const.
 reflexivity.

Defined.

Theorem isoZEq1 : forall n : Z', Z_to_Z'(Z'_to_Z n) = n.
Proof.
refine (Z'_ind _ _ _ _).
 Unshelve.
 Focus 3.
 intros.
 induction x.
  compute.
  apply path.

  transitivity (Z_to_Z' (pred (Z'_to_Z (negative x)))).
   enough (Z'_to_Z (negative x.+1) = pred (Z'_to_Z (negative x))).
    rewrite X.
    reflexivity.

    reflexivity.

   transitivity (pred_Z' (Z_to_Z' (Z'_to_Z (negative x)))).
    Focus 1.
    reflexivity.

    rewrite IHx.
    reflexivity.

 Focus 2.
 intros.
 induction x.
  Focus 1.
  reflexivity.

  transitivity (Z_to_Z' (succ (Z'_to_Z (positive x)))).
   reflexivity.

   transitivity (succ_Z' (Z_to_Z' (Z'_to_Z (positive x)))).
    reflexivity.

    rewrite IHx.
    reflexivity.

 apply everythingSet.
Defined.

Theorem isoZEq2 : forall n : Z, Z'_to_Z(Z_to_Z' n) = n.
Proof.
refine (Z_ind _ _ _ _ _ _).
 Unshelve.
 Focus 1.
 reflexivity.

 Focus 1.
 intros.
 apply everythingSet.

 Focus 1.
 intros.
 apply everythingSet.

 Focus 1.
 intro n.
 intro X.
 transitivity (Z'_to_Z (succ_Z' (Z_to_Z' n))).
  reflexivity.

  transitivity (succ (Z'_to_Z (Z_to_Z' n))).
   Focus 2.
   rewrite X.
   reflexivity.

   enough (forall m : Z', Z'_to_Z (succ_Z' m) = succ (Z'_to_Z m)).
    rewrite X0.
    reflexivity.

    refine (Z'_ind _ _ _ _).
     Unshelve.
     Focus 2.
     intros.
     reflexivity.

     Focus 2.
     intros.
     induction x.
      Focus 1.
      reflexivity.

      compute.
      rewrite <- inv2.
      reflexivity.

     apply everythingSet.

 intros.
 transitivity (Z'_to_Z (pred_Z' (Z_to_Z' n))).
  reflexivity.

  transitivity (pred (Z'_to_Z (Z_to_Z' n))).
   Focus 2.
   rewrite X.
   reflexivity.

   enough (forall m : Z', Z'_to_Z (pred_Z' m) = pred (Z'_to_Z m)).
    rewrite X0.
    reflexivity.

    refine (Z'_ind _ _ _ _).
     Unshelve.
     Focus 1.
     apply everythingSet.

     Focus 1.
     intro x.
     induction x.
      reflexivity.

      compute.
      rewrite <- inv1.
      reflexivity.

     intro x.
     reflexivity.
Defined.

Theorem adj2 : 
  forall x : Z', isoZEq2 (Z'_to_Z x) = ap Z'_to_Z (isoZEq1 x).
Proof.
intro x.
apply everythingSet.
Defined.

Definition isomorphism2 : IsEquiv Z'_to_Z.
Proof.
apply (BuildIsEquiv Z' Z Z'_to_Z Z_to_Z' isoZEq2 isoZEq1 adj2).
Qed.