Commit 07ff13e0 authored by Ralf Jung's avatar Ralf Jung

avoid using iAlways ourselves

parent 6ae02201
Pipeline #31482 canceled with stage
in 6 minutes and 36 seconds
...@@ -501,7 +501,7 @@ Proof. iIntros "#HPQ HQ !>". iNext. by iRewrite "HPQ" in "HQ". Qed. ...@@ -501,7 +501,7 @@ Proof. iIntros "#HPQ HQ !>". iNext. by iRewrite "HPQ" in "HQ". Qed.
Lemma test_iAlways P Q R : Lemma test_iAlways P Q R :
P - <pers> Q R - <pers> <affine> <affine> P Q. P - <pers> Q R - <pers> <affine> <affine> P Q.
Proof. iIntros "#HP #HQ HR". iSplitL. iAlways. done. iAlways. done. Qed. Proof. iIntros "#HP #HQ HR". iSplitL. iModIntro. done. iModIntro. done. Qed.
(* A bunch of test cases from #127 to establish that tactics behave the same on (* A bunch of test cases from #127 to establish that tactics behave the same on
`⌜ φ ⌝ → P` and `∀ _ : φ, P` *) `⌜ φ ⌝ → P` and `∀ _ : φ, P` *)
...@@ -975,7 +975,7 @@ Proof. Fail iStopProof. Abort. ...@@ -975,7 +975,7 @@ Proof. Fail iStopProof. Abort.
Check "iAlways_spatial_non_empty". Check "iAlways_spatial_non_empty".
Lemma iAlways_spatial_non_empty P : Lemma iAlways_spatial_non_empty P :
P - emp. P - emp.
Proof. iIntros "HP". Fail iAlways. Abort. Proof. iIntros "HP". Fail iModIntro. Abort.
Check "iDestruct_bad_name". Check "iDestruct_bad_name".
Lemma iDestruct_bad_name P : Lemma iDestruct_bad_name P :
......
...@@ -71,23 +71,23 @@ Section tests. ...@@ -71,23 +71,23 @@ Section tests.
Qed. Qed.
Lemma test_objectively P Q : <obj> emp - <obj> P - <obj> Q - <obj> (P Q). Lemma test_objectively P Q : <obj> emp - <obj> P - <obj> Q - <obj> (P Q).
Proof. iIntros "#? HP HQ". iAlways. by iSplitL "HP". Qed. Proof. iIntros "#? HP HQ". iModIntro. by iSplitL "HP". Qed.
Lemma test_objectively_absorbing P Q R `{!Absorbing P} : Lemma test_objectively_absorbing P Q R `{!Absorbing P} :
<obj> emp - <obj> P - <obj> Q - R - <obj> (P Q). <obj> emp - <obj> P - <obj> Q - R - <obj> (P Q).
Proof. iIntros "#? HP HQ HR". iAlways. by iSplitL "HP". Qed. Proof. iIntros "#? HP HQ HR". iModIntro. by iSplitL "HP". Qed.
Lemma test_objectively_affine P Q R `{!Affine R} : Lemma test_objectively_affine P Q R `{!Affine R} :
<obj> emp - <obj> P - <obj> Q - R - <obj> (P Q). <obj> emp - <obj> P - <obj> Q - R - <obj> (P Q).
Proof. iIntros "#? HP HQ HR". iAlways. by iSplitL "HP". Qed. Proof. iIntros "#? HP HQ HR". iModIntro. by iSplitL "HP". Qed.
Lemma test_iModIntro_embed P `{!Affine Q} 𝓟 𝓠 : Lemma test_iModIntro_embed P `{!Affine Q} 𝓟 𝓠 :
P - Q - ⎡𝓟⎤ - ⎡𝓠⎤ - 𝓟 𝓠 . P - Q - ⎡𝓟⎤ - ⎡𝓠⎤ - 𝓟 𝓠 .
Proof. iIntros "#H1 _ H2 H3". iAlways. iFrame. Qed. Proof. iIntros "#H1 _ H2 H3". iModIntro. iFrame. Qed.
Lemma test_iModIntro_embed_objective P `{!Objective Q} 𝓟 𝓠 : Lemma test_iModIntro_embed_objective P `{!Objective Q} 𝓟 𝓠 :
P - Q - ⎡𝓟⎤ - ⎡𝓠⎤ - i, 𝓟 𝓠 Q i . P - Q - ⎡𝓟⎤ - ⎡𝓠⎤ - i, 𝓟 𝓠 Q i .
Proof. iIntros "#H1 H2 H3 H4". iAlways. Show. iFrame. Qed. Proof. iIntros "#H1 H2 H3 H4". iModIntro. Show. iFrame. Qed.
Lemma test_iModIntro_embed_nested P 𝓟 𝓠 : Lemma test_iModIntro_embed_nested P 𝓟 𝓠 :
P - ⎡◇ 𝓟⎤ - ⎡◇ 𝓠⎤ - (𝓟 𝓠) . P - ⎡◇ 𝓟⎤ - ⎡◇ 𝓠⎤ - (𝓟 𝓠) .
......
  • Did you also make sure not to use the !# intro pattern? That has the same issue AFAIK.

  • I don't think that triggers the warning? (It would be better if it did though.) I am build-testing this currently.

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