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, 2 insertions, 2 deletions

diff --git a/lib/coq/Sail2_prompt_monad.v b/lib/coq/Sail2_prompt_monad.v
index b26a2ff3..0ff65d28 100644
--- a/lib/coq/Sail2_prompt_monad.v
+++ b/lib/coq/Sail2_prompt_monad.v
@@ -189,7 +189,7 @@ Definition read_memt_bytes {rv A E} rk (addr : mword A) sz : monad rv (list memo
   Read_memt rk (Word.wordToNat (get_word addr)) (Z.to_nat sz) returnm.
 
 (*val read_memt : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv ('b * bitU) 'e*)
-Definition read_memt {rv A B E} `{ArithFact (B >= 0)} rk (addr : mword A) sz : monad rv (mword B * bitU) E :=
+Definition read_memt {rv A B E} `{ArithFact (B >=? 0)} rk (addr : mword A) sz : monad rv (mword B * bitU) E :=
   bind
     (read_memt_bytes rk addr sz)
     (fun '(bytes, tag) =>
@@ -203,7 +203,7 @@ Definition read_mem_bytes {rv A E} rk (addr : mword A) sz : monad rv (list memor
   Read_mem rk (Word.wordToNat (get_word addr)) (Z.to_nat sz) returnm.
 
 (*val read_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv 'b 'e*)
-Definition read_mem {rv A B E} `{ArithFact (B >= 0)} rk (addrsz : Z) (addr : mword A) sz : monad rv (mword B) E :=
+Definition read_mem {rv A B E} `{ArithFact (B >=? 0)} rk (addrsz : Z) (addr : mword A) sz : monad rv (mword B) E :=
   bind
     (read_mem_bytes rk addr sz)
     (fun bytes =>