From 6701e5499f853c7a6792fd10954bc2a4057d7f17 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 20 Jun 2016 11:05:21 -0700
Subject: [PATCH] feat(library/init): remove 'sorry's from sigma

---
 library/init/default.lean   |  2 +-
 library/init/sigma.lean     | 30 ------------------
 library/init/sigma_lex.lean | 63 +++++++++++++++++++++++++++++++++++++
 3 files changed, 64 insertions(+), 31 deletions(-)
 create mode 100644 library/init/sigma_lex.lean

diff --git a/library/init/default.lean b/library/init/default.lean
index f9cad94fe3..e5fd71b800 100644
--- a/library/init/default.lean
+++ b/library/init/default.lean
@@ -11,4 +11,4 @@ import init.funext init.function init.subtype init.classical init.simplifier
 import init.monad init.fin init.list init.char init.string init.to_string
 import init.timeit init.trace init.unsigned init.ordering
 import init.meta
-import init.wf init.wf_k
+import init.wf init.wf_k init.sigma_lex
diff --git a/library/init/sigma.lean b/library/init/sigma.lean
index 82a5196aaa..d1b7ec85fb 100644
--- a/library/init/sigma.lean
+++ b/library/init/sigma.lean
@@ -37,35 +37,5 @@ namespace sigma
     ∀(H₁ : p₁.1 = p₂.1) (H₂ : eq.rec_on H₁ p₁.2 = p₂.2), p₁ = p₂ :=
   destruct p₁ (take a₁ b₁, destruct p₂ (take a₂ b₂ H₁ H₂, dpair_eq H₁ H₂))
 
-  -- Lexicographical order based on Ra and Rb
-  inductive lex : sigma B → sigma B → Prop :=
-  | left  : ∀{a₁ b₁} a₂ b₂, Ra a₁ a₂   → lex ⟨a₁, b₁⟩ ⟨a₂, b₂⟩
-  | right : ∀a {b₁ b₂},     Rb a b₁ b₂ → lex ⟨a, b₁⟩  ⟨a, b₂⟩
-  end
-
-  section
-  parameters {A : Type} {B : A → Type}
-  parameters {Ra  : A → A → Prop} {Rb : Π a : A, B a → B a → Prop}
-  local infix `≺`:50 := lex Ra Rb
-
-  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 : 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
-              @sigma.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₁ : A) (b₁ : B a₁) (a₂ : A) (b₂ : B a₂) (H : Ra a₁ a₂) (eq₂ : a₂ = xa) (eq₃ : b₂ == xb),
-                  sorry) -- 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),
-                  sorry), -- begin cases eq₂, cases eq₃, exact (iHb b₁ H) end),
-            aux rfl !heq.refl)))
-
-  -- The lexicographical order of well founded relations is well-founded
-  definition lex.wf (Ha : well_founded Ra) (Hb : ∀ x, well_founded (Rb x)) : well_founded (lex Ra Rb) :=
-  well_founded.intro (λp, destruct p (λa b, lex.accessible (Ha a) Hb b))
   end
 end sigma
diff --git a/library/init/sigma_lex.lean b/library/init/sigma_lex.lean
new file mode 100644
index 0000000000..a201661e15
--- /dev/null
+++ b/library/init/sigma_lex.lean
@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Leonardo de Moura
+-/
+prelude
+import init.sigma init.meta init.combinator
+
+namespace sigma
+section
+  variables {A : Type} {B : A → Type}
+  variable  (Ra  : A → A → Prop)
+  variable  (Rb  : ∀ a, B a → B a → Prop)
+
+  -- Lexicographical order based on Ra and Rb
+  inductive lex : sigma B → sigma B → Prop :=
+  | left  : ∀{a₁ b₁} a₂ b₂, Ra a₁ a₂   → lex ⟨a₁, b₁⟩ ⟨a₂, b₂⟩
+  | right : ∀a {b₁ b₂},     Rb a b₁ b₂ → lex ⟨a, b₁⟩  ⟨a, b₂⟩
+end
+
+set_option trace.app_builder  true
+
+section
+  open ops well_founded tactic
+  parameters {A : Type} {B : A → Type}
+  parameters {Ra  : A → A → Prop} {Rb : Π a : A, B a → B a → Prop}
+  local infix `≺`:50 := lex Ra Rb
+
+  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 : 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
+              @sigma.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₁ : A) (b₁ : B a₁) (a₂ : A) (b₂ : B a₂) (H : Ra a₁ a₂) (eq₂ : a₂ = xa) (eq₃ : b₂ == xb),
+                  by do
+                     /- TODO(Leo): cleanup using quotations -/
+                     subst "eq₂",
+                     iHa : expr ← get_local "iHa", a₁ ← get_local "a₁", H ← get_local "H", b₁ ← get_local "b₁",
+                     exact (iHa a₁ H b₁))
+                (λ (a : A) (b₁ b₂ : B a) (H : Rb a b₁ b₂) (eq₂ : a = xa) (eq₃ : b₂ == xb),
+                  by do
+                     /- TODO(Leo): cleanup using quotations -/
+                    subst "eq₂",
+                    eq₃ ← get_local "eq₃",
+                    new_eq₃ ← mk_app "eq_of_heq" [eq₃],
+                    note "new_eq₃" new_eq₃,
+                    subst "new_eq₃",
+                    iHb : expr ← get_local "iHb", b₁ ← get_local "b₁", H ← get_local "H",
+                    exact (iHb b₁ H)),
+                   -- begin cases eq₂, cases eq₃, exact (iHb b₁ H) end),
+            aux rfl !heq.refl)))
+
+  -- The lexicographical order of well founded relations is well-founded
+  definition lex.wf (Ha : well_founded Ra) (Hb : ∀ x, well_founded (Rb x)) : well_founded (lex Ra Rb) :=
+  well_founded.intro (λp, destruct p (λa b, lex.accessible (Ha a) Hb b))
+
+end
+end sigma