Commit 3a3f0706 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'use-lia' into 'master'

Use lia to avoid omega deprecation warnings

Closes #319

See merge request !445
parents 5cb8bc17 d7d078a9
Pipeline #28316 passed with stage
in 19 minutes and 36 seconds
...@@ -104,17 +104,17 @@ Section tests. ...@@ -104,17 +104,17 @@ Section tests.
iIntros (Hn) "HΦ". iIntros (Hn) "HΦ".
iInduction (Z.gt_wf n2 n1) as [n1' _] "IH" forall (Hn). iInduction (Z.gt_wf n2 n1) as [n1' _] "IH" forall (Hn).
wp_rec. wp_pures. case_bool_decide; wp_if. wp_rec. wp_pures. case_bool_decide; wp_if.
- iApply ("IH" with "[%] [%] HΦ"); omega. - iApply ("IH" with "[%] [%] HΦ"); lia.
- by assert (n1' = n2 - 1) as -> by omega. - by assert (n1' = n2 - 1) as -> by lia.
Qed. Qed.
Lemma Pred_spec n E Φ : Φ #(n - 1) - WP Pred #n @ E [{ Φ }]. Lemma Pred_spec n E Φ : Φ #(n - 1) - WP Pred #n @ E [{ Φ }].
Proof. Proof.
iIntros "HΦ". wp_lam. iIntros "HΦ". wp_lam.
wp_op. case_bool_decide. wp_op. case_bool_decide.
- wp_apply FindPred_spec; first omega. wp_pures. - wp_apply FindPred_spec; first lia. wp_pures.
by replace (n - 1) with (- (-n + 2 - 1)) by omega. by replace (n - 1) with (- (-n + 2 - 1)) by lia.
- wp_apply FindPred_spec; eauto with omega. - wp_apply FindPred_spec; eauto with lia.
Qed. Qed.
Lemma Pred_user E : Lemma Pred_user E :
......
...@@ -232,7 +232,7 @@ Section counter_proof. ...@@ -232,7 +232,7 @@ Section counter_proof.
wp_cmpxchg_suc. iSplitL "Hl Hγ". wp_cmpxchg_suc. iSplitL "Hl Hγ".
{ iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. } { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
wp_pures. rewrite {3}/C; eauto 10. wp_pures. rewrite {3}/C; eauto 10.
- wp_cmpxchg_fail; first (intros [=]; abstract omega). - wp_cmpxchg_fail; first (intros [=]; abstract lia).
iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|]. iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
wp_pures. iApply ("IH" with "[Hγf]"). rewrite {3}/C; eauto 10. wp_pures. iApply ("IH" with "[Hγf]"). rewrite {3}/C; eauto 10.
Qed. Qed.
...@@ -248,6 +248,6 @@ Section counter_proof. ...@@ -248,6 +248,6 @@ Section counter_proof.
{ iApply own_op. by iFrame. } { iApply own_op. by iFrame. }
rewrite (auth_frag_op c c); last lia; iDestruct "Hγ" as "[Hγ Hγf']". rewrite (auth_frag_op c c); last lia; iDestruct "Hγ" as "[Hγ Hγf']".
iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|]. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
rewrite /C; eauto 10 with omega. rewrite /C; eauto 10 with lia.
Qed. Qed.
End counter_proof. End counter_proof.
...@@ -422,7 +422,7 @@ Lemma test_iInduction_wf (x : nat) P Q : ...@@ -422,7 +422,7 @@ Lemma test_iInduction_wf (x : nat) P Q :
Proof. Proof.
iIntros "#HP HQ". iIntros "#HP HQ".
iInduction (lt_wf x) as [[|x] _] "IH"; simpl; first done. iInduction (lt_wf x) as [[|x] _] "IH"; simpl; first done.
rewrite (inj_iff S). by iApply ("IH" with "[%]"); first omega. rewrite (inj_iff S). by iApply ("IH" with "[%]"); first lia.
Qed. Qed.
Lemma test_iInduction_using (m : gmap nat nat) (Φ : nat nat PROP) y : Lemma test_iInduction_using (m : gmap nat nat) (Φ : nat nat PROP) y :
......
...@@ -48,7 +48,7 @@ Proof. ...@@ -48,7 +48,7 @@ Proof.
wp_load. wp_apply ("IH" with "Hl Htl"). iIntros "[Hl Htl]". wp_load. wp_apply ("IH" with "Hl Htl"). iIntros "[Hl Htl]".
wp_load. wp_apply ("IH1" with "Hl Htr"). iIntros "[Hl Htr]". wp_load. wp_apply ("IH1" with "Hl Htr"). iIntros "[Hl Htr]".
iApply "HΦ". iSplitL "Hl". iApply "HΦ". iSplitL "Hl".
{ by replace (sum tl + sum tr + n) with (sum tr + (sum tl + n)) by omega. } { by replace (sum tl + sum tr + n) with (sum tr + (sum tl + n)) by lia. }
iExists ll, lr, vl, vr. by iFrame. iExists ll, lr, vl, vr. by iFrame.
Qed. Qed.
......
...@@ -46,7 +46,7 @@ Proof. ...@@ -46,7 +46,7 @@ Proof.
iIntros "!> !>". iMod "H" as "(Hσ & He2 & Hefs)". iIntros "!>". iIntros "!> !>". iMod "H" as "(Hσ & He2 & Hefs)". iIntros "!>".
rewrite !app_length /= !app_length. rewrite !app_length /= !app_length.
replace (length t1' + S (length t2' + length efs)) replace (length t1' + S (length t2' + length efs))
with (length efs + (length t1' + S (length t2'))) by omega. iFrame. with (length efs + (length t1' + S (length t2'))) by lia. iFrame.
Qed. Qed.
Lemma wptp_steps s n e1 t1 κs κs' t2 σ1 σ2 Φ : Lemma wptp_steps s n e1 t1 κs κs' t2 σ1 σ2 Φ :
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment