blob: d021fa687e2f35534295fc7dbf4ea2d967aaa759 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(*i $Id$ i*)
Section Dependent_Equality.
Variable U : Set.
Variable P : U->Set.
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.
Induction 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.
Induction 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_rec U q P y p h))->(eq_dep1 p x q y).
Axiom eq_rec_eq : (p:U)(Q:U->Set)(x:(Q p))(h:p=p)
x=(eq_rec U p Q x p h).
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.
Induction 1; Intros eq_qp.
Cut (h:q=p)(y0:(P q))
(x=(eq_rec U q P y0 p h))->(eq_dep p x q y0).
Intros; Apply H0 with eq_qp; Auto.
Rewrite eq_qp; Intros h y0.
Elim eq_rec_eq.
Induction 1; Auto.
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.
Induction 1; Intros.
Apply eq_dep1_intro with (refl_equal U p).
Simpl; Trivial.
Qed.
Lemma eq_dep1_eq : (p:U)(x,y:(P p))(eq_dep1 p x p y)->x=y.
Proof.
Induction 1; Intro.
Elim eq_rec_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.
Lemma equiv_eqex_eqdep : (p,q:U)(x:(P p))(y:(P q))
(existS U P p x)=(existS U P q y) <-> (eq_dep p x q y).
Proof.
Split.
Intros.
Generalize (eq_ind (sigS U P) (existS U P q y)
[pr:(sigS U P)] (eq_dep (projS1 U P pr) (projS2 U P pr) q y)) .
Proof.
Simpl.
Intro.
Generalize (H0 (eq_dep_intro q y)) .
Intro.
Apply (H1 (existS U P p x)).
Auto.
Intros.
Elim H.
Auto.
Qed.
Lemma inj_pair2: (p:U)(x,y:(P p))
(existS U P p x)=(existS U P p y)-> x=y.
Proof.
Intros.
Apply eq_dep_eq.
Generalize (equiv_eqex_eqdep p p x y) .
Induction 1.
Intros.
Auto.
Qed.
End Dependent_Equality.
Hints Resolve eq_dep_intro : core v62.
Hints Immediate eq_dep_sym eq_dep_eq : core v62.
|
