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
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
|
(***********************************************************************)
(* 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 *)
(***********************************************************************)
(* $Id$ *)
Require Export SetoidList.
Set Implicit Arguments.
Unset Strict Implicit.
(** * Types with decidable Equalities (but no ordering) *)
Module Type DecidableType.
Parameter t Set.
Parameter eq t -> t -> Prop.
Axiom eq_refl forall x : t, eq x x.
Axiom eq_sym forall x y : t, eq x y -> eq y x.
Axiom eq_trans forall x y z : t, eq x y -> eq y z -> eq x z.
Parameter eq_dec forall x y : t, { eq x y } + { ~ eq x y }.
Hint Immediate eq_sym.
Hint Resolve eq_refl eq_trans.
End DecidableType.
Module PairDecidableType(DDecidableType).
Import D.
Section Elt.
Variable elt Set.
Notation key=t.
Definition eqk (p p'key*elt) := eq (fst p) (fst p').
Definition eqke (p p'key*elt) :=
eq (fst p) (fst p') /\ (snd p) = (snd p').
Hint Unfold eqk eqke.
Hint Extern 2 (eqke ?a ?b) => split.
(* eqke is stricter than eqk *)
Lemma eqke_eqk forall x x', eqke x x' -> eqk x x'.
Proof.
unfold eqk, eqke; intuition.
Qed.
(* eqk, eqke are equalities *)
Lemma eqk_refl forall e, eqk e e.
Proof. auto. Qed.
Lemma eqke_refl forall e, eqke e e.
Proof. auto. Qed.
Lemma eqk_sym forall e e', eqk e e' -> eqk e' e.
Proof. auto. Qed.
Lemma eqke_sym forall e e', eqke e e' -> eqke e' e.
Proof. unfold eqke; intuition. Qed.
Lemma eqk_trans forall e e' e'', eqk e e' -> eqk e' e'' -> eqk e e''.
Proof. eauto. Qed.
Lemma eqke_trans forall e e' e'', eqke e e' -> eqke e' e'' -> eqke e e''.
Proof.
unfold eqke; intuition; [ eauto | congruence ].
Qed.
Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl.
Hint Immediate eqk_sym eqke_sym.
Lemma InA_eqke_eqk
forall x m, InA eqke x m -> InA eqk x m.
Proof.
unfold eqke; induction 1; intuition.
Qed.
Hint Resolve InA_eqke_eqk.
Lemma InA_eqk forall p q m, eqk p q -> InA eqk p m -> InA eqk q m.
Proof.
intros; apply InA_eqA with p; auto; apply eqk_trans; auto.
Qed.
Definition MapsTo (kkey)(e:elt):= InA eqke (k,e).
Definition In k m = exists e:elt, MapsTo k e m.
Hint Unfold MapsTo In.
(* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *)
Lemma In_alt forall k l, In k l <-> exists e, InA eqk (k,e) l.
Proof.
firstorder.
exists x; auto.
induction H.
destruct y.
exists e; auto.
destruct IHInA as [e H0].
exists e; auto.
Qed.
Lemma MapsTo_eq forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l.
Proof.
intros; unfold MapsTo in *; apply InA_eqA with (x,e); eauto.
Qed.
Lemma In_eq forall l x y, eq x y -> In x l -> In y l.
Proof.
destruct 2 as (e,E); exists e; eapply MapsTo_eq; eauto.
Qed.
Lemma In_inv forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l.
Proof.
inversion 1.
inversion_clear H0; eauto.
destruct H1; simpl in *; intuition.
Qed.
Lemma In_inv_2 forall k k' e e' l,
InA eqk (k, e) ((k', e') : l) -> ~ eq k k' -> InA eqk (k, e) l.
Proof.
inversion_clear 1; compute in H0; intuition.
Qed.
Lemma In_inv_3 forall x x' l,
InA eqke x (x' : l) -> ~ eqk x x' -> InA eqke x l.
Proof.
inversion_clear 1; compute in H0; intuition.
Qed.
End Elt.
Hint Unfold eqk eqke.
Hint Extern 2 (eqke ?a ?b) => split.
Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl.
Hint Immediate eqk_sym eqke_sym.
Hint Resolve InA_eqke_eqk.
Hint Unfold MapsTo In.
Hint Resolve In_inv_2 In_inv_3.
End PairDecidableType.
|