2 files changed, 32 insertions, 6 deletions

diff --git a/aarch64/aarch64_extras.v b/aarch64/aarch64_extras.v
index 7d5020ec..94851ef5 100644
--- a/aarch64/aarch64_extras.v
+++ b/aarch64/aarch64_extras.v
@@ -10,6 +10,31 @@ Axiom set_slice : forall (n : Z) (m : Z), mword n -> Z -> mword m -> mword n.
 Definition length {n} (x : mword n) := length_mword x.
 Hint Unfold length : sail.
 
+
+Lemma Replicate_lemma1 {N M O x} :
+  O * M = N ->
+  O = Z.quot N M ->
+  x = Z.quot N M -> M * x = N.
+intros. rewrite H1.
+rewrite H0 in H.
+rewrite Z.mul_comm.
+assumption.
+Qed.
+Hint Resolve Replicate_lemma1 : sail.
+
+Lemma Replicate_lemma2 {N M x} :
+ M >= 0 /\ N >= 0 ->
+ x = Z.quot N M ->
+ x >= 0.
+intros; subst.
+destruct M; destruct N; intros; try easy.
+unfold Z.quot, Z.quotrem.
+destruct (N.pos_div_eucl p0 (N.pos p)) as [x y].
+case x; easy.
+Qed.
+Hint Resolve Replicate_lemma2 : sail.
+
+
 (*
 let hexchar_to_bool_list c =
   if c = #'0' then      Just ([false;false;false;false])
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 0c806222..0ce6134f 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -921,12 +921,10 @@ Class ReasonableSize (a : Z) : Prop := {
   isPositive : a >= 0
 }.
 
-Hint Resolve -> Z.gtb_lt Z.geb_le Z.ltb_lt Z.leb_le : zbool.
-Hint Resolve <- Z.ge_le_iff Z.gt_lt_iff : zbool.
-
 (* Omega doesn't know about In, but can handle disjunctions. *)
 Ltac unfold_In :=
 repeat match goal with
+| H:context [member_Z_list _ _ = true] |- _ => rewrite member_Z_list_In in H
 | H:context [In ?x (?y :: ?t)] |- _ => change (In x (y :: t)) with (y = x \/ In x t) in H
 | H:context [In ?x []] |- _ => change (In x []) with False in H
 end.
@@ -1002,7 +1000,7 @@ Ltac dump_context :=
   | H:=?X |- _ => idtac H ":=" X; fail
   | H:?X |- _ => idtac H ":" X; fail end;
   match goal with |- ?X => idtac "Goal:" X end.
-Ltac solve_arithfact :=
+Ltac prepare_for_solver :=
 (*dump_context;*)
  clear_non_Z_defns;
  extract_properties;
@@ -1012,12 +1010,15 @@ Ltac solve_arithfact :=
  autounfold with sail in * |- *; (* You can add Hint Unfold ... : sail to let omega see through fns *)
  unbool_comparisons;
  reduce_list_lengths;
- reduce_pow;
+ reduce_pow.
+Ltac solve_arithfact :=
+prepare_for_solver;
 (*dump_context;*)
  solve [apply ArithFact_mword; assumption
        | constructor; omega with Z
          (* The datatypes hints give us some list handling, esp In *)
-       | constructor; auto with datatypes zbool zarith sail].
+       | constructor; eauto with datatypes zarith sail
+       | constructor; idtac "Unable to solve constraint"; dump_context; fail].
 Hint Extern 0 (ArithFact _) => solve_arithfact : typeclass_instances.
 
 Hint Unfold length_mword : sail.