From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001
From: Samuel Mimram <samuel.mimram@ens-lyon.org>
Date: Wed, 28 Jul 2004 21:54:47 +0000
Subject: Imported Upstream version 8.0pl1

---
 theories7/Logic/Eqdep.v | 183 ++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 183 insertions(+)
 create mode 100755 theories7/Logic/Eqdep.v

(limited to 'theories7/Logic/Eqdep.v')

diff --git a/theories7/Logic/Eqdep.v b/theories7/Logic/Eqdep.v
new file mode 100755
index 00000000..fc2dfe52
--- /dev/null
+++ b/theories7/Logic/Eqdep.v
@@ -0,0 +1,183 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: Eqdep.v,v 1.2.2.1 2004/07/16 19:31:29 herbelin Exp $ 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
+
+    - 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
+*)
+
+Section Dependent_Equality.
+
+Variable U : Type.
+Variable P : U->Type.
+
+(** Dependent equality *)
+
+Inductive eq_dep [p:U;x:(P p)] : (q:U)(P q)->Prop :=
+   eq_dep_intro : (eq_dep p x p x).
+Hint constr_eq_dep : core v62 := Constructors eq_dep.
+
+Lemma eq_dep_sym : (p,q:U)(x:(P p))(y:(P q))(eq_dep p x q y)->(eq_dep q y p x).
+Proof.
+NewDestruct 1; Auto.
+Qed.
+Hints Immediate eq_dep_sym : core v62.
+
+Lemma eq_dep_trans : (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.
+NewDestruct 1; Auto.
+Qed.
+
+Inductive eq_dep1 [p:U;x:(P p);q:U;y:(P q)] : Prop :=
+   eq_dep1_intro : (h:q=p)
+                  (x=(eq_rect U q P y p h))->(eq_dep1 p x q y).
+
+Scheme eq_indd := Induction for eq Sort Prop.
+
+Lemma eq_dep1_dep :
+      (p:U)(x:(P p))(q:U)(y:(P q))(eq_dep1 p x q y)->(eq_dep p x q y).
+Proof.
+NewDestruct 1 as [eq_qp H].
+NewDestruct eq_qp using eq_indd.
+Rewrite H.
+Apply eq_dep_intro.
+Qed.
+
+Lemma eq_dep_dep1 : 
+  (p,q:U)(x:(P p))(y:(P q))(eq_dep p x q y)->(eq_dep1 p x q y).
+Proof.
+NewDestruct 1.
+Apply eq_dep1_intro with (refl_equal U p).
+Simpl; Trivial.
+Qed.
+
+(** Invariance by Substitution of Reflexive Equality Proofs *)
+
+Axiom eq_rect_eq : (p:U)(Q:U->Type)(x:(Q p))(h:p=p)
+                  x=(eq_rect U p Q x p h).
+
+(** Injectivity of Dependent Equality is a consequence of *)
+(** Invariance by Substitution of Reflexive Equality Proof *)
+
+Lemma eq_dep1_eq : (p:U)(x,y:(P p))(eq_dep1 p x p y)->x=y.
+Proof.
+Destruct 1; Intro.
+Rewrite <- eq_rect_eq; Auto.
+Qed.
+
+Lemma eq_dep_eq : (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 : (U:Type)(x,y:U)(p1,p2:x=y)p1=p2.
+Proof.
+Intros; Apply eq_dep_eq with P:=[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 : (U:Type)(x:U)(p:x=x)p=(refl_equal U x).
+Proof.
+Intros; Apply UIP.
+Qed.
+
+(** Streicher axiom K is a direct consequence of Uniqueness of
+    Reflexive Identity Proofs *)
+
+Lemma Streicher_K : (U:Type)(x:U)(P:x=x->Prop)
+  (P (refl_equal ? x))->(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 : (U:Type)(P:U->Set)(p:U)(x:(P p))(h:p=p)
+  x=(eq_rec U 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 : (U:Set)(P:U->Set)(p,q:U)(x:(P p))(y:(P q)) 
+    (existS U P p x)=(existS U P q y) <-> (eq_dep U P p x q y).
+Proof.
+Split. 
+(* -> *)
+Intro H.
+Change p with   (projS1 U P (existS U P p x)).
+Change 2 x with (projS2 U P (existS U P p x)).
+Rewrite H.
+Apply eq_dep_intro.
+(* <- *)
+NewDestruct 1; Reflexivity.
+Qed.
+
+(** UIP implies the injectivity of equality on dependent pairs *)
+
+Lemma inj_pair2: (U:Set)(P:U->Set)(p:U)(x,y:(P p))
+    (existS U P p x)=(existS U P p y)-> x=y.
+Proof.
+Intros.
+Apply (eq_dep_eq U P).
+Generalize (equiv_eqex_eqdep U P p p x y) .
+Induction 1.
+Intros.
+Auto.
+Qed.
+
+(** UIP implies the injectivity of equality on dependent pairs *)
+
+Lemma inj_pairT2: (U:Type)(P:U->Type)(p:U)(x,y:(P p))
+    (existT U P p x)=(existT U P p y)-> x=y.
+Proof.
+Intros.
+Apply (eq_dep_eq U P).
+Change 1 p with (projT1 U P (existT U P p x)).
+Change 2 x with (projT2 U P (existT U P p x)).
+Rewrite H.
+Apply eq_dep_intro.
+Qed.
+
+(** The main results to be exported *)
+
+Hints Resolve eq_dep_intro eq_dep_eq : core v62.
+Hints Immediate eq_dep_sym : core v62.
+Hints Resolve inj_pair2 inj_pairT2 : core.
-- 
cgit v1.2.3