Update Coq snapshot

Also tweak Makefile to remove new Coq generated files

8 files changed, 114 insertions, 116 deletions

diff --git a/prover_snapshots/coq/lib/sail/Hoare.v b/prover_snapshots/coq/lib/sail/Hoare.v
index b883b7a..93033ae 100644
--- a/prover_snapshots/coq/lib/sail/Hoare.v
+++ b/prover_snapshots/coq/lib/sail/Hoare.v
@@ -1,6 +1,7 @@
 Require Import String ZArith Setoid Morphisms Equivalence.
 Require Import Sail.State_monad Sail.Prompt Sail.State Sail.State_monad_lemmas.
 Require Import Sail.State_lemmas.
+Require Import Lia.
 
 (*adhoc_overloading
   Monad_Syntax.bind State_monad.bindS*)
@@ -837,7 +838,7 @@ unfold untilST.
 apply PrePostE_use_pre. intros s0 Pre0.
 assert (measure vars >= 0) as Hlimit_0 by eauto. clear s0 Pre0.
 remember (measure vars) as limit eqn: Heqlimit in Hlimit_0 |- *.
-assert (measure vars <= limit) as Hlimit by omega. clear Heqlimit.
+assert (measure vars <= limit) as Hlimit by lia. clear Heqlimit.
 generalize (Sail.Prompt.Zwf_guarded limit).
 revert vars Hlimit.
 apply Wf_Z.natlike_ind with (x := limit).
@@ -857,10 +858,10 @@ apply Wf_Z.natlike_ind with (x := limit).
     intros ? [[? ?] ?]; auto.
   - apply PrePostE_I;
     intros ? ? ? [[Pre ?] ?] ?; exfalso;
-    specialize (Hmeasure _ _ Pre); omega.
+    specialize (Hmeasure _ _ Pre); lia.
 * intros limit' Hlimit' IH vars Hmeasure_limit [acc].
   simpl.
-  destruct (Z_ge_dec _ _); try omega.
+  destruct (Z_ge_dec _ _). 2: lia.
   eapply PrePostE_bindS; [ | apply Hbody].
   intros vars'.
   eapply PrePostE_bindS with (R := (fun c s' => (Inv Q vars' s' /\ (c = true -> Q vars' s')) /\ measure vars' < measure vars)).
@@ -875,14 +876,14 @@ apply Wf_Z.natlike_ind with (x := limit).
   - eapply PrePostE_strengthen_pre; try apply PrePostE_returnS.
     intros ? [[? ?] ?]; auto.
   - gen_reduces.
