1 files changed, 173 insertions, 0 deletions
diff --git a/src/classes/SMT_classes.v b/src/classes/SMT_classes.v
new file mode 100644
index 0000000..5f79faf
--- /dev/null
+++ b/src/classes/SMT_classes.v
@@ -0,0 +1,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.