Commit 6be1cdd2 authored by Ralf Jung's avatar Ralf Jung
Browse files

more exist destruct test cases

parent 06313482
...@@ -457,11 +457,21 @@ Proof. iIntros (?) "HP #HQ HR". iPureIntro; eauto. Qed. ...@@ -457,11 +457,21 @@ Proof. iIntros (?) "HP #HQ HR". iPureIntro; eauto. Qed.
(* Ensure that [% ...] works as a pattern when the left-hand side of and/sep is (* Ensure that [% ...] works as a pattern when the left-hand side of and/sep is
pure. *) pure. *)
Lemma test_pure_and_sep_destruct `{!BiAffine PROP} (φ : Prop) (P : PROP) : Lemma test_pure_and_sep_destruct_affine `{!BiAffine PROP} (φ : Prop) (P : PROP) :
⌜φ⌝ (⌜φ⌝ P) - P. ⌜φ⌝ (⌜φ⌝ P) - P.
Proof. Proof.
iIntros "[% [% $]]". iIntros "[% [% $]]".
Qed. Qed.
Lemma test_pure_and_sep_destruct_1 (φ : Prop) (P : PROP) :
⌜φ⌝ (<affine> ⌜φ⌝ P) - P.
Proof.
iIntros "[% [% $]]".
Qed.
Lemma test_pure_and_sep_destruct_2 (φ : Prop) (P : PROP) :
⌜φ⌝ (⌜φ⌝ <absorb> P) - <absorb> P.
Proof.
iIntros "[% [% $]]".
Qed.
(* Ensure that [% %] also works when the conjunction is *inside* ⌜...⌝ *) (* Ensure that [% %] also works when the conjunction is *inside* ⌜...⌝ *)
Lemma test_pure_inner_and_destruct : Lemma test_pure_inner_and_destruct :
False True @{PROP} False. False True @{PROP} False.
......
Supports Markdown
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