From 2f1ae293a5435df898a72fd45ebb48600932177d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 20 Jun 2018 09:45:37 +0200
Subject: [PATCH] use lia instead of omega
---
theories/algebra/cofe_solver.v | 2 +-
theories/algebra/gmultiset.v | 2 +-
theories/algebra/list.v | 8 ++++----
theories/algebra/local_updates.v | 2 +-
theories/algebra/ofe.v | 10 +++++-----
theories/base_logic/double_negation.v | 28 +++++++++++++--------------
theories/base_logic/upred.v | 4 ++--
theories/heap_lang/lib/counter.v | 2 +-
theories/program_logic/weakestpre.v | 2 +-
9 files changed, 30 insertions(+), 30 deletions(-)
diff --git a/theories/algebra/cofe_solver.v b/theories/algebra/cofe_solver.v
index 0474eb3a8..0b473a792 100644
--- a/theories/algebra/cofe_solver.v
+++ b/theories/algebra/cofe_solver.v
@@ -93,7 +93,7 @@ Proof using Fcontr. intros. by rewrite -(fg (X (S (S k)))) -(g_tower X). Qed.
Lemma ff_tower k i (X : tower) : ff i (X (S k)) ≡{k}≡ X (i + S k).
Proof using Fcontr.
intros; induction i as [|i IH]; simpl; [done|].
- by rewrite IH Nat.add_succ_r (dist_le _ _ _ _ (f_tower _ X)); last omega.
+ by rewrite IH Nat.add_succ_r (dist_le _ _ _ _ (f_tower _ X)); last lia.
Qed.
Lemma gg_tower k i (X : tower) : gg i (X (i + k)) ≡ X k.
Proof. by induction i as [|i IH]; simpl; [done|rewrite g_tower IH]. Qed.
diff --git a/theories/algebra/gmultiset.v b/theories/algebra/gmultiset.v
index 612620318..1916b8f40 100644
--- a/theories/algebra/gmultiset.v
+++ b/theories/algebra/gmultiset.v
@@ -74,7 +74,7 @@ Section gmultiset.
rewrite local_update_unital_discrete=> Z' _ /leibniz_equiv_iff->.
split. done. rewrite !gmultiset_op_union=> x.
repeat (rewrite multiplicity_difference || rewrite multiplicity_union).
- omega.
+ lia.
Qed.
End gmultiset.
diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index 1f20a1592..c620e931f 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -68,11 +68,11 @@ Global Program Instance list_cofe `{Cofe A} : Cofe listC :=
Next Obligation.
intros ? n c; rewrite /compl /list_compl.
destruct (c 0) as [|x l] eqn:Hc0 at 1.
- { by destruct (chain_cauchy c 0 n); auto with omega. }
- rewrite -(λ H, length_ne _ _ _ (chain_cauchy c 0 n H)); last omega.
+ { by destruct (chain_cauchy c 0 n); auto with lia. }
+ rewrite -(λ H, length_ne _ _ _ (chain_cauchy c 0 n H)); last lia.
apply Forall2_lookup=> i. rewrite -dist_option_Forall2 list_lookup_fmap.
destruct (decide (i < length (c n))); last first.
- { rewrite lookup_seq_ge ?lookup_ge_None_2; auto with omega. }
+ { rewrite lookup_seq_ge ?lookup_ge_None_2; auto with lia. }
rewrite lookup_seq //= (conv_compl n (list_chain c _ _)) /=.
destruct (lookup_lt_is_Some_2 (c n) i) as [? Hcn]; first done.
by rewrite Hcn.
@@ -310,7 +310,7 @@ Section properties.
Lemma list_lookup_singletonM_ne i j x :
i ≠j →
({[ i := x ]} : list A) !! j = None ∨ ({[ i := x ]} : list A) !! j = Some ε.
- Proof. revert j; induction i; intros [|j]; naive_solver auto with omega. Qed.
+ Proof. revert j; induction i; intros [|j]; naive_solver auto with lia. Qed.
Lemma list_singletonM_validN n i x : ✓{n} ({[ i := x ]} : list A) ↔ ✓{n} x.
Proof.
rewrite list_lookup_validN. split.
diff --git a/theories/algebra/local_updates.v b/theories/algebra/local_updates.v
index 680126868..32479f799 100644
--- a/theories/algebra/local_updates.v
+++ b/theories/algebra/local_updates.v
@@ -179,7 +179,7 @@ Proof.
move=>Hex. apply local_update_unital=>n z /= Hy Heq. split; first done.
destruct z as [z|]; last done. exfalso.
move: Hy. rewrite Heq /= -Some_op=>Hy. eapply Hex.
- eapply cmra_validN_le. eapply Hy. omega.
+ eapply cmra_validN_le. eapply Hy. lia.
Qed.
(** * Natural numbers *)
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 4eb180241..e68cec85d 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -178,7 +178,7 @@ Section ofe.
Lemma conv_compl' `{Cofe A} n (c : chain A) : compl c ≡{n}≡ c (S n).
Proof.
transitivity (c n); first by apply conv_compl. symmetry.
- apply chain_cauchy. omega.
+ apply chain_cauchy. lia.
Qed.
Lemma discrete_iff n (x : A) `{!Discrete x} y : x ≡ y ↔ x ≡{n}≡ y.
@@ -292,9 +292,9 @@ Program Definition fixpoint_chain {A : ofeT} `{Inhabited A} (f : A → A)
`{!Contractive f} : chain A := {| chain_car i := Nat.iter (S i) f inhabitant |}.
Next Obligation.
intros A ? f ? n.
- induction n as [|n IH]=> -[|i] //= ?; try omega.
+ induction n as [|n IH]=> -[|i] //= ?; try lia.
- apply (contractive_0 f).
- - apply (contractive_S f), IH; auto with omega.
+ - apply (contractive_S f), IH; auto with lia.
Qed.
Program Definition fixpoint_def `{Cofe A, Inhabited A} (f : A → A)
@@ -341,7 +341,7 @@ Section fixpoint.
intros ? [x Hx] Hincr Hlim. set (chcar i := Nat.iter (S i) f x).
assert (Hcauch : ∀ n i : nat, n ≤ i → chcar i ≡{n}≡ chcar n).
{ intros n. rewrite /chcar. induction n as [|n IH]=> -[|i] //=;
- eauto using contractive_0, contractive_S with omega. }
+ eauto using contractive_0, contractive_S with lia. }
set (fp2 := compl {| chain_cauchy := Hcauch |}).
assert (f fp2 ≡ fp2).
{ apply equiv_dist=>n. rewrite /fp2 (conv_compl n) /= /chcar.
@@ -856,7 +856,7 @@ Section discrete_ofe.
{ compl c := c 0 }.
Next Obligation.
intros n c. rewrite /compl /=;
- symmetry; apply (chain_cauchy c 0 n). omega.
+ symmetry; apply (chain_cauchy c 0 n). lia.
Qed.
End discrete_ofe.
diff --git a/theories/base_logic/double_negation.v b/theories/base_logic/double_negation.v
index b8981923b..4ebe5cccc 100644
--- a/theories/base_logic/double_negation.v
+++ b/theories/base_logic/double_negation.v
@@ -90,7 +90,7 @@ Proof.
* rewrite comm -assoc. done.
* rewrite comm -assoc. done.
* exists y'. split=>//. by exists x'.
- - intros; assert (n' < a). omega.
+ - intros; assert (n' < a). lia.
move: laterN_small. uPred.unseal.
naive_solver.
Qed.
@@ -178,22 +178,22 @@ Lemma nnupd_nnupd_k_dist k P: (|=n=> P)%I ≡{k}≡ (|=n=>_k P)%I.
case (decide (k' < n)).
** move: laterN_small; uPred.unseal; naive_solver.
** intros. exfalso. eapply HnnP; eauto.
- assert (n ≤ k'). omega.
+ assert (n ≤ k'). lia.
intros n'' x'' ???.
specialize (HPF n'' x''). exfalso.
eapply laterN_big; last (unseal; eauto).
- eauto. omega.
+ eauto. lia.
* inversion Hle; simpl; subst.
** unseal. intros (HnnP&HnnP_IH) n k' x' ?? HPF.
case (decide (k' < n)).
*** move: laterN_small; uPred.unseal; naive_solver.
- *** intros. exfalso. assert (n ≤ k'). omega.
- assert (n = S k ∨ n < S k) as [->|] by omega.
+ *** intros. exfalso. assert (n ≤ k'). lia.
+ assert (n = S k ∨ n < S k) as [->|] by lia.
**** eapply laterN_big; eauto; unseal.
eapply HnnP; eauto. move: HPF; by unseal.
**** move:nnupd_k_elim. unseal. intros Hnnupdk.
eapply laterN_big; eauto. unseal.
- eapply (Hnnupdk n k); first omega; eauto.
+ eapply (Hnnupdk n k); first lia; eauto.
exists x, x'. split_and!; eauto. eapply uPred_mono; eauto.
** intros HP. eapply IHk; auto.
move:HP. unseal. intros (?&?); naive_solver.
@@ -265,7 +265,7 @@ Proof.
exfalso. eapply laterN_big; last (uPred.unseal; eapply (Hwand n' x')); eauto.
* rewrite comm. done.
* rewrite comm. done.
- - intros; assert (n' < a). omega.
+ - intros; assert (n' < a). lia.
move: laterN_small. uPred.unseal.
naive_solver.
Qed.
@@ -286,7 +286,7 @@ Proof using Type*.
red; rewrite //= => n' x' ???.
case (decide (n' = k)); intros.
- subst. exfalso. eapply Hfal. rewrite (comm op); eauto.
- - assert (n' < k). omega.
+ - assert (n' < k). lia.
move: laterN_small. uPred.unseal. naive_solver.
Qed.
End classical.
@@ -306,7 +306,7 @@ Proof.
split. unseal. intros n' ?? Hupd.
case (decide (n' < n)).
- intros. move: laterN_small. unseal. naive_solver.
- - intros. assert (n ≤ n'). omega.
+ - intros. assert (n ≤ n'). lia.
exfalso. specialize (Hupd n' ε).
eapply Hdne. intros Hfal.
eapply laterN_big; eauto.
@@ -326,14 +326,14 @@ Proof.
specialize (Hf3 (S k) (S k) ε). rewrite right_id in Hf3 *. unseal.
intros Hf3. eapply Hf3; eauto.
intros ??? Hx'. rewrite left_id in Hx' *=> Hx'.
- assert (n' < S k ∨ n' = S k) as [|] by omega.
+ assert (n' < S k ∨ n' = S k) as [|] by lia.
* intros. move:(laterN_small n' (S k) x' False). rewrite //=. unseal. intros Hsmall.
eapply Hsmall; eauto.
* subst. intros. exfalso. eapply Hf2. exists x'. split; eauto using cmra_validN_S.
- intros k P x Hx. rewrite ?Nat_iter_S_r.
- replace (S (S n) + k) with (S n + (S k)) by omega.
- replace (S n + k) with (n + (S k)) by omega.
- intros. eapply IHn. replace (S n + S k) with (S (S n) + k) by omega. eauto.
+ replace (S (S n) + k) with (S n + (S k)) by lia.
+ replace (S n + k) with (n + (S k)) by lia.
+ intros. eapply IHn. replace (S n + S k) with (S (S n) + k) by lia. eauto.
rewrite ?Nat_iter_S_r. eauto.
Qed.
@@ -356,7 +356,7 @@ Proof.
destruct n.
- rewrite //=; unseal; auto.
- intros ??? Hfal.
- eapply (adequacy_helper2 _ n 1); (replace (S n + 1) with (S (S n)) by omega); eauto.
+ eapply (adequacy_helper2 _ n 1); (replace (S n + 1) with (S (S n)) by lia); eauto.
unseal. intros (x'&?&Hphi). simpl in *.
eapply Hfal. auto.
Qed.
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 5f1f20de0..6f04ccb54 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -5,7 +5,7 @@ From Coq.Init Require Import Nat.
Set Default Proof Using "Type".
Local Hint Extern 1 (_ ≼ _) => etrans; [eassumption|].
Local Hint Extern 1 (_ ≼ _) => etrans; [|eassumption].
-Local Hint Extern 10 (_ ≤ _) => omega.
+Local Hint Extern 10 (_ ≤ _) => lia.
(** The basic definition of the uPred type, its metric and functor laws.
You probably do not want to import this file. Instead, import
@@ -466,7 +466,7 @@ Qed.
Lemma later_contractive : Contractive (@uPred_later M).
Proof.
- unseal; intros [|n] P Q HPQ; split=> -[|n'] x ?? //=; try omega.
+ unseal; intros [|n] P Q HPQ; split=> -[|n'] x ?? //=; try lia.
apply HPQ; eauto using cmra_validN_S.
Qed.
diff --git a/theories/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v
index 7e1a0c870..788eb8580 100644
--- a/theories/heap_lang/lib/counter.v
+++ b/theories/heap_lang/lib/counter.v
@@ -130,7 +130,7 @@ Section contrib_spec.
wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]".
destruct (decide (c' = c)) as [->|].
- iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
- { apply frac_auth_update, (nat_local_update _ _ (S c) (S n)); omega. }
+ { apply frac_auth_update, (nat_local_update _ _ (S c) (S n)); lia. }
wp_cas_suc. iModIntro. iSplitL "Hl Hγ".
{ iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
wp_if. by iApply "HΦ".
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 4b97fed7f..27fe865a6 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -58,7 +58,7 @@ Proof.
(* FIXME: reflexivity, as being called many times by f_equiv and f_contractive
is very slow here *)
do 18 (f_contractive || f_equiv). apply IH; first lia.
- intros v. eapply dist_le; eauto with omega.
+ intros v. eapply dist_le; eauto with lia.
Qed.
Global Instance wp_proper s E e :
Proper (pointwise_relation _ (≡) ==> (≡)) (wp (PROP:=iProp Σ) s E e).
--
GitLab