Add documentation: Equality, HProp, Isomorphism, Sigma (#41)

* Add doc: Equality, HProp, Isomorphism, Sigma

* Update documentation with suggestions from Andres

4 files changed, 105 insertions, 1 deletions

diff --git a/src/Util/Equality.v b/src/Util/Equality.v
index 7657f96cb..3c3ddd9ff 100644
--- a/src/Util/Equality.v
+++ b/src/Util/Equality.v
@@ -1,7 +1,23 @@
-(** * Lemmas about [eq] *)
+(** * The Structure of the [eq] Type *)
+(** As described by the project of homotopy type theory, there is a
+    lot of structure inherent in the type of propositional equality,
+    [eq].  We build up enough lemmas about this structure to deal
+    nicely with proofs of equality that come up in practice in this
+    project. *)
 Require Import Crypto.Util.Isomorphism.
 Require Import Crypto.Util.HProp.
 
+(** Most of the structure of proofs of equalities fits into what
+    mathematicians call a weak ∞-groupoid.  (In fact, one way of
+    *defining* a weak ∞-groupoid is via what's called the J-rule,
+    which exactly matches the eliminator [eq_rect] for the equality
+    type [eq].)  The first level of this groupoid is given by the
+    identity [eq_refl], the binary operation [eq_trans], and the
+    inverse of [p : x = y] given by [eq_sym p : y = x].  The second
+    level, which we provide here, says that [id ∘ p = p = p ∘ id],
+    that [(p ∘ q)⁻¹ = q⁻¹ ∘ p⁻¹], that [(p⁻¹)⁻¹ = p], and that [p ∘
+    p⁻¹ = p⁻¹ ∘ p = id].  We prove these here, as well as a few lemmas
+    about functoriality of functions over equality. *)
 Definition concat_1p {A x y} (p : x = y :> A) : eq_trans eq_refl p = p.
 Proof. case p; reflexivity. Defined.
 Definition concat_p1 {A x y} (p : x = y :> A) : eq_trans p eq_refl = p.
@@ -26,6 +42,22 @@ Lemma inv_V {A x y} (p : x = y :> A)
 : eq_sym (eq_sym p) = p.
 Proof. case p; reflexivity. Defined.
 
+(** To classify the equalities of a type [A] at a point [a : A], we
+    must give a "code" that stands in for the type [a = x] for each
+    [x], and a way of "encoding" proofs of equality into the code that
+    we claim represents this type.  To prove that the code is good, it
+    turns out that it sufficies to prove that it is freely generated
+    by the encoding of [eq_refl], i.e., that [{ x : A & a = x }] and
+    [{ x : A & code x }] are equivalent, i.e., that [{ x : A & code x
+    }] is an hProp (has at most one element).  When this is the case,
+    we have fully classified the type of equalities in [A] at [a] up
+    to isomorphism.  This lets us replace proofs of equalities in [A]
+    with their codes, which are frequently easier to manipulate.  (For
+    example, the code for [x = y :> A * B] is [(fst x = fst y) * (snd
+    x = snd y)], whence we can destruct the pair.)
+
+    This method of proof, introduced in homotopy type theory, is
+    called encode-decode. *)
 Section gen.
   Context {A : Type} {x : A} (code : A -> Type)
           (encode : forall y, x = y -> code y)
@@ -61,6 +93,10 @@ Section gen.
   Defined.
 End gen.
 
+(** We use the encode-decode method to prove that if [forall x y : A,
+    x = y], then [forall (x y : A) (p q : x = y), p = q]. *)
+(* It's not clear whether this should be in this file, or in HProp.
+   But we require [IsHProp] above, so we leave it here for now. *)
 Section hprop.
   Context {A} `{IsHProp A}.
 
diff --git a/src/Util/HProp.v b/src/Util/HProp.v
index 273611fad..89ed16698 100644
--- a/src/Util/HProp.v
+++ b/src/Util/HProp.v
@@ -1,3 +1,10 @@
+(** * Homotopy Propositions *)
+(** A homotopy proposition, or hProp, is a subsingleton type, i.e., a
+    type with at most one inhabitant.  The property of being an hProp,
+    i.e., being irrelevant when considering propositional equality
+    ([eq]) of terms, comes up frequently.  Since it is frequently
+    automatically inferrable from the structure of the type, we make a
+    typeclass for it. *)
 Class IsHProp T := allpath_hprop : forall x y : T, x = y.
 
 Notation IsHPropRel R := (forall x y, IsHProp (R x y)).
diff --git a/src/Util/Isomorphism.v b/src/Util/Isomorphism.v
index 0e6553dcd..25984483e 100644
--- a/src/Util/Isomorphism.v
+++ b/src/Util/Isomorphism.v
@@ -1,3 +1,32 @@
+(** * Isomorphisms *)
+(** Following the category-theoretic definition, [f : A → B] is an
+    isomorphism when it has an inverse [f⁻¹ : B → A] which is both a
+    left and a right inverse.  In the language of homotopy type
+    theory, we are formalizing quasi-invertibility; this notion of
+    isomorphism is not an hProp.  The better notations of equivalence
+    (such that all proofs of [IsEquiv f] are equal when only assuming
+    function extensionality) are more complicated.  Possibilities
+    include: *)
+
+(** - Adjoint equivalence, the default of HoTT/HoTT: *)
+(**
+<<
+Definition Sect {A B : Type} (s : A -> B) (r : B -> A) :=
+  forall x : A, r (s x) = x.
+
+Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv {
+  equiv_inv : B -> A ;
+  eisretr : Sect equiv_inv f;
+  eissect : Sect f equiv_inv;
+  eisadj : forall x : A, eisretr (f x) = ap f (eissect x)
+}.
+>> *)
+(** - Contractible fibers: [∀ y : B, Contr { x : A | f x = y }] where
+      [Contr T := { center : T | forall y, center = y }] *)
+
+(** This is useful for classifying equalities in a theoretically nice
+    way. *)
+
 Class IsIso {A B} (f : A -> B) :=
   { iso_inv : B -> A;
     is_right_inv : forall x, f (iso_inv x) = x;
diff --git a/src/Util/Sigma.v b/src/Util/Sigma.v
index f0016dc73..414919493 100644
--- a/src/Util/Sigma.v
+++ b/src/Util/Sigma.v
@@ -1,3 +1,10 @@
+(** * Classification of the Σ Type *)
+(** In this file, we classify the basic structure of Σ types ([sigT],
+    [sig], and [ex], in Coq).  In particular, we classify equalities
+    of dependent pairs (inhabitants of Σ types), so that when we have
+    an equality between two such pairs, or when we want such an
+    equality, we have a systematic way of reducing such equalities to
+    equalities at simpler types. *)
 Require Import Crypto.Util.Equality.
 Require Import Crypto.Util.GlobalSettings.
 
@@ -7,17 +14,21 @@ Local Arguments proj1_sig {_ _} _.
 Local Arguments proj1_sig {_ _} _.
 Local Arguments f_equal {_ _} _ {_ _} _.
 
+(** ** Equality for [sigT] *)
 Section sigT.
+  (** *** Projecting an equality of a pair to equality of the first components *)
   Definition pr1_path {A} {P : A -> Type} {u v : sigT P} (p : u = v)
   : projT1 u = projT1 v
     := f_equal (@projT1 _ _) p.
 
+  (** *** Projecting an equality of a pair to equality of the second components *)
   Definition pr2_path {A} {P : A -> Type} {u v : sigT P} (p : u = v)
   : eq_rect _ _ (projT2 u) _ (pr1_path p) = projT2 v.
   Proof.
     destruct p; reflexivity.
   Defined.
 
+  (** *** Equality of [sigT] is itself a [sigT] *)
   Definition path_sigT_uncurried {A : Type} {P : A -> Type} (u v : sigT P)
              (pq : sigT (fun p : projT1 u = projT1 v => eq_rect _ _ (projT2 u) _ p = projT2 v))
   : u = v.
@@ -28,17 +39,23 @@ Section sigT.
     destruct p; reflexivity.
   Defined.
 
+  (** *** Curried version of proving equality of sigma types *)
   Definition path_sigT {A : Type} {P : A -> Type} (u v : sigT P)
              (p : projT1 u = projT1 v) (q : eq_rect _ _ (projT2 u) _ p = projT2 v)
   : u = v
     := path_sigT_uncurried u v (existT _ p q).
 
+  (** *** Equality of [sigT] when the property is an hProp *)
   Definition path_sigT_hprop {A P} (P_hprop : forall (x : A) (p q : P x), p = q)
              (u v : @sigT A P)
              (p : projT1 u = projT1 v)
     : u = v
     := path_sigT u v p (P_hprop _ _ _).
 
+  (** *** Equivalence of equality of [sigT] with a [sigT] of equality *)
+  (** We could actually use [IsIso] here, but for simplicity, we
+      don't.  If we wanted to deal with proofs of equality of Σ types
+      in dependent positions, we'd need it. *)
   Definition path_sigT_uncurried_iff {A P}
              (u v : @sigT A P)
     : u = v <-> (sigT (fun p : projT1 u = projT1 v => eq_rect _ _ (projT2 u) _ p = projT2 v)).
@@ -46,16 +63,19 @@ Section sigT.
     split; [ intro; subst; exists eq_refl; reflexivity | apply path_sigT_uncurried ].
   Defined.
 
+  (** *** Equivalence of equality of [sigT] involving hProps with equality of the first components *)
   Definition path_sigT_hprop_iff {A P} (P_hprop : forall (x : A) (p q : P x), p = q)
              (u v : @sigT A P)
     : u = v <-> (projT1 u = projT1 v)
     := conj (f_equal projT1) (path_sigT_hprop P_hprop u v).
 
+  (** *** Non-dependent classification of equality of [sigT] *)
   Definition path_sigT_nondep {A B : Type} (u v : @sigT A (fun _ => B))
              (p : projT1 u = projT1 v) (q : projT2 u = projT2 v)
   : u = v
     := @path_sigT _ _ u v p (eq_trans (transport_const _ _) q).
 
+  (** *** Classification of transporting across an equality of [sigT]s *)
   Lemma eq_rect_sigT {A x} {P : A -> Type} (Q : forall a, P a -> Prop) (u : sigT (Q x)) {y} (H : x = y)
   : eq_rect x (fun a => sigT (Q a)) u y H
     = existT
@@ -69,6 +89,7 @@ Section sigT.
   Defined.
 End sigT.
 
+(** ** Equality for [sig] *)
 Section sig.
   Definition proj1_sig_path {A} {P : A -> Prop} {u v : sig P} (p : u = v)
   : proj1_sig u = proj1_sig v
@@ -126,6 +147,7 @@ Section sig.
   Defined.
 End sig.
 
+(** ** Equality for [ex] *)
 Section ex.
   Definition path_ex_uncurried' {A : Type} (P : A -> Prop) {u1 v1 : A} {u2 : P u1} {v2 : P v1}
              (pq : exists p : u1 = v1, eq_rect _ _ u2 _ p = v2)
@@ -163,6 +185,16 @@ Section ex.
   Defined.
 End ex.
 
+(** ** Useful Tactics *)
+(** *** [inversion_sigma] *)
+(** The built-in [inversion] will frequently leave equalities of
+    dependent pairs.  When the first type in the pair is an hProp or
+    otherwise simplifies, [inversion_sigma] is useful; it will replace
+    the equality of pairs with a pair of equalities, one involving a
+    term casted along the other.  This might also prove useful for
+    writing a version of [inversion] / [dependent destruction] which
+    does not lose information, i.e., does not turn a goal which is
+    provable into one which requires axiom K / UIP.  *)
 Ltac simpl_proj_exist_in H :=
   repeat match type of H with
          | context G[proj1_sig (exist _ ?x ?p)]