1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 (*#***********************************************************************)
21 (* v * The Coq Proof Assistant / The Coq Development Team *)
23 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
25 (* \VV/ **************************************************************)
27 (* // * This file is distributed under the terms of the *)
29 (* * GNU Lesser General Public License Version 2.1 *)
31 (*#***********************************************************************)
33 (*i $Id: Eqdep.v,v 1.10.2.1 2004/07/16 19:31:06 herbelin Exp $ i*)
35 (*#* This file defines dependent equality and shows its equivalence with
36 equality on dependent pairs (inhabiting sigma-types). It axiomatizes
37 the invariance by substitution of reflexive equality proofs and
38 shows the equivalence between the 4 following statements
40 - Invariance by Substitution of Reflexive Equality Proofs.
41 - Injectivity of Dependent Equality
42 - Uniqueness of Identity Proofs
43 - Uniqueness of Reflexive Identity Proofs
46 These statements are independent of the calculus of constructions [2].
50 [1] T. Streicher, Semantical Investigations into Intensional Type Theory,
51 Habilitationsschrift, LMU M\252\nchen, 1993.
52 [2] M. Hofmann, T. Streicher, The groupoid interpretation of type theory,
53 Proceedings of the meeting Twenty-five years of constructive
54 type theory, Venice, Oxford University Press, 1998
58 Section Dependent_Equality
62 cic:/Coq/Logic/Eqdep/Dependent_Equality/U.var
66 cic:/Coq/Logic/Eqdep/Dependent_Equality/P.var
69 (*#* Dependent equality *)
71 inline procedural "cic:/Coq/Logic/Eqdep/eq_dep.ind".
74 Hint Constructors eq_dep: core v62.
77 inline procedural "cic:/Coq/Logic/Eqdep/eq_dep_sym.con" as lemma.
80 Hint Immediate eq_dep_sym: core v62.
83 inline procedural "cic:/Coq/Logic/Eqdep/eq_dep_trans.con" as lemma.
85 inline procedural "cic:/Coq/Logic/Eqdep/eq_indd.con" as theorem.
87 inline procedural "cic:/Coq/Logic/Eqdep/eq_dep1.ind".
89 inline procedural "cic:/Coq/Logic/Eqdep/eq_dep1_dep.con" as lemma.
91 inline procedural "cic:/Coq/Logic/Eqdep/eq_dep_dep1.con" as lemma.
93 (*#* Invariance by Substitution of Reflexive Equality Proofs *)
95 inline procedural "cic:/Coq/Logic/Eqdep/eq_rect_eq.con".
97 (*#* Injectivity of Dependent Equality is a consequence of *)
99 (*#* Invariance by Substitution of Reflexive Equality Proof *)
101 inline procedural "cic:/Coq/Logic/Eqdep/eq_dep1_eq.con" as lemma.
103 inline procedural "cic:/Coq/Logic/Eqdep/eq_dep_eq.con" as lemma.
106 End Dependent_Equality
109 (*#* Uniqueness of Identity Proofs (UIP) is a consequence of *)
111 (*#* Injectivity of Dependent Equality *)
113 inline procedural "cic:/Coq/Logic/Eqdep/UIP.con" as lemma.
115 (*#* Uniqueness of Reflexive Identity Proofs is a direct instance of UIP *)
117 inline procedural "cic:/Coq/Logic/Eqdep/UIP_refl.con" as lemma.
119 (*#* Streicher axiom K is a direct consequence of Uniqueness of
120 Reflexive Identity Proofs *)
122 inline procedural "cic:/Coq/Logic/Eqdep/Streicher_K.con" as lemma.
124 (*#* We finally recover eq_rec_eq (alternatively eq_rect_eq) from K *)
126 inline procedural "cic:/Coq/Logic/Eqdep/eq_rec_eq.con" as lemma.
128 (*#* Dependent equality is equivalent to equality on dependent pairs *)
130 inline procedural "cic:/Coq/Logic/Eqdep/equiv_eqex_eqdep.con" as lemma.
132 (*#* UIP implies the injectivity of equality on dependent pairs *)
134 inline procedural "cic:/Coq/Logic/Eqdep/inj_pair2.con" as lemma.
136 (*#* UIP implies the injectivity of equality on dependent pairs *)
138 inline procedural "cic:/Coq/Logic/Eqdep/inj_pairT2.con" as lemma.
140 (*#* The main results to be exported *)
143 Hint Resolve eq_dep_intro eq_dep_eq: core v62.
147 Hint Immediate eq_dep_sym: core v62.
151 Hint Resolve inj_pair2 inj_pairT2: core.