From 4d52d4c7905adbb163932d1bd667106d2f8b8312 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 5 Jun 2015 08:04:55 -0700
Subject: [PATCH] fix(library/init/quot): prove quot.exact

---
 library/init/quot.lean           | 30 +++++++++++++++++++++++++++---
 src/kernel/quotient/quotient.cpp |  5 +----
 2 files changed, 28 insertions(+), 7 deletions(-)

diff --git a/library/init/quot.lean b/library/init/quot.lean
index c4aa68640..49ec6fde6 100644
--- a/library/init/quot.lean
+++ b/library/init/quot.lean
@@ -14,11 +14,10 @@ constant quot.{l}   : Π {A : Type.{l}}, setoid A → Type.{l}
 constant propext {a b : Prop} : (a ↔ b) → a = b
 
 namespace quot
-  constant mk        : Π {A : Type}   [s : setoid A], A → quot s
-  notation `⟦`:max a `⟧`:0 := mk a
+  protected constant mk        : Π {A : Type}   [s : setoid A], A → quot s
+  notation `⟦`:max a `⟧`:0 := quot.mk a
 
   constant sound     : Π {A : Type}   [s : setoid A] {a b : A}, a ≈ b → ⟦a⟧ = ⟦b⟧
-  constant exact     : Π {A : Type}   [s : setoid A] {a b : A}, ⟦a⟧ = ⟦b⟧ → a ≈ b
   constant lift      : Π {A B : Type} [s : setoid A] (f : A → B), (∀ a b, a ≈ b → f a = f b) → quot s → B
   constant ind       : ∀ {A : Type}   [s : setoid A] {B : quot s → Prop}, (∀ a, B ⟦a⟧) → ∀ q, B q
 
@@ -111,6 +110,31 @@ namespace quot
   quot.ind (λ a₁, quot.ind (λ a₂, quot.ind (λ a₃, H a₁ a₂ a₃) q₃) q₂) q₁
   end
 
+  section exact
+  variable {A : Type}
+  variable [s : setoid A]
+  include s
+
+  private definition rel (q₁ q₂ : quot s) : Prop :=
+  quot.lift_on₂ q₁ q₂
+    (λ a₁ a₂, a₁ ≈ a₂)
+    (λ a₁ a₂ b₁ b₂ a₁b₁ a₂b₂,
+      propext (iff.intro
+        (λ a₁a₂, setoid.trans (setoid.symm a₁b₁) (setoid.trans a₁a₂ a₂b₂))
+        (λ b₁b₂, setoid.trans a₁b₁ (setoid.trans b₁b₂ (setoid.symm a₂b₂)))))
+
+  local infix `~`:50 := rel
+
+  private lemma rel.refl : ∀ q : quot s, q ~ q :=
+  λ q, quot.induction_on q (λ a, setoid.refl a)
+
+  private lemma eq_imp_rel {q₁ q₂ : quot s} : q₁ = q₂ → q₁ ~ q₂ :=
+  assume h, eq.rec_on h (rel.refl q₁)
+
+  theorem exact {a b : A} : ⟦a⟧ = ⟦b⟧ → a ≈ b :=
+  assume h, eq_imp_rel h
+  end exact
+
   section
   variables {A B : Type}
   variables [s₁ : setoid A] [s₂ : setoid B]
diff --git a/src/kernel/quotient/quotient.cpp b/src/kernel/quotient/quotient.cpp
index 5b3f0046a..e284ca71c 100644
--- a/src/kernel/quotient/quotient.cpp
+++ b/src/kernel/quotient/quotient.cpp
@@ -19,7 +19,6 @@ static name * g_quotient_lift  = nullptr;
 static name * g_quotient_ind   = nullptr;
 static name * g_quotient_mk    = nullptr;
 static name * g_quotient_sound = nullptr;
-static name * g_quotient_exact = nullptr;
 
 struct quotient_env_ext : public environment_extension {
     bool m_initialized;
@@ -135,7 +134,7 @@ bool is_quotient_decl(environment const & env, name const & n) {
         return false;
     return
         n == *g_propext || n == *g_quotient || n == *g_quotient_lift || n == *g_quotient_ind || n == *g_quotient_mk ||
-        n == *g_quotient_sound || n == *g_quotient_exact;
+        n == *g_quotient_sound;
 }
 
 void initialize_quotient_module() {
@@ -146,7 +145,6 @@ void initialize_quotient_module() {
     g_quotient_ind       = new name{"quot", "ind"};
     g_quotient_mk        = new name{"quot", "mk"};
     g_quotient_sound     = new name{"quot", "sound"};
-    g_quotient_exact     = new name{"quot", "exact"};
     g_ext                = new quotient_env_ext_reg();
 }
 
@@ -159,6 +157,5 @@ void finalize_quotient_module() {
     delete g_quotient_ind;
     delete g_quotient_mk;
     delete g_quotient_sound;
-    delete g_quotient_exact;
 }
 }