evmap.v 4.72 KB
 Zhen Zhang committed Oct 19, 2016 1 ``````(* evmap.v -- generalized heap-like monoid composite *) `````` Ralf Jung committed Nov 01, 2016 2 3 ``````From iris.base_logic Require Export invariants. From iris.program_logic Require Export weakestpre. `````` Zhen Zhang committed Oct 11, 2016 4 5 6 7 ``````From iris.algebra Require Export auth frac gmap dec_agree. From iris.proofmode Require Import tactics. Section evmap. `````` Zhen Zhang committed Oct 19, 2016 8 `````` Context (K A: Type) (Q: cmraT) `{Countable K, EqDecision A}. `````` Zhen Zhang committed Oct 11, 2016 9 10 11 12 13 14 15 16 17 `````` Definition evkR := prodR Q (dec_agreeR A). Definition evmapR := gmapUR K evkR. Definition evidenceR := authR evmapR. Class evidenceG Σ := EvidenceG { evidence_G :> inG Σ evidenceR }. Definition evidenceΣ : gFunctors := #[ GFunctor (constRF evidenceR) ]. Instance subG_evidenceΣ {Σ} : subG evidenceΣ Σ → evidenceG Σ. Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed. `````` Zhen Zhang committed Oct 19, 2016 18 `````` (* Some basic supporting lemmas *) `````` Zhen Zhang committed Oct 11, 2016 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 `````` Lemma map_agree_eq m m' (hd: K) (p q: Q) (x y: A): m !! hd = Some (p, DecAgree y) → m = {[hd := (q, DecAgree x)]} ⋅ m' → x = y. Proof. intros H1 H2. destruct (decide (x = y)) as [->|Hneq]=>//. exfalso. subst. rewrite lookup_op lookup_singleton in H1. destruct (m' !! hd) as [[b [c|]]|] eqn:Heqn; rewrite Heqn in H1; inversion H1=>//. destruct (decide (x = c)) as [->|Hneq3]=>//. - rewrite dec_agree_idemp in H3. by inversion H3. - rewrite dec_agree_ne in H3=>//. Qed. Lemma map_agree_somebot m m' (hd: K) (p q: Q) (x: A): m !! hd = Some (p, DecAgreeBot) → m' !! hd = None → m = {[hd := (q, DecAgree x)]} ⋅ m' → False. Proof. intros H1 H2 H3. subst. rewrite lookup_op lookup_singleton in H1. destruct (m' !! hd) as [[b [c|]]|] eqn:Heqn; rewrite Heqn in H1; inversion H1=>//. Qed. Lemma map_agree_none m m' (hd: K) (q: Q) (x: A): m !! hd = None → m = {[hd := (q, DecAgree x)]} ⋅ m' → False. Proof. intros H1 H2. subst. rewrite lookup_op lookup_singleton in H1. destruct (m' !! hd)=>//. Qed. End evmap. Section evmapR. Context (K A: Type) `{Countable K, EqDecision A}. Context `{!inG Σ (authR (evmapR K A unitR))}. `````` Zhen Zhang committed Oct 19, 2016 53 `````` (* Evidence that k immutably maps to some fixed v *) `````` Zhen Zhang committed Oct 11, 2016 54 55 56 57 58 `````` Definition ev γm (k : K) (v: A) := own γm (◯ {[ k := ((), DecAgree v) ]})%I. Global Instance persistent_ev γm k v : PersistentP (ev γm k v). Proof. apply _. Qed. `````` Zhen Zhang committed Oct 19, 2016 59 60 61 `````` (* Alloc a new mapsto *) Lemma evmap_alloc γm m k v: m !! k = None → `````` Ralf Jung committed Nov 01, 2016 62 `````` own γm (● m) ⊢ |==> own γm (● (<[ k := ((), DecAgree v) ]> m) ⋅ ◯ {[ k := ((), DecAgree v) ]}). `````` Zhen Zhang committed Oct 11, 2016 63 `````` Proof. `````` Zhen Zhang committed Oct 19, 2016 64 `````` iIntros (?) "Hm". `````` Zhen Zhang committed Oct 11, 2016 65 66 67 68 `````` iDestruct (own_update with "Hm") as "?"; last by iAssumption. apply auth_update_alloc. apply alloc_singleton_local_update=>//. Qed. `````` Zhen Zhang committed Oct 19, 2016 69 `````` (* Some other supporting lemmas *) `````` Zhen Zhang committed Oct 11, 2016 70 71 `````` Lemma map_agree_none' γm (m: evmapR K A unitR) hd x: m !! hd = None → `````` Zhen Zhang committed Nov 14, 2016 72 `````` own γm (● m) ∗ ev γm hd x ⊢ False. `````` Zhen Zhang committed Oct 11, 2016 73 74 75 76 77 78 79 80 `````` Proof. iIntros (?) "[Hom Hev]". iCombine "Hom" "Hev" as "Hauth". iDestruct (own_valid with "Hauth") as %Hvalid. iPureIntro. apply auth_valid_discrete_2 in Hvalid as [[af Compose%leibniz_equiv_iff] Valid]. eapply (map_agree_none _ _ _ m)=>//. Qed. `````` Zhen Zhang committed Oct 19, 2016 81 82 `````` Lemma map_agree_eq' γm m hd x agy: m !! hd = Some ((), agy) → `````` Zhen Zhang committed Nov 14, 2016 83 `````` ev γm hd x ∗ own γm (● m) ⊢ DecAgree x = agy. `````` Zhen Zhang committed Oct 11, 2016 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 `````` Proof. iIntros (?) "[#Hev Hom]". iCombine "Hom" "Hev" as "Hauth". iDestruct (own_valid γm (● m ⋅ ◯ {[hd := (_, DecAgree x)]}) with "[Hauth]") as %Hvalid=>//. apply auth_valid_discrete_2 in Hvalid as [[af Compose%leibniz_equiv_iff] Valid]. destruct agy as [y|]. - iDestruct "Hauth" as "[? ?]". iFrame. iPureIntro. apply f_equal. eapply (map_agree_eq _ _ _ m)=>//. - iAssert (✓ m)%I as "H"=>//. rewrite (gmap_validI m). iDestruct ("H" \$! hd) as "%". exfalso. subst. rewrite H0 in H1. by destruct H1 as [? ?]. Qed. `````` Zhen Zhang committed Oct 19, 2016 99 `````` `````` Zhen Zhang committed Oct 19, 2016 100 `````` (* Evidence is the witness of membership *) `````` Zhen Zhang committed Oct 19, 2016 101 `````` Lemma ev_map_witness γm m hd x: `````` Zhen Zhang committed Nov 14, 2016 102 `````` ev γm hd x ∗ own γm (● m) ⊢ m !! hd = Some (∅, DecAgree x). `````` Zhen Zhang committed Oct 19, 2016 103 104 105 `````` Proof. iIntros "[#Hev Hom]". destruct (m !! hd) as [[[] agy]|] eqn:Heqn. `````` Zhen Zhang committed Oct 19, 2016 106 107 `````` - iDestruct (map_agree_eq' with "[-]") as %H'=>//; first by iFrame. by subst. - iExFalso. iApply map_agree_none'=>//. by iFrame. `````` Zhen Zhang committed Oct 19, 2016 108 `````` Qed. `````` Zhen Zhang committed Oct 11, 2016 109 `````` `````` Zhen Zhang committed Oct 19, 2016 110 111 `````` (* Two evidences coincides *) Lemma evmap_frag_agree_split γm p (a1 a2: A): `````` Zhen Zhang committed Nov 14, 2016 112 `````` ev γm p a1 ∗ ev γm p a2 ⊢ a1 = a2. `````` Zhen Zhang committed Oct 11, 2016 113 114 115 116 117 `````` Proof. iIntros "[Ho Ho']". destruct (decide (a1 = a2)) as [->|Hneq]. - by iFrame. - iCombine "Ho" "Ho'" as "Ho". `````` Zhen Zhang committed Oct 19, 2016 118 `````` rewrite -(@auth_frag_op (evmapR K A unitR) {[p := (_, DecAgree a1)]} {[p := (_, DecAgree a2)]}). `````` Zhen Zhang committed Oct 11, 2016 119 `````` iDestruct (own_valid with "Ho") as %Hvalid. `````` Zhen Zhang committed Oct 19, 2016 120 `````` exfalso. rewrite op_singleton in Hvalid. `````` Zhen Zhang committed Oct 11, 2016 121 122 123 124 125 126 `````` apply auth_valid_discrete in Hvalid. simpl in Hvalid. apply singleton_valid in Hvalid. destruct Hvalid as [_ Hvalid]. apply dec_agree_op_inv in Hvalid. inversion Hvalid. subst. auto. Qed. End evmapR.``````