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 include "Init/Prelude.ma".
21 (*#***********************************************************************)
23 (* v * The Coq Proof Assistant / The Coq Development Team *)
25 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
27 (* \VV/ **************************************************************)
29 (* // * This file is distributed under the terms of the *)
31 (* * GNU Lesser General Public License Version 2.1 *)
33 (*#***********************************************************************)
35 (*i $Id: Eqdep.v,v 1.10.2.1 2004/07/16 19:31:06 herbelin Exp $ i*)
37 (*#* This file defines dependent equality and shows its equivalence with
38 equality on dependent pairs (inhabiting sigma-types). It axiomatizes
39 the invariance by substitution of reflexive equality proofs and
40 shows the equivalence between the 4 following statements
42 - Invariance by Substitution of Reflexive Equality Proofs.
43 - Injectivity of Dependent Equality
44 - Uniqueness of Identity Proofs
45 - Uniqueness of Reflexive Identity Proofs
48 These statements are independent of the calculus of constructions [2].
52 [1] T. Streicher, Semantical Investigations into Intensional Type Theory,
53 Habilitationsschrift, LMU M\252\nchen, 1993.
54 [2] M. Hofmann, T. Streicher, The groupoid interpretation of type theory,
55 Proceedings of the meeting Twenty-five years of constructive
56 type theory, Venice, Oxford University Press, 1998
60 Section Dependent_Equality
64 cic:/Coq/Logic/Eqdep/Dependent_Equality/U.var
68 cic:/Coq/Logic/Eqdep/Dependent_Equality/P.var
71 (*#* Dependent equality *)
73 inline procedural "cic:/Coq/Logic/Eqdep/eq_dep.ind".
76 Hint Constructors eq_dep: core v62.
79 inline procedural "cic:/Coq/Logic/Eqdep/eq_dep_sym.con" as lemma.
82 Hint Immediate eq_dep_sym: core v62.
85 inline procedural "cic:/Coq/Logic/Eqdep/eq_dep_trans.con" as lemma.
87 inline procedural "cic:/Coq/Logic/Eqdep/eq_indd.con" as theorem.
89 inline procedural "cic:/Coq/Logic/Eqdep/eq_dep1.ind".
91 inline procedural "cic:/Coq/Logic/Eqdep/eq_dep1_dep.con" as lemma.
93 inline procedural "cic:/Coq/Logic/Eqdep/eq_dep_dep1.con" as lemma.
95 (*#* Invariance by Substitution of Reflexive Equality Proofs *)
97 inline procedural "cic:/Coq/Logic/Eqdep/eq_rect_eq.con".
99 (*#* Injectivity of Dependent Equality is a consequence of *)
101 (*#* Invariance by Substitution of Reflexive Equality Proof *)
103 inline procedural "cic:/Coq/Logic/Eqdep/eq_dep1_eq.con" as lemma.
105 inline procedural "cic:/Coq/Logic/Eqdep/eq_dep_eq.con" as lemma.
108 End Dependent_Equality
111 (*#* Uniqueness of Identity Proofs (UIP) is a consequence of *)
113 (*#* Injectivity of Dependent Equality *)
115 inline procedural "cic:/Coq/Logic/Eqdep/UIP.con" as lemma.
117 (*#* Uniqueness of Reflexive Identity Proofs is a direct instance of UIP *)
119 inline procedural "cic:/Coq/Logic/Eqdep/UIP_refl.con" as lemma.
121 (*#* Streicher axiom K is a direct consequence of Uniqueness of
122 Reflexive Identity Proofs *)
124 inline procedural "cic:/Coq/Logic/Eqdep/Streicher_K.con" as lemma.
126 (*#* We finally recover eq_rec_eq (alternatively eq_rect_eq) from K *)
128 inline procedural "cic:/Coq/Logic/Eqdep/eq_rec_eq.con" as lemma.
130 (*#* Dependent equality is equivalent to equality on dependent pairs *)
132 inline procedural "cic:/Coq/Logic/Eqdep/equiv_eqex_eqdep.con" as lemma.
134 (*#* UIP implies the injectivity of equality on dependent pairs *)
136 inline procedural "cic:/Coq/Logic/Eqdep/inj_pair2.con" as lemma.
138 (*#* UIP implies the injectivity of equality on dependent pairs *)
140 inline procedural "cic:/Coq/Logic/Eqdep/inj_pairT2.con" as lemma.
142 (*#* The main results to be exported *)
145 Hint Resolve eq_dep_intro eq_dep_eq: core v62.
149 Hint Immediate eq_dep_sym: core v62.
153 Hint Resolve inj_pair2 inj_pairT2: core.