From 3d4475b7d9af3be576bdb091eb5f6edf92f89039 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 19 Sep 2015 17:24:26 -0700
Subject: [PATCH] refactor(library/logic/cast): simplify proofs

---
 library/logic/cast.lean | 49 ++++++++++-------------------------------
 1 file changed, 12 insertions(+), 37 deletions(-)

diff --git a/library/logic/cast.lean b/library/logic/cast.lean
index ffed5c9c7..98f86e7d0 100644
--- a/library/logic/cast.lean
+++ b/library/logic/cast.lean
@@ -43,18 +43,15 @@ section
 
   theorem hcongr_fun {f : Π x, P x} {f' : Π x, P' x} (a : A) (H₁ : f == f') (H₂ : P = P') :
     f a == f' a :=
-  have aux : ∀ (f : Π x, P x) (f' : Π x, P x), f == f' → f a == f' a, from
-    take f f' H, heq.to_eq H ▸ heq.refl (f a),
-  (H₂ ▸ aux) f f' H₁
+  begin
+    cases H₂, cases H₁, reflexivity
+  end
 
   theorem hcongr {P' : A' → Type} {f : Π a, P a} {f' : Π a', P' a'} {a : A} {a' : A'}
       (Hf : f == f') (HP : P == P') (Ha : a == a') : f a == f' a' :=
-  have H1 : ∀ (B P' : A → Type) (f : Π x, P x) (f' : Π x, P' x), f == f' → (λx, P x) == (λx, P' x)
-              → f a == f' a, from
-    take P P' f f' Hf HB, hcongr_fun a Hf (heq.to_eq HB),
-  have H2 : ∀ (B : A → Type) (P' : A' → Type) (f : Π x, P x) (f' : Π x, P' x),
-      f == f' → (λx, P x) == (λx, P' x) → f a == f' a', from heq.subst Ha H1,
-  H2 P P' f f' Hf HP
+  begin
+    cases Ha, cases HP, cases Hf, reflexivity
+  end
 
   theorem hcongr_arg (f : Πx, P x) {a b : A} (H : a = b) : f a == f b :=
   H ▸ (heq.refl (f a))
@@ -78,9 +75,7 @@ section
 
   -- should H₁ be explicit (useful in e.g. hproof_irrel)
   theorem eq_rec_to_heq {H₁ : a = a'} {p : P a} {p' : P a'} (H₂ : eq.rec_on H₁ p = p') : p == p' :=
-  calc
-    p == eq.rec_on H₁ p : heq.symm (eq_rec_heq H₁ p)
-   ... =  p'            : H₂
+  by subst H₁; subst H₂
 
   theorem cast_to_heq {H₁ : A = B} (H₂ : cast H₁ a = b) : a == b :=
   eq_rec_to_heq H₂
@@ -91,18 +86,13 @@ section
   --TODO: generalize to eq.rec. This is a special case of rec_on_compose in eq.lean
   theorem cast_trans (Hab : A = B) (Hbc : B = C) (a : A) :
     cast Hbc (cast Hab a) = cast (Hab ⬝ Hbc) a :=
-  heq.to_eq (calc
-    cast Hbc (cast Hab a)  == cast Hab a         : eq_rec_heq Hbc (cast Hab a)
-                       ... == a                  : eq_rec_heq Hab a
-                       ... == cast (Hab ⬝ Hbc) a : heq.symm (eq_rec_heq (Hab ⬝ Hbc) a))
+  by subst Hab
 
   theorem pi_eq (H : P = P') : (Π x, P x) = (Π x, P' x) :=
-  H ▸ (eq.refl (Π x, P x))
+  by subst H
 
   theorem rec_on_app (H : P = P') (f : Π x, P x) (a : A) : eq.rec_on H f a == f a :=
-  have aux : ∀ H : P = P, eq.rec_on H f a == f a, from
-    take H : P = P, heq.refl (eq.rec_on H f a),
-  (H ▸ aux) H
+  by subst H
 
   theorem rec_on_pull (H : P = P') (f : Π x, P x) (a : A) :
     eq.rec_on H f a = eq.rec_on (congr_fun H a) (f a) :=
@@ -111,18 +101,13 @@ section
       ... == eq.rec_on (congr_fun H a) (f a) : heq.symm (eq_rec_heq (congr_fun H a) (f a)))
 
   theorem cast_app (H : P = P') (f : Π x, P x) (a : A) : cast (pi_eq H) f a == f a :=
-  have H₁ : ∀ (H : (Π x, P x) = (Π x, P x)), cast H f a == f a, from
-    assume H, heq.of_eq (congr_fun (cast_eq H f) a),
-  have H₂ : ∀ (H : (Π x, P x) = (Π x, P' x)), cast H f a == f a, from
-    H ▸ H₁,
-  H₂ (pi_eq H)
+  by subst H
 end
 
 -- function extensionality wrt heterogeneous equality
 theorem hfunext {A : Type} {B : A → Type} {B' : A → Type} {f : Π x, B x} {g : Π x, B' x}
                 (H : ∀ a, f a == g a) : f == g :=
-let HH : B = B' := (funext (λ x, heq.type_eq (H x))) in
-  cast_to_heq (funext (λ a, heq.to_eq (heq.trans (cast_app HH f a) (H a))))
+cast_to_heq (funext (λ a, heq.to_eq (heq.trans (cast_app (funext (λ x, heq.type_eq (H x))) f a) (H a))))
 
 section
   variables {A : Type} {B : A → Type} {C : Πa, B a → Type} {D : Πa b, C a b → Type}
@@ -168,14 +153,4 @@ section
       (Hd : cast (hdcongr_arg3 D Ha Hb Hc) d = d')
         : f a b c d = f a' b' c' d' :=
   heq.to_eq (hcongr_arg4 f Ha Hb (eq_rec_to_heq Hc) (eq_rec_to_heq Hd))
-
-  --Is a reasonable version of "hcongr2" provable without pi_ext and funext?
-  --It looks like you need some ugly extra conditions
-
-  -- theorem hcongr2' {A A' : Type} {B : A → Type} {B' : A' → Type} {C : Πa, B a → Type} {C' : Πa, B' a  → Type}
-  --     {f : Π a b, C a b} {f' : Π a' b', C' a' b'} {a : A} {a' : A'} {b : B a} {b' : B' a'}
-  --     (HBB' : B == B') (HCC' : C == C')
-  --     (Hff' : f == f') (Haa' : a == a') (Hbb' : b == b') : f a b == f' a' b' :=
-  -- hcongr (hcongr Hff' (sorry) Haa') (hcongr HCC' (sorry) Haa') Hbb'
-
 end