From b900e9171d8d6fbd130d64b38d8470860d598f3b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 12 Dec 2014 12:36:51 -0800
Subject: [PATCH] refactor(library/init/sigma): simplify lex.accessible proof
 using 'cases' tactic

---
 library/init/sigma.lean | 42 +++++------------------------------------
 1 file changed, 5 insertions(+), 37 deletions(-)

diff --git a/library/init/sigma.lean b/library/init/sigma.lean
index 113a77334..a3ac19c60 100644
--- a/library/init/sigma.lean
+++ b/library/init/sigma.lean
@@ -37,52 +37,20 @@ namespace sigma
   parameters {Ra  : A → A → Prop} {Rb : Π a : A, B a → B a → Prop}
   infix `≺`:50 := lex Ra Rb
 
-  set_option pp.beta true
-
-  variables {C : Πa, B a → Type} {D : Πa b, C a b → Type}
-  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'}
-
-  private theorem hcongr_arg2 (f : Πa b, C a b) (Ha : a = a') (Hb : b == b') : f a b == f a' b' :=
-  hcongr (hcongr_arg f Ha) (hcongr_arg C Ha) Hb
-
-  private theorem hcongr_arg3 (f : Πa b c, D a b c) (Ha : a = a') (Hb : b == b') (Hc : c == c')
-      : f a b c == f a' b' c' :=
-  hcongr (hcongr_arg2 f Ha Hb) (hcongr_arg2 D Ha Hb) Hc
-
   definition lex.accessible {a} (aca : acc Ra a) (acb : ∀a, well_founded (Rb a)) : ∀ (b : B a), acc (lex Ra Rb) ⟨a, b⟩ :=
   acc.rec_on aca
     (λxa aca (iHa : ∀y, Ra y xa → ∀b : B y, acc (lex Ra Rb) ⟨y, b⟩),
       λb : B xa, acc.rec_on (acb xa b)
         (λxb acb
-          (iHb : ∀y, Rb xa y xb → acc (lex Ra Rb) ⟨xa, y⟩),
+          (iHb : ∀ (y : B xa), Rb xa y xb → acc (lex Ra Rb) ⟨xa, y⟩),
           acc.intro ⟨xa, xb⟩ (λp (lt : p ≺ ⟨xa, xb⟩),
             have aux : xa = xa → xb == xb → acc (lex Ra Rb) p, from
               @lex.rec_on A B Ra Rb (λp₁ p₂, p₂.1 = xa → p₂.2 == xb → acc (lex Ra Rb) p₁)
                          p ⟨xa, xb⟩ lt
-                (λa₁ b₁ a₂ b₂ (H : Ra a₁ a₂) (eq₂ : a₂ = xa) (eq₃ : b₂ == xb),
-                  show acc (lex Ra Rb) ⟨a₁, b₁⟩, from
-                  have Ra₁  : Ra a₁ xa, from eq.rec_on eq₂ H,
-                  iHa a₁ Ra₁ b₁)
-                (λa b₁ b₂ (H : Rb a b₁ b₂) (eq₂ : a = xa) (eq₃ : b₂ == xb),
-                  -- TODO(Leo): cleanup this proof
-                  show acc (lex Ra Rb) ⟨a, b₁⟩, from
-                  let b₁' : B xa := eq.rec_on eq₂ b₁ in
-                  have aux₁ : b₁ == b₁', from
-                    heq.symm (eq_rec_heq eq₂ b₁),
-                  have aux₂ : Rb a b₁ b₂ = Rb xa b₁' xb, from
-                    heq.to_eq (hcongr_arg3 Rb eq₂ aux₁ eq₃),
-                  have aux₃ : Rb xa b₁' xb, from
-                    eq.rec_on aux₂ H,
-                  have aux₄ : acc (lex Ra Rb) ⟨xa, b₁'⟩, from
-                    iHb b₁' aux₃,
-                  have aux₅ : ∀ (b₁ b₂ : B a) (H₁ : a = a) (H₂ : b₁ == b₂), acc (lex Ra Rb) ⟨a, b₁⟩ → acc (lex Ra Rb) ⟨a, b₂⟩, from
-                    λ b₁ b₂ H₁ H₂ Ha, eq.rec_on (heq.to_eq H₂) Ha,
-                  have aux₆ : ∀ (b₁ : B xa) (b₂ : B a) (H₁ : a = xa) (H₂ : b₁ == b₂), acc (lex Ra Rb) ⟨xa, b₁⟩ → acc (lex Ra Rb) ⟨a, b₂⟩, from
-                    eq.rec_on eq₂ aux₅,
-                  aux₆ b₁' b₁ eq₂ (heq.symm aux₁) aux₄),
+                (λ (a₁ : A) (b₁ : B a₁) (a₂ : A) (b₂ : B a₂) (H : Ra a₁ a₂) (eq₂ : a₂ = xa) (eq₃ : b₂ == xb),
+                  begin cases eq₂, exact (iHa a₁ H b₁) end)
+                (λ (a : A) (b₁ b₂ : B a) (H : Rb a b₁ b₂) (eq₂ : a = xa) (eq₃ : b₂ == xb),
+                  begin cases eq₂, cases eq₃, exact (iHb b₁ H) end),
             aux rfl !heq.refl)))
 
   -- The lexicographical order of well founded relations is well-founded