diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coq/Sail2_values.v | 10 | ||||
| -rw-r--r-- | lib/flow.sail | 2 |
2 files changed, 10 insertions, 2 deletions
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 13352f4b..ab557ff4 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -928,12 +928,17 @@ 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 [andb _ _ = true] |- _ => apply andb_prop in H + | H:context [orb _ _ = false] |- _ => rewrite Bool.orb_false_iff in H + | H:context [andb _ _ = true] |- _ => rewrite Bool.andb_true_iff in H + | H:context [andb _ _ = false] |- _ => rewrite Bool.andb_false_iff in H + | H:context [negb _ = true] |- _ => rewrite Bool.negb_true_iff in H + | H:context [negb _ = false] |- _ => rewrite Bool.negb_false_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 *) Ltac extract_properties := repeat match goal with H := (projT1 ?X) |- _ => @@ -987,6 +992,9 @@ Hint Extern 0 (ArithFact _) => solve_arithfact : typeclass_instances. Hint Unfold length_mword : sail. +Definition neq_atom (x : Z) (y : Z) : bool := negb (Z.eqb x y). +Hint Unfold neq_atom : sail. + Lemma ReasonableSize_witness (a : Z) (w : mword a) : ReasonableSize a. constructor. destruct a. diff --git a/lib/flow.sail b/lib/flow.sail index 304f14bc..b4440eaa 100644 --- a/lib/flow.sail +++ b/lib/flow.sail @@ -9,7 +9,7 @@ val or_bool = {coq: "orb", _: "or_bool"} : (bool, bool) -> bool val eq_atom = {ocaml: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : forall 'n 'm. (atom('n), atom('m)) -> bool -val neq_atom = {lem: "neq"} : forall 'n 'm. (atom('n), atom('m)) -> bool +val neq_atom = {lem: "neq", coq: "neq_atom"} : forall 'n 'm. (atom('n), atom('m)) -> bool function neq_atom (x, y) = not_bool(eq_atom(x, y)) |