diff options
Diffstat (limited to 'theories/Logic/Eqdep.v')
-rw-r--r--[-rwxr-xr-x] | theories/Logic/Eqdep.v | 182 |
1 files changed, 14 insertions, 168 deletions
diff --git a/theories/Logic/Eqdep.v b/theories/Logic/Eqdep.v index 24905039..2fe9d1a6 100755..100644 --- a/theories/Logic/Eqdep.v +++ b/theories/Logic/Eqdep.v @@ -6,183 +6,29 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Eqdep.v,v 1.10.2.1 2004/07/16 19:31:06 herbelin Exp $ i*) +(*i $Id: Eqdep.v 8642 2006-03-17 10:09:02Z notin $ i*) -(** This file defines dependent equality and shows its equivalence with - equality on dependent pairs (inhabiting sigma-types). It axiomatizes - the invariance by substitution of reflexive equality proofs and - shows the equivalence between the 4 following statements +(** This file axiomatizes the invariance by substitution of reflexive + equality proofs [[Streicher93]] and exports its consequences, such + as the injectivity of the projection of the dependent pair. - - Invariance by Substitution of Reflexive Equality Proofs. - - Injectivity of Dependent Equality - - Uniqueness of Identity Proofs - - Uniqueness of Reflexive Identity Proofs - - Streicher's Axiom K - - These statements are independent of the calculus of constructions [2]. - - References: - - [1] T. Streicher, Semantical Investigations into Intensional Type Theory, - Habilitationsschrift, LMU München, 1993. - [2] M. Hofmann, T. Streicher, The groupoid interpretation of type theory, - Proceedings of the meeting Twenty-five years of constructive - type theory, Venice, Oxford University Press, 1998 + [[Streicher93]] T. Streicher, Semantical Investigations into + Intensional Type Theory, Habilitationsschrift, LMU München, 1993. *) -Section Dependent_Equality. - -Variable U : Type. -Variable P : U -> Type. - -(** Dependent equality *) - -Inductive eq_dep (p:U) (x:P p) : forall q:U, P q -> Prop := - eq_dep_intro : eq_dep p x p x. -Hint Constructors eq_dep: core v62. - -Lemma eq_dep_sym : - forall (p q:U) (x:P p) (y:P q), eq_dep p x q y -> eq_dep q y p x. -Proof. -destruct 1; auto. -Qed. -Hint Immediate eq_dep_sym: core v62. +Require Export EqdepFacts. -Lemma eq_dep_trans : - forall (p q r:U) (x:P p) (y:P q) (z:P r), - eq_dep p x q y -> eq_dep q y r z -> eq_dep p x r z. -Proof. -destruct 1; auto. -Qed. - -Scheme eq_indd := Induction for eq Sort Prop. - -Inductive eq_dep1 (p:U) (x:P p) (q:U) (y:P q) : Prop := - eq_dep1_intro : forall h:q = p, x = eq_rect q P y p h -> eq_dep1 p x q y. - -Lemma eq_dep1_dep : - forall (p:U) (x:P p) (q:U) (y:P q), eq_dep1 p x q y -> eq_dep p x q y. -Proof. -destruct 1 as (eq_qp, H). -destruct eq_qp using eq_indd. -rewrite H. -apply eq_dep_intro. -Qed. - -Lemma eq_dep_dep1 : - forall (p q:U) (x:P p) (y:P q), eq_dep p x q y -> eq_dep1 p x q y. -Proof. -destruct 1. -apply eq_dep1_intro with (refl_equal p). -simpl in |- *; trivial. -Qed. - -(** Invariance by Substitution of Reflexive Equality Proofs *) +Module Eq_rect_eq. Axiom eq_rect_eq : - forall (p:U) (Q:U -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h. - -(** Injectivity of Dependent Equality is a consequence of *) -(** Invariance by Substitution of Reflexive Equality Proof *) - -Lemma eq_dep1_eq : forall (p:U) (x y:P p), eq_dep1 p x p y -> x = y. -Proof. -simple destruct 1; intro. -rewrite <- eq_rect_eq; auto. -Qed. - -Lemma eq_dep_eq : forall (p:U) (x y:P p), eq_dep p x p y -> x = y. -Proof. -intros; apply eq_dep1_eq; apply eq_dep_dep1; trivial. -Qed. - -End Dependent_Equality. - -(** Uniqueness of Identity Proofs (UIP) is a consequence of *) -(** Injectivity of Dependent Equality *) - -Lemma UIP : forall (U:Type) (x y:U) (p1 p2:x = y), p1 = p2. -Proof. -intros; apply eq_dep_eq with (P := fun y => x = y). -elim p2 using eq_indd. -elim p1 using eq_indd. -apply eq_dep_intro. -Qed. - -(** Uniqueness of Reflexive Identity Proofs is a direct instance of UIP *) - -Lemma UIP_refl : forall (U:Type) (x:U) (p:x = x), p = refl_equal x. -Proof. -intros; apply UIP. -Qed. - -(** Streicher axiom K is a direct consequence of Uniqueness of - Reflexive Identity Proofs *) - -Lemma Streicher_K : - forall (U:Type) (x:U) (P:x = x -> Prop), - P (refl_equal x) -> forall p:x = x, P p. -Proof. -intros; rewrite UIP_refl; assumption. -Qed. - -(** We finally recover eq_rec_eq (alternatively eq_rect_eq) from K *) - -Lemma eq_rec_eq : - forall (U:Type) (P:U -> Set) (p:U) (x:P p) (h:p = p), x = eq_rec p P x p h. -Proof. -intros. -apply Streicher_K with (p := h). -reflexivity. -Qed. - -(** Dependent equality is equivalent to equality on dependent pairs *) - -Lemma equiv_eqex_eqdep : - forall (U:Set) (P:U -> Set) (p q:U) (x:P p) (y:P q), - existS P p x = existS P q y <-> eq_dep U P p x q y. -Proof. -split. -(* -> *) -intro H. -change p with (projS1 (existS P p x)) in |- *. -change x at 2 with (projS2 (existS P p x)) in |- *. -rewrite H. -apply eq_dep_intro. -(* <- *) -destruct 1; reflexivity. -Qed. - -(** UIP implies the injectivity of equality on dependent pairs *) - -Lemma inj_pair2 : - forall (U:Set) (P:U -> Set) (p:U) (x y:P p), - existS P p x = existS P p y -> x = y. -Proof. -intros. -apply (eq_dep_eq U P). -generalize (equiv_eqex_eqdep U P p p x y). -simple induction 1. -intros. -auto. -Qed. + forall (U:Type) (p:U) (Q:U -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h. -(** UIP implies the injectivity of equality on dependent pairs *) +End Eq_rect_eq. -Lemma inj_pairT2 : - forall (U:Type) (P:U -> Type) (p:U) (x y:P p), - existT P p x = existT P p y -> x = y. -Proof. -intros. -apply (eq_dep_eq U P). -change p at 1 with (projT1 (existT P p x)) in |- *. -change x at 2 with (projT2 (existT P p x)) in |- *. -rewrite H. -apply eq_dep_intro. -Qed. +Module EqdepTheory := EqdepTheory(Eq_rect_eq). +Export EqdepTheory. -(** The main results to be exported *) +(** Exported hints *) -Hint Resolve eq_dep_intro eq_dep_eq: core v62. -Hint Immediate eq_dep_sym: core v62. +Hint Resolve eq_dep_eq: core v62. Hint Resolve inj_pair2 inj_pairT2: core. |