Commit fe2b525c authored by Ralf Jung's avatar Ralf Jung
Browse files

use the new pattern features in a few places to shorten proofs a bit

parent 93ae382f
......@@ -196,7 +196,7 @@ Section gen_heap.
meta_token l E1 - meta_token l E2 - meta_token l (E1 E2).
Proof.
rewrite meta_token_eq /meta_token_def.
iDestruct 1 as (γm1) "[#Hγm1 Hm1]". iDestruct 1 as (γm2) "[#Hγm2 Hm2]".
iIntros "(%γm1 & #Hγm1 & Hm1) (%γm2 & #Hγm2 & Hm2)".
iDestruct (ghost_map_elem_valid_2 with "Hγm1 Hγm2") as %[_ ->].
iDestruct (own_valid_2 with "Hm1 Hm2") as %?%reservation_map_token_valid_op.
iExists γm2. iFrame "Hγm2". rewrite reservation_map_token_union //. by iSplitL "Hm1".
......@@ -219,7 +219,7 @@ Section gen_heap.
meta l i x1 - meta l i x2 - x1 = x2.
Proof.
rewrite meta_eq /meta_def.
iDestruct 1 as (γm1) "[Hγm1 Hm1]"; iDestruct 1 as (γm2) "[Hγm2 Hm2]".
iIntros "(%γm1 & Hγm1 & Hm1) (%γm2 & Hγm2 & Hm2)".
iDestruct (ghost_map_elem_valid_2 with "Hγm1 Hγm2") as %[_ ->].
iDestruct (own_valid_2 with "Hm1 Hm2") as %Hγ; iPureIntro.
move: Hγ. rewrite -reservation_map_data_op reservation_map_data_valid.
......
......@@ -45,7 +45,7 @@ Section proofs.
Lemma na_inv_iff p N P Q : na_inv p N P - (P Q) - na_inv p N Q.
Proof.
iIntros "HI #HPQ". rewrite /na_inv. iDestruct "HI" as (i ?) "HI".
rewrite /na_inv. iIntros "(%i & % & HI) #HPQ".
iExists i. iSplit; first done. iApply (inv_iff with "HI").
iIntros "!> !>".
iSplit; iIntros "[[? Ho]|$]"; iLeft; iFrame "Ho"; by iApply "HPQ".
......@@ -97,8 +97,7 @@ Section proofs.
na_inv p N P - na_own p F ={E}= P na_own p (F∖↑N)
( P na_own p (F∖↑N) ={E}= na_own p F).
Proof.
rewrite /na_inv. iIntros (??) "#Hnainv Htoks".
iDestruct "Hnainv" as (i) "[% Hinv]".
rewrite /na_inv. iIntros (??) "#(%i & % & Hinv) Htoks".
rewrite [F as X in na_own p X](union_difference_L (N) F) //.
rewrite [X in (X _)](union_difference_L {[i]} (N)) ?na_own_union; [|set_solver..].
iDestruct "Htoks" as "[[Htoki $] $]".
......
......@@ -234,7 +234,7 @@ Section proof.
Proof.
iIntros "Hvs". iInduction vs as [|v vs] "IH" forall (Q); simpl.
{ iExists []. by auto. }
iDestruct "Hvs" as "[Hv Hvs]"; iDestruct "Hv" as (x ->) "Hv".
iDestruct "Hvs" as "[(%x & -> & Hv) Hvs]".
iDestruct ("IH" with "Hvs") as (xs ->) "Hxs".
iExists (x :: xs). by iFrame.
Qed.
......
......@@ -65,7 +65,7 @@ Section proof.
Lemma locked_exclusive (γ : gname) : locked γ - locked γ - False.
Proof.
iDestruct 1 as (o1) "H1". iDestruct 1 as (o2) "H2".
iIntros "[%σ1 H1] [%σ2 H2]".
iDestruct (own_valid_2 with "H1 H2") as %[[] _]%auth_frag_op_valid_1.
Qed.
......@@ -74,7 +74,7 @@ Section proof.
Proof.
iDestruct 1 as (lo ln ->) "#Hinv"; iIntros "#HR".
iExists lo, ln; iSplit; [done|]. iApply (inv_iff with "Hinv").
iIntros "!> !>"; iSplit; iDestruct 1 as (o n) "(Ho & Hn & H● & H)";
iIntros "!> !>"; iSplit; iIntros "(%o & %n & Ho & Hn & H● & H)";
iExists o, n; iFrame "Ho Hn H●";
(iDestruct "H" as "[[H◯ H]|H◯]"; [iLeft; iFrame "H◯"; by iApply "HR"|by iRight]).
Qed.
......
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