wsat.v 8.57 KB
 Robbert Krebbers committed Mar 10, 2016 1 2 3 ``````From iris.prelude Require Export co_pset. From iris.program_logic Require Export model. From iris.algebra Require Export cmra_big_op cmra_tactics. `````` Robbert Krebbers committed Jan 18, 2016 4 ``````Local Hint Extern 10 (_ ≤ _) => omega. `````` Robbert Krebbers committed Jan 16, 2016 5 ``````Local Hint Extern 10 (✓{_} _) => solve_validN. `````` Robbert Krebbers committed Feb 11, 2016 6 7 ``````Local Hint Extern 1 (✓{_} gst _) => apply gst_validN. Local Hint Extern 1 (✓{_} wld _) => apply wld_validN. `````` Robbert Krebbers committed Jan 16, 2016 8 `````` `````` Robbert Krebbers committed Feb 01, 2016 9 10 ``````Record wsat_pre {Λ Σ} (n : nat) (E : coPset) (σ : state Λ) (rs : gmap positive (iRes Λ Σ)) (r : iRes Λ Σ) := { `````` Robbert Krebbers committed Jan 16, 2016 11 `````` wsat_pre_valid : ✓{S n} r; `````` Robbert Krebbers committed May 28, 2016 12 `````` wsat_pre_state : pst r ≡ Excl' σ; `````` Robbert Krebbers committed Jan 16, 2016 13 14 15 `````` wsat_pre_dom i : is_Some (rs !! i) → i ∈ E ∧ is_Some (wld r !! i); wsat_pre_wld i P : i ∈ E → `````` Robbert Krebbers committed Feb 10, 2016 16 `````` wld r !! i ≡{S n}≡ Some (to_agree (Next (iProp_unfold P))) → `````` Robbert Krebbers committed Jan 16, 2016 17 18 `````` ∃ r', rs !! i = Some r' ∧ P n r' }. `````` Robbert Krebbers committed Feb 01, 2016 19 20 21 22 ``````Arguments wsat_pre_valid {_ _ _ _ _ _ _} _. Arguments wsat_pre_state {_ _ _ _ _ _ _} _. Arguments wsat_pre_dom {_ _ _ _ _ _ _} _ _ _. Arguments wsat_pre_wld {_ _ _ _ _ _ _} _ _ _ _ _. `````` Robbert Krebbers committed Jan 16, 2016 23 `````` `````` Robbert Krebbers committed Feb 01, 2016 24 25 ``````Definition wsat {Λ Σ} (n : nat) (E : coPset) (σ : state Λ) (r : iRes Λ Σ) : Prop := `````` Robbert Krebbers committed Jan 16, 2016 26 `````` match n with 0 => True | S n => ∃ rs, wsat_pre n E σ rs (r ⋅ big_opM rs) end. `````` Robbert Krebbers committed Feb 01, 2016 27 ``````Instance: Params (@wsat) 5. `````` Robbert Krebbers committed Jan 18, 2016 28 ``````Arguments wsat : simpl never. `````` Robbert Krebbers committed Jan 16, 2016 29 30 `````` Section wsat. `````` Ralf Jung committed Mar 07, 2016 31 ``````Context {Λ : language} {Σ : iFunctor}. `````` Robbert Krebbers committed Feb 01, 2016 32 33 34 35 36 ``````Implicit Types σ : state Λ. Implicit Types r : iRes Λ Σ. Implicit Types rs : gmap positive (iRes Λ Σ). Implicit Types P : iProp Λ Σ. Implicit Types m : iGst Λ Σ. `````` Robbert Krebbers committed Jan 16, 2016 37 `````` `````` Robbert Krebbers committed Feb 01, 2016 38 ``````Instance wsat_ne' : Proper (dist n ==> impl) (@wsat Λ Σ n E σ). `````` Robbert Krebbers committed Jan 16, 2016 39 40 41 42 ``````Proof. intros [|n] E σ r1 r2 Hr; first done; intros [rs [Hdom Hv Hs Hinv]]. exists rs; constructor; intros until 0; setoid_rewrite <-Hr; eauto. Qed. `````` Robbert Krebbers committed Feb 01, 2016 43 ``````Global Instance wsat_ne n : Proper (dist n ==> iff) (@wsat Λ Σ n E σ) | 1. `````` Robbert Krebbers committed Jan 16, 2016 44 ``````Proof. by intros E σ w1 w2 Hw; split; apply wsat_ne'. Qed. `````` Robbert Krebbers committed Apr 19, 2016 45 ``````Global Instance wsat_proper' n : Proper ((≡) ==> iff) (@wsat Λ Σ n E σ) | 1. `````` Robbert Krebbers committed Jan 16, 2016 46 ``````Proof. by intros E σ w1 w2 Hw; apply wsat_ne, equiv_dist. Qed. `````` Robbert Krebbers committed Apr 19, 2016 47 ``````Lemma wsat_proper n E1 E2 σ r1 r2 : `````` Ralf Jung committed Apr 19, 2016 48 `````` E1 = E2 → r1 ≡ r2 → wsat n E1 σ r1 → wsat n E2 σ r2. `````` Robbert Krebbers committed Apr 19, 2016 49 ``````Proof. by move=>->->. Qed. `````` Robbert Krebbers committed Jan 18, 2016 50 51 52 53 54 ``````Lemma wsat_le n n' E σ r : wsat n E σ r → n' ≤ n → wsat n' E σ r. Proof. destruct n as [|n], n' as [|n']; simpl; try by (auto with lia). intros [rs [Hval Hσ HE Hwld]] ?; exists rs; constructor; auto. intros i P ? HiP; destruct (wld (r ⋅ big_opM rs) !! i) as [P'|] eqn:HP'; `````` Robbert Krebbers committed Feb 11, 2016 55 `````` [apply (inj Some) in HiP|inversion_clear HiP]. `````` Robbert Krebbers committed Feb 10, 2016 56 `````` assert (P' ≡{S n}≡ to_agree \$ Next \$ iProp_unfold \$ `````` Robbert Krebbers committed Jan 18, 2016 57 58 `````` iProp_fold \$ later_car \$ P' (S n)) as HPiso. { rewrite iProp_unfold_fold later_eta to_agree_car //. `````` Robbert Krebbers committed May 23, 2016 59 `````` apply (lookup_validN_Some _ (wld (r ⋅ big_opM rs)) i); rewrite ?HP'; auto. } `````` Ralf Jung committed Feb 10, 2016 60 `````` assert (P ≡{n'}≡ iProp_fold (later_car (P' (S n)))) as HPP'. `````` Robbert Krebbers committed Feb 11, 2016 61 `````` { apply (inj iProp_unfold), (inj Next), (inj to_agree). `````` Robbert Krebbers committed Jan 18, 2016 62 63 64 65 `````` by rewrite -HiP -(dist_le _ _ _ _ HPiso). } destruct (Hwld i (iProp_fold (later_car (P' (S n))))) as (r'&?&?); auto. { by rewrite HP' -HPiso. } assert (✓{S n} r') by (apply (big_opM_lookup_valid _ rs i); auto). `````` Robbert Krebbers committed May 27, 2016 66 `````` exists r'; split; [done|]. apply HPP', uPred_closed with n; auto. `````` Robbert Krebbers committed Jan 18, 2016 67 ``````Qed. `````` Robbert Krebbers committed Feb 10, 2016 68 ``````Lemma wsat_valid n E σ r : n ≠ 0 → wsat n E σ r → ✓{n} r. `````` Robbert Krebbers committed Jan 16, 2016 69 ``````Proof. `````` Robbert Krebbers committed Feb 10, 2016 70 71 `````` destruct n; first done. intros _ [rs ?]; eapply cmra_validN_op_l, wsat_pre_valid; eauto. `````` Robbert Krebbers committed Jan 16, 2016 72 ``````Qed. `````` Robbert Krebbers committed May 28, 2016 73 ``````Lemma wsat_init k E σ m : ✓{S k} m → wsat (S k) E σ (Res ∅ (Excl' σ) m). `````` Robbert Krebbers committed Jan 20, 2016 74 ``````Proof. `````` Ralf Jung committed Jan 25, 2016 75 `````` intros Hv. exists ∅; constructor; auto. `````` Robbert Krebbers committed Feb 17, 2016 76 `````` - rewrite big_opM_empty right_id. `````` Robbert Krebbers committed Feb 19, 2016 77 `````` split_and!; try (apply cmra_valid_validN, ra_empty_valid); `````` Ralf Jung committed Jan 25, 2016 78 `````` constructor || apply Hv. `````` Robbert Krebbers committed Feb 17, 2016 79 80 `````` - by intros i; rewrite lookup_empty=>-[??]. - intros i P ?; rewrite /= left_id lookup_empty; inversion_clear 1. `````` Robbert Krebbers committed Jan 20, 2016 81 ``````Qed. `````` Robbert Krebbers committed Jan 16, 2016 82 ``````Lemma wsat_open n E σ r i P : `````` Robbert Krebbers committed Feb 10, 2016 83 `````` wld r !! i ≡{S n}≡ Some (to_agree (Next (iProp_unfold P))) → i ∉ E → `````` Robbert Krebbers committed Jan 16, 2016 84 85 86 `````` wsat (S n) ({[i]} ∪ E) σ r → ∃ rP, wsat (S n) E σ (rP ⋅ r) ∧ P n rP. Proof. intros HiP Hi [rs [Hval Hσ HE Hwld]]. `````` Robbert Krebbers committed Feb 17, 2016 87 `````` destruct (Hwld i P) as (rP&?&?); [set_solver +|by apply lookup_wld_op_l|]. `````` Robbert Krebbers committed Jan 16, 2016 88 `````` assert (rP ⋅ r ⋅ big_opM (delete i rs) ≡ r ⋅ big_opM rs) as Hr. `````` Robbert Krebbers committed Feb 11, 2016 89 `````` { by rewrite (comm _ rP) -assoc big_opM_delete. } `````` Robbert Krebbers committed Jan 16, 2016 90 `````` exists rP; split; [exists (delete i rs); constructor; rewrite ?Hr|]; auto. `````` Robbert Krebbers committed Feb 17, 2016 91 `````` - intros j; rewrite lookup_delete_is_Some Hr. `````` Robbert Krebbers committed Feb 17, 2016 92 `````` generalize (HE j); set_solver +Hi. `````` Robbert Krebbers committed Feb 17, 2016 93 `````` - intros j P'; rewrite Hr=> Hj ?. `````` Robbert Krebbers committed Feb 17, 2016 94 95 `````` setoid_rewrite lookup_delete_ne; last (set_solver +Hi Hj). apply Hwld; [set_solver +Hj|done]. `````` Robbert Krebbers committed Jan 16, 2016 96 97 ``````Qed. Lemma wsat_close n E σ r i P rP : `````` Robbert Krebbers committed Feb 10, 2016 98 `````` wld rP !! i ≡{S n}≡ Some (to_agree (Next (iProp_unfold P))) → i ∉ E → `````` Robbert Krebbers committed Jan 16, 2016 99 100 101 102 103 `````` wsat (S n) E σ (rP ⋅ r) → P n rP → wsat (S n) ({[i]} ∪ E) σ r. Proof. intros HiP HiE [rs [Hval Hσ HE Hwld]] ?. assert (rs !! i = None) by (apply eq_None_not_Some; naive_solver). assert (r ⋅ big_opM (<[i:=rP]> rs) ≡ rP ⋅ r ⋅ big_opM rs) as Hr. `````` Robbert Krebbers committed Feb 11, 2016 104 `````` { by rewrite (comm _ rP) -assoc big_opM_insert. } `````` Robbert Krebbers committed Jan 16, 2016 105 `````` exists (<[i:=rP]>rs); constructor; rewrite ?Hr; auto. `````` Robbert Krebbers committed Feb 17, 2016 106 `````` - intros j; rewrite Hr lookup_insert_is_Some=>-[?|[??]]; subst. `````` Robbert Krebbers committed Feb 22, 2016 107 `````` + split. set_solver. rewrite !lookup_op HiP !op_is_Some; eauto. `````` Robbert Krebbers committed Feb 17, 2016 108 `````` + destruct (HE j) as [Hj Hj']; auto; set_solver +Hj Hj'. `````` Robbert Krebbers committed Feb 17, 2016 109 `````` - intros j P'; rewrite Hr elem_of_union elem_of_singleton=>-[?|?]; subst. `````` Robbert Krebbers committed Jan 16, 2016 110 `````` + rewrite !lookup_wld_op_l ?HiP; auto=> HP. `````` Robbert Krebbers committed Feb 11, 2016 111 `````` apply (inj Some), (inj to_agree), (inj Next), (inj iProp_unfold) in HP. `````` Robbert Krebbers committed Jan 16, 2016 112 113 114 115 `````` exists rP; split; [rewrite lookup_insert|apply HP]; auto. + intros. destruct (Hwld j P') as (r'&?&?); auto. exists r'; rewrite lookup_insert_ne; naive_solver. Qed. `````` Robbert Krebbers committed Jan 18, 2016 116 ``````Lemma wsat_update_pst n E σ1 σ1' r rf : `````` Robbert Krebbers committed May 28, 2016 117 `````` pst r ≡{S n}≡ Excl' σ1 → wsat (S n) E σ1' (r ⋅ rf) → `````` Robbert Krebbers committed Jan 18, 2016 118 `````` σ1' = σ1 ∧ ∀ σ2, wsat (S n) E σ2 (update_pst σ2 r ⋅ rf). `````` Robbert Krebbers committed Jan 16, 2016 119 ``````Proof. `````` Robbert Krebbers committed Jan 18, 2016 120 121 `````` intros Hpst_r [rs [(?&?&?) Hpst HE Hwld]]; simpl in *. assert (pst rf ⋅ pst (big_opM rs) = ∅) as Hpst'. `````` Robbert Krebbers committed Feb 26, 2016 122 `````` { by apply: (excl_validN_inv_l (S n) _ σ1); rewrite -Hpst_r assoc. } `````` Robbert Krebbers committed Jan 18, 2016 123 124 `````` assert (σ1' = σ1) as ->. { apply leibniz_equiv, (timeless _), dist_le with (S n); auto. `````` Robbert Krebbers committed May 28, 2016 125 `````` apply (inj Excl), (inj Some). `````` Robbert Krebbers committed Feb 11, 2016 126 `````` by rewrite -Hpst_r -Hpst -assoc Hpst' right_id. } `````` Robbert Krebbers committed Jan 18, 2016 127 `````` split; [done|exists rs]. `````` Robbert Krebbers committed Feb 19, 2016 128 `````` by constructor; first split_and!; try rewrite /= -assoc Hpst'. `````` Robbert Krebbers committed Jan 16, 2016 129 ``````Qed. `````` Ralf Jung committed Mar 07, 2016 130 131 ``````Lemma wsat_update_gst n E σ r rf m1 (P : iGst Λ Σ → Prop) : m1 ≼{S n} gst r → m1 ~~>: P → `````` Robbert Krebbers committed Jan 16, 2016 132 133 `````` wsat (S n) E σ (r ⋅ rf) → ∃ m2, wsat (S n) E σ (update_gst m2 r ⋅ rf) ∧ P m2. Proof. `````` Robbert Krebbers committed Feb 08, 2016 134 `````` intros [mf Hr] Hup [rs [(?&?&?) Hσ HE Hwld]]. `````` Robbert Krebbers committed May 28, 2016 135 `````` destruct (Hup (S n) (Some (mf ⋅ gst (rf ⋅ big_opM rs)))) as (m2&?&Hval'); try done. `````` Ralf Jung committed Mar 07, 2016 136 `````` { by rewrite /= (assoc _ m1) -Hr assoc. } `````` Robbert Krebbers committed Feb 19, 2016 137 138 `````` exists m2; split; [exists rs|done]. by constructor; first split_and!; auto. `````` Robbert Krebbers committed Jan 16, 2016 139 140 141 142 ``````Qed. Lemma wsat_alloc n E1 E2 σ r P rP : ¬set_finite E1 → P n rP → wsat (S n) (E1 ∪ E2) σ (rP ⋅ r) → ∃ i, wsat (S n) (E1 ∪ E2) σ `````` Robbert Krebbers committed Feb 17, 2016 143 `````` (Res {[i := to_agree (Next (iProp_unfold P))]} ∅ ∅ ⋅ r) ∧ `````` Robbert Krebbers committed Jan 16, 2016 144 145 146 147 148 149 150 151 152 153 154 155 156 157 `````` wld r !! i = None ∧ i ∈ E1. Proof. intros HE1 ? [rs [Hval Hσ HE Hwld]]. assert (∃ i, i ∈ E1 ∧ wld r !! i = None ∧ wld rP !! i = None ∧ wld (big_opM rs) !! i = None) as (i&Hi&Hri&HrPi&Hrsi). { exists (coPpick (E1 ∖ (dom _ (wld r) ∪ (dom _ (wld rP) ∪ dom _ (wld (big_opM rs)))))). rewrite -!not_elem_of_dom -?not_elem_of_union -elem_of_difference. apply coPpick_elem_of=>HE'; eapply HE1, (difference_finite_inv _ _), HE'. by repeat apply union_finite; apply dom_finite. } assert (rs !! i = None). { apply eq_None_not_Some=>?; destruct (HE i) as [_ Hri']; auto; revert Hri'. rewrite /= !lookup_op !op_is_Some -!not_eq_None_Some; tauto. } assert (r ⋅ big_opM (<[i:=rP]> rs) ≡ rP ⋅ r ⋅ big_opM rs) as Hr. `````` Robbert Krebbers committed Feb 11, 2016 158 `````` { by rewrite (comm _ rP) -assoc big_opM_insert. } `````` Robbert Krebbers committed Feb 19, 2016 159 `````` exists i; split_and?; [exists (<[i:=rP]>rs); constructor| |]; auto. `````` Robbert Krebbers committed Feb 17, 2016 160 `````` - destruct Hval as (?&?&?); rewrite -assoc Hr. `````` Robbert Krebbers committed Feb 19, 2016 161 `````` split_and!; rewrite /= ?left_id; [|eauto|eauto]. `````` Robbert Krebbers committed Jan 16, 2016 162 `````` intros j; destruct (decide (j = i)) as [->|]. `````` Robbert Krebbers committed Feb 11, 2016 163 164 `````` + by rewrite !lookup_op Hri HrPi Hrsi !right_id lookup_singleton. + by rewrite lookup_op lookup_singleton_ne // left_id. `````` Robbert Krebbers committed Feb 17, 2016 165 166 `````` - by rewrite -assoc Hr /= left_id. - intros j; rewrite -assoc Hr; destruct (decide (j = i)) as [->|]. `````` Robbert Krebbers committed Feb 22, 2016 167 168 `````` + intros _; split; first set_solver +Hi. rewrite /= !lookup_op lookup_singleton !op_is_Some; eauto. `````` Robbert Krebbers committed Jan 16, 2016 169 `````` + rewrite lookup_insert_ne //. `````` Robbert Krebbers committed Feb 01, 2016 170 `````` rewrite lookup_op lookup_singleton_ne // left_id; eauto. `````` Robbert Krebbers committed Feb 17, 2016 171 `````` - intros j P'; rewrite -assoc Hr; destruct (decide (j=i)) as [->|]. `````` Robbert Krebbers committed Feb 01, 2016 172 `````` + rewrite /= !lookup_op Hri HrPi Hrsi right_id lookup_singleton=>? HP. `````` Robbert Krebbers committed Feb 11, 2016 173 `````` apply (inj Some), (inj to_agree), (inj Next), (inj iProp_unfold) in HP. `````` Robbert Krebbers committed Jan 16, 2016 174 `````` exists rP; rewrite lookup_insert; split; [|apply HP]; auto. `````` Robbert Krebbers committed Feb 01, 2016 175 `````` + rewrite /= lookup_op lookup_singleton_ne // left_id=> ??. `````` Robbert Krebbers committed Jan 16, 2016 176 177 178 179 `````` destruct (Hwld j P') as [r' ?]; auto. by exists r'; rewrite lookup_insert_ne. Qed. End wsat.``````