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
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
|
(**************************************************************************)
(* *)
(* SMTCoq *)
(* Copyright (C) 2011 - 2019 *)
(* *)
(* See file "AUTHORS" for the list of authors *)
(* *)
(* This file is distributed under the terms of the CeCILL-C licence *)
(* *)
(**************************************************************************)
Require Import Bool OrderedType.
(** This file defines a number of typeclasses which are useful to build the
terms of SMT (in particular arrays indexed by instances of these
classes). *)
(** Boolean equality to decidable equality *)
Definition eqb_to_eq_dec :
forall T (eqb : T -> T -> bool) (eqb_spec : forall x y, eqb x y = true <-> x = y) (x y : T),
{ x = y } + { x <> y }.
intros.
case_eq (eqb x y); intro.
left. apply eqb_spec; auto.
right. red. intro. apply eqb_spec in H0. rewrite H in H0. now contradict H0.
Defined.
(** Types with a Boolean equality that reflects in Leibniz equality *)
Class EqbType T := {
eqb : T -> T -> bool;
eqb_spec : forall x y, eqb x y = true <-> x = y
}.
(** Types with a decidable equality *)
Class DecType T := {
eq_refl : forall x : T, x = x;
eq_sym : forall x y : T, x = y -> y = x;
eq_trans : forall x y z : T, x = y -> y = z -> x = z;
eq_dec : forall x y : T, { x = y } + { x <> y }
}.
Hint Immediate eq_sym.
Hint Resolve eq_refl eq_trans.
(** Types equipped with Boolean equality are decidable *)
Instance EqbToDecType T `(EqbType T) : DecType T.
Proof.
destruct H.
split; auto.
intros; subst; auto.
apply (eqb_to_eq_dec _ eqb0); auto.
Defined.
(** Class of types with a partial order *)
Class OrdType T := {
lt: T -> T -> Prop;
lt_trans : forall x y z : T, lt x y -> lt y z -> lt x z;
lt_not_eq : forall x y : T, lt x y -> ~ eq x y
(* compare : forall x y : T, Compare lt eq x y *)
}.
Hint Resolve lt_not_eq lt_trans.
Global Instance StrictOrder_OrdType T `(OrdType T) :
StrictOrder (lt : T -> T -> Prop).
Proof.
split.
unfold Irreflexive, Reflexive, complement.
intros. apply lt_not_eq in H0; auto.
unfold Transitive. intros x y z. apply lt_trans.
Qed.
(** Augment class of partial order with a compare function to obtain a total
order *)
Class Comparable T {ot:OrdType T} := {
compare : forall x y : T, Compare lt eq x y
}.
(** Class of inhabited types *)
Class Inhabited T := {
default_value : T
}.
(** * CompDec: Merging all previous classes *)
Class CompDec T := {
ty := T;
Eqb :> EqbType ty;
Decidable := EqbToDecType ty Eqb;
Ordered :> OrdType ty;
Comp :> @Comparable ty Ordered;
Inh :> Inhabited ty
}.
Instance ord_of_compdec t `{c: CompDec t} : (OrdType t) :=
let (_, _, _, ord, _, _) := c in ord.
Instance inh_of_compdec t `{c: CompDec t} : (Inhabited t) :=
let (_, _, _, _, _, inh) := c in inh.
Instance comp_of_compdec t `{c: CompDec t} : @Comparable t (ord_of_compdec t).
destruct c; trivial.
Defined.
Instance eqbtype_of_compdec t `{c: CompDec t} : EqbType t :=
let (_, eqbtype, _, _, _, inh) := c in eqbtype.
Instance dec_of_compdec t `{c: CompDec t} : DecType t :=
let (_, _, dec, _, _, inh) := c in dec.
Definition type_compdec {ty:Type} (cd : CompDec ty) := ty.
Definition eqb_of_compdec {t} (c : CompDec t) : t -> t -> bool :=
match c with
| {| ty := ty; Eqb := {| eqb := eqb |} |} => eqb
end.
Lemma compdec_eq_eqb {T:Type} {c : CompDec T} : forall x y : T,
x = y <-> eqb_of_compdec c x y = true.
Proof.
destruct c. destruct Eqb0.
simpl. intros. rewrite eqb_spec0. reflexivity.
Qed.
Hint Resolve
ord_of_compdec
inh_of_compdec
comp_of_compdec
eqbtype_of_compdec
dec_of_compdec : typeclass_instances.
Record typ_compdec : Type := Typ_compdec {
te_carrier : Type;
te_compdec : CompDec te_carrier
}.
Section CompDec_from.
Variable T : Type.
Variable eqb' : T -> T -> bool.
Variable lt' : T -> T -> Prop.
Variable d : T.
Hypothesis eqb_spec' : forall x y : T, eqb' x y = true <-> x = y.
Hypothesis lt_trans': forall x y z : T, lt' x y -> lt' y z -> lt' x z.
Hypothesis lt_neq': forall x y : T, lt' x y -> x <> y.
Variable compare': forall x y : T, Compare lt' eq x y.
Program Instance CompDec_from : (CompDec T) := {|
Eqb := {| eqb := eqb' |};
Ordered := {| lt := lt'; lt_trans := lt_trans' |};
Comp := {| compare := compare' |};
Inh := {| default_value := d |}
|}.
Definition typ_compdec_from : typ_compdec :=
Typ_compdec T CompDec_from.
End CompDec_from.
|
