diff options
Diffstat (limited to 'theories/Logic/EqdepFacts.v')
| -rw-r--r-- | theories/Logic/EqdepFacts.v | 332 |
1 files changed, 166 insertions, 166 deletions
diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index 7963555a..a257ef55 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 8674 2006-03-30 06:56:50Z herbelin $ i*) +(*i $Id: EqdepFacts.v 9245 2006-10-17 12:53:34Z notin $ i*) (** This file defines dependent equality and shows its equivalence with equality on dependent pairs (inhabiting sigma-types). It derives @@ -32,70 +32,70 @@ Table of contents: -A. Definition of dependent equality and equivalence with equality +1. Definition of dependent equality and equivalence with equality -B. Eq_rect_eq <-> Eq_dep_eq <-> UIP <-> UIP_refl <-> K +2. Eq_rect_eq <-> Eq_dep_eq <-> UIP <-> UIP_refl <-> K -C. Definition of the functor that builds properties of dependent +3. Definition of the functor that builds properties of dependent equalities assuming axiom eq_rect_eq *) (************************************************************************) -(** *** A. Definition of dependent equality and equivalence with equality of dependent pairs *) +(** * Definition of dependent equality and equivalence with equality of dependent pairs *) Section Dependent_Equality. + + Variable U : Type. + Variable P : U -> Type. -Variable U : Type. -Variable P : U -> Type. + (** Dependent equality *) -(** Dependent equality *) - -Inductive eq_dep (p:U) (x:P p) : forall q:U, P q -> Prop := + 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. + Hint Constructors eq_dep: core v62. -Lemma eq_dep_refl : forall (p:U) (x:P p), eq_dep p x p x. -Proof eq_dep_intro. + Lemma eq_dep_refl : forall (p:U) (x:P p), eq_dep p x p x. + Proof eq_dep_intro. -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. + 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. -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. + 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. + Scheme eq_indd := Induction for eq Sort Prop. -(** Equivalent definition of dependent equality expressed as a non - dependent inductive type *) + (** Equivalent definition of dependent equality expressed as a non + dependent inductive type *) -Inductive eq_dep1 (p:U) (x:P p) (q:U) (y:P q) : 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. + 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. End Dependent_Equality. @@ -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: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. Proof. intros. dependent rewrite H. @@ -114,10 +114,10 @@ Proof. Qed. Lemma equiv_eqex_eqdep : - forall (U:Set) (P:U -> Set) (p q:U) (x:P p) (y:P q), + 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. Proof. -split. + split. (* -> *) apply eq_sigS_eq_dep. (* <- *) @@ -125,8 +125,8 @@ split. Qed. Lemma eq_sigT_eq_dep : - 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. + 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. @@ -134,8 +134,8 @@ Proof. Qed. Lemma eq_dep_eq_sigT : - forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q), - eq_dep p x q y -> existT P p x = existT P q y. + forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q), + eq_dep p x q y -> existT P p x = existT P q y. Proof. destruct 1; reflexivity. Qed. @@ -146,90 +146,90 @@ Hint Resolve eq_dep_intro: core v62. Hint Immediate eq_dep_sym: core v62. (************************************************************************) -(** *** B. Eq_rect_eq <-> Eq_dep_eq <-> UIP <-> UIP_refl <-> K *) +(** * Eq_rect_eq <-> Eq_dep_eq <-> UIP <-> UIP_refl <-> K *) Section Equivalences. - -Variable U:Type. - -(** Invariance by Substitution of Reflexive Equality Proofs *) - -Definition 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 *) - -Definition Eq_dep_eq := - forall (P:U->Type) (p:U) (x y:P p), eq_dep p x p y -> x = y. - -(** Uniqueness of Identity Proofs (UIP) *) - -Definition UIP_ := - forall (x y:U) (p1 p2:x = y), p1 = p2. - -(** Uniqueness of Reflexive Identity Proofs *) - -Definition UIP_refl_ := - forall (x:U) (p:x = x), p = refl_equal x. - -(** Streicher's axiom K *) - -Definition Streicher_K_ := - forall (x:U) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p. - -(** Injectivity of Dependent Equality is a consequence of *) -(** Invariance by Substitution of Reflexive Equality Proof *) - -Lemma eq_rect_eq__eq_dep1_eq : - Eq_rect_eq -> forall (P:U->Type) (p:U) (x y:P p), eq_dep1 p x p y -> x = y. -Proof. - intro eq_rect_eq. - simple destruct 1; intro. - rewrite <- eq_rect_eq; auto. -Qed. - -Lemma eq_rect_eq__eq_dep_eq : Eq_rect_eq -> Eq_dep_eq. -Proof. - intros eq_rect_eq; red; intros. - apply (eq_rect_eq__eq_dep1_eq eq_rect_eq); apply eq_dep_dep1; trivial. -Qed. - -(** Uniqueness of Identity Proofs (UIP) is a consequence of *) -(** Injectivity of Dependent Equality *) - -Lemma eq_dep_eq__UIP : Eq_dep_eq -> UIP_. -Proof. - intro eq_dep_eq; red. - 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__UIP_refl : UIP_ -> UIP_refl_. -Proof. - intro UIP; red; intros; apply UIP. -Qed. - -(** Streicher's axiom K is a direct consequence of Uniqueness of - Reflexive Identity Proofs *) - -Lemma UIP_refl__Streicher_K : UIP_refl_ -> Streicher_K_. -Proof. - intro UIP_refl; red; intros; rewrite UIP_refl; assumption. -Qed. - -(** We finally recover from K the Invariance by Substitution of - Reflexive Equality Proofs *) - -Lemma Streicher_K__eq_rect_eq : Streicher_K_ -> Eq_rect_eq. -Proof. - intro Streicher_K; red; intros. - apply Streicher_K with (p := h). - reflexivity. -Qed. + + Variable U:Type. + + (** Invariance by Substitution of Reflexive Equality Proofs *) + + Definition 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 *) + + Definition Eq_dep_eq := + forall (P:U->Type) (p:U) (x y:P p), eq_dep p x p y -> x = y. + + (** Uniqueness of Identity Proofs (UIP) *) + + Definition UIP_ := + forall (x y:U) (p1 p2:x = y), p1 = p2. + + (** Uniqueness of Reflexive Identity Proofs *) + + Definition UIP_refl_ := + forall (x:U) (p:x = x), p = refl_equal x. + + (** Streicher's axiom K *) + + Definition Streicher_K_ := + forall (x:U) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p. + + (** Injectivity of Dependent Equality is a consequence of *) + (** Invariance by Substitution of Reflexive Equality Proof *) + + Lemma eq_rect_eq__eq_dep1_eq : + Eq_rect_eq -> forall (P:U->Type) (p:U) (x y:P p), eq_dep1 p x p y -> x = y. + Proof. + intro eq_rect_eq. + simple destruct 1; intro. + rewrite <- eq_rect_eq; auto. + Qed. + + Lemma eq_rect_eq__eq_dep_eq : Eq_rect_eq -> Eq_dep_eq. + Proof. + intros eq_rect_eq; red; intros. + apply (eq_rect_eq__eq_dep1_eq eq_rect_eq); apply eq_dep_dep1; trivial. + Qed. + + (** Uniqueness of Identity Proofs (UIP) is a consequence of *) + (** Injectivity of Dependent Equality *) + + Lemma eq_dep_eq__UIP : Eq_dep_eq -> UIP_. + Proof. + intro eq_dep_eq; red. + 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__UIP_refl : UIP_ -> UIP_refl_. + Proof. + intro UIP; red; intros; apply UIP. + Qed. + + (** Streicher's axiom K is a direct consequence of Uniqueness of + Reflexive Identity Proofs *) + + Lemma UIP_refl__Streicher_K : UIP_refl_ -> Streicher_K_. + Proof. + intro UIP_refl; red; intros; rewrite UIP_refl; assumption. + Qed. + + (** We finally recover from K the Invariance by Substitution of + Reflexive Equality Proofs *) + + Lemma Streicher_K__eq_rect_eq : Streicher_K_ -> Eq_rect_eq. + Proof. + intro Streicher_K; red; intros. + apply Streicher_K with (p := h). + reflexivity. + Qed. (** Remark: It is reasonable to think that [eq_rect_eq] is strictly stronger than [eq_rec_eq] (which is [eq_rect_eq] restricted on [Set]): @@ -246,37 +246,37 @@ Qed. 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. + + 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. + + Lemma eq_dep_eq__inj_pair2 : Eq_dep_eq V -> Inj_dep_pairS. Proof. intro eq_dep_eq; red; intros. apply eq_dep_eq. - apply eq_sigT_eq_dep. + apply eq_sigS_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. - -Lemma eq_dep_eq__inj_pair2 : Eq_dep_eq V -> Inj_dep_pairS. -Proof. - intro eq_dep_eq; red; intros. - apply eq_dep_eq. - apply eq_sigS_eq_dep. - assumption. -Qed. - End Corollaries. (************************************************************************) @@ -286,16 +286,16 @@ Module Type EqdepElimination. Axiom eq_rect_eq : forall (U:Type) (p:U) (Q:U -> Type) (x:Q p) (h:p = p), - x = eq_rect p Q x p h. + x = eq_rect p Q x p h. End EqdepElimination. Module EqdepTheory (M:EqdepElimination). - -Section Axioms. - -Variable U:Type. - + + Section Axioms. + + Variable U:Type. + (** Invariance by Substitution of Reflexive Equality Proofs *) Lemma eq_rect_eq : |