From 810a399699e14e8acf9234d922ab79a4d7a42345 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Wed, 18 Nov 2015 15:08:06 -0500
Subject: [PATCH] style(homotopy/circle): clean-up encode-decode proof

---
 hott/homotopy/circle.hlean | 38 ++++++++++++++------------------------
 hott/types/int/basic.hlean |  1 +
 2 files changed, 15 insertions(+), 24 deletions(-)

diff --git a/hott/homotopy/circle.hlean b/hott/homotopy/circle.hlean
index 61070f7a4..13e11aa25 100644
--- a/hott/homotopy/circle.hlean
+++ b/hott/homotopy/circle.hlean
@@ -186,7 +186,7 @@ namespace circle
 
   open int
 
-  protected definition code (x : circle) : Type₀ :=
+  protected definition code [unfold 1] (x : circle) : Type₀ :=
   circle.elim_type_on x ℤ equiv_succ
 
   definition transport_code_loop (a : ℤ) : transport circle.code loop a = succ a :=
@@ -196,10 +196,10 @@ namespace circle
     : transport circle.code loop⁻¹ a = pred a :=
   ap10 !elim_type_loop_inv a
 
-  protected definition encode {x : circle} (p : base = x) : circle.code x :=
-  transport circle.code p (of_num 0) -- why is the explicit coercion needed here?
+  protected definition encode [unfold 2] {x : circle} (p : base = x) : circle.code x :=
+  transport circle.code p (of_num 0)
 
-  protected definition decode {x : circle} : circle.code x → base = x :=
+  protected definition decode [unfold 1] {x : circle} : circle.code x → base = x :=
   begin
     induction x,
     { exact power loop},
@@ -207,31 +207,21 @@ namespace circle
       rewrite [power_con,transport_code_loop]}
   end
 
-  --remove this theorem after #484
-  theorem encode_decode {x : circle} : Π(a : circle.code x), circle.encode (circle.decode a) = a :=
-  begin
-    unfold circle.decode, induction x,
-    { intro a, esimp [base,base1], --simplify after #587
-      apply rec_nat_on a,
-      { exact idp},
-      { intros n p,
-        apply transport (λ(y : base = base), transport circle.code y _ = _), apply power_con,
-        rewrite [▸*,con_tr, transport_code_loop, ↑[circle.encode,circle.code] at p], krewrite p},
-      { intros n p,
-        apply transport (λ(y : base = base), transport circle.code y _ = _),
-        { exact !power_con_inv ⬝ ap (power loop) !neg_succ⁻¹},
-        rewrite [▸*,@con_tr _ circle.code,transport_code_loop_inv, ↑[circle.encode] at p, p, -neg_succ]}},
-    { apply pathover_of_tr_eq, apply eq_of_homotopy, intro a, apply @is_hset.elim,
-      esimp [circle.code,base,base1], exact _}
-      --simplify after #587
-  end
-
   definition circle_eq_equiv [constructor] (x : circle) : (base = x) ≃ circle.code x :=
   begin
     fapply equiv.MK,
     { exact circle.encode},
     { exact circle.decode},
-    { exact circle.encode_decode},
+    { exact abstract [irreducible] begin
+      induction x,
+      { intro a, esimp, apply rec_nat_on a,
+        { exact idp},
+        { intros n p, rewrite [↑circle.encode, -power_con, con_tr, transport_code_loop],
+          exact ap succ p},
+        { intros n p, rewrite [↑circle.encode, nat_succ_eq_int_succ, neg_succ, -power_con_inv,
+            @con_tr _ circle.code, transport_code_loop_inv, ↑[circle.encode] at p, p, -neg_succ] }},
+      { apply pathover_of_tr_eq, apply eq_of_homotopy, intro a, apply @is_hset.elim,
+        esimp, exact _} end end},
     { intro p, cases p, exact idp},
   end
 
diff --git a/hott/types/int/basic.hlean b/hott/types/int/basic.hlean
index e09199e26..b8b5a24d5 100644
--- a/hott/types/int/basic.hlean
+++ b/hott/types/int/basic.hlean
@@ -804,6 +804,7 @@ by rewrite [neg_succ_of_nat_eq, -of_nat_add_of_nat, neg_add]
 
 definition succ (a : ℤ) := a + (nat.succ zero)
 definition pred (a : ℤ) := a - (nat.succ zero)
+definition nat_succ_eq_int_succ (n : ℕ) : nat.succ n = int.succ n := idp
 definition pred_succ (a : ℤ) : pred (succ a) = a := !sub_add_cancel
 definition succ_pred (a : ℤ) : succ (pred a) = a := !add_sub_cancel
 definition neg_succ (a : ℤ) : -succ a = pred (-a) :=