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
|
(***********************************************************************)
(* 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 Equalities, 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 Equalities (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.
|
