Skip to content
Snippets Groups Projects
Commit 87916dfb authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

More use of `iDestruct .. gives`.

parent 8a65d1b4
No related branches found
No related tags found
No related merge requests found
Pipeline #79253 failed
Hide whitespace changes
Inline Side-by-side
theories/examples/symbol.v
+ 5
− 6
View file @ 87916dfb
...@@ -63,8 +63,7 @@ Section rules. ...@@ -63,8 +63,7 @@ Section rules.
⌜m ≤ n⌝. ⌜m ≤ n⌝.
Proof. Proof.
iIntros "Hn Hm". iIntros "Hn Hm".
by iDestruct (own_valid_2 with "Hn Hm") by iCombine "Hn Hm" gives %[?%max_nat_included _]%auth_both_valid_discrete.
as %[?%max_nat_included _]%auth_both_valid_discrete.
Qed. Qed.
Lemma same_size (n m : nat) : Lemma same_size (n m : nat) :
...@@ -152,8 +151,8 @@ Section proof. ...@@ -152,8 +151,8 @@ Section proof.
"(Ha & Hs1' & Hs2' & Htbl1' & Htbl2' & #Hls)" "Hcl". "(Ha & Hs1' & Hs2' & Htbl1' & Htbl2' & #Hls)" "Hcl".
iModIntro. iExists _. iFrame. iNext. iIntros "Hs1'". iModIntro. iExists _. iFrame. iNext. iIntros "Hs1'".
rel_load_r. rel_pure_r. rel_pure_r. rel_load_r. rel_pure_r. rel_pure_r.
iDestruct (own_valid_2 with "Ha Hn") iCombine "Ha Hn"
as %[?%max_nat_included _]%auth_both_valid_discrete; simpl in *. gives %[?%max_nat_included _]%auth_both_valid_discrete; simpl in *.
rel_op_l. rel_op_r. rewrite bool_decide_true; last lia. rel_op_l. rel_op_r. rewrite bool_decide_true; last lia.
rel_pure_r. rel_load_r. rel_op_r. rel_pure_r. rel_load_r. rel_op_r.
iMod ("Hcl" with "[Ha Hs1' Hs2' Htbl1' Htbl2' Hls]") as "_". iMod ("Hcl" with "[Ha Hs1' Hs2' Htbl1' Htbl2' Hls]") as "_".
...@@ -189,8 +188,8 @@ Section proof. ...@@ -189,8 +188,8 @@ Section proof.
rel_load_l_atomic. rel_load_l_atomic.
iInv sizeN as (m ls) "(Ha & Hs1' & >Hs2' & >Htbl1' & >Htbl2' & Hls)" "Hcl". iInv sizeN as (m ls) "(Ha & Hs1' & >Hs2' & >Htbl1' & >Htbl2' & Hls)" "Hcl".
iModIntro. iExists _. iFrame. iNext. iIntros "Hs1'". iModIntro. iExists _. iFrame. iNext. iIntros "Hs1'".
iDestruct (own_valid_2 with "Ha Hn") iCombine "Ha Hn"
as %[?%max_nat_included _]%auth_both_valid_discrete; simpl in *. gives %[?%max_nat_included _]%auth_both_valid_discrete; simpl in *.
iMod ("Hcl" with "[Ha Hs1' Hs2' Htbl1' Htbl2' Hls]") as "_". iMod ("Hcl" with "[Ha Hs1' Hs2' Htbl1' Htbl2' Hls]") as "_".
{ iNext. iExists _,_. by iFrame. } { iNext. iExists _,_. by iFrame. }
clear ls. repeat rel_pure_l. clear ls. repeat rel_pure_l.
......
theories/examples/ticket_lock.v
+ 2
− 2
View file @ 87916dfb
...@@ -45,8 +45,8 @@ Section refinement. ...@@ -45,8 +45,8 @@ Section refinement.
Lemma ticket_nondup γ n : ticket γ n -∗ ticket γ n -∗ False. Lemma ticket_nondup γ n : ticket γ n -∗ ticket γ n -∗ False.
Proof. Proof.
iIntros "Ht1 Ht2". iDestruct (own_valid_2 with "Ht1 Ht2") iIntros "Ht1 Ht2". iCombine "Ht1 Ht2"
as %?%auth_frag_op_valid_1%gset_disj_valid_op. gives %?%auth_frag_op_valid_1%gset_disj_valid_op.
set_solver. set_solver.
Qed. Qed.
......
theories/examples/various.v
+ 1
− 3
View file @ 87916dfb
...@@ -55,9 +55,7 @@ Section proofs. ...@@ -55,9 +55,7 @@ Section proofs.
Lemma shot_not_pending γ `{oneshotG Σ} : Lemma shot_not_pending γ `{oneshotG Σ} :
shot γ -∗ pending γ -∗ False. shot γ -∗ pending γ -∗ False.
Proof. Proof.
iIntros "Hs Hp". iIntros "Hs Hp". iCombine "Hs Hp" gives %[].
iPoseProof (own_valid_2 with "Hs Hp") as "H".
iDestruct "H" as %[].
Qed. Qed.
Lemma refinement2 `{oneshotG Σ} : Lemma refinement2 `{oneshotG Σ} :
......
theories/logic/spec_rules.v
+ 34
− 34
View file @ 87916dfb
...@@ -51,8 +51,8 @@ Section rules. ...@@ -51,8 +51,8 @@ Section rules.
iDestruct "Hspec" as (ρ) "Hspec". iDestruct "Hspec" as (ρ) "Hspec".
iInv specN as (tp σ) ">[Hown Hrtc]" "Hclose". iInv specN as (tp σ) ">[Hown Hrtc]" "Hclose".
iDestruct "Hrtc" as %Hrtc. iDestruct "Hrtc" as %Hrtc.
iDestruct (own_valid_2 with "Hown Hj") iCombine "Hown Hj"
as %[[Htpj%tpool_singleton_included' _]%prod_included ?]%auth_both_valid_discrete. gives %[[Htpj%tpool_singleton_included' _]%prod_included ?]%auth_both_valid_discrete.
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]". iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ eapply auth_update, prod_local_update_1. { eapply auth_update, prod_local_update_1.
by eapply (singleton_local_update _ j (Excl (fill K e))), by eapply (singleton_local_update _ j (Excl (fill K e))),
...@@ -96,8 +96,8 @@ Section rules. ...@@ -96,8 +96,8 @@ Section rules.
rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def /=. rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def /=.
iDestruct "Hinv" as (ρ) "Hinv". iDestruct "Hinv" as (ρ) "Hinv".
iInv specN as (tp σ) ">[Hown %]" "Hclose". iInv specN as (tp σ) ">[Hown %]" "Hclose".
iDestruct (own_valid_2 with "Hown Hj") iCombine "Hown Hj"
as %[[?%tpool_singleton_included' _]%prod_included _]%auth_both_valid_discrete. gives %[[?%tpool_singleton_included' _]%prod_included _]%auth_both_valid_discrete.
destruct (exist_fresh (used_proph_id σ)) as [p Hp]. destruct (exist_fresh (used_proph_id σ)) as [p Hp].
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]". iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1, { by eapply auth_update, prod_local_update_1,
...@@ -117,8 +117,8 @@ Section rules. ...@@ -117,8 +117,8 @@ Section rules.
rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def /=. rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def /=.
iDestruct "Hinv" as (ρ) "Hinv". iDestruct "Hinv" as (ρ) "Hinv".
iInv specN as (tp σ) ">[Hown %]" "Hclose". iInv specN as (tp σ) ">[Hown %]" "Hclose".
iDestruct (own_valid_2 with "Hown Hj") iCombine "Hown Hj"
as %[[?%tpool_singleton_included' _]%prod_included _]%auth_both_valid_discrete. gives %[[?%tpool_singleton_included' _]%prod_included _]%auth_both_valid_discrete.
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]". iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1, { by eapply auth_update, prod_local_update_1,
singleton_local_update, (exclusive_local_update _ (Excl (fill K #()))). } singleton_local_update, (exclusive_local_update _ (Excl (fill K #()))). }
...@@ -139,8 +139,8 @@ Section rules. ...@@ -139,8 +139,8 @@ Section rules.
iDestruct "Hinv" as (ρ) "Hinv". iDestruct "Hinv" as (ρ) "Hinv".
iInv specN as (tp σ) ">[Hown %]" "Hclose". iInv specN as (tp σ) ">[Hown %]" "Hclose".
destruct (exist_fresh (dom (heap σ))) as [l Hl%not_elem_of_dom]. destruct (exist_fresh (dom (heap σ))) as [l Hl%not_elem_of_dom].
iDestruct (own_valid_2 with "Hown Hj") iCombine "Hown Hj"
as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_both_valid_discrete. gives %[[?%tpool_singleton_included' _]%prod_included ?]%auth_both_valid_discrete.
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]". iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1, { by eapply auth_update, prod_local_update_1,
singleton_local_update, (exclusive_local_update _ (Excl (fill K (#l)%E))). } singleton_local_update, (exclusive_local_update _ (Excl (fill K (#l)%E))). }
...@@ -167,10 +167,10 @@ Section rules. ...@@ -167,10 +167,10 @@ Section rules.
iDestruct "Hinv" as (ρ) "Hinv". iDestruct "Hinv" as (ρ) "Hinv".
rewrite heapS_mapsto_eq /heapS_mapsto_def /=. rewrite heapS_mapsto_eq /heapS_mapsto_def /=.
iInv specN as (tp σ) ">[Hown %]" "Hclose". iInv specN as (tp σ) ">[Hown %]" "Hclose".
iDestruct (own_valid_2 with "Hown Hj") iCombine "Hown Hj"
as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_both_valid_discrete. gives %[[?%tpool_singleton_included' _]%prod_included ?]%auth_both_valid_discrete.
iDestruct (own_valid_2 with "Hown Hl") iCombine "Hown Hl"
as %[[? ?%heap_singleton_included]%prod_included ?]%auth_both_valid_discrete. gives %[[? ?%heap_singleton_included]%prod_included ?]%auth_both_valid_discrete.
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]". iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1, singleton_local_update, { by eapply auth_update, prod_local_update_1, singleton_local_update,
(exclusive_local_update _ (Excl (fill K (of_val v)))). } (exclusive_local_update _ (Excl (fill K (of_val v)))). }
...@@ -191,10 +191,10 @@ Section rules. ...@@ -191,10 +191,10 @@ Section rules.
iDestruct "Hinv" as (ρ) "Hinv". iDestruct "Hinv" as (ρ) "Hinv".
rewrite heapS_mapsto_eq /heapS_mapsto_def /=. rewrite heapS_mapsto_eq /heapS_mapsto_def /=.
iInv specN as (tp σ) ">[Hown %]" "Hclose". iInv specN as (tp σ) ">[Hown %]" "Hclose".
iDestruct (own_valid_2 with "Hown Hj") iCombine "Hown Hj"
as %[[?%tpool_singleton_included' _]%prod_included _]%auth_both_valid_discrete. gives %[[?%tpool_singleton_included' _]%prod_included _]%auth_both_valid_discrete.
iDestruct (own_valid_2 with "Hown Hl") iCombine "Hown Hl"
as %[[_ Hl%heap_singleton_included]%prod_included _]%auth_both_valid_discrete. gives %[[_ Hl%heap_singleton_included]%prod_included _]%auth_both_valid_discrete.
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]". iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1, singleton_local_update, { by eapply auth_update, prod_local_update_1, singleton_local_update,
(exclusive_local_update _ (Excl (fill K #()))). } (exclusive_local_update _ (Excl (fill K #()))). }
...@@ -222,10 +222,10 @@ Section rules. ...@@ -222,10 +222,10 @@ Section rules.
iDestruct "Hinv" as (ρ) "Hinv". iDestruct "Hinv" as (ρ) "Hinv".
rewrite heapS_mapsto_eq /heapS_mapsto_def /=. rewrite heapS_mapsto_eq /heapS_mapsto_def /=.
iInv specN as (tp σ) ">[Hown %]" "Hclose". iInv specN as (tp σ) ">[Hown %]" "Hclose".
iDestruct (own_valid_2 with "Hown Hj") iCombine "Hown Hj"
as %[[?%tpool_singleton_included' _]%prod_included _]%auth_both_valid_discrete. gives %[[?%tpool_singleton_included' _]%prod_included _]%auth_both_valid_discrete.
iDestruct (own_valid_2 with "Hown Hl") iCombine "Hown Hl"
as %[[_ Hl%heap_singleton_included]%prod_included _]%auth_both_valid_discrete. gives %[[_ Hl%heap_singleton_included]%prod_included _]%auth_both_valid_discrete.
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]". iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1, singleton_local_update, { by eapply auth_update, prod_local_update_1, singleton_local_update,
(exclusive_local_update _ (Excl (fill K (of_val v')))). } (exclusive_local_update _ (Excl (fill K (of_val v')))). }
...@@ -256,10 +256,10 @@ Section rules. ...@@ -256,10 +256,10 @@ Section rules.
rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def. rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
iDestruct "Hinv" as (ρ) "Hinv". iDestruct "Hinv" as (ρ) "Hinv".
iInv specN as (tp σ) ">[Hown %]" "Hclose". iInv specN as (tp σ) ">[Hown %]" "Hclose".
iDestruct (own_valid_2 with "Hown Hj") iCombine "Hown Hj"
as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_both_valid_discrete. gives %[[?%tpool_singleton_included' _]%prod_included ?]%auth_both_valid_discrete.
iDestruct (own_valid_2 with "Hown Hl") iCombine "Hown Hl"
as %[[_ ?%heap_singleton_included]%prod_included _]%auth_both_valid_discrete. gives %[[_ ?%heap_singleton_included]%prod_included _]%auth_both_valid_discrete.
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]". iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1, singleton_local_update, { by eapply auth_update, prod_local_update_1, singleton_local_update,
(exclusive_local_update _ (Excl (fill K (_, #false)%V))). } (exclusive_local_update _ (Excl (fill K (_, #false)%V))). }
...@@ -283,10 +283,10 @@ Section rules. ...@@ -283,10 +283,10 @@ Section rules.
rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def. rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
iDestruct "Hinv" as (ρ) "Hinv". iDestruct "Hinv" as (ρ) "Hinv".
iInv specN as (tp σ) ">[Hown %]" "Hclose". iInv specN as (tp σ) ">[Hown %]" "Hclose".
iDestruct (own_valid_2 with "Hown Hj") iCombine "Hown Hj"
as %[[?%tpool_singleton_included' _]%prod_included _]%auth_both_valid_discrete. gives %[[?%tpool_singleton_included' _]%prod_included _]%auth_both_valid_discrete.
iDestruct (own_valid_2 with "Hown Hl") iCombine "Hown Hl"
as %[[_ Hl%heap_singleton_included]%prod_included _]%auth_both_valid_discrete. gives %[[_ Hl%heap_singleton_included]%prod_included _]%auth_both_valid_discrete.
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]". iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1, singleton_local_update, { by eapply auth_update, prod_local_update_1, singleton_local_update,
(exclusive_local_update _ (Excl (fill K (_, #true)%V))). } (exclusive_local_update _ (Excl (fill K (_, #true)%V))). }
...@@ -314,10 +314,10 @@ Section rules. ...@@ -314,10 +314,10 @@ Section rules.
rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def. rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
iDestruct "Hinv" as (ρ) "Hinv". iDestruct "Hinv" as (ρ) "Hinv".
iInv specN as (tp σ) ">[Hown %]" "Hclose". iInv specN as (tp σ) ">[Hown %]" "Hclose".
iDestruct (own_valid_2 with "Hown Hj") iCombine "Hown Hj"
as %[[?%tpool_singleton_included' _]%prod_included _]%auth_both_valid_discrete. gives %[[?%tpool_singleton_included' _]%prod_included _]%auth_both_valid_discrete.
iDestruct (own_valid_2 with "Hown Hl") iCombine "Hown Hl"
as %[[_ Hl%heap_singleton_included]%prod_included _]%auth_both_valid_discrete. gives %[[_ Hl%heap_singleton_included]%prod_included _]%auth_both_valid_discrete.
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]". iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1, singleton_local_update, { by eapply auth_update, prod_local_update_1, singleton_local_update,
(exclusive_local_update _ (Excl (fill K (# i1)))). } (exclusive_local_update _ (Excl (fill K (# i1)))). }
...@@ -344,8 +344,8 @@ Section rules. ...@@ -344,8 +344,8 @@ Section rules.
rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def. rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def.
iDestruct "Hspec" as (ρ) "Hspec". iDestruct "Hspec" as (ρ) "Hspec".
iInv specN as (tp σ) ">[Hown %]" "Hclose". iInv specN as (tp σ) ">[Hown %]" "Hclose".
iDestruct (own_valid_2 with "Hown Hj") iCombine "Hown Hj"
as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_both_valid_discrete. gives %[[?%tpool_singleton_included' _]%prod_included ?]%auth_both_valid_discrete.
assert (j < length tp) by eauto using lookup_lt_Some. assert (j < length tp) by eauto using lookup_lt_Some.
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]". iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1, { by eapply auth_update, prod_local_update_1,
......
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