proof.v 3.01 KB
 Amin Timany committed Dec 15, 2017 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 ``````From iris.algebra Require Import frac gmap auth. From iris.base_logic Require Export invariants. From iris.proofmode Require Import tactics. From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Export lifting notation. From iris.heap_lang.lib Require Import par. From iris.base_logic Require Import cancelable_invariants. Import uPred. From iris_examples.spanning_tree Require Import graph mon spanning. Section wp_span. Context `{heapG Σ, cinvG Σ, inG Σ (authR markingUR), inG Σ (authR graphUR), spawnG Σ}. Lemma wp_span g (markings : gmap loc loc) (x : val) (l : loc) : l ∈ dom (gset loc) g → maximal g → connected g l → ([∗ map] l ↦ v ∈ g, ∃ (m : loc), ⌜markings !! l = Some m⌝ ∗ l ↦ (#m, children_to_val v) ∗ m ↦ #false) ⊢ WP span (SOME #l) {{ _, ∃ g', ([∗ map] l ↦ v ∈ g', ∃ m : loc, ⌜markings !! l = Some m⌝ ∗ l ↦ (#m, children_to_val v) ∗ m ↦ #true) ∗ ⌜dom (gset loc) g = dom (gset loc) g'⌝ ∗ ⌜strict_subgraph g g'⌝ ∗ ⌜tree g' l⌝ }}. Proof. iIntros (Hgl Hgmx Hgcn) "Hgr". iMod (graph_ctx_alloc _ g markings with "[Hgr]") as (Ig κ) "(key & #Hgr & Hg)"; eauto. `````` Jacques-Henri Jourdan committed Oct 31, 2018 33 `````` iApply wp_fupd. wp_pures. `````` Amin Timany committed Dec 15, 2017 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 `````` iApply wp_wand_l; iSplitR; [|iApply ((rec_wp_span κ g markings 1 1 (SOMEV #l)) with "[Hg key]"); eauto; iFrame "#"; iFrame]. iIntros (v) "[H key]". unfold graph_ctx. iMod (cinv_cancel ⊤ graphN κ (graph_inv g markings) with "[#] [key]") as ">Hinv"; first done; try by iFrame. iClear "Hgr". unfold graph_inv. iDestruct "Hinv" as (G) "(Hi1 & Hi2 & Hi3 & Hi4)". iDestruct "Hi4" as %Hi4. iDestruct "H" as "[H|H]". - iDestruct "H" as "(_ & H)". iDestruct "H" as (l') "(H1 & H2 & Hl')". iDestruct "H1" as %Hl; inversion Hl; subst. iDestruct "H2" as (G' gmr gtr) "(Hl1 & Hl2 & Hl3 & Hl4 & Hl5)". iDestruct "Hl2" as %Hl2. iDestruct "Hl3" as %Hl3. iDestruct "Hl4" as %Hl4. iDestruct (whole_frac with "[Hi1 Hl1]") as %Heq; [by iFrame|]; subst. iDestruct (marked_is_marked_in_auth_sepS with "[Hi2 Hl5]") as %Hmrk; [by iFrame|]. iDestruct (own_graph_valid with "Hl1") as %Hvl. iExists (Gmon_graph G'). assert (dom (gset positive) g = dom (gset positive) (Gmon_graph G')). { erewrite front_t_t_dom; eauto. - by rewrite Gmon_graph_dom. - eapply front_mono; rewrite Gmon_graph_dom; eauto. } iModIntro. repeat iSplitL; try by iPureIntro. rewrite /heap_owns of_graph_dom_eq //=. by rewrite big_sepM_fmap /=. - iDestruct "H" as "(_ & [H|H] & Hx)". + iDestruct "H" as %Heq. inversion Heq. + iDestruct "H" as (l') "(_ & Hl)". iDestruct (marked_is_marked_in_auth with "[Hi2 Hl]") as %Hmrk; [by iFrame|]. iDestruct (whole_frac with "[Hx Hi1]") as %Heq; [by iFrame|]; subst. exfalso; revert Hmrk. rewrite dom_empty. inversion 1. Qed. `````` Jacques-Henri Jourdan committed Oct 31, 2018 69 ``End wp_span.``