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
|
(***********************************************************************)
(* 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 RelationClasses.
Set Implicit Arguments.
Unset Strict Implicit.
(** * Types with Equality, and nothing more (for subtyping purpose) *)
Module Type EqualityType.
Parameter Inline t : Type.
Parameter Inline eq : t -> t -> Prop.
Instance eq_equiv : Equivalence eq.
Hint Resolve (@Equivalence_Reflexive _ _ eq_equiv).
Hint Resolve (@Equivalence_Transitive _ _ eq_equiv).
Hint Immediate (@Equivalence_Symmetric _ _ eq_equiv).
End EqualityType.
(** * Types with decidable Equality (but no ordering) *)
Module Type DecidableType.
Include Type EqualityType.
Parameter eq_dec : forall x y : t, { eq x y } + { ~ eq x y }.
End DecidableType.
(** * Old versions of [DecidableType], with reflexivity, symmetry,
transitivity as three separate axioms. *)
Module Type EqualityTypeOrig.
Parameter Inline t : Type.
Parameter Inline 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.
Hint Immediate eq_sym.
Hint Resolve eq_refl eq_trans.
End EqualityTypeOrig.
Module Type DecidableTypeOrig.
Include Type EqualityTypeOrig.
Parameter eq_dec : forall x y : t, { eq x y } + { ~ eq x y }.
End DecidableTypeOrig.
(** * Compatibility wrapper from/to the old version of [DecidableType] *)
(** Interestingly, a module can be at the same time a [DecidableType]
and a [DecidableTypeOrig]. For the sake of compatibility,
this will be the case of all [DecidableType] modules provided here.
*)
Module Backport_ET (E:EqualityType) <: EqualityTypeOrig.
Include E.
Definition eq_refl := @Equivalence_Reflexive _ _ eq_equiv.
Definition eq_sym := @Equivalence_Symmetric _ _ eq_equiv.
Definition eq_trans := @Equivalence_Transitive _ _ eq_equiv.
End Backport_ET.
Module Update_ET (E:EqualityTypeOrig) <: EqualityType.
Include E.
Instance eq_equiv : Equivalence eq.
Proof. exact (Build_Equivalence _ _ eq_refl eq_sym eq_trans). Qed.
End Update_ET.
Module Backport_DT (E:DecidableType) <: DecidableTypeOrig.
Include Backport_ET E.
Definition eq_dec := E.eq_dec.
End Backport_DT.
Module Update_DT (E:DecidableTypeOrig) <: DecidableType.
Include Update_ET E.
Definition eq_dec := E.eq_dec.
End Update_DT.
(** * UsualDecidableType
A particular case of [DecidableType] where the equality is
the usual one of Coq. *)
Module Type UsualDecidableType.
Parameter Inline t : Type.
Definition eq := @eq t.
Program Instance eq_equiv : Equivalence eq.
Parameter eq_dec : forall x y, { eq x y }+{~eq x y }.
End UsualDecidableType.
(** a [UsualDecidableType] is in particular an [DecidableType]. *)
Module UDT_to_DT (U:UsualDecidableType) <: DecidableType := U.
(** an shortcut for easily building a UsualDecidableType *)
Module Type MiniDecidableType.
Parameter Inline t : Type.
Parameter eq_dec : forall x y:t, { x=y }+{ x<>y }.
End MiniDecidableType.
Module Make_UDT (M:MiniDecidableType) <: UsualDecidableType.
Definition t:=M.t.
Definition eq := @eq M.t.
Program Instance eq_equiv : Equivalence eq.
Definition eq_dec := M.eq_dec.
(* For building DecidableTypeOrig at the same time: *)
Definition eq_refl := @Equivalence_Reflexive _ _ eq_equiv.
Definition eq_sym := @Equivalence_Symmetric _ _ eq_equiv.
Definition eq_trans := @Equivalence_Transitive _ _ eq_equiv.
End Make_UDT.
(** * Boolean Equality *)
(** Having [eq_dec] is the same as having a boolean equality plus
a correctness proof. *)
Module Type BooleanEqualityType.
Include Type EqualityType.
Parameter Inline eqb : t -> t -> bool.
Parameter eqb_eq : forall x y, eqb x y = true <-> eq x y.
End BooleanEqualityType.
Module Bool_to_Dec (E:BooleanEqualityType) <: DecidableType.
Include E.
Lemma eq_dec : forall x y, {eq x y}+{~eq x y}.
Proof.
intros x y. assert (H:=eqb_eq x y).
destruct (eqb x y); [left|right].
apply -> H; auto.
intro EQ. apply H in EQ. discriminate.
Defined.
End Bool_to_Dec.
Module Dec_to_Bool (E:DecidableType) <: BooleanEqualityType.
Include E.
Definition eqb x y := if eq_dec x y then true else false.
Lemma eqb_eq : forall x y, eqb x y = true <-> eq x y.
Proof.
intros x y. unfold eqb. destruct eq_dec as [EQ|NEQ].
auto with *.
split. discriminate. intro EQ; elim NEQ; auto.
Qed.
End Dec_to_Bool.
|
