diff options
Diffstat (limited to 'theories/Logic/EqdepFacts.v')
| -rw-r--r-- | theories/Logic/EqdepFacts.v | 124 |
1 files changed, 105 insertions, 19 deletions
diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index 2d5f1537..d84cd824 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -1,13 +1,17 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: EqdepFacts.v 14641 2011-11-06 11:59:10Z herbelin $ i*) +(* File Eqdep.v created by Christine Paulin-Mohring in Coq V5.6, May 1992 *) +(* Further documentation and variants of eq_rect_eq by Hugo Herbelin, + Apr 2003 *) +(* Abstraction with respect to the eq_rect_eq axiom and renaming to + EqdepFacts.v by Hugo Herbelin, Mar 2006 *) (** This file defines dependent equality and shows its equivalence with equality on dependent pairs (inhabiting sigma-types). It derives @@ -33,7 +37,8 @@ Table of contents: -1. Definition of dependent equality and equivalence with equality +1. Definition of dependent equality and equivalence with equality of + dependent pairs and with dependent pair of equalities 2. Eq_rect_eq <-> Eq_dep_eq <-> UIP <-> UIP_refl <-> K @@ -45,6 +50,8 @@ Table of contents: (************************************************************************) (** * Definition of dependent equality and equivalence with equality of dependent pairs *) +Import EqNotations. + Section Dependent_Equality. Variable U : Type. @@ -75,11 +82,11 @@ Section Dependent_Equality. 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 as a dependent pair of + equalities *) 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. + eq_dep1_intro : forall h:q = p, x = rew h in y -> 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. @@ -95,13 +102,13 @@ Section Dependent_Equality. Proof. destruct 1. apply eq_dep1_intro with (refl_equal p). - simpl in |- *; trivial. + simpl; trivial. Qed. End Dependent_Equality. -Implicit Arguments eq_dep [U P]. -Implicit Arguments eq_dep1 [U P]. +Arguments eq_dep [U P] p x q _. +Arguments eq_dep1 [U P] p x q y. (** Dependent equality is equivalent to equality on dependent pairs *) @@ -116,24 +123,103 @@ Qed. Notation eq_sigS_eq_dep := eq_sigT_eq_dep (only parsing). (* Compatibility *) -Lemma equiv_eqex_eqdep : +Lemma eq_dep_eq_sigT : 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. + eq_dep p x q y -> existT P p x = existT P q y. Proof. - split. - (* -> *) - apply eq_sigT_eq_dep. - (* <- *) destruct 1; reflexivity. Qed. -Lemma eq_dep_eq_sigT : +Lemma eq_sigT_iff_eq_dep : 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. + existT P p x = existT P q y <-> eq_dep p x q y. +Proof. + split; auto using eq_sigT_eq_dep, eq_dep_eq_sigT. +Qed. + +Notation equiv_eqex_eqdep := eq_sigT_iff_eq_dep (only parsing). (* Compat *) + +Lemma eq_sig_eq_dep : + forall (U:Prop) (P:U -> Prop) (p q:U) (x:P p) (y:P q), + exist P p x = exist P q y -> eq_dep p x q y. +Proof. + intros. + dependent rewrite H. + apply eq_dep_intro. +Qed. + +Lemma eq_dep_eq_sig : + forall (U:Prop) (P:U -> Prop) (p q:U) (x:P p) (y:P q), + eq_dep p x q y -> exist P p x = exist P q y. Proof. destruct 1; reflexivity. Qed. +Lemma eq_sig_iff_eq_dep : + forall (U:Prop) (P:U -> Prop) (p q:U) (x:P p) (y:P q), + exist P p x = exist P q y <-> eq_dep p x q y. +Proof. + split; auto using eq_sig_eq_dep, eq_dep_eq_sig. +Qed. + +(** Dependent equality is equivalent to a dependent pair of equalities *) + +Set Implicit Arguments. + +Lemma eq_sigT_sig_eq : forall X P (x1 x2:X) H1 H2, existT P x1 H1 = existT P x2 H2 <-> {H:x1=x2 | rew H in H1 = H2}. +Proof. + intros; split; intro H. + - change x2 with (projT1 (existT P x2 H2)). + change H2 with (projT2 (existT P x2 H2)) at 5. + destruct H. simpl. + exists eq_refl. + reflexivity. + - destruct H as (->,<-). + reflexivity. +Defined. + +Lemma eq_sigT_fst : + forall X P (x1 x2:X) H1 H2 (H:existT P x1 H1 = existT P x2 H2), x1 = x2. +Proof. + intros. + change x2 with (projT1 (existT P x2 H2)). + destruct H. + reflexivity. +Defined. + +Lemma eq_sigT_snd : + forall X P (x1 x2:X) H1 H2 (H:existT P x1 H1 = existT P x2 H2), rew (eq_sigT_fst H) in H1 = H2. +Proof. + intros. + unfold eq_sigT_fst. + change x2 with (projT1 (existT P x2 H2)). + change H2 with (projT2 (existT P x2 H2)) at 3. + destruct H. + reflexivity. +Defined. + +Lemma eq_sig_fst : + forall X P (x1 x2:X) H1 H2 (H:exist P x1 H1 = exist P x2 H2), x1 = x2. +Proof. + intros. + change x2 with (proj1_sig (exist P x2 H2)). + destruct H. + reflexivity. +Defined. + +Lemma eq_sig_snd : + forall X P (x1 x2:X) H1 H2 (H:exist P x1 H1 = exist P x2 H2), rew (eq_sig_fst H) in H1 = H2. +Proof. + intros. + unfold eq_sig_fst, eq_ind. + change x2 with (proj1_sig (exist P x2 H2)). + change H2 with (proj2_sig (exist P x2 H2)) at 3. + destruct H. + reflexivity. +Defined. + +Unset Implicit Arguments. + (** Exported hints *) Hint Resolve eq_dep_intro: core. @@ -326,5 +412,5 @@ Notation inj_pairT2 := inj_pair2. End EqdepTheory. -Implicit Arguments eq_dep []. -Implicit Arguments eq_dep1 []. +Arguments eq_dep U P p x q _ : clear implicits. +Arguments eq_dep1 U P p x q y : clear implicits. |