-    replace (Z.succ limit' - 1) with limit'; [ | omega].
+    replace (Z.succ limit' - 1) with limit'; [ | lia].
     intro acc'.
     apply PrePostE_use_pre. intros sx [[Pre _] Hreduces].
     apply Hmeasure in Pre.
     eapply PrePostE_strengthen_pre; [apply IH | ].
-    + omega.
+    + lia.
     + tauto.
-* omega.
+* lia.
 Qed.
 
 
diff --git a/prover_snapshots/coq/lib/sail/Makefile b/prover_snapshots/coq/lib/sail/Makefile
index 1b6435e..59f0e38 100644
--- a/prover_snapshots/coq/lib/sail/Makefile
+++ b/prover_snapshots/coq/lib/sail/Makefile
@@ -20,7 +20,7 @@ TARGETS=$(SRC:.v=.vo)
 
 all: $(TARGETS)
 clean:
-	rm -f -- $(TARGETS) $(TARGETS:.vo=.glob) $(TARGETS:%.vo=.%.aux) deps
+	rm -f -- $(TARGETS) $(TARGETS:.vo=.glob) $(TARGETS:.vo=.vos) $(TARGETS:.vo=.vok) $(TARGETS:%.vo=.%.aux) deps
 
 $(TARGETS): %.vo: %.v
 	coqc $(COQ_LIBS) $<
diff --git a/prover_snapshots/coq/lib/sail/Operators_mwords.v b/prover_snapshots/coq/lib/sail/Operators_mwords.v
index ccb3b1d..bfbf654 100644
--- a/prover_snapshots/coq/lib/sail/Operators_mwords.v
+++ b/prover_snapshots/coq/lib/sail/Operators_mwords.v
@@ -6,7 +6,7 @@ Require Import bbv.Word.
 Require bbv.BinNotation.
 Require Import Arith.
 Require Import ZArith.
-Require Import Omega.
+Require Import Lia.
 Require Import Eqdep_dec.
 Local Open Scope Z.
 
@@ -106,14 +106,14 @@ intros.
 unwrap_ArithFacts.
 unbool_comparisons.
 split.
-+ apply Z2Nat.inj_le; omega.
-+ apply Z2Nat.inj_lt; omega.
++ apply Z2Nat.inj_le; lia.
++ apply Z2Nat.inj_lt; lia.
 Qed.
 Lemma subrange_lemma1 {n m o} : (o <= m < n -> n = m + 1 + (n - (m + 1)))%nat.
-intros. omega.
+intros. lia.
 Qed.
 Lemma subrange_lemma2 {n m o} : (o <= m < n -> m+1 = o+(m-o+1))%nat.
-omega.
+lia.
 Qed.
 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.
@@ -121,9 +121,8 @@ unwrap_ArithFacts.
 unbool_comparisons.
 rewrite Nat2Z.inj_add.
 rewrite Nat2Z.inj_sub.
-repeat rewrite Z2Nat.id; try omega.
-reflexivity.
-apply Z2Nat.inj_le; omega.
+repeat rewrite Z2Nat.id; lia.
+apply Z2Nat.inj_le; lia.
 Qed.
 
 Definition subrange_vec_dec {n} (v : mword n) m o `{ArithFact (0 <=? o)} `{ArithFact (o <=? m <? n)} : mword (m - o + 1) :=
@@ -159,10 +158,10 @@ rewrite <- subrange_lemma3.
 rewrite !Nat2Z.inj_add.
 rewrite !Nat2Z.inj_sub.
 rewrite Nat2Z.inj_add.
-repeat rewrite Z2Nat.id; try omega.
+repeat rewrite Z2Nat.id; lia.
 rewrite Nat.add_1_r.
-apply Z2Nat.inj_lt; omega.
-apply Z2Nat.inj_le; omega.
+apply Z2Nat.inj_lt; lia.
+apply Z2Nat.inj_le; lia.
 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.
@@ -186,8 +185,8 @@ 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).
 
 Lemma mword_nonneg {a} : mword a -> a >= 0.
-destruct a;
-auto using Z.le_ge, Zle_0_pos with zarith.
+destruct a.
+1,2: auto using Z.le_ge, Zle_0_pos with zarith.
 destruct 1.
 Qed.
 
@@ -197,7 +196,7 @@ 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 <- Z2Nat.inj_add; [ | lia | lia ].
 rewrite Zplus_minus.
 apply Z2Nat.id.
 auto with zarith.
@@ -209,7 +208,7 @@ 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 <- Z2Nat.inj_add; [ | lia | lia ].
 rewrite Zplus_minus.
 apply Z2Nat.id.
 auto with zarith.
@@ -230,32 +229,32 @@ Defined.
 Lemma truncate_eq {m n} : m >= 0 -> m <= n -> (Z.to_nat n = Z.to_nat m + (Z.to_nat n - Z.to_nat m))%nat.
 intros.
 assert ((Z.to_nat m <= Z.to_nat n)%nat).
-{ apply Z2Nat.inj_le; omega. }
-omega.
+{ apply Z2Nat.inj_le; lia. }
+lia.
 Qed.
 Lemma truncateLSB_eq {m n} : m >= 0 -> m <= n -> (Z.to_nat n = (Z.to_nat n - Z.to_nat m) + Z.to_nat m)%nat.
 intros.
 assert ((Z.to_nat m <= Z.to_nat n)%nat).
-{ apply Z2Nat.inj_le; omega. }
-omega.
+{ apply Z2Nat.inj_le; lia. }
+lia.
 Qed.
 
 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).
