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

10 files changed, 415 insertions, 286 deletions

diff --git a/lib/coq/Hoare.v b/lib/coq/Hoare.v
index c91814b0..44a81971 100644
--- a/lib/coq/Hoare.v
+++ b/lib/coq/Hoare.v
@@ -193,9 +193,9 @@ eapply PrePost_bindS.
 Qed.
 
 Lemma PrePost_and_boolSP (*[PrePost_compositeI]:*) Regs E PP QQ RR H
-  (l : monadS Regs {b : bool & Sail2_values.ArithFact (PP b)} E)
-  (r : monadS Regs {b : bool & Sail2_values.ArithFact (QQ b)} E)
-  P (Q : result {b : bool & Sail2_values.ArithFact (RR b)} E -> predS Regs) R :
+  (l : monadS Regs {b : bool & Sail2_values.ArithFactP (PP b)} E)
+  (r : monadS Regs {b : bool & Sail2_values.ArithFactP (QQ b)} E)
+  P (Q : result {b : bool & Sail2_values.ArithFactP (RR b)} E -> predS Regs) R :
   (forall p,
       PrePost R r
               (fun r =>
@@ -237,9 +237,9 @@ eapply PrePost_bindS.
 Qed.
 
 Lemma PrePost_or_boolSP (*[PrePost_compositeI]:*) Regs E PP QQ RR H
-  (l : monadS Regs {b : bool & Sail2_values.ArithFact (PP b)} E)
-  (r : monadS Regs {b : bool & Sail2_values.ArithFact (QQ b)} E)
-  P (Q : result {b : bool & Sail2_values.ArithFact (RR b)} E -> predS Regs) R :
+  (l : monadS Regs {b : bool & Sail2_values.ArithFactP (PP b)} E)
+  (r : monadS Regs {b : bool & Sail2_values.ArithFactP (QQ b)} E)
+  P (Q : result {b : bool & Sail2_values.ArithFactP (RR b)} E -> predS Regs) R :
   (forall p,
       PrePost R r
               (fun r =>
@@ -608,9 +608,9 @@ Qed.
    and prevents the reduction of the function application. *)
 
 Lemma PrePostE_and_boolSP (*[PrePost_compositeI]:*) Regs Ety PP QQ RR H
-  (l : monadS Regs {b : bool & Sail2_values.ArithFact (PP b)} Ety)
-  (r : monadS Regs {b : bool & Sail2_values.ArithFact (QQ b)} Ety)
-  P (Q : {b : bool & Sail2_values.ArithFact (RR b)} -> predS Regs) E R :
+  (l : monadS Regs {b : bool & Sail2_values.ArithFactP (PP b)} Ety)
+  (r : monadS Regs {b : bool & Sail2_values.ArithFactP (QQ b)} Ety)
+  P (Q : {b : bool & Sail2_values.ArithFactP (RR b)} -> predS Regs) E R :
   PrePostE R r (fun r s => forall pf, Q (existT _ (projT1 r) pf) s) E ->
   PrePostE P l
           (fun r s => match r with
@@ -645,9 +645,9 @@ eapply PrePostE_bindS.
 Qed.
 
 Lemma PrePostE_or_boolSP (*[PrePost_compositeI]:*) Regs Ety PP QQ RR H
-  (l : monadS Regs {b : bool & Sail2_values.ArithFact (PP b)} Ety)
-  (r : monadS Regs {b : bool & Sail2_values.ArithFact (QQ b)} Ety)
-  P (Q : {b : bool & Sail2_values.ArithFact (RR b)} -> predS Regs) E R :
+  (l : monadS Regs {b : bool & Sail2_values.ArithFactP (PP b)} Ety)
+  (r : monadS Regs {b : bool & Sail2_values.ArithFactP (QQ b)} Ety)
+  P (Q : {b : bool & Sail2_values.ArithFactP (RR b)} -> predS Regs) E R :
   PrePostE R r (fun r s => forall pf, Q (existT _ (projT1 r) pf) s) E ->
   PrePostE P l
           (fun r s => match r with
@@ -774,7 +774,7 @@ apply PrePost_foreachS_invariant with (Q := fun v => match v with Value a => Q a
 auto.
 Qed.
 
-Lemma PrePostE_foreach_ZS_up_invariant Regs Vars Ety from to step (H : Sail2_values.ArithFact (0 < step)%Z) vars body (Q : Vars -> predS Regs) (E : ex Ety -> predS Regs) :
+Lemma PrePostE_foreach_ZS_up_invariant Regs Vars Ety from to step (H : Sail2_values.ArithFact (0 <? step)%Z) vars body (Q : Vars -> predS Regs) (E : ex Ety -> predS Regs) :
   (forall i range vars, PrePostE (Q vars) (body i range vars) Q E) ->
   PrePostE (Q vars) (foreach_ZS_up from to step vars body) Q E.
 intro INV.
@@ -793,7 +793,7 @@ induction (S (Z.abs_nat (from - to))); intros.
   + apply PrePostE_returnS.
 Qed.
 
-Lemma PrePostE_foreach_ZS_down_invariant Regs Vars Ety from to step (H : Sail2_values.ArithFact (0 < step)%Z) vars body (Q : Vars -> predS Regs) (E : ex Ety -> predS Regs) :
+Lemma PrePostE_foreach_ZS_down_invariant Regs Vars Ety from to step (H : Sail2_values.ArithFact (0 <? step)%Z) vars body (Q : Vars -> predS Regs) (E : ex Ety -> predS Regs) :
   (forall i range vars, PrePostE (Q vars) (body i range vars) Q E) ->
   PrePostE (Q vars) (foreach_ZS_down from to step vars body) Q E.
 intro INV.
@@ -1038,7 +1038,7 @@ Qed.
 
 Local Open Scope Z.
 
-Lemma PrePostE_undefined_bitvectorS_any Regs Ety n `{Sail2_values.ArithFact (n >= 0)} (Q : Sail2_values.mword n -> predS Regs) (E : ex Ety -> predS Regs) :
+Lemma PrePostE_undefined_bitvectorS_any Regs Ety n `{Sail2_values.ArithFact (n >=? 0)} (Q : Sail2_values.mword n -> predS Regs) (E : ex Ety -> predS Regs) :
   PrePostE (fun s => forall w, Q w s) (undefined_bitvectorS n) Q E.
 unfold undefined_bitvectorS.
 eapply PrePostE_strengthen_pre.
@@ -1049,15 +1049,15 @@ simpl.
 auto.
 Qed.
 
-Lemma PrePostE_undefined_bitvectorS_ignore Regs Ety n `{Sail2_values.ArithFact (n >= 0)} (Q : predS Regs) (E : ex Ety -> predS Regs) :
+Lemma PrePostE_undefined_bitvectorS_ignore Regs Ety n `{Sail2_values.ArithFact (n >=? 0)} (Q : predS Regs) (E : ex Ety -> predS Regs) :
   PrePostE Q (undefined_bitvectorS n) (fun _ => Q) E.
 eapply PrePostE_strengthen_pre.
 apply PrePostE_undefined_bitvectorS_any; auto.
 simpl; auto.
 Qed.
 
-Lemma PrePostE_build_trivial_exS Regs (T:Type) Ety (m : monadS Regs T Ety) P (Q : {T & Sail2_values.ArithFact True} -> predS Regs) E :
-  PrePostE P m (fun v => Q (existT _ v (Sail2_values.Build_ArithFact _ I))) E ->
+Lemma PrePostE_build_trivial_exS Regs (T:Type) Ety (m : monadS Regs T Ety) P (Q : {T & Sail2_values.ArithFact true} -> predS Regs) E :
+  PrePostE P m (fun v => Q (existT _ v (Sail2_values.Build_ArithFactP _ eq_refl))) E ->
   PrePostE P (build_trivial_exS m) Q E.
 intro H.
 unfold build_trivial_exS.
diff --git a/lib/coq/Sail2_operators_mwords.v b/lib/coq/Sail2_operators_mwords.v
index 698ca51b..dfc7fc46 100644
--- a/lib/coq/Sail2_operators_mwords.v
+++ b/lib/coq/Sail2_operators_mwords.v
@@ -43,11 +43,17 @@ destruct m.
 * simpl. rewrite cast_positive_refl. reflexivity.
 Qed.
 
-Definition autocast {T : Z -> Type} {m n} (x : T m) `{H:ArithFact (m = n)} : T n :=
-  cast_T x (use_ArithFact H).
+Definition autocast {T : Z -> Type} {m n} (x : T m) `{H:ArithFact (m =? n)} : T n.
+refine (cast_T x _).
+apply Z.eqb_eq.
+apply (use_ArithFact H).
+Defined.
 
-Definition autocast_m {rv e m n} (x : monad rv (mword m) e) `{H:ArithFact (m = n)} : monad rv (mword n) e :=
-  x >>= fun x => returnm (cast_T x (use_ArithFact H)).
+Definition autocast_m {rv e m n} (x : monad rv (mword m) e) `{H:ArithFact (m =? n)} : monad rv (mword n) e.
+refine (x >>= fun x => returnm (cast_T x _)).
+apply Z.eqb_eq.
+apply (use_ArithFact H).
+Defined.
 
 Definition cast_word {m n} (x : Word.word m) (eq : m = n) : Word.word n :=
   DepEqNat.nat_cast _ eq x.
@@ -94,9 +100,10 @@ Definition update_vec_inc {a} (w : mword a) i b : mword a :=
 (*val update_vec_dec : forall 'a. Size 'a => mword 'a -> integer -> bitU -> mword 'a*)
 Definition update_vec_dec {a} (w : mword a) i b : mword a := opt_def w (update_mword_dec w i b).
 
-Lemma subrange_lemma0 {n m o} `{ArithFact (0 <= o)} `{ArithFact (o <= m < n)} : (Z.to_nat o <= Z.to_nat m < Z.to_nat n)%nat.
+Lemma subrange_lemma0 {n m o} `{ArithFact (0 <=? o)} `{ArithFact (o <=? m <? n)} : (Z.to_nat o <= Z.to_nat m < Z.to_nat n)%nat.
 intros.
 unwrap_ArithFacts.
+unbool_comparisons.
 split.
 + apply Z2Nat.inj_le; omega.
 + apply Z2Nat.inj_lt; omega.
@@ -107,9 +114,10 @@ Qed.
 Lemma subrange_lemma2 {n m o} : (o <= m < n -> m+1 = o+(m-o+1))%nat.
 omega.
 Qed.
-Lemma subrange_lemma3 {m o} `{ArithFact (0 <= o)} `{ArithFact (o <= m)} :
+Lemma subrange_lemma3 {m o} `{ArithFact (0 <=? o)} `{ArithFact (o <=? m)} :
   Z.of_nat (Z.to_nat m - Z.to_nat o + 1)%nat = m - o + 1.
 unwrap_ArithFacts.
+unbool_comparisons.
 rewrite Nat2Z.inj_add.
 rewrite Nat2Z.inj_sub.
 repeat rewrite Z2Nat.id; try omega.
@@ -117,7 +125,7 @@ reflexivity.
 apply Z2Nat.inj_le; omega.
 Qed.
 
-Definition subrange_vec_dec {n} (v : mword n) m o `{ArithFact (0 <= o)} `{ArithFact (o <= m < n)} : mword (m - o + 1) :=
+Definition subrange_vec_dec {n} (v : mword n) m o `{ArithFact (0 <=? o)} `{ArithFact (o <=? m <? n)} : mword (m - o + 1) :=
   let n := Z.to_nat n in
   let m := Z.to_nat m in
   let o := Z.to_nat o in
@@ -127,10 +135,10 @@ Definition subrange_vec_dec {n} (v : mword n) m o `{ArithFact (0 <= o)} `{ArithF
                         (cast_word (split1 (m+1) (n-(m+1)) (cast_word w (subrange_lemma1 prf)))
                                    (subrange_lemma2 prf))) subrange_lemma3.
 
-Definition subrange_vec_inc {n} (v : mword n) m o `{ArithFact (0 <= m)} `{ArithFact (m <= o < n)} : mword (o - m + 1) := autocast (subrange_vec_dec v (n-1-m) (n-1-o)).
+Definition subrange_vec_inc {n} (v : mword n) m o `{ArithFact (0 <=? m)} `{ArithFact (m <=? o <? n)} : mword (o - m + 1) := autocast (subrange_vec_dec v (n-1-m) (n-1-o)).
 
 (* TODO: get rid of bogus default *)
-Parameter dummy_vector : forall {n} `{ArithFact (n >= 0)}, mword n.
+Parameter dummy_vector : forall {n} `{ArithFact (n >=? 0)}, mword n.
 
 (*val update_subrange_vec_inc : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b -> mword 'a*)
 Definition update_subrange_vec_inc_unchecked {a b} (v : mword a) i j (w : mword b) : mword a :=
@@ -141,10 +149,11 @@ Definition update_subrange_vec_dec_unchecked {a b} (v : mword a) i j (w : mword
   opt_def dummy_vector (of_bits (update_subrange_bv_dec v i j w)).
 
 Lemma update_subrange_vec_dec_pf {o m n} :
-ArithFact (0 <= o) ->
-ArithFact (o <= m < n) ->
+ArithFact (0 <=? o) ->
+ArithFact (o <=? m <? n) ->
 Z.of_nat (Z.to_nat o + (Z.to_nat (m - o + 1) + (Z.to_nat n - (Z.to_nat m + 1)))) = n.
 intros [H1] [H2].
+unbool_comparisons.
 rewrite <- subrange_lemma3.
 rewrite !Nat2Z.inj_add.
 rewrite !Nat2Z.inj_sub.
@@ -155,7 +164,7 @@ apply Z2Nat.inj_lt; omega.
 apply Z2Nat.inj_le; omega.
 Qed.
 
-Definition update_subrange_vec_dec {n} (v : mword n) m o `{ArithFact (0 <= o)} `{ArithFact (o <= m < n)} (w : mword (m - o + 1)) : mword n.
+Definition update_subrange_vec_dec {n} (v : mword n) m o `{ArithFact (0 <=? o)} `{ArithFact (o <=? m <? n)} (w : mword (m - o + 1)) : mword n.
 refine (
   let n := Z.to_nat n in
   let m := Z.to_nat m in
@@ -173,7 +182,7 @@ refine (
   cast_to_mword z (update_subrange_vec_dec_pf _ _)).
 Defined.
 
-Definition update_subrange_vec_inc {n} (v : mword n) m o `{ArithFact (0 <= m)} `{ArithFact (m <= o < n)} (w : mword (o - m + 1)) : mword n := update_subrange_vec_dec v (n-1-m) (n-1-o) (autocast w).
+Definition update_subrange_vec_inc {n} (v : mword n) m o `{ArithFact (0 <=? m)} `{ArithFact (m <=? o <? n)} (w : mword (o - m + 1)) : mword n := update_subrange_vec_dec v (n-1-m) (n-1-o) (autocast w).
 
 Lemma mword_nonneg {a} : mword a -> a >= 0.
 destruct a;
@@ -182,9 +191,10 @@ destruct 1.
 Qed.
 
 (*val extz_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b*)
-Definition extz_vec {a b} `{ArithFact (b >= a)} (n : Z) (v : mword a) : mword b.
+Definition extz_vec {a b} `{ArithFact (b >=? a)} (n : Z) (v : mword a) : mword b.
 refine (cast_to_mword (Word.zext (get_word v) (Z.to_nat (b - a))) _).
 unwrap_ArithFacts.
+unbool_comparisons.
 assert (a >= 0). { apply mword_nonneg. assumption. }
 rewrite <- Z2Nat.inj_add; try omega.
 rewrite Zplus_minus.
@@ -193,9 +203,10 @@ auto with zarith.
 Defined.
 
 (*val exts_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b*)
-Definition exts_vec {a b} `{ArithFact (b >= a)} (n : Z) (v : mword a) : mword b.
+Definition exts_vec {a b} `{ArithFact (b >=? a)} (n : Z) (v : mword a) : mword b.
 refine (cast_to_mword (Word.sext (get_word v) (Z.to_nat (b - a))) _).
 unwrap_ArithFacts.
+unbool_comparisons.
 assert (a >= 0). { apply mword_nonneg. assumption. }
 rewrite <- Z2Nat.inj_add; try omega.
 rewrite Zplus_minus.
@@ -203,13 +214,14 @@ apply Z2Nat.id.
 auto with zarith.
 Defined.
 
-Definition zero_extend {a} (v : mword a) (n : Z) `{ArithFact (n >= a)} : mword n := extz_vec n v.
+Definition zero_extend {a} (v : mword a) (n : Z) `{ArithFact (n >=? a)} : mword n := extz_vec n v.
 
-Definition sign_extend {a} (v : mword a) (n : Z) `{ArithFact (n >= a)} : mword n := exts_vec n v.
+Definition sign_extend {a} (v : mword a) (n : Z) `{ArithFact (n >=? a)} : mword n := exts_vec n v.
 
-Definition zeros (n : Z) `{ArithFact (n >= 0)} : mword n.
+Definition zeros (n : Z) `{ArithFact (n >=? 0)} : mword n.
 refine (cast_to_mword (Word.wzero (Z.to_nat n)) _).
 unwrap_ArithFacts.
+unbool_comparisons.
 apply Z2Nat.id.
 auto with zarith.
 Defined.
@@ -227,11 +239,17 @@ assert ((Z.to_nat m <= Z.to_nat n)%nat).
 omega.
 Qed.
 
-Definition vector_truncate {n} (v : mword n) (m : Z) `{ArithFact (m >= 0)} `{ArithFact (m <= n)} : mword m :=
-  cast_to_mword (Word.split1 _ _ (cast_word (get_word v) (ltac:(unwrap_ArithFacts; apply truncate_eq; auto) : Z.to_nat n = Z.to_nat m + (Z.to_nat n - Z.to_nat m))%nat)) (ltac:(unwrap_ArithFacts; apply Z2Nat.id; omega) : Z.of_nat (Z.to_nat m) = m).
+Definition vector_truncate {n} (v : mword n) (m : Z) `{ArithFact (m >=? 0)} `{ArithFact (m <=? n)} : mword m.
+refine (cast_to_mword (Word.split1 _ _ (cast_word (get_word v) (_ : Z.to_nat n = Z.to_nat m + (Z.to_nat n - Z.to_nat m))%nat)) (_ : Z.of_nat (Z.to_nat m) = m)).
+abstract (unwrap_ArithFacts; unbool_comparisons; apply truncate_eq; auto with zarith).
+abstract (unwrap_ArithFacts; unbool_comparisons; apply Z2Nat.id; omega).
+Defined.
 
-Definition vector_truncateLSB {n} (v : mword n) (m : Z) `{ArithFact (m >= 0)} `{ArithFact (m <= n)} : mword m :=
-  cast_to_mword (Word.split2 _ _ (cast_word (get_word v) (ltac:(unwrap_ArithFacts; apply truncateLSB_eq; auto) : Z.to_nat n = (Z.to_nat n - Z.to_nat m) + Z.to_nat m)%nat)) (ltac:(unwrap_ArithFacts; apply Z2Nat.id; omega) : Z.of_nat (Z.to_nat m) = m).
+Definition vector_truncateLSB {n} (v : mword n) (m : Z) `{ArithFact (m >=? 0)} `{ArithFact (m <=? n)} : mword m.
+refine (cast_to_mword (Word.split2 _ _ (cast_word (get_word v) (_ : Z.to_nat n = (Z.to_nat n - Z.to_nat m) + Z.to_nat m)%nat)) (_ : Z.of_nat (Z.to_nat m) = m)).
+abstract (unwrap_ArithFacts; unbool_comparisons; apply truncateLSB_eq; auto with zarith).
+abstract (unwrap_ArithFacts; unbool_comparisons; apply Z2Nat.id; omega).
+Defined.
 
 Lemma concat_eq {a b} : a >= 0 -> b >= 0 -> Z.of_nat (Z.to_nat b + Z.to_nat a)%nat = a + b.
 intros.
@@ -270,13 +288,15 @@ induction n.
   reflexivity.
 Qed.
 
-Program Definition uint {a} (x : mword a) : {z : Z & ArithFact (0 <= z /\ z <= 2 ^ a - 1)} :=
+Program Definition uint {a} (x : mword a) : {z : Z & ArithFact (0 <=? z <=? 2 ^ a - 1)} :=
  existT _ (Z.of_N (Word.wordToN (get_word x))) _.
 Next Obligation.
 constructor.
+apply Bool.andb_true_iff.
 constructor.
-* apply N2Z.is_nonneg.
-* assert (2 ^ a - 1 = Z.of_N (2 ^ (Z.to_N a) - 1)). {
+* apply Z.leb_le. apply N2Z.is_nonneg.
+* apply Z.leb_le.
+  assert (2 ^ a - 1 = Z.of_N (2 ^ (Z.to_N a) - 1)). {
     rewrite N2Z.inj_sub.
     * rewrite N2Z.inj_pow.
       rewrite Z2N.id; auto.
@@ -303,12 +323,14 @@ induction n.
   rewrite Z.pow_succ_r; auto with zarith.
 Qed.
 
-Program Definition sint {a} `{ArithFact (a > 0)} (x : mword a) : {z : Z & ArithFact (-(2^(a-1)) <= z /\ z <= 2 ^ (a-1) - 1)} :=
+Program Definition sint {a} `{ArithFact (a >? 0)} (x : mword a) : {z : Z & ArithFact (-(2^(a-1)) <=? z <=? 2 ^ (a-1) - 1)} :=
   existT _ (Word.wordToZ (get_word x)) _.
 Next Obligation.
 destruct H.
+unbool_comparisons.
 destruct a; try inversion fact.
 constructor.
+unbool_comparisons_goal.
 generalize (get_word x).
 rewrite <- positive_nat_Z.
 destruct (Pos2Nat.is_succ p) as [n eq].
@@ -326,10 +348,10 @@ rewrite <- Z.lt_le_pred.
 auto.
 Defined.
 
-Definition sint0 {a} `{ArithFact (a >= 0)} (x : mword a) : Z :=
+Definition sint0 {a} `{ArithFact (a >=? 0)} (x : mword a) : Z :=
   if sumbool_of_bool (Z.eqb a 0) then 0 else projT1 (sint x).
 
-Lemma length_list_pos : forall {A} {l:list A}, length_list l >= 0.
+Lemma length_list_pos : forall {A} {l:list A}, 0 <= Z.of_nat (List.length l).
 unfold length_list.
 auto with zarith.
 Qed.
@@ -369,9 +391,9 @@ val smult_vec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> mword 'a -> mword
 Definition add_vec   {n} : mword n -> mword n -> mword n := word_binop Word.wplus.
 (*Definition sadd_vec  {n} : mword n -> mword n -> mword n := sadd_bv w.*)
 Definition sub_vec   {n} : mword n -> mword n -> mword n := word_binop Word.wminus.
-Definition mult_vec  {n m} `{ArithFact (m >= n)} (l : mword n) (r : mword n) : mword m :=
+Definition mult_vec  {n m} `{ArithFact (m >=? n)} (l : mword n) (r : mword n) : mword m :=
   word_binop Word.wmult (zero_extend l _) (zero_extend r _).
-Definition mults_vec  {n m} `{ArithFact (m >= n)} (l : mword n) (r : mword n) : mword m :=
+Definition mults_vec  {n m} `{ArithFact (m >=? n)} (l : mword n) (r : mword n) : mword m :=
   word_binop Word.wmult (sign_extend l _) (sign_extend r _).
 
 (*val add_vec_int   : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
@@ -456,14 +478,14 @@ match n with
 | O => Word.WO
 | S m => Word.combine w (replicate_bits_aux w m)
 end.
-Lemma replicate_ok {n a} `{ArithFact (n >= 0)} `{ArithFact (a >= 0)} :
+Lemma replicate_ok {n a} `{ArithFact (n >=? 0)} `{ArithFact (a >=? 0)} :
    Z.of_nat (Z.to_nat n * Z.to_nat a) = a * n.
-destruct H. destruct H0.
+destruct H. destruct H0. unbool_comparisons.
 rewrite <- Z2Nat.id; auto with zarith.
 rewrite Z2Nat.inj_mul; auto with zarith.
 rewrite Nat.mul_comm. reflexivity.
 Qed.
-Definition replicate_bits {a} (w : mword a) (n : Z) `{ArithFact (n >= 0)} : mword (a * n) :=
+Definition replicate_bits {a} (w : mword a) (n : Z) `{ArithFact (n >=? 0)} : mword (a * n) :=
  cast_to_mword (replicate_bits_aux (get_word w) (Z.to_nat n)) replicate_ok.
 
 (*val duplicate : forall 'a. Size 'a => bitU -> integer -> mword 'a
@@ -520,7 +542,7 @@ Qed.
 
 Definition reverse_endianness {n} (bits : mword n) := with_word (P := id) reverse_endianness_word bits.
 
-Definition get_slice_int {a} `{ArithFact (a >= 0)} : Z -> Z -> Z -> mword a := get_slice_int_bv.
+Definition get_slice_int {a} `{ArithFact (a >=? 0)} : Z -> Z -> Z -> mword a := get_slice_int_bv.
 
 Definition set_slice n m (v : mword n) x (w : mword m) : mword n :=
   update_subrange_vec_dec_unchecked v (x + m - 1) x w.
@@ -535,7 +557,7 @@ Definition set_slice_int len n lo (v : mword len) : Z :=
   else n.
 
 (* Variant of bitvector slicing for the ARM model with few constraints *)
-Definition slice {m} (v : mword m) lo len `{ArithFact (0 <= len)} : mword len :=
+Definition slice {m} (v : mword m) lo len `{ArithFact (0 <=? len)} : mword len :=
   if sumbool_of_bool (orb (len =? 0) (lo <? 0))
   then zeros len
   else
@@ -563,15 +585,15 @@ destruct (sumbool_of_bool _).
 *)
 
 Import ListNotations.
-Definition count_leading_zeros {N : Z} (x : mword N) `{ArithFact (N >= 1)} 
-: {n : Z & ArithFact (0 <= n /\ n <= N)} :=
-  let r : {n : Z & ArithFact (0 <= n /\ n <= N)} := build_ex N in
+Definition count_leading_zeros {N : Z} (x : mword N) `{ArithFact (N >=? 1)} 
+: {n : Z & ArithFact (0 <=? n <=? N)} :=
+  let r : {n : Z & ArithFact (0 <=? n <=? N)} := build_ex N in
   foreach_Z_up 0 (N - 1) 1 r
     (fun i _ r =>
       (if ((eq_vec (vec_of_bits [access_vec_dec x i]  : mword 1) (vec_of_bits [B1]  : mword 1)))
        then build_ex
             (Z.sub (Z.sub (length_mword x) i) 1)
-             : {n : Z & ArithFact (0 <= n /\ n <= N)}
+             : {n : Z & ArithFact (0 <=? n <=? N)}
        else r))
    .
 
diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v
index fbc0f5b1..aeca1248 100644
--- a/lib/coq/Sail2_prompt.v
+++ b/lib/coq/Sail2_prompt.v
@@ -30,7 +30,7 @@ match l with
   foreachM xs vars body
 end.
 
-Fixpoint foreach_ZM_up' {rv e Vars} (from to step off : Z) (n : nat) `{ArithFact (0 < step)} `{ArithFact (0 <= off)} (vars : Vars) (body : forall (z : Z) `(ArithFact (from <= z <= to)), Vars -> monad rv Vars e) {struct n} : monad rv Vars e.
+Fixpoint foreach_ZM_up' {rv e Vars} (from to step off : Z) (n : nat) `{ArithFact (0 <? step)} `{ArithFact (0 <=? off)} (vars : Vars) (body : forall (z : Z) `(ArithFact (from <=? z <=? to)), Vars -> monad rv Vars e) {struct n} : monad rv Vars e.
 exact (
   if sumbool_of_bool (from + off <=? to) then
     match n with
@@ -40,7 +40,7 @@ exact (
   else returnm vars).
 Defined.
 
-Fixpoint foreach_ZM_down' {rv e Vars} (from to step off : Z) (n : nat) `{ArithFact (0 < step)} `{ArithFact (off <= 0)} (vars : Vars) (body : forall (z : Z) `(ArithFact (to <= z <= from)), Vars -> monad rv Vars e) {struct n} : monad rv Vars e.
+Fixpoint foreach_ZM_down' {rv e Vars} (from to step off : Z) (n : nat) `{ArithFact (0 <? step)} `{ArithFact (off <=? 0)} (vars : Vars) (body : forall (z : Z) `(ArithFact (to <=? z <=? from)), Vars -> monad rv Vars e) {struct n} : monad rv Vars e.
 exact (
   if sumbool_of_bool (to <=? from + off) then
     match n with
@@ -50,9 +50,9 @@ exact (
   else returnm vars).
 Defined.
 
-Definition foreach_ZM_up {rv e Vars} from to step vars body `{ArithFact (0 < step)} :=
+Definition foreach_ZM_up {rv e Vars} from to step vars body `{ArithFact (0 <? step)} :=
     foreach_ZM_up' (rv := rv) (e := e) (Vars := Vars) from to step 0 (S (Z.abs_nat (from - to))) vars body.
-Definition foreach_ZM_down {rv e Vars} from to step vars body `{ArithFact (0 < step)} :=
+Definition foreach_ZM_down {rv e Vars} from to step vars body `{ArithFact (0 <? step)} :=
     foreach_ZM_down' (rv := rv) (e := e) (Vars := Vars) from to step 0 (S (Z.abs_nat (from - to))) vars body.
 
 (*declare {isabelle} termination_argument foreachM = automatic*)
@@ -69,9 +69,9 @@ Definition and_boolM {rv E} (l : monad rv bool E) (r : monad rv bool E) : monad
    the state monad and program logic rules.  They are not currently used in the proof
    rules because it was more convenient to quantify over them instead. *)
 Definition and_bool_left_proof {P Q R:bool -> Prop} :
-  ArithFact (P false) ->
-  ArithFact (forall l r, P l -> (l = true -> Q r) -> R (andb l r)) ->
-  ArithFact (R false).
+  ArithFactP (P false) ->
+  (forall l r, ArithFactP (P l -> ((l = true -> (Q r)) -> (R (andb l r))))) ->
+  ArithFactP (R false).
 intros [p] [h].
 constructor.
 change false with (andb false false).
@@ -80,20 +80,20 @@ congruence.
 Qed.
 
 Definition and_bool_full_proof {P Q R:bool -> Prop} {r} :
-  ArithFact (P true) ->
-  ArithFact (Q r) ->
-  ArithFact (forall l r, P l -> (l = true -> Q r) -> R (andb l r)) ->
-  ArithFact (R r).
+  ArithFactP (P true) ->
+  ArithFactP (Q r) ->
+  (forall l r, ArithFactP ((P l) -> ((l = true -> (Q r)) -> (R (andb l r))))) ->
+  ArithFactP (R r).
 intros [p] [q] [h].
 constructor.
 change r with (andb true r).
 apply h; auto.
 Qed.
 
-Definition and_boolMP {rv E} {P Q R:bool->Prop} (x : monad rv {b:bool & ArithFact (P b)} E) (y : monad rv {b:bool & ArithFact (Q b)} E)
-  `{H:ArithFact (forall l r, P l -> (l = true -> Q r) -> R (andb l r))}
-  : monad rv {b:bool & ArithFact (R b)} E :=
-  x >>= fun '(existT _ x p) => (if x return ArithFact (P x) -> _ then
+Definition and_boolMP {rv E} {P Q R:bool->Prop} (x : monad rv {b:bool & ArithFactP (P b)} E) (y : monad rv {b:bool & ArithFactP (Q b)} E)
+  `{H:forall l r, ArithFactP ((P l) -> ((l = true -> (Q r)) -> (R (andb l r))))}
+  : monad rv {b:bool & ArithFactP (R b)} E :=
+  x >>= fun '(existT _ x p) => (if x return ArithFactP (P x) -> _ then
     fun p => y >>= fun '(existT _ y q) => returnm (existT _ y (and_bool_full_proof p q H))
   else fun p => returnm (existT _ false (and_bool_left_proof p H))) p.
 
@@ -103,9 +103,9 @@ Definition or_boolM {rv E} (l : monad rv bool E) (r : monad rv bool E) : monad r
 
 
 Definition or_bool_left_proof {P Q R:bool -> Prop} :
-  ArithFact (P true) ->
-  ArithFact (forall l r, P l -> (l = false -> Q r) -> R (orb l r)) ->
-  ArithFact (R true).
+  ArithFactP (P true) ->
+  (forall l r, ArithFactP ((P l) -> (((l = false) -> (Q r)) -> (R (orb l r))))) ->
+  ArithFactP (R true).
 intros [p] [h].
 constructor.
 change true with (orb true false).
@@ -114,25 +114,25 @@ congruence.
 Qed.
 
 Definition or_bool_full_proof {P Q R:bool -> Prop} {r} :
-  ArithFact (P false) ->
-  ArithFact (Q r) ->
-  ArithFact (forall l r, P l -> (l = false -> Q r) -> R (orb l r)) ->
-  ArithFact (R r).
+  ArithFactP (P false) ->
+  ArithFactP (Q r) ->
+  (forall l r, ArithFactP ((P l) -> (((l = false) -> (Q r)) -> (R (orb l r))))) ->
+  ArithFactP (R r).
 intros [p] [q] [h].
 constructor.
 change r with (orb false r).
 apply h; auto.
 Qed.
 
-Definition or_boolMP {rv E} {P Q R:bool -> Prop} (l : monad rv {b : bool & ArithFact (P b)} E) (r : monad rv {b : bool & ArithFact (Q b)} E)
- `{ArithFact (forall l r, P l -> (l = false -> Q r) -> R (orb l r))}
- : monad rv {b : bool & ArithFact (R b)} E :=
+Definition or_boolMP {rv E} {P Q R:bool -> Prop} (l : monad rv {b : bool & ArithFactP (P b)} E) (r : monad rv {b : bool & ArithFactP (Q b)} E)
+ `{forall l r, ArithFactP ((P l) -> (((l = false) -> (Q r)) -> (R (orb l r))))}
+ : monad rv {b : bool & ArithFactP (R b)} E :=
  l >>= fun '(existT _ l p) =>
-  (if l return ArithFact (P l) -> _ then fun p => returnm (existT _ true (or_bool_left_proof p H))
+  (if l return ArithFactP (P l) -> _ then fun p => returnm (existT _ true (or_bool_left_proof p H))
    else fun p => r >>= fun '(existT _ r q) => returnm (existT _ r (or_bool_full_proof p q H))) p.
 
-Definition build_trivial_ex {rv E} {T:Type} (x:monad rv T E) : monad rv {x : T & ArithFact True} E :=
-  x >>= fun x => returnm (existT _ x (Build_ArithFact _ I)).
+Definition build_trivial_ex {rv E} {T:Type} (x:monad rv T E) : monad rv {x : T & ArithFact true} E :=
+  x >>= fun x => returnm (existT _ x (Build_ArithFactP _ eq_refl)).
 
 (*val bool_of_bitU_fail : forall 'rv 'e. bitU -> monad 'rv bool 'e*)
 Definition bool_of_bitU_fail {rv E} (b : bitU) : monad rv bool E :=
@@ -164,9 +164,10 @@ Definition of_bits_fail {rv A E} `{Bitvector A} (bits : list bitU) : monad rv A
 
 (* For termination of recursive functions.  We don't name assertions, so use
    the type class mechanism to find it. *)
-Definition _limit_reduces {_limit} (_acc:Acc (Zwf 0) _limit) `{ArithFact (_limit >= 0)} : Acc (Zwf 0) (_limit - 1).
+Definition _limit_reduces {_limit} (_acc:Acc (Zwf 0) _limit) `{ArithFact (_limit >=? 0)} : Acc (Zwf 0) (_limit - 1).
 refine (Acc_inv _acc _).
 destruct H.
+unbool_comparisons.
 red.
 omega.
 Defined.
@@ -269,18 +270,18 @@ Fixpoint undefined_word_nat {rv e} n : monad rv (Word.word n) e :=
     returnm (Word.WS b t)
   end.
 
-Definition undefined_bitvector {rv e} n `{ArithFact (n >= 0)} : monad rv (mword n) e :=
+Definition undefined_bitvector {rv e} n `{ArithFact (n >=? 0)} : monad rv (mword n) e :=
   undefined_word_nat (Z.to_nat n) >>= fun w =>
   returnm (word_to_mword w).
 
 (* If we need to build an existential after a monadic operation, assume that
    we can do it entirely from the type. *)
 
-Definition build_ex_m {rv e} {T:Type} (x:monad rv T e) {P:T -> Prop} `{H:forall x, ArithFact (P x)} : monad rv {x : T & ArithFact (P x)} e :=
+Definition build_ex_m {rv e} {T:Type} (x:monad rv T e) {P:T -> Prop} `{H:forall x, ArithFactP (P x)} : monad rv {x : T & ArithFactP (P x)} e :=
   x >>= fun y => returnm (existT _ y (H y)).
 
 Definition projT1_m {rv e} {T:Type} {P:T -> Prop} (x: monad rv {x : T & P x} e) : monad rv T e :=
   x >>= fun y => returnm (projT1 y).
 
-Definition derive_m {rv e} {T:Type} {P Q:T -> Prop} (x : monad rv {x : T & P x} e) `{forall x, ArithFact (P x) -> ArithFact (Q x)} : monad rv {x : T & (ArithFact (Q x))} e :=
+Definition derive_m {rv e} {T:Type} {P Q:T -> Prop} (x : monad rv {x : T & ArithFactP (P x)} e) `{forall x, ArithFactP (P x) -> ArithFactP (Q x)} : monad rv {x : T & (ArithFactP (Q x))} e :=
   x >>= fun y => returnm (build_ex (projT1 y)).
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 =>
diff --git a/lib/coq/Sail2_state.v b/lib/coq/Sail2_state.v
index 0cfc9f17..51a8e5fd 100644
--- a/lib/coq/Sail2_state.v
+++ b/lib/coq/Sail2_state.v
@@ -33,7 +33,7 @@ end.
 (* This uses the same subproof as the prompt version to get around proof relevance issues
    in Sail2_state_lemmas.  TODO: if we switch to boolean properties this shouldn't be
    necessary. *)
-Fixpoint foreach_ZS_up' {rv e Vars} (from to step off : Z) (n : nat) `{ArithFact (0 < step)} `{ArithFact (0 <= off)} (vars : Vars) (body : forall (z : Z) `(ArithFact (from <= z <= to)), Vars -> monadS rv Vars e) {struct n} : monadS rv Vars e.
+Fixpoint foreach_ZS_up' {rv e Vars} (from to step off : Z) (n : nat) `{ArithFact (0 <? step)} `{ArithFact (0 <=? off)} (vars : Vars) (body : forall (z : Z) `(ArithFact (from <=? z <=? to)), Vars -> monadS rv Vars e) {struct n} : monadS rv Vars e.
 exact (
   match sumbool_of_bool (from + off <=? to) with left LE =>
     match n with
@@ -44,7 +44,7 @@ exact (
   end).
 Defined.
 
-Fixpoint foreach_ZS_down' {rv e Vars} (from to step off : Z) (n : nat) `{ArithFact (0 < step)} `{ArithFact (off <= 0)} (vars : Vars) (body : forall (z : Z) `(ArithFact (to <= z <= from)), Vars -> monadS rv Vars e) {struct n} : monadS rv Vars e.
+Fixpoint foreach_ZS_down' {rv e Vars} (from to step off : Z) (n : nat) `{ArithFact (0 <? step)} `{ArithFact (off <=? 0)} (vars : Vars) (body : forall (z : Z) `(ArithFact (to <=? z <=? from)), Vars -> monadS rv Vars e) {struct n} : monadS rv Vars e.
 exact (
   match sumbool_of_bool (to <=? from + off) with left LE =>
     match n with
@@ -55,9 +55,9 @@ exact (
   end).
 Defined.
 
-Definition foreach_ZS_up {rv e Vars} from to step vars body `{ArithFact (0 < step)} :=
+Definition foreach_ZS_up {rv e Vars} from to step vars body `{ArithFact (0 <? step)} :=
     foreach_ZS_up' (rv := rv) (e := e) (Vars := Vars) from to step 0 (S (Z.abs_nat (from - to))) vars body.
-Definition foreach_ZS_down {rv e Vars} from to step vars body `{ArithFact (0 < step)} :=
+Definition foreach_ZS_down {rv e Vars} from to step vars body `{ArithFact (0 <? step)} :=
     foreach_ZS_down' (rv := rv) (e := e) (Vars := Vars) from to step 0 (S (Z.abs_nat (from - to))) vars body.
 
 (*val genlistS : forall 'a 'rv 'e. (nat -> monadS 'rv 'a 'e) -> nat -> monadS 'rv (list 'a) 'e*)
@@ -73,22 +73,22 @@ Definition and_boolS {RV E} (l r : monadS RV bool E) : monadS RV bool E :=
 Definition or_boolS {RV E} (l r : monadS RV bool E) : monadS RV bool E :=
  l >>$= (fun l => if l then returnS true else r).
 
-Definition and_boolSP {rv E} {P Q R:bool->Prop} (x : monadS rv {b:bool & ArithFact (P b)} E) (y : monadS rv {b:bool & ArithFact (Q b)} E)
-  `{H:ArithFact (forall l r, P l -> (l = true -> Q r) -> R (andb l r))}
-  : monadS rv {b:bool & ArithFact (R b)} E :=
-  x >>$= fun '(existT _ x p) => (if x return ArithFact (P x) -> _ then
+Definition and_boolSP {rv E} {P Q R:bool->Prop} (x : monadS rv {b:bool & ArithFactP (P b)} E) (y : monadS rv {b:bool & ArithFactP (Q b)} E)
+  `{H:forall l r, ArithFactP ((P l) -> ((l = true -> (Q r)) -> (R (andb l r))))}
+  : monadS rv {b:bool & ArithFactP (R b)} E :=
+  x >>$= fun '(existT _ x p) => (if x return ArithFactP (P x) -> _ then
     fun p => y >>$= fun '(existT _ y q) => returnS (existT _ y (and_bool_full_proof p q H))
   else fun p => returnS (existT _ false (and_bool_left_proof p H))) p.
 
-Definition or_boolSP {rv E} {P Q R:bool -> Prop} (l : monadS rv {b : bool & ArithFact (P b)} E) (r : monadS rv {b : bool & ArithFact (Q b)} E)
- `{ArithFact (forall l r, P l -> (l = false -> Q r) -> R (orb l r))}
- : monadS rv {b : bool & ArithFact (R b)} E :=
+Definition or_boolSP {rv E} {P Q R:bool -> Prop} (l : monadS rv {b : bool & ArithFactP (P b)} E) (r : monadS rv {b : bool & ArithFactP (Q b)} E)
+ `{forall l r, ArithFactP ((P l) -> (((l = false) -> (Q r)) -> (R (orb l r))))}
+ : monadS rv {b : bool & ArithFactP (R b)} E :=
  l >>$= fun '(existT _ l p) =>
-  (if l return ArithFact (P l) -> _ then fun p => returnS (existT _ true (or_bool_left_proof p H))
+  (if l return ArithFactP (P l) -> _ then fun p => returnS (existT _ true (or_bool_left_proof p H))
    else fun p => r >>$= fun '(existT _ r q) => returnS (existT _ r (or_bool_full_proof p q H))) p.
 
-Definition build_trivial_exS {rv E} {T:Type} (x : monadS rv T E) : monadS rv {x : T & ArithFact True} E :=
- x >>$= fun x => returnS (existT _ x (Build_ArithFact _ I)).
+Definition build_trivial_exS {rv E} {T:Type} (x : monadS rv T E) : monadS rv {x : T & ArithFact true} E :=
+ x >>$= fun x => returnS (existT _ x (Build_ArithFactP _ eq_refl)).
 
 (*val bool_of_bitU_fail : forall 'rv 'e. bitU -> monadS 'rv bool 'e*)
 Definition bool_of_bitU_fail {RV E} (b : bitU) : monadS RV bool E :=
@@ -114,12 +114,12 @@ Definition bools_of_bits_nondetS {RV E} bits : monadS RV (list bool) E :=
       returnS (bools ++ [b]))).
 
 (*val of_bits_nondetS : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monadS 'rv 'a 'e*)
-Definition of_bits_nondetS {RV A E} bits `{ArithFact (A >= 0)} : monadS RV (mword A) E :=
+Definition of_bits_nondetS {RV A E} bits `{ArithFact (A >=? 0)} : monadS RV (mword A) E :=
   bools_of_bits_nondetS bits >>$= (fun bs =>
   returnS (of_bools bs)).
 
 (*val of_bits_failS : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monadS 'rv 'a 'e*)
-Definition of_bits_failS {RV A E} bits `{ArithFact (A >= 0)} : monadS RV (mword A) E :=
+Definition of_bits_failS {RV A E} bits `{ArithFact (A >=? 0)} : monadS RV (mword A) E :=
  maybe_failS "of_bits" (of_bits bits).
 
 (*val mword_nondetS : forall 'rv 'a 'e. Size 'a => unit -> monadS 'rv (mword 'a) 'e
@@ -199,7 +199,7 @@ Fixpoint undefined_word_natS {rv e} n : monadS rv (Word.word n) e :=
     returnS (Word.WS b t)
   end.
 
-Definition undefined_bitvectorS {rv e} n `{ArithFact (n >= 0)} : monadS rv (mword n) e :=
+Definition undefined_bitvectorS {rv e} n `{ArithFact (n >=? 0)} : monadS rv (mword n) e :=
   undefined_word_natS (Z.to_nat n) >>$= fun w =>
   returnS (word_to_mword w).
 
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.
diff --git a/lib/coq/Sail2_state_monad.v b/lib/coq/Sail2_state_monad.v
index bf5c5916..3fb1f8d9 100644
--- a/lib/coq/Sail2_state_monad.v
+++ b/lib/coq/Sail2_state_monad.v
@@ -182,14 +182,14 @@ Definition read_mem_bytesS {Regs E} (rk : read_kind) addr sz : monadS Regs (list
   returnS bytes).
 
 (*val read_memtS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs ('b * bitU) 'e*)
-Definition read_memtS {Regs E A B} (rk : read_kind) (a : mword A) sz `{ArithFact (B >= 0)} : monadS Regs (mword B * bitU) E :=
+Definition read_memtS {Regs E A B} (rk : read_kind) (a : mword A) sz `{ArithFact (B >=? 0)} : monadS Regs (mword B * bitU) E :=
   let a := Word.wordToNat (get_word a) in
   read_memt_bytesS rk a (Z.to_nat sz) >>$= (fun '(bytes, tag) =>
   maybe_failS "bits_of_mem_bytes" (of_bits (bits_of_mem_bytes bytes)) >>$= (fun mem_val =>
   returnS (mem_val, tag))).
 
 (*val read_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs 'b 'e*)
-Definition read_memS {Regs E A B} rk (a : mword A) sz `{ArithFact (B >= 0)} : monadS Regs (mword B) E :=
+Definition read_memS {Regs E A B} rk (a : mword A) sz `{ArithFact (B >=? 0)} : monadS Regs (mword B) E :=
   read_memtS rk a sz >>$= (fun '(bytes, _) =>
   returnS bytes).
 
diff --git a/lib/coq/Sail2_string.v b/lib/coq/Sail2_string.v
index a0a23933..152c003a 100644
--- a/lib/coq/Sail2_string.v
+++ b/lib/coq/Sail2_string.v
@@ -8,15 +8,15 @@ Definition string_startswith s expected :=
   let prefix := String.substring 0 (String.length expected) s in
   generic_eq prefix expected.
 
-Definition string_drop s (n : Z) `{ArithFact (n >= 0)} :=
+Definition string_drop s (n : Z) `{ArithFact (n >=? 0)} :=
   let n := Z.to_nat n in
   String.substring n (String.length s - n) s.
 
-Definition string_take s (n : Z) `{ArithFact (n >= 0)} :=
+Definition string_take s (n : Z) `{ArithFact (n >=? 0)} :=
   let n := Z.to_nat n in
   String.substring 0 n s.
 
-Definition string_length s : {n : Z & ArithFact (n >= 0)} :=
+Definition string_length s : {n : Z & ArithFact (n >=? 0)} :=
  build_ex (Z.of_nat (String.length s)).
 
 Definition string_append := String.append.
@@ -56,7 +56,7 @@ match s with
     else (acc, len)
   end
 end.
-Local Definition int_of (s : string) (base : Z) (len : nat) : option (Z * {n : Z & ArithFact (n >= 0)}) :=
+Local Definition int_of (s : string) (base : Z) (len : nat) : option (Z * {n : Z & ArithFact (n >=? 0)}) :=
 match s with
 | EmptyString => None
 | String h t =>
@@ -74,7 +74,7 @@ end.
 (* I've stuck closely to OCaml's int_of_string, because that's what's currently
    used elsewhere. *)
 
-Definition maybe_int_of_prefix (s : string) : option (Z * {n : Z & ArithFact (n >= 0)}) :=
+Definition maybe_int_of_prefix (s : string) : option (Z * {n : Z & ArithFact (n >=? 0)}) :=
 match s with
 | EmptyString => None
 | String "0" (String ("x"|"X") t) => int_of t 16 2
@@ -105,16 +105,16 @@ Fixpoint n_leading_spaces (s:string) : nat :=
   | _ => 0
   end.
 
-Definition opt_spc_matches_prefix s : option (unit * {n : Z & ArithFact (n >= 0)}) :=
+Definition opt_spc_matches_prefix s : option (unit * {n : Z & ArithFact (n >=? 0)}) :=
   Some (tt, build_ex (Z.of_nat (n_leading_spaces s))).
 
-Definition spc_matches_prefix s : option (unit * {n : Z & ArithFact (n >= 0)}) :=
+Definition spc_matches_prefix s : option (unit * {n : Z & ArithFact (n >=? 0)}) :=
   match n_leading_spaces s with
   | O => None
   | S n => Some (tt, build_ex (Z.of_nat (S n)))
   end.
 
-Definition hex_bits_n_matches_prefix sz `{ArithFact (sz >= 0)} s : option (mword sz * {n : Z & ArithFact (n >= 0)}) :=
+Definition hex_bits_n_matches_prefix sz `{ArithFact (sz >=? 0)} s : option (mword sz * {n : Z & ArithFact (n >=? 0)}) :=
   match maybe_int_of_prefix s with
   | None => None
   | Some (n, len) =>
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 404d585d..d25ab00b 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -14,6 +14,7 @@ Require Import Lia.
 Import ListNotations.
 
 Open Scope Z.
+Open Scope bool.
 
 Module Z_eq_dec.
 Definition U := Z.
@@ -26,8 +27,14 @@ Module ZEqdep := DecidableEqDep (Z_eq_dec).
    can be added to, and a typeclass to wrap constraint arguments in to
    trigger automatic solving. *)
 Create HintDb sail.
-Class ArithFact (P : Prop) := { fact : P }.
-Lemma use_ArithFact {P} `(ArithFact P) : P.
+(* Facts translated from Sail's type system are wrapped in ArithFactP or
+   ArithFact so that the solver can be invoked automatically by Coq's
+   typeclass mechanism.  Most properties are boolean, which enjoys proof
+   irrelevance by UIP. *)
+Class ArithFactP (P : Prop) := { fact : P }.
+Class ArithFact (P : bool) := ArithFactClass : ArithFactP (P = true).
+Lemma use_ArithFact {P} `(ArithFact P) : P = true.
+unfold ArithFact in *.
 apply fact.
 Defined.
 
@@ -35,18 +42,17 @@ Defined.
 Require Import Coq.Classes.Morphisms.
 Require Import Coq.Program.Basics.
 Require Import Coq.Program.Tactics.
+
 Section Morphism.
 Local Obligation Tactic := try solve [simpl_relation | firstorder auto].
-
-Global Program Instance ArithFact_iff_morphism :
-  Proper (iff ==> iff) ArithFact.
+Global Program Instance ArithFactP_iff_morphism :
+  Proper (iff ==> iff) ArithFactP.
 End Morphism.
 
-
-Definition build_ex {T:Type} (n:T) {P:T -> Prop} `{H:ArithFact (P n)} : {x : T & ArithFact (P x)} :=
+Definition build_ex {T:Type} (n:T) {P:T -> Prop} `{H:ArithFactP (P n)} : {x : T & ArithFactP (P x)} :=
   existT _ n H.
 
-Definition build_ex2 {T:Type} {T':T -> Type} (n:T) (m:T' n) {P:T -> Prop} `{H:ArithFact (P n)} : {x : T & T' x & ArithFact (P x)} :=
+Definition build_ex2 {T:Type} {T':T -> Type} (n:T) (m:T' n) {P:T -> Prop} `{H:ArithFactP (P n)} : {x : T & T' x & ArithFactP (P x)} :=
   existT2 _ _ n m H.
 
 Definition generic_eq {T:Type} (x y:T) `{Decidable (x = y)} := Decidable_witness.
@@ -132,16 +138,20 @@ Ltac cmp_record_field x y :=
   ].
 
 
+Notation "x <=? y <=? z" := ((x <=? y) && (y <=? z)) (at level 70, y at next level) : Z_scope.
+Notation "x <=? y <? z" := ((x <=? y) && (y <? z)) (at level 70, y at next level) : Z_scope.
+Notation "x <? y <? z" := ((x <? y) && (y <? z)) (at level 70, y at next level) : Z_scope.
+Notation "x <? y <=? z" := ((x <? y) && (y <=? z)) (at level 70, y at next level) : Z_scope.
 
 (* Project away range constraints in comparisons *)
-Definition ltb_range_l {lo hi} (l : {x & ArithFact (lo <= x /\ x <= hi)}) r := Z.ltb (projT1 l) r.
-Definition leb_range_l {lo hi} (l : {x & ArithFact (lo <= x /\ x <= hi)}) r := Z.leb (projT1 l) r.
-Definition gtb_range_l {lo hi} (l : {x & ArithFact (lo <= x /\ x <= hi)}) r := Z.gtb (projT1 l) r.
-Definition geb_range_l {lo hi} (l : {x & ArithFact (lo <= x /\ x <= hi)}) r := Z.geb (projT1 l) r.
-Definition ltb_range_r {lo hi} l (r : {x & ArithFact (lo <= x /\ x <= hi)}) := Z.ltb l (projT1 r).
-Definition leb_range_r {lo hi} l (r : {x & ArithFact (lo <= x /\ x <= hi)}) := Z.leb l (projT1 r).
-Definition gtb_range_r {lo hi} l (r : {x & ArithFact (lo <= x /\ x <= hi)}) := Z.gtb l (projT1 r).
-Definition geb_range_r {lo hi} l (r : {x & ArithFact (lo <= x /\ x <= hi)}) := Z.geb l (projT1 r).
+Definition ltb_range_l {lo hi} (l : {x & ArithFact (lo <=? x <=? hi)}) r := Z.ltb (projT1 l) r.
+Definition leb_range_l {lo hi} (l : {x & ArithFact (lo <=? x <=? hi)}) r := Z.leb (projT1 l) r.
+Definition gtb_range_l {lo hi} (l : {x & ArithFact (lo <=? x <=? hi)}) r := Z.gtb (projT1 l) r.
+Definition geb_range_l {lo hi} (l : {x & ArithFact (lo <=? x <=? hi)}) r := Z.geb (projT1 l) r.
+Definition ltb_range_r {lo hi} l (r : {x & ArithFact (lo <=? x <=? hi)}) := Z.ltb l (projT1 r).
+Definition leb_range_r {lo hi} l (r : {x & ArithFact (lo <=? x <=? hi)}) := Z.leb l (projT1 r).
+Definition gtb_range_r {lo hi} l (r : {x & ArithFact (lo <=? x <=? hi)}) := Z.gtb l (projT1 r).
+Definition geb_range_r {lo hi} l (r : {x & ArithFact (lo <=? x <=? hi)}) := Z.geb l (projT1 r).
 
 Definition ii := Z.
 Definition nn := nat.
@@ -149,11 +159,11 @@ Definition nn := nat.
 (*val pow : Z -> Z -> Z*)
 Definition pow m n := m ^ n.
 
-Program Definition pow2 n : {z : Z & ArithFact (2 ^ n <= z <= 2 ^ n)} := existT _ (pow 2 n) _.
+Program Definition pow2 n : {z : Z & ArithFact (2 ^ n <=? z <=? 2 ^ n)} := existT _ (pow 2 n) _.
 Next Obligation.
 constructor.
 unfold pow.
-auto using Z.le_refl.
+auto using Z.leb_refl with bool.
 Qed.
 
 Lemma ZEuclid_div_pos : forall x y, y > 0 -> x >= 0 -> ZEuclid.div x y >= 0.
@@ -206,6 +216,13 @@ Qed.
 
 Hint Resolve ZEuclid_div_pos ZEuclid_pos_div ZEuclid_div_ge ZEuclid_div_mod0 : sail.
 
+Lemma Z_geb_ge n m : (n >=? m) = true <-> n >= m.
+rewrite Z.geb_leb.
+split.
+* intro. apply Z.le_ge, Z.leb_le. assumption.
+* intro. apply Z.ge_le in H. apply Z.leb_le. assumption.
+Qed.
+
 
 (*
 Definition inline lt := (<)
@@ -817,19 +834,25 @@ apply Z2Nat.inj_lt.
 Close Scope nat.
 
 (*val access_list_inc : forall a. list a -> Z -> a*)
-Definition access_list_inc {A} (xs : list A) n `{ArithFact (0 <= n)} `{ArithFact (n < length_list xs)} := nth_in_range (Z.to_nat n) xs (nth_Z_nat (use_ArithFact _) (use_ArithFact _)).
+Definition access_list_inc {A} (xs : list A) n `{ArithFact (0 <=? n)} `{ArithFact (n <? length_list xs)} : A.
+refine (nth_in_range (Z.to_nat n) xs (nth_Z_nat _ _)).
+* apply Z.leb_le.
+  auto using use_ArithFact.
+* apply Z.ltb_lt.
+  auto using use_ArithFact.
+Defined.
 
 (*val access_list_dec : forall a. list a -> Z -> a*)
-Definition access_list_dec {A} (xs : list A) n `{ArithFact (0 <= n)} `{ArithFact (n < length_list xs)} : A.
+Definition access_list_dec {A} (xs : list A) n `{H1:ArithFact (0 <=? n)} `{H2:ArithFact (n <? length_list xs)} : A.
 refine (
   let top := (length_list xs) - 1 in
   @access_list_inc A xs (top - n) _ _).
-constructor. apply use_ArithFact in H. apply use_ArithFact in H0. omega.
-constructor. apply use_ArithFact in H. apply use_ArithFact in H0. omega.
+abstract (constructor; apply use_ArithFact, Z.leb_le in H1; apply use_ArithFact, Z.ltb_lt in H2; apply Z.leb_le; omega).
+abstract (constructor; apply use_ArithFact, Z.leb_le in H1; apply use_ArithFact, Z.ltb_lt in H2; apply Z.ltb_lt; omega).
 Defined.
 
 (*val access_list : forall a. bool -> list a -> Z -> a*)
-Definition access_list {A} (is_inc : bool) (xs : list A) n `{ArithFact (0 <= n)} `{ArithFact (n < length_list xs)} :=
+Definition access_list {A} (is_inc : bool) (xs : list A) n `{ArithFact (0 <=? n)} `{ArithFact (n <? length_list xs)} :=
   if is_inc then access_list_inc xs n else access_list_dec xs n.
 
 Definition access_list_opt_inc {A} (xs : list A) n := nth_error xs (Z.to_nat n).
@@ -886,15 +909,15 @@ match n with
 | Zpos _ => fun f w => f w
 end.
 
-Program Definition to_word {n} : n >= 0 -> word (Z.to_nat n) -> mword n :=
+Program Definition to_word {n} : n >=? 0 = true -> word (Z.to_nat n) -> mword n :=
   match n with
   | Zneg _ => fun H _ => _
   | Z0 => fun _ w => w
   | Zpos _ => fun _ w => w
   end.
 
-Definition word_to_mword {n} (w : word (Z.to_nat n)) `{H:ArithFact (n >= 0)} : mword n :=
-  to_word (match H with Build_ArithFact _ H' => H' end) w.
+Definition word_to_mword {n} (w : word (Z.to_nat n)) `{H:ArithFact (n >=? 0)} : mword n :=
+  to_word (use_ArithFact H) w.
 
 (*val length_mword : forall a. mword a -> Z*)
 Definition length_mword {n} (w : mword n) := n.
@@ -970,7 +993,7 @@ Definition update_mword {a} (is_inc : bool) (w : mword a) n b :=
   if is_inc then update_mword_inc w n b else update_mword_dec w n b.
 
 (*val int_of_mword : forall 'a. bool -> mword 'a -> integer*)
-Definition int_of_mword {a} `{ArithFact (a >= 0)} (sign : bool) (w : mword a) :=
+Definition int_of_mword {a} `{ArithFact (a >=? 0)} (sign : bool) (w : mword a) :=
   if sign then wordToZ (get_word w) else Z.of_N (wordToN (get_word w)).
 
 
@@ -979,16 +1002,18 @@ Definition mword_of_int len n :=
   let w := wordFromInteger n in
   if (length_mword w = len) then w else failwith "unexpected word length"
 *)
-Program Definition mword_of_int {len} `{H:ArithFact (len >= 0)} n : mword len :=
+Program Definition mword_of_int {len} `{H:ArithFact (len >=? 0)} n : mword len :=
 match len with
 | Zneg _ => _
 | Z0 => ZToWord 0 n
 | Zpos p => ZToWord (Pos.to_nat p) n
 end.
 Next Obligation.
-destruct H.
-auto.
+destruct H as [H].
+unfold Z.geb, Z.compare in H.
+discriminate.
 Defined.
+
 (*
 (* Translating between a type level number (itself n) and an integer *)
 
@@ -1057,7 +1082,7 @@ Instance bitlist_Bitvector {a : Type} `{BitU a} : (Bitvector (list a)) := {
 }.
 
 Class ReasonableSize (a : Z) : Prop := {
-  isPositive : a >= 0
+  isPositive : a >=? 0 = true
 }.
 
 (* Omega doesn't know about In, but can handle disjunctions. *)
@@ -1083,7 +1108,7 @@ repeat match goal with X := _ |- _ =>
   match goal with _ : context[X] |- _ => idtac end || clear X
 end.
 
-Lemma ArithFact_mword (a : Z) (w : mword a) : ArithFact (a >= 0).
+Lemma ArithFact_mword (a : Z) (w : mword a) : ArithFact (a >=? 0).
 constructor.
 destruct a.
 auto with zarith.
@@ -1091,9 +1116,16 @@ auto using Z.le_ge, Zle_0_pos.
 destruct w.
 Qed.
 Ltac unwrap_ArithFacts :=
-  repeat match goal with H:(ArithFact _) |- _ => let H' := fresh H in case H as [H']; clear H end.
+  repeat match goal with
+  | H:(ArithFact _) |- _ => let H' := fresh H in case H as [H']; clear H
+  | H:(ArithFactP _) |- _ => let H' := fresh H in case H as [H']; clear H
+  end.
 Ltac unbool_comparisons :=
   repeat match goal with
+  | H:?v = true |- _ => is_var v; subst v
+  | H:?v = false |- _ => is_var v; subst v
+  | H:true = ?v |- _ => is_var v; subst v
+  | H:false = ?v |- _ => is_var v; subst v
   | H:context [Z.geb _ _] |- _ => rewrite Z.geb_leb in H
   | H:context [Z.gtb _ _] |- _ => rewrite Z.gtb_ltb in H
   | H:context [Z.leb _ _ = true] |- _ => rewrite Z.leb_le in H
@@ -1108,6 +1140,8 @@ Ltac unbool_comparisons :=
   | 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 [Bool.eqb _ _ = true] |- _ => rewrite Bool.eqb_true_iff in H
+  | H:context [Bool.eqb _ _ = false] |- _ => rewrite Bool.eqb_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
@@ -1131,6 +1165,8 @@ Ltac unbool_comparisons_goal :=
   | |- context [andb _ _ = false] => setoid_rewrite Bool.andb_false_iff
   | |- context [negb _ = true] => setoid_rewrite Bool.negb_true_iff
   | |- context [negb _ = false] => setoid_rewrite Bool.negb_false_iff
+  | |- context [Bool.eqb _ _ = true] => setoid_rewrite Bool.eqb_true_iff
+  | |- context [Bool.eqb _ _ = false] => setoid_rewrite Bool.eqb_false_iff
   | |- context [generic_eq _ _ = true] => apply generic_eq_true
   | |- context [generic_eq _ _ = false] => apply generic_eq_false
   | |- context [generic_neq _ _ = true] => apply generic_neq_true
@@ -1361,10 +1397,16 @@ end;
 (* We may have uncovered more conjunctions *)
 repeat match goal with H:and _ _ |- _ => destruct H end.
 
+(* Remove details of embedded proofs and provide a copy that nothing
+   depends upon so that rewrites on it will work. *)
 Ltac generalize_embedded_proofs :=
+  let gen X :=
+    let Y := fresh "Y" in pose X as Y; generalize Y; generalize dependent X
+  in
   repeat match goal with H:context [?X] |- _ =>
-    match type of X with ArithFact _ =>
-      generalize dependent X
+    match type of X with
+    | ArithFact _ => gen X
+    | ArithFactP _ => gen X
     end
   end;
   intros.
@@ -1427,9 +1469,9 @@ Ltac prepare_for_solver :=
  subst;
  clean_up_props.
 
-Lemma trivial_range {x : Z} : ArithFact (x <= x /\ x <= x).
+Lemma trivial_range {x : Z} : ArithFact ((x <=? x <=? x)).
 constructor.
-auto with zarith.
+auto using Z.leb_refl with bool.
 Qed.
 
 Lemma ArithFact_self_proof {P} : forall x : {y : Z & ArithFact (P y)}, ArithFact (P (projT1 x)).
@@ -1437,14 +1479,19 @@ intros [x H].
 exact H.
 Qed.
 
+Lemma ArithFactP_self_proof {P} : forall x : {y : Z & ArithFactP (P y)}, ArithFactP (P (projT1 x)).
+intros [x H].
+exact H.
+Qed.
+
 Ltac fill_in_evar_eq :=
- match goal with |- ArithFact (?x = ?y) =>
+ match goal with |- ArithFact (?x =? ?y) =>
    (is_evar x || is_evar y);
    (* compute to allow projections to remove proofs that might not be allowed in the evar *)
 (* Disabled because cbn may reduce definitions, even after clearbody
    let x := eval cbn in x in
    let y := eval cbn in y in*)
-   idtac "Warning: unknown equality constraint"; constructor; exact (eq_refl _ : x = y) end.
+   idtac "Warning: unknown equality constraint"; constructor; exact (Z.eqb_refl _ : x =? y = true) end.
 
 Ltac bruteforce_bool_exists :=
 match goal with
@@ -1479,6 +1526,61 @@ repeat match goal with
   intros
 end;
 nia.
+(* Try to get the linear arithmetic solver to do booleans. *)
+
+Lemma b2z_true x : x = true <-> Z.b2z x = 1.
+destruct x; compute; split; congruence.
+Qed.
+
+Lemma b2z_false x : x = false <-> Z.b2z x = 0.
+destruct x; compute; split; congruence.
+Qed.
+
+Lemma b2z_tf x : 0 <= Z.b2z x <= 1.
+destruct x; simpl; omega.
+Qed.
+
+Lemma b2z_andb a b :
+  Z.b2z (a && b) = Z.min (Z.b2z a) (Z.b2z b).
+destruct a,b; reflexivity.
+Qed.
+Lemma b2z_orb a b :
+  Z.b2z (a || b) = Z.max (Z.b2z a) (Z.b2z b).
+destruct a,b; reflexivity.
+Qed.
+
+Lemma b2z_eq : forall a b, Z.b2z a = Z.b2z b <-> a = b.
+intros [|] [|];
+simpl;
+intuition try congruence.
+Qed.
+
+Ltac solve_bool_with_Z :=
+  subst;
+  rewrite ?truefalse, ?falsetrue, ?or_False_l, ?or_False_r in *;
+  (* I did try phrasing these as rewrites, but Coq was oddly reluctant to use them *)
+  repeat match goal with
+  | H:?x = ?x <-> _ |- _ => apply iff_equal_l in H
+  | H:_ <-> ?x = ?x |- _ => apply iff_equal_r in H
+  end;
+  repeat match goal with
+  |  H:context [?v = true] |- _  => is_var v; rewrite (b2z_true v) in *
+  | |- context [?v = true]       => is_var v; rewrite (b2z_true v) in *
+  |  H:context [?v = false] |- _ => is_var v; rewrite (b2z_false v) in *
+  | |- context [?v = false]      => is_var v; rewrite (b2z_false v) in *
+  | H:context [?v = ?w] |- _ => rewrite <- (b2z_eq v w) in H
+  | |- context [?v = ?w]     => rewrite <- (b2z_eq v w)
+  | H:context [Z.b2z (?v && ?w)] |- _ => rewrite (b2z_andb v w) in H
+  | |- context [Z.b2z (?v && ?w)]     => rewrite (b2z_andb v w)
+  | H:context [Z.b2z (?v || ?w)] |- _ => rewrite (b2z_orb v w) in H
+  | |- context [Z.b2z (?v || ?w)]     => rewrite (b2z_orb v w)
+  end;
+  repeat match goal with
+  | _:context [Z.b2z ?v] |- _ => generalize (b2z_tf v); generalize dependent (Z.b2z v)
+  | |- context [Z.b2z ?v]     => generalize (b2z_tf v); generalize dependent (Z.b2z v)
+  end;
+  intros;
+  lia.
 
 (* A more ambitious brute force existential solver. *)
 
@@ -1497,8 +1599,8 @@ Ltac guess_ex_solver :=
     guess_ex_solver*)
   | |- @ex bool _ => exists true; guess_ex_solver
   | |- @ex bool _ => exists false; guess_ex_solver
-  | x : Z |- @ex Z _ => exists x; guess_ex_solver
-  | _ => solve [tauto | eauto 3 with zarith sail | omega | intuition]
+  | x : ?ty |- @ex ?ty _ => exists x; guess_ex_solver
+  | _ => solve [tauto | eauto 3 with zarith sail | solve_bool_with_Z | omega | intuition]
   end.
 
 (* A straightforward solver for simple problems like
@@ -1657,40 +1759,6 @@ Ltac z_comparisons :=
   | exact Z_compare_gt_eq
   ].
 
-(* Try to get the linear arithmetic solver to do booleans. *)
-
-Lemma b2z_true x : x = true <-> Z.b2z x = 1.
-destruct x; compute; split; congruence.
-Qed.
-
-Lemma b2z_false x : x = false <-> Z.b2z x = 0.
-destruct x; compute; split; congruence.
-Qed.
-
-Lemma b2z_tf x : 0 <= Z.b2z x <= 1.
-destruct x; simpl; omega.
-Qed.
-
-Ltac solve_bool_with_Z :=
-  subst;
-  rewrite ?truefalse, ?falsetrue, ?or_False_l, ?or_False_r in *;
-  (* I did try phrasing these as rewrites, but Coq was oddly reluctant to use them *)
-  repeat match goal with
-  | H:?x = ?x <-> _ |- _ => apply iff_equal_l in H
-  | H:_ <-> ?x = ?x |- _ => apply iff_equal_r in H
-  end;
-  repeat match goal with
-  |  H:context [?v = true] |- _  => is_var v; rewrite (b2z_true v) in *
-  | |- context [?v = true]       => is_var v; rewrite (b2z_true v) in *
-  |  H:context [?v = false] |- _ => is_var v; rewrite (b2z_false v) in *
-  | |- context [?v = false]      => is_var v; rewrite (b2z_false v) in *
-  end;
-  repeat match goal with
-  | _:context [Z.b2z ?v] |- _ => generalize (b2z_tf v); generalize dependent (Z.b2z v)
-  | |- context [Z.b2z ?v]     => generalize (b2z_tf v); generalize dependent (Z.b2z v)
-  end;
-  intros;
-  lia.
 
 
 (* Redefine this to add extra solver tactics *)
@@ -1779,21 +1847,29 @@ Ltac simple_omega :=
   end; omega.
 
 Ltac solve_unknown :=
-  match goal with |- (ArithFact (?x ?y)) =>
+  match goal with
+  | |- (ArithFact (?x ?y)) =>
+    is_evar x;
+    idtac "Warning: unknown constraint";
+    let t := type of y in
+    unify x (fun (_ : t) => true);
+    exact (Build_ArithFactP _ eq_refl : ArithFact true)
+  | |- (ArithFactP (?x ?y)) =>
     is_evar x;
     idtac "Warning: unknown constraint";
     let t := type of y in
     unify x (fun (_ : t) => True);
-    exact (Build_ArithFact _ I)
+    exact (Build_ArithFactP _ I : ArithFactP True)
   end.
 
 Ltac run_main_solver_impl :=
 (* Attempt a simple proof first to avoid lengthy preparation steps (especially
    as the large proof terms can upset subsequent proofs). *)
-try (constructor; simple_omega);
+constructor;
+try simple_omega;
 prepare_for_solver;
 (*dump_context;*)
-constructor;
+unbool_comparisons_goal; (* Applying the ArithFact constructor will reveal an = true, so this might do more than it did in prepare_for_solver *)
 repeat match goal with |- and _ _ => split end;
 main_solver.
 
@@ -1819,14 +1895,17 @@ Ltac clear_fixpoints :=
 Ltac solve_arithfact :=
   intros; (* To solve implications for derive_m *)
   clear_fixpoints; (* Avoid using recursive calls *)
+  cbv beta; (* Goal might be eta-expanded *)
   solve
     [ solve_unknown
-    | match goal with |- ArithFact (?x <= ?x <= ?x) => exact trivial_range end
+    | assumption
+    | match goal with |- ArithFact ((?x <=? ?x <=? ?x)) => exact trivial_range end
     | fill_in_evar_eq
     | match goal with |- context [projT1 ?X] => apply (ArithFact_self_proof X) end
+    | match goal with |- context [projT1 ?X] => apply (ArithFactP_self_proof X) end
     (* Trying reflexivity will fill in more complex metavariable examples than
-       fill_in_evar_eq above, e.g., 8 * n = 8 * ?Goal3 *)
-    | constructor; reflexivity
+       fill_in_evar_eq above, e.g., 8 * n =? 8 * ?Goal3 *)
+    | constructor; unbool_comparisons_goal; reflexivity
     | constructor; repeat match goal with |- and _ _ => split end; z_comparisons
     | run_main_solver
     ].
@@ -1836,6 +1915,7 @@ Ltac solve_arithfact :=
 Ltac run_solver := solve_arithfact.
 
 Hint Extern 0 (ArithFact _) => run_solver : typeclass_instances.
+Hint Extern 0 (ArithFactP _) => run_solver : typeclass_instances.
 
 Hint Unfold length_mword : sail.
 
@@ -1855,13 +1935,11 @@ auto using Z.le_ge, Zle_0_pos.
 destruct w.
 Qed.
 
-Hint Extern 0 (ReasonableSize ?A) => (unwrap_ArithFacts; solve [apply ReasonableSize_witness; assumption | constructor; omega]) : typeclass_instances.
-
-Definition to_range (x : Z) : {y : Z & ArithFact (x <= y <= x)} := build_ex x.
-
+Hint Extern 0 (ReasonableSize ?A) => (unwrap_ArithFacts; solve [apply ReasonableSize_witness; assumption | constructor; auto with zarith]) : typeclass_instances.
 
+Definition to_range (x : Z) : {y : Z & ArithFact ((x <=? y <=? x))} := build_ex x.
 
-Instance mword_Bitvector {a : Z} `{ArithFact (a >= 0)} : (Bitvector (mword a)) := {
+Instance mword_Bitvector {a : Z} `{ArithFact (a >=? 0)} : (Bitvector (mword a)) := {
   bits_of v := List.map bitU_of_bool (bitlistFromWord (get_word v));
   of_bits v := option_map (fun bl => to_word isPositive (fit_bbv_word (wordFromBitlist bl))) (just_list (List.map bool_of_bitU v));
   of_bools v := to_word isPositive (fit_bbv_word (wordFromBitlist v));
@@ -2194,7 +2272,7 @@ Fixpoint foreach_Z' {Vars} from to step n (vars : Vars) (body : Z -> Vars -> Var
 Definition foreach_Z {Vars} from to step vars body :=
   foreach_Z' (Vars := Vars) from to step (S (Z.abs_nat (from - to))) vars body.
 
-Fixpoint foreach_Z_up' {Vars} from to step off n `{ArithFact (0 < step)} `{ArithFact (0 <= off)} (vars : Vars) (body : forall (z : Z) `(ArithFact (from <= z <= to)), Vars -> Vars) {struct n} : Vars :=
+Fixpoint foreach_Z_up' {Vars} (from to step off : Z) (n:nat) `{ArithFact (0 <? step)} `{ArithFact (0 <=? off)} (vars : Vars) (body : forall (z : Z) `(ArithFact ((from <=? z <=? to))), Vars -> Vars) {struct n} : Vars :=
   if sumbool_of_bool (from + off <=? to) then
     match n with
     | O => vars
@@ -2202,7 +2280,7 @@ Fixpoint foreach_Z_up' {Vars} from to step off n `{ArithFact (0 < step)} `{Arith
     end
   else vars.
 
-Fixpoint foreach_Z_down' {Vars} from to step off n `{ArithFact (0 < step)} `{ArithFact (off <= 0)} (vars : Vars) (body : forall (z : Z) `(ArithFact (to <= z <= from)), Vars -> Vars) {struct n} : Vars :=
+Fixpoint foreach_Z_down' {Vars} from to step off n `{ArithFact (0 <? step)} `{ArithFact (off <=? 0)} (vars : Vars) (body : forall (z : Z) `(ArithFact ((to <=? z <=? from))), Vars -> Vars) {struct n} : Vars :=
   if sumbool_of_bool (to <=? from + off) then
     match n with
     | O => vars
@@ -2210,9 +2288,9 @@ Fixpoint foreach_Z_down' {Vars} from to step off n `{ArithFact (0 < step)} `{Ari
     end
   else vars.
 
-Definition foreach_Z_up {Vars} from to step vars body `{ArithFact (0 < step)} :=
+Definition foreach_Z_up {Vars} from to step vars body `{ArithFact (0 <? step)} :=
     foreach_Z_up' (Vars := Vars) from to step 0 (S (Z.abs_nat (from - to))) vars body.
-Definition foreach_Z_down {Vars} from to step vars body `{ArithFact (0 < step)} :=
+Definition foreach_Z_down {Vars} from to step vars body `{ArithFact (0 <? step)} :=
     foreach_Z_down' (Vars := Vars) from to step 0 (S (Z.abs_nat (from - to))) vars body.
 
 (*val while : forall vars. vars -> (vars -> bool) -> (vars -> vars) -> vars
@@ -2305,27 +2383,27 @@ end
 (* Arithmetic functions which return proofs that match the expected Sail
    types in smt.sail. *)
 
-Definition ediv_with_eq n m : {o : Z & ArithFact (o = ZEuclid.div n m)} := build_ex (ZEuclid.div n m).
-Definition emod_with_eq n m : {o : Z & ArithFact (o = ZEuclid.modulo n m)} := build_ex (ZEuclid.modulo n m).
-Definition abs_with_eq n   : {o : Z & ArithFact (o = Z.abs n)} := build_ex (Z.abs n).
+Definition ediv_with_eq n m : {o : Z & ArithFact (o =? ZEuclid.div n m)} := build_ex (ZEuclid.div n m).
+Definition emod_with_eq n m : {o : Z & ArithFact (o =? ZEuclid.modulo n m)} := build_ex (ZEuclid.modulo n m).
+Definition abs_with_eq n   : {o : Z & ArithFact (o =? Z.abs n)} := build_ex (Z.abs n).
 
 (* Similarly, for ranges (currently in MIPS) *)
 
-Definition eq_range {n m o p} (l : {l & ArithFact (n <= l <= m)}) (r : {r & ArithFact (o <= r <= p)}) : bool :=
+Definition eq_range {n m o p} (l : {l & ArithFact (n <=? l <=? m)}) (r : {r & ArithFact (o <=? r <=? p)}) : bool :=
   (projT1 l) =? (projT1 r).
-Definition add_range {n m o p} (l : {l & ArithFact (n <= l <= m)}) (r : {r & ArithFact (o <= r <= p)})
-  : {x & ArithFact (n+o <= x <= m+p)} :=
+Definition add_range {n m o p} (l : {l & ArithFact (n <=? l <=? m)}) (r : {r & ArithFact (o <=? r <=? p)})
+  : {x & ArithFact (n+o <=? x <=? m+p)} :=
   build_ex ((projT1 l) + (projT1 r)).
-Definition sub_range {n m o p} (l : {l & ArithFact (n <= l <= m)}) (r : {r & ArithFact (o <= r <= p)})
-  : {x & ArithFact (n-p <= x <= m-o)} :=
+Definition sub_range {n m o p} (l : {l & ArithFact (n <=? l <=? m)}) (r : {r & ArithFact (o <=? r <=? p)})
+  : {x & ArithFact (n-p <=? x <=? m-o)} :=
   build_ex ((projT1 l) - (projT1 r)).
-Definition negate_range {n m} (l : {l : Z & ArithFact (n <= l <= m)})
-  : {x : Z & ArithFact ((- m) <= x <= (- n))} :=
+Definition negate_range {n m} (l : {l : Z & ArithFact (n <=? l <=? m)})
+  : {x : Z & ArithFact ((- m) <=? x <=? (- n))} :=
   build_ex (- (projT1 l)).
 
-Definition min_atom (a : Z) (b : Z) : {c : Z & ArithFact ((c = a \/ c = b) /\ c <= a /\ c <= b)} :=
+Definition min_atom (a : Z) (b : Z) : {c : Z & ArithFact (((c =? a) || (c =? b)) && (c <=? a) && (c <=? b))} :=
   build_ex (Z.min a b).
-Definition max_atom (a : Z) (b : Z) : {c : Z & ArithFact ((c = a \/ c = b) /\ c >= a /\ c >= b)} :=
+Definition max_atom (a : Z) (b : Z) : {c : Z & ArithFact (((c =? a) || (c =? b)) && (c >=? a) && (c >=? b))} :=
   build_ex (Z.max a b).
 
 
@@ -2333,15 +2411,18 @@ Definition max_atom (a : Z) (b : Z) : {c : Z & ArithFact ((c = a \/ c = b) /\ c
 
 Definition vec (T:Type) (n:Z) := { l : list T & length_list l = n }.
 Definition vec_length {T n} (v : vec T n) := n.
-Definition vec_access_dec {T n} (v : vec T n) m `{ArithFact (0 <= m < n)} : T :=
+Definition vec_access_dec {T n} (v : vec T n) m `{ArithFact ((0 <=? m <? n))} : T :=
   access_list_dec (projT1 v) m.
-Definition vec_access_inc {T n} (v : vec T n) m `{ArithFact (0 <= m < n)} : T :=
+
+Definition vec_access_inc {T n} (v : vec T n) m `{ArithFact (0 <=? m <? n)} : T :=
   access_list_inc (projT1 v) m.
 
-Program Definition vec_init {T} (t : T) (n : Z) `{ArithFact (n >= 0)} : vec T n :=
+Program Definition vec_init {T} (t : T) (n : Z) `{ArithFact (n >=? 0)} : vec T n :=
   existT _ (repeat [t] n) _.
 Next Obligation.
-rewrite repeat_length; auto using fact.
+intros.
+cbv beta.
+rewrite repeat_length. 2: apply Z_geb_ge, fact.
 unfold length_list.
 simpl.
 auto with zarith.
@@ -2389,21 +2470,25 @@ rewrite skipn_length;
 omega.
 Qed.
 
-Program Definition vec_update_dec {T n} (v : vec T n) m t `{ArithFact (0 <= m < n)} : vec T n := existT _ (update_list_dec (projT1 v) m t) _.
+Program Definition vec_update_dec {T n} (v : vec T n) m t `{ArithFact (0 <=? m <? n)} : vec T n := existT _ (update_list_dec (projT1 v) m t) _.
 Next Obligation.
+intros; cbv beta.
 unfold update_list_dec.
 rewrite update_list_inc_length.
 + destruct v. apply e.
-+ destruct H.
++ destruct H as [H].
+  unbool_comparisons.
   destruct v. simpl (projT1 _). rewrite e.
   omega.
 Qed.
 
-Program Definition vec_update_inc {T n} (v : vec T n) m t `{ArithFact (0 <= m < n)} : vec T n := existT _ (update_list_inc (projT1 v) m t) _.
+Program Definition vec_update_inc {T n} (v : vec T n) m t `{ArithFact (0 <=? m <? n)} : vec T n := existT _ (update_list_inc (projT1 v) m t) _.
 Next Obligation.
+intros; cbv beta.
 rewrite update_list_inc_length.
 + destruct v. apply e.
 + destruct H.
+  unbool_comparisons.
   destruct v. simpl (projT1 _). rewrite e.
   omega.
 Qed.
@@ -2423,6 +2508,7 @@ Program Definition just_vec {A n} (v : vec (option A) n) : option (vec A n) :=
   | Some v' => Some (existT _ v' _)
   end.
 Next Obligation.
+intros; cbv beta.
 rewrite <- (just_list_length_Z _ _ Heq_anonymous).
 destruct v.
 assumption.
@@ -2461,51 +2547,59 @@ match a with
 | None => None
 end.
 
-Definition sub_nat (x : Z) `{ArithFact (x >= 0)} (y : Z) `{ArithFact (y >= 0)} :
-  {z : Z & ArithFact (z >= 0)} :=
+Definition sub_nat (x : Z) `{ArithFact (x >=? 0)} (y : Z) `{ArithFact (y >=? 0)} :
+  {z : Z & ArithFact (z >=? 0)} :=
   let z := x - y in
   if sumbool_of_bool (z >=? 0) then build_ex z else build_ex 0.
 
-Definition min_nat (x : Z) `{ArithFact (x >= 0)} (y : Z) `{ArithFact (y >= 0)} :
-  {z : Z & ArithFact (z >= 0)} :=
+Definition min_nat (x : Z) `{ArithFact (x >=? 0)} (y : Z) `{ArithFact (y >=? 0)} :
+  {z : Z & ArithFact (z >=? 0)} :=
   build_ex (Z.min x y).
 
-Definition max_nat (x : Z) `{ArithFact (x >= 0)} (y : Z) `{ArithFact (y >= 0)} :
-  {z : Z & ArithFact (z >= 0)} :=
+Definition max_nat (x : Z) `{ArithFact (x >=? 0)} (y : Z) `{ArithFact (y >=? 0)} :
+  {z : Z & ArithFact (z >=? 0)} :=
   build_ex (Z.max x y).
 
-Definition shl_int_8 (x y : Z) `{HE:ArithFact (x = 8)} `{HR:ArithFact (0 <= y <= 3)}: {z : Z & ArithFact (In z [8;16;32;64])}.
+Definition shl_int_8 (x y : Z) `{HE:ArithFact (x =? 8)} `{HR:ArithFact (0 <=? y <=? 3)}: {z : Z & ArithFact (member_Z_list z [8;16;32;64])}.
 refine (existT _ (shl_int x y) _).
 destruct HE as [HE].
 destruct HR as [HR].
+unbool_comparisons.
 assert (H : y = 0 \/ y = 1 \/ y = 2 \/ y = 3) by omega.
 constructor.
 intuition (subst; compute; auto).
 Defined.
 
-Definition shl_int_32 (x y : Z) `{HE:ArithFact (x = 32)} `{HR:ArithFact (In y [0;1])}: {z : Z & ArithFact (In z [32;64])}.
+Definition shl_int_32 (x y : Z) `{HE:ArithFact (x =? 32)} `{HR:ArithFact (member_Z_list y [0;1])}: {z : Z & ArithFact (member_Z_list z [32;64])}.
 refine (existT _ (shl_int x y) _).
 destruct HE as [HE].
-destruct HR as [[HR1 | [HR2 | []]]];
+destruct HR as [HR].
+constructor.
+unbool_comparisons.
+apply member_Z_list_In in HR.
+destruct HR as [HR | [HR | []]];
 subst; compute;
-auto using Build_ArithFact.
+auto.
 Defined.
 
-Definition shr_int_32 (x y : Z) `{HE:ArithFact (0 <= x <= 31)} `{HR:ArithFact (y = 1)}: {z : Z & ArithFact (0 <= z <= 15)}.
+Definition shr_int_32 (x y : Z) `{HE:ArithFact (0 <=? x <=? 31)} `{HR:ArithFact (y =? 1)}: {z : Z & ArithFact (0 <=? z <=? 15)}.
 refine (existT _ (shr_int x y) _).
-destruct HE as [HE].
-destruct HR as [HR];
-subst.
-unfold shr_int.
-rewrite <- Z.div2_spec.
-constructor.
-rewrite Z.div2_div.
-specialize (Z.div_mod x 2).
-specialize (Z.mod_pos_bound x 2).
-generalize (Z.div x 2).
-generalize (x mod 2).
-intros.
-nia.
+abstract (
+  destruct HE as [HE];
+  destruct HR as [HR];
+  unbool_comparisons;
+  subst;
+  constructor;
+  unbool_comparisons_goal;
+  unfold shr_int;
+  rewrite <- Z.div2_spec;
+  rewrite Z.div2_div;
+  specialize (Z.div_mod x 2);
+  specialize (Z.mod_pos_bound x 2);
+  generalize (Z.div x 2);
+  generalize (x mod 2);
+  intros;
+  nia).
 Defined.
 
 Lemma shl_8_ge_0 {n} : shl_int 8 n >= 0.
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 3a37d9ff..8b147572 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -394,10 +394,12 @@ let doc_nc_fn_prop id =
   | _ -> doc_id_type id
 
 (* n_constraint functions are currently just Z3 functions *)
-let doc_nc_fn id =
-  match string_of_id id with
-  | "not" -> string "negb"
-  | s -> string s
+let doc_nc_fn (Id_aux (id,_) as full_id) =
+  match id with
+  | Id "not" -> string "negb"
+  | Operator "-->" -> string "implb"
+  | Id "iff" -> string "Bool.eqb"
+  | _ -> doc_id full_id
 
 let merge_kid_count = KBindings.union (fun _ m n -> Some (m+n))
 
@@ -622,7 +624,7 @@ let rec doc_typ_fns ctx env =
          | Bool_boring -> string "bool"
          | Bool_complex (_,_,atom_nc) -> (* simplify won't introduce new kopts *)
             let var = mk_kid "_bool" in (* TODO collision avoid *)
-            let nc = nice_iff (nc_var var) atom_nc in
+            let nc = nice_iff atom_nc (nc_var var) in
             braces (separate space
                       [doc_var ctx var; colon; string "bool";
                        ampersand;
@@ -676,7 +678,7 @@ let rec doc_typ_fns ctx env =
              let length_constraint_pp =
                if KidSet.is_empty (KidSet.inter kid_set (nexp_frees m))
                then None
-               else Some (separate space [len_pp; doc_var ctx var; equals; doc_nexp ctx m])
+               else Some (separate space [len_pp; doc_var ctx var; string "=?"; doc_nexp ctx m])
              in
              braces (separate space
                        [doc_var ctx var; colon; tpp;
@@ -694,7 +696,7 @@ let rec doc_typ_fns ctx env =
              let length_constraint_pp =
                if KidSet.is_empty (KidSet.inter kid_set (nexp_frees m))
                then None
-               else Some (separate space [len_pp; doc_var ctx var; equals; doc_nexp ctx m])
+               else Some (separate space [len_pp; doc_var ctx var; string "=?"; doc_nexp ctx m])
              in
              braces (separate space
                        [doc_var ctx var; colon; tpp;
@@ -705,7 +707,7 @@ let rec doc_typ_fns ctx env =
              | Bool_boring -> string "bool"
              | Bool_complex (kopts,nc,atom_nc) ->
                 let var = mk_kid "_bool" in (* TODO collision avoid *)
-                let nc = nice_and (nice_iff (nc_var var) atom_nc) nc in
+                let nc = nice_and (nice_iff atom_nc (nc_var var)) nc in
                 braces (separate space
                           [doc_var ctx var; colon; string "bool";
                            ampersand;
@@ -779,18 +781,17 @@ and doc_typ ctx env = let f,_,_ = doc_typ_fns ctx env in f
 and doc_atomic_typ ctx env = let _,f,_ = doc_typ_fns ctx env in f
 and doc_typ_arg ctx env = let _,_,f = doc_typ_fns ctx env in f
 
-and doc_arithfact ?(prop_vars=false) ctxt env ?(exists = []) ?extra nc =
-  let prop = doc_nc_prop ~prop_vars ctxt env nc in
+and doc_arithfact ctxt env ?(exists = []) ?extra nc =
+  let prop = doc_nc_exp ctxt env nc in
   let prop = match extra with
     | None -> prop
-    | Some pp -> separate space [pp; string "/\\"; parens prop]
-  in
-  let prop =
-    match exists with
-    | [] -> prop
-    | _ -> separate space ([string "exists"]@(List.map (doc_var ctxt) exists)@[comma; prop])
+    | Some pp -> separate space [parens pp; string "&&"; parens prop]
   in
-  string "ArithFact" ^^ space ^^ parens prop
+  let prop = prop in
+  match exists with
+  | [] -> string "ArithFact" ^^ space ^^ parens prop
+  | _ -> string "ArithFactP" ^^ space ^^
+           parens (separate space ([string "exists"]@(List.map (doc_var ctxt) exists)@[comma; prop; equals; string "true"]))
 
 (* Follows Coq precedence levels *)
 and doc_nc_prop ?(top = true) ?(prop_vars = false) ctx env nc =
@@ -860,7 +861,7 @@ and doc_nc_prop ?(top = true) ?(prop_vars = false) ctx env nc =
   in if top then newnc l85 nc else newnc l0 nc
 
 (* Follows Coq precedence levels *)
-let rec doc_nc_exp ctx env nc =
+and doc_nc_exp ctx env nc =
   let locals = Env.get_locals env |> Bindings.bindings in
   let nc = Env.expand_constraint_synonyms env nc in
   let nc_id_map =
@@ -871,6 +872,9 @@ let rec doc_nc_exp ctx env nc =
            (flatten_nc nc, v)::m
         | _ -> m) [] locals
   in
+  (* Look for variables in the environment which exactly express the nc, and use
+     them instead.  As well as often being shorter, this avoids unbound type
+     variables added by Sail's type checker. *)
   let rec newnc f nc =
     let ncs = flatten_nc nc in
     let candidates =
@@ -903,10 +907,16 @@ let rec doc_nc_exp ctx env nc =
        separate space [string "member_Z_list"; doc_var ctx kid;
                        brackets (separate (string "; ")
                                    (List.map (fun i -> string (Nat_big_num.to_string i)) is))]
+    | NC_app (f,args) -> separate space (doc_nc_fn f::List.map doc_typ_arg_exp args)
+    | _ -> l0 nc_full
+  and l0 (NC_aux (nc,_) as nc_full) =
+    match nc with
     | NC_true -> string "true"
     | NC_false -> string "false"
-    | NC_app (f,args) -> separate space (doc_nc_fn f::List.map (doc_typ_arg_exp ctx env) args)
     | NC_var kid -> doc_nexp ctx (nvar kid)
+    | NC_not_equal _
+    | NC_set _
+    | NC_app _
     | NC_equal _
     | NC_bounded_ge _
     | NC_bounded_gt _
@@ -914,13 +924,13 @@ let rec doc_nc_exp ctx env nc =
     | NC_bounded_lt _
     | NC_or _
     | NC_and _ -> parens (l70 nc_full)
-  in newnc l70 nc
-and doc_typ_arg_exp ctx env (A_aux (arg,l)) =
-  match arg with
-  | A_nexp nexp -> doc_nexp ctx nexp
-  | A_bool nc -> doc_nc_exp ctx env nc
-  | A_order _ | A_typ _ ->
+  and doc_typ_arg_exp (A_aux (arg,l)) =
+    match arg with
+    | A_nexp nexp -> doc_nexp ctx nexp
+    | A_bool nc -> newnc l0 nc
+    | A_order _ | A_typ _ ->
        raise (Reporting.err_unreachable l __POS__ "Tried to pass Type or Order kind to SMT function")
+  in newnc l70 nc
 
 (* Check for variables in types that would be pretty-printed and are not
    bound in the val spec of the function. *)
@@ -1024,7 +1034,7 @@ let doc_quant_item_constr ?(prop_vars=false) ctx env delimit (QI_aux (qi,_)) =
   match qi with
   | QI_id  _ -> None
   | QI_constant _ -> None
-  | QI_constraint nc -> Some (bquote ^^ braces (doc_arithfact ~prop_vars ctx env nc))
+  | QI_constraint nc -> Some (bquote ^^ braces (doc_arithfact ctx env nc))
 
 (* At the moment these are all anonymous - when used we rely on Coq to fill
    them in. *)
@@ -2515,9 +2525,9 @@ let doc_typdef generic_eq_types (TD_aux(td, (l, annot))) =
      let idpp = doc_id_type id in
      doc_op coloneq
        (separate space [string "Definition"; idpp;
-                        doc_typquant_items ~prop_vars:true empty_ctxt Env.empty parens typq;
-                        colon; string "Prop"])
-       (doc_nc_prop ~prop_vars:true empty_ctxt Env.empty nc) ^^ dot ^^ hardline ^^
+                        doc_typquant_items empty_ctxt Env.empty parens typq;
+                        colon; string "bool"])
+       (doc_nc_exp empty_ctxt Env.empty nc) ^^ dot ^^ hardline ^^
      separate space [string "Hint Unfold"; idpp; colon; string "sail."] ^^
      twice hardline
   | TD_abbrev _ -> empty (* TODO? *)
@@ -2743,7 +2753,7 @@ let rec atom_constraint ctxt (pat, typ) =
            None
      | _ ->
         Some (bquote ^^ braces (string "ArithFact" ^^ space ^^
-                                  parens (doc_op equals (doc_id id) (doc_nexp ctxt nexp)))))
+                                  parens (doc_op (string "=?") (doc_id id) (doc_nexp ctxt nexp)))))
   | P_aux (P_typ (_,p),_), _ -> atom_constraint ctxt (p, typ)
   | _ -> None
 
@@ -3205,7 +3215,7 @@ let doc_axiom_typschm typ_env l (tqs,typ) =
           let v = fresh_var () in
           parens (v ^^ string " : Z") ^/^
             bquote ^^ braces (string "ArithFact " ^^
-                                parens (v ^^ string " = " ^^ string (Big_int.to_string n)))
+                                parens (v ^^ string " =? " ^^ string (Big_int.to_string n)))
        | _ ->
           match Type_check.destruct_atom_bool typ_env typ with
           | Some (NC_aux (NC_var kid,_)) when KidSet.mem kid args ->
@@ -3377,6 +3387,7 @@ try
         hardline;
         string "Open Scope string."; hardline;
         string "Open Scope bool."; hardline;
+        string "Open Scope Z."; hardline;
         hardline;
         hardline;
         separate empty (List.map doc_def defs);