Coq: switch to boolean predicates for Sail-type properties

- ArithFact takes a boolean predicate
- defined in terms of ArithFactP, which takes a Prop predicate,
  and is used directly for existentials
- used abstract in more definitions with direct proofs
- beef up solve_bool_with_Z to handle more equalities, andb and orb

1 files changed, 4 insertions, 3 deletions

diff --git a/lib/coq/Sail2_state_lemmas.v b/lib/coq/Sail2_state_lemmas.v
index e5394f32..39406208 100644
--- a/lib/coq/Sail2_state_lemmas.v
+++ b/lib/coq/Sail2_state_lemmas.v
@@ -196,8 +196,7 @@ Lemma build_trivial_exS_cong {RV T E} x x' :
   @build_trivial_exS RV T E x === build_trivial_exS x'.
 intros E1.
 unfold build_trivial_exS.
-rewrite E1.
-reflexivity.
+apply bindS_cong; auto.
 Qed.
 
 (* Monad lifting *)
@@ -513,6 +512,8 @@ Lemma liftState_build_trivial_ex Regs Regval E T r m :
   @liftState Regs Regval _ E r (@build_trivial_ex _ _ T m) ===
     build_trivial_exS (liftState r m).
 unfold build_trivial_ex, build_trivial_exS.
+unfold ArithFact.
+intro.
 rewrite liftState_bind.
 reflexivity.
 Qed.
@@ -805,7 +806,7 @@ Qed.
 Hint Rewrite liftState_undefined_word_nat : liftState.
 Hint Resolve liftState_undefined_word_nat : liftState.
 
-Lemma liftState_undefined_bitvector Regs Regval E r n `{ArithFact (n >= 0)} :
+Lemma liftState_undefined_bitvector Regs Regval E r n `{ArithFact (n >=? 0)} :
   liftState (Regs := Regs) (Regval := Regval) (E := E) r (undefined_bitvector n) === undefined_bitvectorS n.
 unfold undefined_bitvector, undefined_bitvectorS.
 rewrite_liftState.