diff options
author | Samuel Mimram <smimram@debian.org> | 2007-02-13 13:48:12 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2007-02-13 13:48:12 +0000 |
commit | 7f076db2a924377e9de3f9a6d838b8c44ed2e16d (patch) | |
tree | e075c526532a227c83d951c9dff8c944ea0c4d15 /theories/Logic/EqdepFacts.v | |
parent | 2a14f39fdfa80b021227396b22e38ed7c35356df (diff) | |
parent | 55ce117e8083477593cf1ff2e51a3641c7973830 (diff) |
Merge commit 'upstream/8.1+dfsg' into 8.1
Diffstat (limited to 'theories/Logic/EqdepFacts.v')
-rw-r--r-- | theories/Logic/EqdepFacts.v | 47 |
1 files changed, 16 insertions, 31 deletions
diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index a257ef55..94a577ca 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: EqdepFacts.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: EqdepFacts.v 9597 2007-02-06 19:44:05Z herbelin $ i*) (** This file defines dependent equality and shows its equivalence with equality on dependent pairs (inhabiting sigma-types). It derives @@ -105,8 +105,8 @@ Implicit Arguments eq_dep1 [U P]. (** Dependent equality is equivalent to equality on dependent pairs *) Lemma eq_sigS_eq_dep : - 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 p x q y. + forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q), + existT P p x = existT P q y -> eq_dep p x q y. Proof. intros. dependent rewrite H. @@ -114,7 +114,7 @@ Proof. Qed. Lemma equiv_eqex_eqdep : - forall (U:Set) (P:U -> Set) (p q:U) (x:P p) (y:P q), + forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q), existS P p x = existS P q y <-> eq_dep p x q y. Proof. split. @@ -248,28 +248,13 @@ End Equivalences. Section Corollaries. Variable U:Type. - Variable V:Set. (** UIP implies the injectivity of equality on dependent pairs in Type *) - - Definition Inj_dep_pairT := - forall (P:U -> Type) (p:U) (x y:P p), - existT P p x = existT P p y -> x = y. - - Lemma eq_dep_eq__inj_pairT2 : Eq_dep_eq U -> Inj_dep_pairT. - Proof. - intro eq_dep_eq; red; intros. - apply eq_dep_eq. - apply eq_sigT_eq_dep. - assumption. - Qed. - - (** UIP implies the injectivity of equality on dependent pairs in Set *) - Definition Inj_dep_pairS := - forall (P:V -> Set) (p:V) (x y:P p), existS P p x = existS P p y -> x = y. + Definition Inj_dep_pair := + forall (P:U -> Type) (p:U) (x y:P p), existT P p x = existT P p y -> x = y. - Lemma eq_dep_eq__inj_pair2 : Eq_dep_eq V -> Inj_dep_pairS. + Lemma eq_dep_eq__inj_pair2 : Eq_dep_eq U -> Inj_dep_pair. Proof. intro eq_dep_eq; red; intros. apply eq_dep_eq. @@ -279,6 +264,11 @@ Section Corollaries. End Corollaries. +Notation Inj_dep_pairS := Inj_dep_pair. +Notation Inj_dep_pairT := Inj_dep_pair. +Notation eq_dep_eq__inj_pairT2 := eq_dep_eq__inj_pair2. + + (************************************************************************) (** *** C. Definition of the functor that builds properties of dependent equalities assuming axiom eq_rect_eq *) @@ -303,7 +293,7 @@ Lemma eq_rect_eq : Proof M.eq_rect_eq U. Lemma eq_rec_eq : - forall (p:U) (Q:U -> Set) (x:Q p) (h:p = p), x = eq_rect p Q x p h. + forall (p:U) (Q:U -> Set) (x:Q p) (h:p = p), x = eq_rec p Q x p h. Proof (fun p Q => M.eq_rect_eq U p Q). (** Injectivity of Dependent Equality *) @@ -333,18 +323,13 @@ End Axioms. (** UIP implies the injectivity of equality on dependent pairs in Type *) -Lemma inj_pairT2 : +Lemma inj_pair2 : forall (U:Type) (P:U -> Type) (p:U) (x y:P p), existT P p x = existT P p y -> x = y. -Proof (fun U => eq_dep_eq__inj_pairT2 U (eq_dep_eq U)). - -(** UIP implies the injectivity of equality on dependent pairs in Set *) - -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 (fun U => eq_dep_eq__inj_pair2 U (eq_dep_eq U)). +Notation inj_pairT2 := inj_pair2. + End EqdepTheory. Implicit Arguments eq_dep []. |