summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/coq/Hoare.v13
-rw-r--r--lib/coq/Operators_mwords.v43
-rw-r--r--lib/coq/Prompt.v3
-rw-r--r--lib/coq/Real.v13
-rw-r--r--lib/coq/State_lemmas.v37
-rw-r--r--lib/coq/Values.v6
6 files changed, 59 insertions, 56 deletions
diff --git a/lib/coq/Hoare.v b/lib/coq/Hoare.v
index b883b7a7..93033ae9 100644
--- a/lib/coq/Hoare.v
+++ b/lib/coq/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/lib/coq/Operators_mwords.v b/lib/coq/Operators_mwords.v
index 337706fa..9b38c95c 100644
--- a/lib/coq/Operators_mwords.v
+++ b/lib/coq/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.
@@ -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,26 +229,26 @@ 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.
@@ -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/lib/coq/Prompt.v b/lib/coq/Prompt.v
index 718b2f47..6167f5b7 100644
--- a/lib/coq/Prompt.v
+++ b/lib/coq/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/lib/coq/Real.v b/lib/coq/Real.v
index a2da0e71..34b2a12f 100644
--- a/lib/coq/Real.v
+++ b/lib/coq/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/lib/coq/State_lemmas.v b/lib/coq/State_lemmas.v
index 6a620f27..9f419b49 100644
--- a/lib/coq/State_lemmas.v
+++ b/lib/coq/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/lib/coq/Values.v b/lib/coq/Values.v
index e335ad42..e6fb212d 100644
--- a/lib/coq/Values.v
+++ b/lib/coq/Values.v
@@ -1499,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.
@@ -1511,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;
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 00:58:00 +0000