From a662f925cb4354f182e5beae2adb267ae94a26da Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Sat, 23 May 2015 14:21:16 +1000
Subject: [PATCH] refactor(library/data/quotient.lean): improve comments

---
 library/data/quotient/basic.lean     | 28 +++++++++++-----------------
 library/data/quotient/classical.lean | 14 ++++++++------
 library/data/quotient/quotient.md    |  6 +++++-
 library/data/quotient/util.lean      |  3 ---
 4 files changed, 24 insertions(+), 27 deletions(-)

diff --git a/library/data/quotient/basic.lean b/library/data/quotient/basic.lean
index 537720a00..872e1429e 100644
--- a/library/data/quotient/basic.lean
+++ b/library/data/quotient/basic.lean
@@ -1,10 +1,10 @@
--- Copyright (c) 2014 Floris van Doorn. All rights reserved.
--- Released under Apache 2.0 license as described in the file LICENSE.
--- Author: Floris van Doorn
-
--- Theory data.quotient
--- ====================
+/-
+Copyright (c) 2014 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Floris van Doorn
 
+An explicit treatment of quotients, without using Lean's built-in quotient types.
+-/
 import logic data.subtype logic.cast algebra.relation data.prod
 import logic.instances
 import .util
@@ -14,9 +14,7 @@ open subtype relation.iff_ops
 
 namespace quotient
 
-
--- definition and basics
--- ---------------------
+/- definition and basics -/
 
 -- TODO: make this a structure
 definition is_quotient {A B : Type} (R : A → A → Prop) (abs : A → B) (rep : B → A) : Prop :=
@@ -107,9 +105,7 @@ have Hc : R c c, from refl_right Q Hbc,
 have Hac : abs a = abs c, from eq.trans (eq_abs Q Hab) (eq_abs Q Hbc),
 R_intro Q Ha Hc Hac
 
-
--- recursion
--- ---------
+/- recursion -/
 
 -- (maybe some are superfluous)
 
@@ -195,8 +191,8 @@ theorem comp_quotient_map_binary_refl {A B : Type} {R : A → A → Prop} (Hrefl
   (a b : A) : quotient_map_binary Q f (abs a) (abs b) = abs (f a b) :=
 comp_quotient_map_binary Q H (Hrefl a) (Hrefl b)
 
--- image
--- -----
+/- image -/
+
 definition image {A B : Type} (f : A → B) := subtype (fun b, ∃a, f a = b)
 
 theorem image_inhabited {A B : Type} (f : A → B) (H : inhabited A) : inhabited (image f) :=
@@ -253,9 +249,7 @@ calc
     ... = f a : H a
     ... = elt_of u : Ha
 
-
--- construct quotient from representative map
--- ------------------------------------------
+/- construct quotient from representative map -/
 
 theorem representative_map_idempotent {A : Type} {R : A → A → Prop} {f : A → A}
     (H1 : ∀a, R a (f a)) (H2 : ∀a b, R a b ↔ R a a ∧ R b b ∧ f a = f b) (a : A) :
diff --git a/library/data/quotient/classical.lean b/library/data/quotient/classical.lean
index c3da18b1f..bbf89c2cf 100644
--- a/library/data/quotient/classical.lean
+++ b/library/data/quotient/classical.lean
@@ -1,6 +1,10 @@
--- Copyright (c) 2014 Floris van Doorn. All rights reserved.
--- Released under Apache 2.0 license as described in the file LICENSE.
--- Author: Floris van Doorn
+/-
+Copyright (c) 2014 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Floris van Doorn
+
+A classical treatment of quotients, using Hilbert choice.
+-/
 import algebra.relation data.subtype logic.axioms.classical logic.axioms.hilbert
 import .basic
 
@@ -8,8 +12,7 @@ namespace quotient
 
 open relation nonempty subtype
 
--- abstract quotient
--- -----------------
+/- abstract quotient -/
 
 definition prelim_map {A : Type} (R : A → A → Prop) (a : A) :=
 -- TODO: it is interesting how the elaborator fails here
@@ -46,7 +49,6 @@ fun_image (prelim_map R)
 
 definition quotient_elt_of {A : Type} (R : A → A → Prop) : quotient R → A := elt_of
 
--- TODO: I had to make is_quotient transparent -- change this?
 theorem quotient_is_quotient  {A : Type} (R : A → A → Prop) (H : is_equivalence R)
   : is_quotient R (quotient_abs R) (quotient_elt_of R) :=
 representative_map_to_quotient_equiv
diff --git a/library/data/quotient/quotient.md b/library/data/quotient/quotient.md
index 09bb1f145..da837789a 100644
--- a/library/data/quotient/quotient.md
+++ b/library/data/quotient/quotient.md
@@ -1,6 +1,10 @@
 data.quotient
 =============
 
-* [aux](aux.lean) : auxiliary facts about products
+* [util](util.lean) : auxiliary facts about products
 * [basic](basic.lean) : the constructive core of the quotient construction
 * [classical](classical.lean) : the classical version, using Hilbert choice
+
+These files provide an approach to defining quotients, without using
+the built-in quotient types. They were initially used to define the
+integers, but are no longer used there.
\ No newline at end of file
diff --git a/library/data/quotient/util.lean b/library/data/quotient/util.lean
index f2d6ef3d6..44722ec5f 100644
--- a/library/data/quotient/util.lean
+++ b/library/data/quotient/util.lean
@@ -1,11 +1,8 @@
 /-
 Copyright (c) 2014 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.quotient.util
 Author: Floris van Doorn
 -/
-
 import logic ..prod algebra.relation
 import tools.fake_simplifier