From 212b073990426dccd8799294c583e2e58a015463 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 1 Aug 2016 13:22:21 -0700 Subject: Add documentation: Equality, HProp, Isomorphism, Sigma (#41) * Add doc: Equality, HProp, Isomorphism, Sigma * Update documentation with suggestions from Andres --- src/Util/Equality.v | 38 +++++++++++++++++++++++++++++++++++++- src/Util/HProp.v | 7 +++++++ src/Util/Isomorphism.v | 29 +++++++++++++++++++++++++++++ src/Util/Sigma.v | 32 ++++++++++++++++++++++++++++++++ 4 files changed, 105 insertions(+), 1 deletion(-) (limited to 'src') 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)] -- cgit v1.2.3