+abstract (unwrap_ArithFacts; unbool_comparisons; apply Z2Nat.id; lia).
 Defined.
 
 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).
+abstract (unwrap_ArithFacts; unbool_comparisons; apply Z2Nat.id; lia).
 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.
 rewrite Nat2Z.inj_add.
-rewrite Z2Nat.id; auto with zarith.
+rewrite Z2Nat.id. 2: solve [ auto with zarith ].
 rewrite Z2Nat.id; auto with zarith.
 Qed.
 
@@ -303,9 +302,9 @@ constructor.
   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.
-      destruct a; auto with zarith. destruct x.
-    * apply N.le_trans with (m := (2^0)%N); auto using N.le_refl.
+      rewrite Z2N.id. solve [ auto ].
+      destruct a. 1,2: auto with zarith. destruct x.
+    * apply N.le_trans with (m := (2^0)%N). solve [ auto using N.le_refl ].
       apply N.pow_le_mono_r.
       inversion 1.
       apply N.le_0_l.
@@ -346,8 +345,8 @@ rewrite eq.
 rewrite Nat2Z.id.
 intro w.
 destruct (Word.wordToZ_size' w) as [LO HI].
-replace 1 with (Z.of_nat 1); auto.
-rewrite <- Nat2Z.inj_sub; auto with arith.
+replace 1 with (Z.of_nat 1). 2: solve [ auto ].
+rewrite <- Nat2Z.inj_sub. 2: solve [ auto with arith ].
 simpl.
 rewrite <- minus_n_O.
 rewrite Zpow_pow2.
@@ -489,8 +488,8 @@ end.
 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. unbool_comparisons.
-rewrite <- Z2Nat.id; auto with zarith.
-rewrite Z2Nat.inj_mul; auto with zarith.
+rewrite <- Z2Nat.id. 2: solve [ auto with zarith ].
+rewrite Z2Nat.inj_mul. 2,3: solve [ auto with zarith ].
 rewrite Nat.mul_comm. reflexivity.
 Qed.
 Definition replicate_bits {a} (w : mword a) (n : Z) `{ArithFact (n >=? 0)} : mword (a * n) :=
@@ -529,7 +528,7 @@ destruct n.
   compute. intuition.
 * simpl in *. destruct (weq v w).
   + subst. rewrite weqb_eq; tauto.
-  + rewrite weqb_ne; auto. intuition.
+  + rewrite weqb_ne; auto. split; congruence.
 * destruct v.
 Qed.
 
@@ -567,7 +566,7 @@ Program Fixpoint reverse_endianness_word {n} (bits : word n) : word n :=
   | _ => bits
   end.
 Next Obligation.
-omega.
+lia.
 Qed.
 
 Definition reverse_endianness {n} (bits : mword n) := with_word (P := id) reverse_endianness_word bits.
@@ -604,11 +603,11 @@ unfold slice.
 destruct (sumbool_of_bool _).
 * exfalso.
   unbool_comparisons.
-  omega.
+  lia.
 * destruct (sumbool_of_bool _).
   + exfalso.
     unbool_comparisons.  
-    omega.
+    lia.
   + repeat replace_ArithFact_proof.
     reflexivity.
 Qed.
diff --git a/prover_snapshots/coq/lib/sail/Prompt.v b/prover_snapshots/coq/lib/sail/Prompt.v
index 718b2f4..6167f5b 100644
--- a/prover_snapshots/coq/lib/sail/Prompt.v
+++ b/prover_snapshots/coq/lib/sail/Prompt.v
@@ -1,6 +1,7 @@
 Require Import Sail.Values.
 Require Import Sail.Prompt_monad.
 Require Export ZArith.Zwf.
+Require Import Lia.
 Require Import List.
 Import ListNotations.
 Local Open Scope Z.
@@ -169,7 +170,7 @@ refine (Acc_inv _acc _).
 destruct H.
 unbool_comparisons.
 red.
-omega.
+lia.
 Defined.
 
 (* A version of well-foundedness of measures with a guard to ensure that
diff --git a/prover_snapshots/coq/lib/sail/Real.v b/prover_snapshots/coq/lib/sail/Real.v
index a2da0e7..34b2a12 100644
--- a/prover_snapshots/coq/lib/sail/Real.v
+++ b/prover_snapshots/coq/lib/sail/Real.v
@@ -2,6 +2,7 @@ Require Export Rbase.
 Require Import Reals.
 Require Export ROrderedType.
 Require Import Sail.Values.
+Require Import Lia.
 Local Open Scope Z.
 
 (* "Decidable" in a classical sense... *)
@@ -53,7 +54,7 @@ apply IZR_le.
 apply Z.mul_div_le.
 assumption.
 discrR.
-omega.
+lia.
 Qed.
 
 (* One annoying use of reals in the ARM spec I've been looking at. *)
@@ -80,13 +81,13 @@ assert (diveq : n*((m+n-1)/n) = (m+n-1) - (m+n-1) mod n).
 apply Zplus_minus_eq.
 rewrite (Z.add_comm ((m+n-1) mod n)).
 apply Z.div_mod.
-omega.
+lia.
 rewrite diveq.
 assert (modmax : (m+n-1) mod n < n).
 specialize (Z.mod_pos_bound (m+n-1) n). intuition.
-omega.
+lia.
 
-discrR; omega.
+discrR; lia.
 
 rewrite <- Z.opp_sub_distr.
 rewrite Ropp_Ropp_IZR.
@@ -96,7 +97,7 @@ auto using IZR_lt.
 unfold Rdiv.
 rewrite <- Rmult_assoc.
 rewrite Rinv_r_simpl_m.
-2: { discrR. omega. }
+2: { discrR. lia. }
 rewrite <- mult_IZR.
 apply IZR_lt.
 rewrite Z.mul_sub_distr_l.
@@ -104,5 +105,5 @@ apply Z.le_lt_trans with (m := m+n-1-n*1).
 apply Z.sub_le_mono_r.
 apply Z.mul_div_le.
 assumption.
-omega.
+lia.
 Qed.
diff --git a/prover_snapshots/coq/lib/sail/State_lemmas.v b/prover_snapshots/coq/lib/sail/State_lemmas.v
index 6a620f2..9f419b4 100644
--- a/prover_snapshots/coq/lib/sail/State_lemmas.v
+++ b/prover_snapshots/coq/lib/sail/State_lemmas.v
@@ -1,5 +1,6 @@
 Require Import Sail.Values Sail.Prompt_monad Sail.Prompt Sail.State_monad Sail.State Sail.State Sail.State_lifting.
 Require Import Sail.State_monad_lemmas.
+Require Import Lia.
 
 Local Open Scope equiv_scope.
 Local Open Scope Z.
@@ -88,18 +89,19 @@ destruct (Z.le_decidable 0 limit).
     reflexivity.
   + clear limit H.
     intros limit H IH [acc] vars s. simpl.
-    destruct (Z_ge_dec _ _); try omega.
+    destruct (Z_ge_dec _ _). 2: lia.
     apply bindS_cong; auto.
     intros [|]; auto.
     apply bindS_cong; auto.
     intros.
     gen_reduces.
-    replace (Z.succ limit - 1) with limit; try omega. intro acc'.
+    replace (Z.succ limit - 1) with limit. 2: lia. intro acc'.
     apply IH.
   + assumption.
 * intros. simpl.
-  destruct (Z_ge_dec _ _); try omega.
-  reflexivity.
+  destruct (Z_ge_dec _ _).
+  + lia.
+  + reflexivity.
 Qed.
 
 Lemma untilST_cong RV Vars E measure vars cond cond' (body body' : Vars -> monadS RV Vars E) :
@@ -121,17 +123,18 @@ destruct (Z.le_decidable 0 limit).
     reflexivity.
   + clear limit H.
     intros limit H IH [acc] vars s. simpl.
-    destruct (Z_ge_dec _ _); try omega.
+    destruct (Z_ge_dec _ _). 2: lia.
     apply bindS_cong; auto.
     intros. apply bindS_cong; auto.
     intros [|]; auto.
     gen_reduces.
-    replace (Z.succ limit - 1) with limit; try omega. intro acc'.
+    replace (Z.succ limit - 1) with limit. 2: lia. intro acc'.
     apply IH.
   + assumption.
 * intros. simpl.
-  destruct (Z_ge_dec _ _); try omega.
-  reflexivity.
+  destruct (Z_ge_dec _ _).
+  + lia.
+  + reflexivity.
 Qed.
 
 Lemma genlistS_cong {A RV E} f f' n :
@@ -966,19 +969,20 @@ destruct (Z.le_decidable 0 limit).
     reflexivity.
   + clear limit H.
     intros limit H IH [acc1] [acc2] vars s. simpl.
-    destruct (Z_ge_dec _ _); try omega.
+    destruct (Z_ge_dec _ _). 2: lia.
     rewrite_liftState.
     apply bindS_cong; auto.
     intros [|]; auto.
     apply bindS_cong; auto.
     intros.
     repeat gen_reduces.
-    replace (Z.succ limit - 1) with limit; try omega. intros acc1' acc2'.
+    replace (Z.succ limit - 1) with limit. 2: lia. intros acc1' acc2'.
     apply IH.
   + assumption.
 * intros. simpl.
-  destruct (Z_ge_dec _ _); try omega.
-  reflexivity.
+  destruct (Z_ge_dec _ _).
+  + lia.
+  + reflexivity.
 Qed.
 Hint Resolve liftState_whileM : liftState.
 
@@ -1039,18 +1043,19 @@ destruct (Z.le_decidable 0 limit).
     reflexivity.
   + clear limit H.
     intros limit H IH [acc1] [acc2] vars s. simpl.
-    destruct (Z_ge_dec _ _); try omega.
+    destruct (Z_ge_dec _ _). 2: lia.
     rewrite_liftState.
     apply bindS_cong; auto.
     intros. apply bindS_cong; auto.
     intros [|]; auto.
     repeat gen_reduces.
-    replace (Z.succ limit - 1) with limit; try omega. intros acc1' acc2'.
+    replace (Z.succ limit - 1) with limit. 2: lia. intros acc1' acc2'.
     apply IH.
   + assumption.
 * intros. simpl.
-  destruct (Z_ge_dec _ _); try omega.
-  reflexivity.
+  destruct (Z_ge_dec _ _).
+  + lia.
+  + reflexivity.
 Qed.
 Hint Resolve liftState_untilM : liftState.
 
diff --git a/prover_snapshots/coq/lib/sail/Values.v b/prover_snapshots/coq/lib/sail/Values.v
index 2cab87f..e6fb212 100644
--- a/prover_snapshots/coq/lib/sail/Values.v
+++ b/prover_snapshots/coq/lib/sail/Values.v
@@ -213,7 +213,8 @@ Lemma ZEuclid_div_pos : forall x y, 0 < y -> 0 <= x -> 0 <= ZEuclid.div x y.
 intros.
 unfold ZEuclid.div.
 change 0 with (0 * 0).
-apply Zmult_le_compat; auto with zarith.
+apply Zmult_le_compat.
+3,4: auto with zarith.
 * apply Z.sgn_nonneg. auto with zarith.
 * apply Z_div_pos; auto. apply Z.lt_gt. apply Z.abs_pos. auto with zarith.
 Qed.
@@ -231,19 +232,14 @@ Qed.
 Lemma ZEuclid_div_ge : forall x y, y > 0 -> x >= 0 -> x - ZEuclid.div x y >= 0.
 intros.
 unfold ZEuclid.div.
-rewrite Z.sgn_pos; auto with zarith.
+rewrite Z.sgn_pos. 2: solve [ auto with zarith ].
 rewrite Z.mul_1_l.
 apply Z.le_ge.
 apply Zle_minus_le_0.
 apply Z.div_le_upper_bound.
 * apply Z.abs_pos. auto with zarith.
 * rewrite Z.mul_comm.
-  assert (0 < Z.abs y). {
-    apply Z.abs_pos.
-    omega.
-  }
-  revert H1.
-  generalize (Z.abs y). intros. nia.
+  nia.
 Qed.
 
 Lemma ZEuclid_div_mod0 : forall x y, y <> 0 ->
@@ -841,7 +837,7 @@ refine
   end).
 exfalso. inversion H.
 exfalso. inversion H.
-simpl in H. omega.
+simpl in H. lia.
 Defined.
 
 Lemma nth_in_range_is_nth : forall A n (l : list A) d (H : n < length l),
@@ -863,17 +859,6 @@ rewrite Nat2Z.id in bounded.
 assumption.
 Qed.
 
-(*
-Lemma nth_top_aux {A} {n} {xs : list A} : Z.to_nat n < length xs -> let top := ((length_list xs) - 1)%Z in Z.to_nat (top - n)%Z < length xs.
-unfold length_list.
-generalize (length xs).
-intro n0.
-rewrite <- (Nat2Z.id n0).
-intro H.
-apply Z2Nat.inj_lt.
-* omega. 
-*)
-
 Close Scope nat.
 
 (*val access_list_inc : forall a. list a -> Z -> a*)
@@ -890,8 +875,8 @@ Definition access_list_dec {A} (xs : list A) n `{H1:ArithFact (0 <=? n)} `{H2:Ar
 refine (
   let top := (length_list xs) - 1 in
   @access_list_inc A xs (top - n) _ _).
-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).
+abstract (constructor; apply use_ArithFact, Z.leb_le in H1; apply use_ArithFact, Z.ltb_lt in H2; apply Z.leb_le; lia).
+abstract (constructor; apply use_ArithFact, Z.leb_le in H1; apply use_ArithFact, Z.ltb_lt in H2; apply Z.ltb_lt; lia).
 Defined.
 
 (*val access_list : forall a. bool -> list a -> Z -> a*)
@@ -1152,9 +1137,9 @@ Qed.
 Lemma ArithFact_mword (a : Z) (w : mword a) : ArithFact (a >=? 0).
 constructor.
 destruct a.
-auto with zarith.
-auto using Z.le_ge, Zle_0_pos.
-destruct w.
+* auto with zarith.
+* auto using Z.le_ge, Zle_0_pos.
+* destruct w.
 Qed.
 (* Remove constructor from ArithFact(P)s and if they're used elsewhere
    in the context create a copy that rewrites will work on. *)
@@ -1514,10 +1499,6 @@ Ltac clean_up_props :=
   | H1:?P, H2:?R <-> ?Q |- _ => constr_eq P Q; apply (iff_known_r H1) in H2
   | H:context[_ \/ False] |- _ => rewrite or_False_r in H
   | H:context[False \/ _] |- _ => rewrite or_False_l in H
- (* omega doesn't cope well with extra "True"s in the goal.
-    Check that they actually appear because setoid_rewrite can fill in evars. *)
-  | |- context[True /\ _] => setoid_rewrite True_left
-  | |- context[_ /\ True] => setoid_rewrite True_right
   end;
   remove_unnecessary_casesplit.
 
@@ -1526,7 +1507,7 @@ Ltac prepare_for_solver :=
  generalize_embedded_proofs;
  clear_irrelevant_defns;
  clear_non_Z_bool_defns;
- autounfold with sail in * |- *; (* You can add Hint Unfold ... : sail to let omega see through fns *)
+ autounfold with sail in * |- *; (* You can add Hint Unfold ... : sail to let lia see through fns *)
  split_cases;
  extract_properties;
  repeat match goal with w:mword ?n |- _ => apply ArithFact_mword in w end;
@@ -1612,7 +1593,7 @@ destruct x; compute; split; congruence.
 Qed.
 
 Lemma b2z_tf x : 0 <= Z.b2z x <= 1.
-destruct x; simpl; omega.
+destruct x; simpl; lia.
 Qed.
 
 Lemma b2z_andb a b :
@@ -1685,7 +1666,7 @@ Ltac guess_ex_solver :=
   | |- @ex bool _ => exists true; guess_ex_solver
   | |- @ex bool _ => exists false; guess_ex_solver
   | x : ?ty |- @ex ?ty _ => exists x; guess_ex_solver
-  | _ => solve [tauto | eauto 3 with zarith sail | solve_bool_with_Z | omega]
+  | _ => solve [tauto | eauto 3 with zarith sail | solve_bool_with_Z | lia]
   end.
 
 (* A straightforward solver for simple problems like
@@ -1814,7 +1795,7 @@ Ltac ex_iff_solve :=
   match goal with
   | |- @ex _ _ => eexists; ex_iff_solve
   (* Range constraints are attached to the right *)
-  | |- _ /\ _ => split; [ex_iff_solve | omega]
+  | |- _ /\ _ => split; [ex_iff_solve | lia]
   | |- _ <-> _ => conjuncts_iff_solve || (symmetry; conjuncts_iff_solve)
   end.
 
@@ -1896,7 +1877,7 @@ in
    remaining evar with left over.  TODO: apply to goals without an evar clause *)
 match goal with
   | |- @ex _ _ => eexists; clause_matching_bool_solver
-  | |- _ = _ /\ _ <= _ <= _ => split; [clause_matching_bool_solver | omega]
+  | |- _ = _ /\ _ <= _ <= _ => split; [clause_matching_bool_solver | lia]
   | |- ?l = ?r =>
   let rec clause l r :=
       match l with
@@ -1920,7 +1901,7 @@ Ltac main_solver :=
  solve
  [ apply ArithFact_mword; assumption
  | z_comparisons
- | omega with Z
+ | lia
    (* Try sail hints before dropping the existential *)
  | subst; eauto 3 with zarith sail
    (* The datatypes hints give us some list handling, esp In *)
@@ -1998,7 +1979,7 @@ Ltac main_solver :=
 Ltac simple_omega :=
   repeat match goal with
   H := projT1 _ |- _ => clearbody H
-  end; omega.
+  end; lia.
 
 Ltac solve_unknown :=
   match goal with
@@ -2205,9 +2186,9 @@ Hint Unfold neq_atom : sail.
 Lemma ReasonableSize_witness (a : Z) (w : mword a) : ReasonableSize a.
 constructor.
 destruct a.
-auto with zarith.
-auto using Z.le_ge, Zle_0_pos.
-destruct w.
+* auto with zarith.
+* auto using Z.le_ge, Zle_0_pos.
+* destruct w.
 Qed.
 
 Hint Extern 0 (ReasonableSize ?A) => (unwrap_ArithFacts; solve [apply ReasonableSize_witness; assumption | constructor; auto with zarith]) : typeclass_instances.
@@ -2547,21 +2528,30 @@ 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 : Z) (n:nat) `{ArithFact (0 <? step)} `{ArithFact (0 <=? off)} (vars : Vars) (body : forall (z : Z) `(ArithFact ((from <=? z <=? to))), Vars -> Vars) {struct n} : Vars :=
+(* Define these in proof mode to avoid anomalies related to abstract.
+   (See https://github.com/coq/coq/issues/10959) *)
+
+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.
+refine (
   if sumbool_of_bool (from + off <=? to) then
     match n with
     | O => vars
-    | S n => let vars := body (from + off) _ vars in foreach_Z_up' from to step (off + step) n vars body
+    | S n => let vars := body (from + off) _ vars in foreach_Z_up' _ from to step (off + step) n _ _ vars body
     end
-  else vars.
+  else vars
+).
+Defined.
 
-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:nat) `{ArithFact (0 <? step)} `{ArithFact (off <=? 0)} (vars : Vars) (body : forall (z : Z) `(ArithFact ((to <=? z <=? from))), Vars -> Vars) {struct n} : Vars.
+refine (
   if sumbool_of_bool (to <=? from + off) then
     match n with
     | O => vars
-    | S n => let vars := body (from + off) _ vars in foreach_Z_down' from to step (off - step) n vars body
+    | S n => let vars := body (from + off) _ vars in foreach_Z_down' _ from to step (off - step) n _ _ vars body
     end
-  else vars.
+  else vars
+).
+Defined.
 
 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.
@@ -2739,10 +2729,10 @@ assert ((0 <= Z.to_nat m < Datatypes.length l)%nat).
     apply Z2Nat.inj_lt; auto with zarith.
 }
 rewrite app_length.
-rewrite firstn_length_le; only 2:omega.
+rewrite firstn_length_le; only 2:lia.
 cbn -[skipn].
 rewrite skipn_length;
-omega.
+lia.
 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) _.
@@ -2754,7 +2744,7 @@ rewrite update_list_inc_length.
 + destruct H as [H].
   unbool_comparisons.
   destruct v. simpl (projT1 _). rewrite e.
-  omega.
+  lia.
 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) _.
@@ -2765,7 +2755,7 @@ rewrite update_list_inc_length.
 + destruct H.
   unbool_comparisons.
   destruct v. simpl (projT1 _). rewrite e.
-  omega.
+  auto.
 Qed.
 
 Program Definition vec_map {S T} (f : S -> T) {n} (v : vec S n) : vec T n := existT _ (List.map f (projT1 v)) _.
@@ -2840,7 +2830,7 @@ refine (existT _ (shl_int x y) _).
 destruct HE as [HE].
 destruct HR as [HR].
 unbool_comparisons.
-assert (y = 0 \/ y = 1 \/ y = 2 \/ y = 3) by omega.
+assert (y = 0 \/ y = 1 \/ y = 2 \/ y = 3) by lia.
 constructor.
 intuition (subst; compute; auto).
 Defined.
@@ -2850,7 +2840,7 @@ refine (existT _ (shl_int x y) _).
 destruct HE as [HE].
 destruct HR as [HR].
 unbool_comparisons.
-assert (y = 0 \/ y = 1 \/ y = 2 \/ y = 3) by omega.
+assert (y = 0 \/ y = 1 \/ y = 2 \/ y = 3) by lia.
 constructor.
 intuition (subst; compute; auto).
 Defined.
@@ -2890,7 +2880,7 @@ Lemma shl_8_ge_0 {n} : shl_int 8 n >= 0.
 unfold shl_int.
 apply Z.le_ge.  
 apply <- Z.shiftl_nonneg.
-omega.
+lia.
 Qed.
 Hint Resolve shl_8_ge_0 : sail.
 
@@ -2899,6 +2889,6 @@ Hint Resolve shl_8_ge_0 : sail.
 
 Lemma sail_lt_ge (x y : Z) :
   x < y <-> y >= x +1.
-omega.
+lia.
 Qed.
 Hint Resolve sail_lt_ge : sail.
diff --git a/prover_snapshots/coq/lib/sail/_CoqProject b/prover_snapshots/coq/lib/sail/_CoqProject
index bef6a4d..fbefc69 100644
--- a/prover_snapshots/coq/lib/sail/_CoqProject
+++ b/prover_snapshots/coq/lib/sail/_CoqProject
@@ -1 +1,2 @@
 -Q . Sail
+-Q ../../../bbv/theories bbv