CompDec clean-up (#93)

Clean-up the definition of CompDec, leaving the required minimum (in particular for functional arrays)

1 files changed, 100 insertions, 51 deletions

diff --git a/src/classes/SMT_classes.v b/src/classes/SMT_classes.v
index 5f79faf..f8d5b50 100644
--- a/src/classes/SMT_classes.v
+++ b/src/classes/SMT_classes.v
@@ -28,7 +28,7 @@ Definition eqb_to_eq_dec :
   Defined.
 
 
-(** Types with a Boolean equality that reflects in Leibniz equality *)
+(** Types with a Boolean equality that reflects Leibniz equality *)
 Class EqbType T := {
  eqb : T -> T -> bool;
  eqb_spec : forall x y, eqb x y = true <-> x = y
@@ -37,32 +37,65 @@ Class EqbType T := {
 
 (** 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.
+Section EqbToDecType.
+  Generalizable Variable T.
+  Context `{ET : EqbType T}.
+
+  Instance EqbToDecType : DecType T.
+  Proof.
+    destruct ET as [eqb0 Heqb0]. split.
+    apply (eqb_to_eq_dec _ eqb0); auto.
+  Defined.
+End EqbToDecType.
+
+
+(** Basic properties on types with Boolean equality *)
+Section EqbTypeProp.
+  Generalizable Variable T.
+  Context `{ET : EqbType T}.
+
+  Lemma eqb_refl x : eqb x x = true.
+  Proof. now rewrite eqb_spec. Qed.
+
+  Lemma eqb_sym x y : eqb x y = true -> eqb y x = true.
+  Proof. rewrite !eqb_spec. now intros ->. Qed.
+
+  Lemma eqb_trans x y z : eqb x y = true -> eqb y z = true -> eqb x z = true.
+  Proof. rewrite !eqb_spec. now intros ->. Qed.
+
+  Lemma eqb_spec_false x y : eqb x y = false <-> x <> y.
+  Proof.
+    split.
+    - intros H1 H2. subst y. rewrite eqb_refl in H1. inversion H1.
+    - intro H. case_eq (eqb x y); auto. intro H1. elim H. now rewrite <- eqb_spec.
+  Qed.
+
+  Lemma reflect_eqb x y : reflect (x = y) (eqb x y).
+  Proof.
+    case_eq (eqb x y); intro H; constructor.
+    - now rewrite eqb_spec in H.
+    - now rewrite eqb_spec_false in H.
+  Qed.
+
+  Lemma eqb_sym2 x y : eqb x y = eqb y x.
+  Proof.
+    case_eq (eqb y x); intro H.
+    - now apply eqb_sym.
+    - rewrite eqb_spec_false in *. auto.
+  Qed.
+End EqbTypeProp.
 
 
 (** 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 *)
+  lt_not_eq : forall x y : T, lt x y -> x <> y
 }.
 
 Hint Resolve lt_not_eq lt_trans.
@@ -84,6 +117,29 @@ Class Comparable T {ot:OrdType T} := {
 }.
 
 
+(* A Comparable type is also an EqbType *)
+Section Comparable2EqbType.
+  Generalizable Variable T.
+  Context `{OTT : OrdType T}.
+  Context `{CT : Comparable T}.
+
+  Definition compare2eqb (x y:T) : bool :=
+    match compare x y with
+    | EQ _ => true
+    | _ => false
+    end.
+
+  Lemma compare2eqb_spec x y : compare2eqb x y = true <-> x = y.
+  Proof.
+    unfold compare2eqb.
+    case_eq (compare x y); simpl; intros e He; split; try discriminate;
+      try (intros ->; elim (lt_not_eq _ _ e (eq_refl _))); auto.
+  Qed.
+
+  Instance Comparable2EqbType : EqbType T := Build_EqbType _ _ compare2eqb_spec.
+End Comparable2EqbType.
+
+
 (** Class of inhabited types *)
 Class Inhabited T := {
   default_value : T
@@ -92,53 +148,44 @@ Class Inhabited 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
+  Eqb :> EqbType T;             (* This is redundant since implied by Comp, but it actually allows us to choose a specific equality function *)
+  Ordered :> OrdType T;
+  Comp :> @Comparable T Ordered;
+  Inh :> Inhabited T
 }.
 
 
-Instance ord_of_compdec t `{c: CompDec t} : (OrdType t) := 
-  let (_, _, _, ord, _, _) := c in ord.
+Instance eqbtype_of_compdec t `{c: CompDec t} : (EqbType t) :=
+  let (eqb, _, _, _) := c in eqb.
 
-Instance inh_of_compdec t `{c: CompDec t} : (Inhabited t) := 
-  let (_, _, _, _, _, inh) := c in inh.
+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.
+  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
+  match eqbtype_of_compdec t with
+  | {| 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.
+  intros x y. destruct c as [[E HE] O C I]. unfold eqb_of_compdec. simpl. now rewrite HE.
 Qed.
 
 Hint Resolve
      ord_of_compdec
      inh_of_compdec
      comp_of_compdec
-     eqbtype_of_compdec
-     dec_of_compdec : typeclass_instances.
+     eqbtype_of_compdec : typeclass_instances.
 
 
 Record typ_compdec : Type := Typ_compdec {
@@ -146,28 +193,30 @@ Record typ_compdec : Type := Typ_compdec {
   te_compdec : CompDec te_carrier
 }.
 
+
 Section CompDec_from.
 
   Variable T : Type.
+
   Variable eqb' : T -> T -> bool.
+  Variable eqb'_spec : forall x y, eqb' x y = true <-> x = y.
+
   Variable lt' : T -> T -> Prop.
-  Variable d : T.
+  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.
 
-  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.
-  
+
+  Variable d : T.
+
   Program Instance CompDec_from : (CompDec T) := {|
-    Eqb := {| eqb := eqb' |};
-    Ordered := {| lt := lt'; lt_trans := lt_trans' |};
+    Eqb := {| eqb := eqb'; eqb_spec := eqb'_spec |};
+    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.