Coq: add typeclass based comparison, and instantiate for enums

3 files changed, 47 insertions, 10 deletions

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 229a9c09..137be85c 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -6,6 +6,7 @@ Require Export String.
 Require Import bbv.Word.
 Require Export List.
 Require Export Sumbool.
+Require Export DecidableClass.
 Import ListNotations.
 
 Open Scope Z.
@@ -22,6 +23,39 @@ Defined.
 Definition build_ex (n:Z) {P:Z -> Prop} `{H:ArithFact (P n)} : {x : Z & ArithFact (P x)} :=
   existT _ n H.
 
+Definition generic_eq {T:Type} (x y:T) `{Decidable (x = y)} := Decidable_witness.
+Definition generic_neq {T:Type} (x y:T) `{Decidable (x = y)} := negb Decidable_witness.
+Lemma generic_eq_true {T} {x y:T} `{Decidable (x = y)} : generic_eq x y = true -> x = y.
+apply Decidable_spec.
+Qed.
+Lemma generic_eq_false {T} {x y:T} `{Decidable (x = y)} : generic_eq x y = false -> x <> y.
+unfold generic_eq.
+intros H1 H2.
+rewrite <- Decidable_spec in H2.
+congruence.
+Qed.
+Lemma generic_neq_true {T} {x y:T} `{Decidable (x = y)} : generic_neq x y = true -> x <> y.
+unfold generic_neq.
+intros H1 H2.
+rewrite <- Decidable_spec in H2.
+destruct Decidable_witness; simpl in *; 
+congruence.
+Qed.
+Lemma generic_neq_false {T} {x y:T} `{Decidable (x = y)} : generic_neq x y = false -> x = y.
+unfold generic_neq.
+intro H1.
+rewrite <- Decidable_spec.
+destruct Decidable_witness; simpl in *; 
+congruence.
+Qed.
+Instance Decidable_eq_from_dec {T:Type} (eqdec: forall x y : T, {x = y} + {x <> y}) : 
+  forall (x y : T), Decidable (eq x y) := {
+  Decidable_witness := proj1_sig (bool_of_sumbool (eqdec x y))
+}.
+destruct (eqdec x y); simpl; split; congruence.
+Qed.
+
+
 (* Project away range constraints in comparisons *)
 Definition ltb_range_l {P} (l : sigT P) r := Z.ltb (projT1 l) r.
 Definition leb_range_l {P} (l : sigT P) r := Z.leb (projT1 l) r.
@@ -821,6 +855,10 @@ Ltac unbool_comparisons :=
   | H:context [Z.ltb _ _ = false] |- _ => rewrite Z.ltb_ge in H
   | H:context [Z.eqb _ _ = false] |- _ => rewrite Z.eqb_neq in H
   | H:context [orb _ _ = true] |- _ => rewrite Bool.orb_true_iff in H
+  | H:context [generic_eq _ _ = true] |- _ => apply generic_eq_true in H
+  | H:context [generic_eq _ _ = false] |- _ => apply generic_eq_false in H
+  | H:context [generic_neq _ _ = true] |- _ => apply generic_neq_true in H
+  | H:context [generic_neq _ _ = false] |- _ => apply generic_neq_false in H
   end.
 (* Split up dependent pairs to get at proofs of properties *)
 (* TODO: simpl is probably too strong here *)
@@ -867,12 +905,6 @@ auto using Z.le_ge, Zle_0_pos.
 destruct w.
 Qed.
 
-Goal forall x y, ArithFact (x > y) -> ArithFact (y > 0) -> x >= 0.
-intros.
-unwrap_ArithFacts.
-omega.
-Abort.
-
 Hint Extern 0 (ReasonableSize ?A) => (unwrap_ArithFacts; solve [apply ReasonableSize_witness; assumption | constructor; omega]) : typeclass_instances.
 
 Instance mword_Bitvector {a : Z} `{ArithFact (a >= 0)} : (Bitvector (mword a)) := {
diff --git a/mips/prelude.sail b/mips/prelude.sail
index 6821469e..08b0dd99 100644
--- a/mips/prelude.sail
+++ b/mips/prelude.sail
@@ -15,7 +15,7 @@ $include <arith.sail>
 $include <option.sail>
 $include <vector_dec.sail>
 
-val eq_anything = {ocaml: "(fun (x, y) -> x = y)", lem: "eq", _:"eq_anything"} : forall ('a : Type). ('a, 'a) -> bool
+val eq_anything = {ocaml: "(fun (x, y) -> x = y)", lem: "eq", coq: "generic_eq", _:"eq_anything"} : forall ('a : Type). ('a, 'a) -> bool
 overload operator == = {eq_anything}
 
 val not_vec = {c:"not_bits", _:"not_vec"} : forall 'n. bits('n) -> bits('n)
@@ -27,7 +27,7 @@ val not = {coq:"negb", _:"not"} : bool -> bool
 val neq_vec = {lem: "neq"} : forall 'n. (bits('n), bits('n)) -> bool
 function neq_vec (x, y) = not_bool(eq_bits(x, y))
 
-val neq_anything = {lem: "neq"} : forall ('a : Type). ('a, 'a) -> bool
+val neq_anything = {lem: "neq", coq: "generic_neq"} : forall ('a : Type). ('a, 'a) -> bool
 function neq_anything (x, y) = not_bool(x == y)
 
 overload operator != = {neq_atom, neq_int, neq_vec, neq_anything}
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 5a07cb1b..ffe376e0 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1336,10 +1336,15 @@ let doc_typdef (TD_aux(td, (l, annot))) = match td with
       | Id_aux ((Id "diafp"),_) -> empty
       | _ ->
          let enums_doc = group (separate_map (break 1 ^^ pipe ^^ space) doc_id_ctor enums) in
+         let id_pp = doc_id_type id in
          let typ_pp = (doc_op coloneq)
-                        (concat [string "Inductive"; space; doc_id_type id;])
+                        (concat [string "Inductive"; space; id_pp])
                         (enums_doc) in
-          typ_pp ^^ dot ^^ hardline ^^ hardline)
+         let eq1_pp = string "Scheme Equality for" ^^ space ^^ id_pp ^^ dot in
+         let eq2_pp = string "Instance Decidable_eq_" ^^ id_pp ^^ space ^^ colon ^^ space ^^
+           string "forall (x y : " ^^ id_pp ^^ string "), Decidable (x = y) :=" ^/^
+           string "Decidable_eq_from_dec " ^^ id_pp ^^ string "_eq_dec." in
+          typ_pp ^^ dot ^^ hardline ^^ eq1_pp ^^ hardline ^^ eq2_pp ^^ hardline)
     | _ -> raise (Reporting_basic.err_unreachable l "register with non-constant indices")
 
 let args_of_typ l env typs =