From a41850227a626d2ef58204da7a1b3ca75f83fbc6 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 10 Oct 2014 14:52:21 -0700
Subject: [PATCH] refactor(library/logic): use new K-like reduction to simplify
 some proofs

---
 library/logic/cast.lean |  3 +--
 library/logic/eq.lean   | 18 +++++++++---------
 2 files changed, 10 insertions(+), 11 deletions(-)

diff --git a/library/logic/cast.lean b/library/logic/cast.lean
index 65269b2f41..25c94e0928 100644
--- a/library/logic/cast.lean
+++ b/library/logic/cast.lean
@@ -16,8 +16,7 @@ theorem cast_proof_irrel {A B : Type} (H₁ H₂ : A = B) (a : A) : cast H₁ a
 rfl
 
 theorem cast_eq {A : Type} (H : A = A) (a : A) : cast H a = a :=
-calc cast H a = cast (eq.refl A) a : rfl
-         ...  = a                  : rfl
+rfl
 
 inductive heq.{l} {A : Type.{l}} (a : A) : Π {B : Type.{l}}, B → Prop :=
 refl : heq a a
diff --git a/library/logic/eq.lean b/library/logic/eq.lean
index e8722e2e32..063b9ce26a 100644
--- a/library/logic/eq.lean
+++ b/library/logic/eq.lean
@@ -26,7 +26,7 @@ section
   variables {A : Type}
   variables {a b c : A}
   theorem id_refl (H₁ : a = a) : H₁ = (eq.refl a) :=
-  !proof_irrel
+  rfl
 
   theorem irrel (H₁ H₂ : a = b) : H₁ = H₂ :=
   !proof_irrel
@@ -58,7 +58,7 @@ namespace eq
   eq.rec (λH₁ : a = a, show B a H₁, from H₂) H₁ H₁
 
   theorem rec_on_id {A : Type} {a : A} {B : Πa' : A, a = a' → Type} (H : a = a) (b : B a H) : rec_on H b = b :=
-  refl (rec_on rfl b)
+  rfl
 
   theorem rec_on_constant {A : Type} {a a' : A} {B : Type} (H : a = a') (b : B) : rec_on H b = b :=
   rec_on H (λ(H' : a = a), rec_on_id H' b) H
@@ -72,7 +72,7 @@ namespace eq
   rec_on H (λ(H : a = a) (H' : f a = f a), rec_on_id H b ⬝ rec_on_id H' b⁻¹) H H'
 
   theorem rec_id {A : Type} {a : A} {B : A → Type} (H : a = a) (b : B a) : rec b H = b :=
-  id_refl H⁻¹ ▸ refl (eq.rec b (refl a))
+  rfl
 
   theorem rec_on_compose {A : Type} {a b c : A} {P : A → Type} (H₁ : a = b) (H₂ : b = c)
           (u : P a) :
@@ -127,12 +127,12 @@ end
 
 section
   variables {A : Type} {B : A → Type} {C : Πa, B a → Type} {D : Πa b, C a b → Type} {R : Type}
-  variables {a₁ a₂ : A} 
-            {b₁ : B a₁} {b₂ : B a₂} 
-            {c₁ : C a₁ b₁} {c₂ : C a₂ b₂} 
+  variables {a₁ a₂ : A}
+            {b₁ : B a₁} {b₂ : B a₂}
+            {c₁ : C a₁ b₁} {c₂ : C a₂ b₂}
             {d₁ : D a₁ b₁ c₁} {d₂ : D a₂ b₂ c₂}
 
-  theorem congr_arg2_dep (f : Πa, B a → R) (H₁ : a₁ = a₂) (H₂ : eq.rec_on H₁ b₁ = b₂) 
+  theorem congr_arg2_dep (f : Πa, B a → R) (H₁ : a₁ = a₂) (H₂ : eq.rec_on H₁ b₁ = b₂)
       : f a₁ b₁ = f a₂ b₂ :=
   eq.rec_on H₁
     (λ (b₂ : B a₁) (H₁ : a₁ = a₁) (H₂ : eq.rec_on H₁ b₁ = b₂),
@@ -152,7 +152,7 @@ section
 
   -- for the moment the following theorem is commented out, because it takes long to prove
   -- theorem congr_arg4_dep (f : Πa b c, D a b c → R) (H₁ : a₁ = a₂) (H₂ : eq.rec_on H₁ b₁ = b₂)
-  --     (H₃ : eq.rec_on (congr_arg2_dep C H₁ H₂) c₁ = c₂) 
+  --     (H₃ : eq.rec_on (congr_arg2_dep C H₁ H₂) c₁ = c₂)
   --     (H₄ : eq.rec_on (congr_arg3_dep D H₁ H₂ H₃) d₁ = d₂) : f a₁ b₁ c₁ d₁ = f a₂ b₂ c₂ d₂ :=
   -- eq.rec_on H₁
   --   (λ b₂ H₂ c₂ H₃ d₂ (H₄ : _),
@@ -261,5 +261,5 @@ definition elim {A : Type} (H : subsingleton A) : ∀(a b : A), a = b :=
 rec (fun p, p) H
 end subsingleton
 
-protected definition prop.subsingleton [instance] (P : Prop) : subsingleton P := 
+protected definition prop.subsingleton [instance] (P : Prop) : subsingleton P :=
 subsingleton.intro (λa b, !proof_irrel)