upred_big_op.v 16.8 KB
 Robbert Krebbers committed Mar 21, 2016 1 ``````From iris.algebra Require Export upred list. `````` Robbert Krebbers committed Apr 11, 2016 2 ``````From iris.prelude Require Import gmap fin_collections functions. `````` Ralf Jung committed Feb 17, 2016 3 ``````Import uPred. `````` Robbert Krebbers committed Feb 14, 2016 4 `````` `````` Robbert Krebbers committed May 24, 2016 5 6 7 8 9 10 11 12 13 14 15 ``````(** We define the following big operators: - The operators [ [★] Ps ] and [ [∧] Ps ] fold [★] and [∧] over the list [Ps]. This operator is not a quantifier, so it binds strongly. - The operator [ [★ map] k ↦ x ∈ m, P ] asserts that [P] holds separately for each [k ↦ x] in the map [m]. This operator is a quantifier, and thus has the same precedence as [∀] and [∃]. - The operator [ [★ set] x ∈ X, P ] asserts that [P] holds separately for each [x] in the set [X]. This operator is a quantifier, and thus has the same precedence as [∀] and [∃]. *) `````` Robbert Krebbers committed Feb 16, 2016 16 17 ``````(** * Big ops over lists *) (* These are the basic building blocks for other big ops *) `````` Robbert Krebbers committed May 24, 2016 18 ``````Fixpoint uPred_big_and {M} (Ps : list (uPred M)) : uPred M := `````` Robbert Krebbers committed Feb 16, 2016 19 20 `````` match Ps with [] => True | P :: Ps => P ∧ uPred_big_and Ps end%I. Instance: Params (@uPred_big_and) 1. `````` Robbert Krebbers committed May 24, 2016 21 ``````Notation "'[∧]' Ps" := (uPred_big_and Ps) (at level 20) : uPred_scope. `````` Robbert Krebbers committed Feb 16, 2016 22 23 24 ``````Fixpoint uPred_big_sep {M} (Ps : list (uPred M)) : uPred M := match Ps with [] => True | P :: Ps => P ★ uPred_big_sep Ps end%I. Instance: Params (@uPred_big_sep) 1. `````` Robbert Krebbers committed May 24, 2016 25 ``````Notation "'[★]' Ps" := (uPred_big_sep Ps) (at level 20) : uPred_scope. `````` Robbert Krebbers committed Feb 14, 2016 26 `````` `````` Robbert Krebbers committed Feb 16, 2016 27 28 ``````(** * Other big ops *) (** We use a type class to obtain overloaded notations *) `````` Robbert Krebbers committed Feb 17, 2016 29 ``````Definition uPred_big_sepM {M} `{Countable K} {A} `````` Robbert Krebbers committed Feb 18, 2016 30 `````` (m : gmap K A) (Φ : K → A → uPred M) : uPred M := `````` Robbert Krebbers committed May 24, 2016 31 `````` [★] (curry Φ <\$> map_to_list m). `````` Robbert Krebbers committed Feb 17, 2016 32 ``````Instance: Params (@uPred_big_sepM) 6. `````` Robbert Krebbers committed May 24, 2016 33 34 35 ``````Notation "'[★' 'map' ] k ↦ x ∈ m , P" := (uPred_big_sepM m (λ k x, P)) (at level 200, m at level 10, k, x at level 1, right associativity, format "[★ map ] k ↦ x ∈ m , P") : uPred_scope. `````` Robbert Krebbers committed Feb 14, 2016 36 `````` `````` Robbert Krebbers committed Feb 17, 2016 37 ``````Definition uPred_big_sepS {M} `{Countable A} `````` Robbert Krebbers committed May 24, 2016 38 `````` (X : gset A) (Φ : A → uPred M) : uPred M := [★] (Φ <\$> elements X). `````` Robbert Krebbers committed Feb 17, 2016 39 ``````Instance: Params (@uPred_big_sepS) 5. `````` Robbert Krebbers committed May 24, 2016 40 41 42 ``````Notation "'[★' 'set' ] x ∈ X , P" := (uPred_big_sepS X (λ x, P)) (at level 200, X at level 10, x at level 1, right associativity, format "[★ set ] x ∈ X , P") : uPred_scope. `````` Robbert Krebbers committed Feb 16, 2016 43 `````` `````` Robbert Krebbers committed Apr 08, 2016 44 ``````(** * Persistence of lists of uPreds *) `````` Robbert Krebbers committed Mar 11, 2016 45 ``````Class PersistentL {M} (Ps : list (uPred M)) := `````` Robbert Krebbers committed Mar 15, 2016 46 `````` persistentL : Forall PersistentP Ps. `````` Robbert Krebbers committed Mar 11, 2016 47 ``````Arguments persistentL {_} _ {_}. `````` Robbert Krebbers committed Feb 14, 2016 48 `````` `````` Robbert Krebbers committed Apr 08, 2016 49 ``````(** * Properties *) `````` Robbert Krebbers committed Feb 14, 2016 50 ``````Section big_op. `````` Robbert Krebbers committed May 27, 2016 51 ``````Context {M : ucmraT}. `````` Robbert Krebbers committed Feb 14, 2016 52 53 54 ``````Implicit Types Ps Qs : list (uPred M). Implicit Types A : Type. `````` Robbert Krebbers committed Apr 08, 2016 55 ``````(** ** Big ops over lists *) `````` Ralf Jung committed Mar 10, 2016 56 ``````Global Instance big_and_proper : Proper ((≡) ==> (⊣⊢)) (@uPred_big_and M). `````` Robbert Krebbers committed Feb 14, 2016 57 ``````Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed. `````` Ralf Jung committed Mar 10, 2016 58 ``````Global Instance big_sep_proper : Proper ((≡) ==> (⊣⊢)) (@uPred_big_sep M). `````` Robbert Krebbers committed Feb 14, 2016 59 ``````Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed. `````` Robbert Krebbers committed Feb 17, 2016 60 `````` `````` Robbert Krebbers committed Mar 21, 2016 61 ``````Global Instance big_and_ne n : Proper (dist n ==> dist n) (@uPred_big_and M). `````` Robbert Krebbers committed Feb 17, 2016 62 ``````Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed. `````` Robbert Krebbers committed Mar 21, 2016 63 ``````Global Instance big_sep_ne n : Proper (dist n ==> dist n) (@uPred_big_sep M). `````` Robbert Krebbers committed Feb 17, 2016 64 65 ``````Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed. `````` Ralf Jung committed Mar 10, 2016 66 ``````Global Instance big_and_mono' : Proper (Forall2 (⊢) ==> (⊢)) (@uPred_big_and M). `````` Robbert Krebbers committed Feb 17, 2016 67 ``````Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed. `````` Ralf Jung committed Mar 10, 2016 68 ``````Global Instance big_sep_mono' : Proper (Forall2 (⊢) ==> (⊢)) (@uPred_big_sep M). `````` Robbert Krebbers committed Feb 17, 2016 69 70 ``````Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed. `````` Ralf Jung committed Mar 10, 2016 71 ``````Global Instance big_and_perm : Proper ((≡ₚ) ==> (⊣⊢)) (@uPred_big_and M). `````` Robbert Krebbers committed Feb 14, 2016 72 73 ``````Proof. induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto. `````` Robbert Krebbers committed Feb 17, 2016 74 75 `````` - by rewrite IH. - by rewrite !assoc (comm _ P). `````` Ralf Jung committed Feb 20, 2016 76 `````` - etrans; eauto. `````` Robbert Krebbers committed Feb 14, 2016 77 ``````Qed. `````` Ralf Jung committed Mar 10, 2016 78 ``````Global Instance big_sep_perm : Proper ((≡ₚ) ==> (⊣⊢)) (@uPred_big_sep M). `````` Robbert Krebbers committed Feb 14, 2016 79 80 ``````Proof. induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto. `````` Robbert Krebbers committed Feb 17, 2016 81 82 `````` - by rewrite IH. - by rewrite !assoc (comm _ P). `````` Ralf Jung committed Feb 20, 2016 83 `````` - etrans; eauto. `````` Robbert Krebbers committed Feb 14, 2016 84 ``````Qed. `````` Robbert Krebbers committed Feb 17, 2016 85 `````` `````` Robbert Krebbers committed May 31, 2016 86 ``````Lemma big_and_app Ps Qs : [∧] (Ps ++ Qs) ⊣⊢ [∧] Ps ∧ [∧] Qs. `````` Robbert Krebbers committed May 24, 2016 87 ``````Proof. induction Ps as [|?? IH]; by rewrite /= ?left_id -?assoc ?IH. Qed. `````` Robbert Krebbers committed May 31, 2016 88 ``````Lemma big_sep_app Ps Qs : [★] (Ps ++ Qs) ⊣⊢ [★] Ps ★ [★] Qs. `````` Robbert Krebbers committed Feb 14, 2016 89 ``````Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed. `````` Robbert Krebbers committed Feb 17, 2016 90 `````` `````` Robbert Krebbers committed May 24, 2016 91 ``````Lemma big_and_contains Ps Qs : Qs `contains` Ps → [∧] Ps ⊢ [∧] Qs. `````` Robbert Krebbers committed Feb 17, 2016 92 ``````Proof. `````` Ralf Jung committed Feb 17, 2016 93 `````` intros [Ps' ->]%contains_Permutation. by rewrite big_and_app and_elim_l. `````` Robbert Krebbers committed Feb 17, 2016 94 ``````Qed. `````` Robbert Krebbers committed May 24, 2016 95 ``````Lemma big_sep_contains Ps Qs : Qs `contains` Ps → [★] Ps ⊢ [★] Qs. `````` Robbert Krebbers committed Feb 17, 2016 96 ``````Proof. `````` Ralf Jung committed Feb 17, 2016 97 `````` intros [Ps' ->]%contains_Permutation. by rewrite big_sep_app sep_elim_l. `````` Robbert Krebbers committed Feb 17, 2016 98 99 ``````Qed. `````` Robbert Krebbers committed May 24, 2016 100 ``````Lemma big_sep_and Ps : [★] Ps ⊢ [∧] Ps. `````` Robbert Krebbers committed Feb 14, 2016 101 ``````Proof. by induction Ps as [|P Ps IH]; simpl; auto with I. Qed. `````` Robbert Krebbers committed Feb 17, 2016 102 `````` `````` Robbert Krebbers committed May 24, 2016 103 ``````Lemma big_and_elem_of Ps P : P ∈ Ps → [∧] Ps ⊢ P. `````` Robbert Krebbers committed Feb 14, 2016 104 ``````Proof. induction 1; simpl; auto with I. Qed. `````` Robbert Krebbers committed May 24, 2016 105 ``````Lemma big_sep_elem_of Ps P : P ∈ Ps → [★] Ps ⊢ P. `````` Robbert Krebbers committed Feb 14, 2016 106 107 ``````Proof. induction 1; simpl; auto with I. Qed. `````` Robbert Krebbers committed Apr 08, 2016 108 ``````(** ** Big ops over finite maps *) `````` Robbert Krebbers committed Feb 17, 2016 109 110 111 ``````Section gmap. Context `{Countable K} {A : Type}. Implicit Types m : gmap K A. `````` Robbert Krebbers committed Feb 18, 2016 112 `````` Implicit Types Φ Ψ : K → A → uPred M. `````` Robbert Krebbers committed Feb 14, 2016 113 `````` `````` Robbert Krebbers committed Feb 18, 2016 114 `````` Lemma big_sepM_mono Φ Ψ m1 m2 : `````` Robbert Krebbers committed May 30, 2016 115 `````` m2 ⊆ m1 → (∀ k x, m2 !! k = Some x → Φ k x ⊢ Ψ k x) → `````` Robbert Krebbers committed May 31, 2016 116 `````` ([★ map] k ↦ x ∈ m1, Φ k x) ⊢ [★ map] k ↦ x ∈ m2, Ψ k x. `````` Robbert Krebbers committed Feb 16, 2016 117 `````` Proof. `````` Robbert Krebbers committed May 24, 2016 118 `````` intros HX HΦ. trans ([★ map] k↦x ∈ m2, Φ k x)%I. `````` Robbert Krebbers committed Feb 17, 2016 119 `````` - by apply big_sep_contains, fmap_contains, map_to_list_contains. `````` Robbert Krebbers committed Mar 21, 2016 120 `````` - apply big_sep_mono', Forall2_fmap, Forall_Forall2. `````` Robbert Krebbers committed Feb 18, 2016 121 `````` apply Forall_forall=> -[i x] ? /=. by apply HΦ, elem_of_map_to_list. `````` Robbert Krebbers committed Feb 16, 2016 122 `````` Qed. `````` Robbert Krebbers committed Apr 11, 2016 123 `````` Lemma big_sepM_proper Φ Ψ m1 m2 : `````` Robbert Krebbers committed May 30, 2016 124 `````` m1 ≡ m2 → (∀ k x, m1 !! k = Some x → m2 !! k = Some x → Φ k x ⊣⊢ Ψ k x) → `````` Robbert Krebbers committed May 24, 2016 125 `````` ([★ map] k ↦ x ∈ m1, Φ k x) ⊣⊢ ([★ map] k ↦ x ∈ m2, Ψ k x). `````` Robbert Krebbers committed Apr 11, 2016 126 `````` Proof. `````` Robbert Krebbers committed Apr 18, 2016 127 128 129 `````` (* FIXME: Coq bug since 8.5pl1. Without the @ in [@lookup_weaken] it gives File "./algebra/upred_big_op.v", line 114, characters 4-131: Anomaly: Uncaught exception Univ.AlreadyDeclared. Please report. *) `````` Robbert Krebbers committed Apr 11, 2016 130 `````` intros [??] ?; apply (anti_symm (⊢)); apply big_sepM_mono; `````` Robbert Krebbers committed Apr 18, 2016 131 `````` eauto using equiv_entails, equiv_entails_sym, @lookup_weaken. `````` Robbert Krebbers committed Apr 11, 2016 132 `````` Qed. `````` Robbert Krebbers committed Feb 17, 2016 133 134 135 136 137 `````` Global Instance big_sepM_ne m n : Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n)) (uPred_big_sepM (M:=M) m). Proof. `````` Robbert Krebbers committed Feb 18, 2016 138 `````` intros Φ1 Φ2 HΦ. apply big_sep_ne, Forall2_fmap. `````` Robbert Krebbers committed Mar 21, 2016 139 `````` apply Forall_Forall2, Forall_true=> -[i x]; apply HΦ. `````` Robbert Krebbers committed Feb 17, 2016 140 `````` Qed. `````` Robbert Krebbers committed Apr 11, 2016 141 `````` Global Instance big_sepM_proper' m : `````` Ralf Jung committed Mar 10, 2016 142 `````` Proper (pointwise_relation _ (pointwise_relation _ (⊣⊢)) ==> (⊣⊢)) `````` Robbert Krebbers committed Feb 17, 2016 143 `````` (uPred_big_sepM (M:=M) m). `````` Robbert Krebbers committed Apr 11, 2016 144 `````` Proof. intros Φ1 Φ2 HΦ. by apply big_sepM_proper; intros; last apply HΦ. Qed. `````` Robbert Krebbers committed Feb 17, 2016 145 `````` Global Instance big_sepM_mono' m : `````` Ralf Jung committed Mar 10, 2016 146 `````` Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (⊢)) `````` Robbert Krebbers committed Feb 17, 2016 147 `````` (uPred_big_sepM (M:=M) m). `````` Robbert Krebbers committed Apr 11, 2016 148 `````` Proof. intros Φ1 Φ2 HΦ. by apply big_sepM_mono; intros; last apply HΦ. Qed. `````` Robbert Krebbers committed Feb 17, 2016 149 `````` `````` Robbert Krebbers committed May 24, 2016 150 `````` Lemma big_sepM_empty Φ : ([★ map] k↦x ∈ ∅, Φ k x) ⊣⊢ True. `````` Robbert Krebbers committed Feb 17, 2016 151 `````` Proof. by rewrite /uPred_big_sepM map_to_list_empty. Qed. `````` Robbert Krebbers committed May 30, 2016 152 `````` `````` Robbert Krebbers committed May 31, 2016 153 `````` Lemma big_sepM_insert Φ m i x : `````` Robbert Krebbers committed May 24, 2016 154 `````` m !! i = None → `````` Robbert Krebbers committed May 31, 2016 155 `````` ([★ map] k↦y ∈ <[i:=x]> m, Φ k y) ⊣⊢ Φ i x ★ [★ map] k↦y ∈ m, Φ k y. `````` Robbert Krebbers committed Feb 17, 2016 156 `````` Proof. intros ?; by rewrite /uPred_big_sepM map_to_list_insert. Qed. `````` Robbert Krebbers committed May 30, 2016 157 `````` `````` Robbert Krebbers committed May 31, 2016 158 `````` Lemma big_sepM_delete Φ m i x : `````` Robbert Krebbers committed May 24, 2016 159 `````` m !! i = Some x → `````` Robbert Krebbers committed May 31, 2016 160 `````` ([★ map] k↦y ∈ m, Φ k y) ⊣⊢ Φ i x ★ [★ map] k↦y ∈ delete i m, Φ k y. `````` Robbert Krebbers committed May 31, 2016 161 162 163 164 `````` Proof. intros. rewrite -big_sepM_insert ?lookup_delete //. by rewrite insert_delete insert_id. Qed. `````` Robbert Krebbers committed May 30, 2016 165 `````` `````` Robbert Krebbers committed May 31, 2016 166 167 168 169 `````` Lemma big_sepM_lookup Φ m i x : m !! i = Some x → ([★ map] k↦y ∈ m, Φ k y) ⊢ Φ i x. Proof. intros. by rewrite big_sepM_delete // sep_elim_l. Qed. `````` Robbert Krebbers committed May 24, 2016 170 `````` Lemma big_sepM_singleton Φ i x : ([★ map] k↦y ∈ {[i:=x]}, Φ k y) ⊣⊢ Φ i x. `````` Robbert Krebbers committed Feb 14, 2016 171 172 173 174 `````` Proof. rewrite -insert_empty big_sepM_insert/=; last auto using lookup_empty. by rewrite big_sepM_empty right_id. Qed. `````` Ralf Jung committed Feb 17, 2016 175 `````` `````` Robbert Krebbers committed May 31, 2016 176 177 178 179 180 181 182 `````` Lemma big_sepM_fmap {B} (f : A → B) (Φ : K → B → uPred M) m : ([★ map] k↦y ∈ f <\$> m, Φ k y) ⊣⊢ ([★ map] k↦y ∈ m, Φ k (f y)). Proof. rewrite /uPred_big_sepM map_to_list_fmap -list_fmap_compose. f_equiv; apply reflexive_eq, list_fmap_ext. by intros []. done. Qed. `````` Robbert Krebbers committed May 31, 2016 183 `````` Lemma big_sepM_insert_override (Φ : K → uPred M) m i x y : `````` Robbert Krebbers committed May 31, 2016 184 `````` m !! i = Some x → `````` Robbert Krebbers committed May 31, 2016 185 `````` ([★ map] k↦_ ∈ <[i:=y]> m, Φ k) ⊣⊢ ([★ map] k↦_ ∈ m, Φ k). `````` Robbert Krebbers committed May 31, 2016 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 `````` Proof. intros. rewrite -insert_delete big_sepM_insert ?lookup_delete //. by rewrite -big_sepM_delete. Qed. Lemma big_sepM_fn_insert (Ψ : K → A → uPred M → uPred M) (Φ : K → uPred M) m i x P : m !! i = None → ([★ map] k↦y ∈ <[i:=x]> m, Ψ k y (<[i:=P]> Φ k)) ⊣⊢ (Ψ i x P ★ [★ map] k↦y ∈ m, Ψ k y (Φ k)). Proof. intros. rewrite big_sepM_insert // fn_lookup_insert. apply sep_proper, big_sepM_proper; auto=> k y ??. by rewrite fn_lookup_insert_ne; last set_solver. Qed. Lemma big_sepM_fn_insert' (Φ : K → uPred M) m i x P : m !! i = None → ([★ map] k↦y ∈ <[i:=x]> m, <[i:=P]> Φ k) ⊣⊢ (P ★ [★ map] k↦y ∈ m, Φ k). Proof. apply (big_sepM_fn_insert (λ _ _, id)). Qed. `````` Robbert Krebbers committed Feb 18, 2016 205 `````` Lemma big_sepM_sepM Φ Ψ m : `````` Robbert Krebbers committed May 24, 2016 206 `````` ([★ map] k↦x ∈ m, Φ k x ★ Ψ k x) `````` Robbert Krebbers committed May 31, 2016 207 `````` ⊣⊢ ([★ map] k↦x ∈ m, Φ k x) ★ ([★ map] k↦x ∈ m, Ψ k x). `````` Ralf Jung committed Feb 17, 2016 208 `````` Proof. `````` Robbert Krebbers committed Feb 17, 2016 209 210 `````` rewrite /uPred_big_sepM. induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?right_id //. `````` Robbert Krebbers committed Feb 18, 2016 211 `````` by rewrite IH -!assoc (assoc _ (Ψ _ _)) [(Ψ _ _ ★ _)%I]comm -!assoc. `````` Ralf Jung committed Feb 17, 2016 212 `````` Qed. `````` Robbert Krebbers committed May 31, 2016 213 `````` `````` Robbert Krebbers committed May 24, 2016 214 `````` Lemma big_sepM_later Φ m : `````` Robbert Krebbers committed May 31, 2016 215 `````` ▷ ([★ map] k↦x ∈ m, Φ k x) ⊣⊢ ([★ map] k↦x ∈ m, ▷ Φ k x). `````` Ralf Jung committed Feb 17, 2016 216 `````` Proof. `````` Robbert Krebbers committed Feb 17, 2016 217 218 219 `````` rewrite /uPred_big_sepM. induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?later_True //. by rewrite later_sep IH. `````` Ralf Jung committed Feb 17, 2016 220 `````` Qed. `````` Robbert Krebbers committed May 31, 2016 221 222 223 224 225 226 227 228 229 230 `````` Lemma big_sepM_always Φ m : (□ [★ map] k↦x ∈ m, Φ k x) ⊣⊢ ([★ map] k↦x ∈ m, □ Φ k x). Proof. rewrite /uPred_big_sepM. induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?always_const //. by rewrite always_sep IH. Qed. Lemma big_sepM_always_if p Φ m : `````` Robbert Krebbers committed May 31, 2016 231 `````` □?p ([★ map] k↦x ∈ m, Φ k x) ⊣⊢ ([★ map] k↦x ∈ m, □?p Φ k x). `````` Robbert Krebbers committed May 31, 2016 232 `````` Proof. destruct p; simpl; auto using big_sepM_always. Qed. `````` Robbert Krebbers committed May 31, 2016 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 `````` Lemma big_sepM_forall Φ m : (∀ k x, PersistentP (Φ k x)) → ([★ map] k↦x ∈ m, Φ k x) ⊣⊢ (∀ k x, m !! k = Some x → Φ k x). Proof. intros. apply (anti_symm _). { apply forall_intro=> k; apply forall_intro=> x. apply impl_intro_l, const_elim_l=> ?; by apply big_sepM_lookup. } rewrite /uPred_big_sepM. setoid_rewrite <-elem_of_map_to_list. induction (map_to_list m) as [|[i x] l IH]; csimpl; auto. rewrite -always_and_sep_l; apply and_intro. - rewrite (forall_elim i) (forall_elim x) const_equiv; last by left. by rewrite True_impl. - rewrite -IH. apply forall_mono=> k; apply forall_mono=> y. apply impl_intro_l, const_elim_l=> ?. rewrite const_equiv; last by right. by rewrite True_impl. Qed. Lemma big_sepM_impl Φ Ψ m : `````` Robbert Krebbers committed May 31, 2016 252 `````` □ (∀ k x, m !! k = Some x → Φ k x → Ψ k x) ∧ ([★ map] k↦x ∈ m, Φ k x) `````` Robbert Krebbers committed May 31, 2016 253 254 255 256 257 258 259 `````` ⊢ [★ map] k↦x ∈ m, Ψ k x. Proof. rewrite always_and_sep_l. do 2 setoid_rewrite always_forall. setoid_rewrite always_impl; setoid_rewrite always_const. rewrite -big_sepM_forall -big_sepM_sepM. apply big_sepM_mono; auto=> k x ?. by rewrite -always_wand_impl always_elim wand_elim_l. Qed. `````` Robbert Krebbers committed Feb 17, 2016 260 261 ``````End gmap. `````` Robbert Krebbers committed Apr 08, 2016 262 ``````(** ** Big ops over finite sets *) `````` Robbert Krebbers committed Feb 17, 2016 263 264 265 ``````Section gset. Context `{Countable A}. Implicit Types X : gset A. `````` Robbert Krebbers committed Feb 18, 2016 266 `````` Implicit Types Φ : A → uPred M. `````` Robbert Krebbers committed Feb 17, 2016 267 `````` `````` Robbert Krebbers committed Feb 18, 2016 268 `````` Lemma big_sepS_mono Φ Ψ X Y : `````` Robbert Krebbers committed May 24, 2016 269 `````` Y ⊆ X → (∀ x, x ∈ Y → Φ x ⊢ Ψ x) → `````` Robbert Krebbers committed May 31, 2016 270 `````` ([★ set] x ∈ X, Φ x) ⊢ [★ set] x ∈ Y, Ψ x. `````` Robbert Krebbers committed Feb 17, 2016 271 `````` Proof. `````` Robbert Krebbers committed May 24, 2016 272 `````` intros HX HΦ. trans ([★ set] x ∈ Y, Φ x)%I. `````` Robbert Krebbers committed Feb 17, 2016 273 `````` - by apply big_sep_contains, fmap_contains, elements_contains. `````` Robbert Krebbers committed Mar 21, 2016 274 `````` - apply big_sep_mono', Forall2_fmap, Forall_Forall2. `````` Robbert Krebbers committed Feb 18, 2016 275 `````` apply Forall_forall=> x ? /=. by apply HΦ, elem_of_elements. `````` Robbert Krebbers committed Feb 17, 2016 276 `````` Qed. `````` Robbert Krebbers committed Apr 11, 2016 277 `````` Lemma big_sepS_proper Φ Ψ X Y : `````` Robbert Krebbers committed May 24, 2016 278 279 `````` X ≡ Y → (∀ x, x ∈ X → x ∈ Y → Φ x ⊣⊢ Ψ x) → ([★ set] x ∈ X, Φ x) ⊣⊢ ([★ set] x ∈ Y, Ψ x). `````` Robbert Krebbers committed Apr 11, 2016 280 281 282 283 `````` Proof. intros [??] ?; apply (anti_symm (⊢)); apply big_sepS_mono; eauto using equiv_entails, equiv_entails_sym. Qed. `````` Robbert Krebbers committed Feb 17, 2016 284 285 286 287 `````` Lemma big_sepS_ne X n : Proper (pointwise_relation _ (dist n) ==> dist n) (uPred_big_sepS (M:=M) X). Proof. `````` Robbert Krebbers committed Feb 18, 2016 288 `````` intros Φ1 Φ2 HΦ. apply big_sep_ne, Forall2_fmap. `````` Robbert Krebbers committed Mar 21, 2016 289 `````` apply Forall_Forall2, Forall_true=> x; apply HΦ. `````` Robbert Krebbers committed Feb 17, 2016 290 `````` Qed. `````` Robbert Krebbers committed Apr 11, 2016 291 `````` Lemma big_sepS_proper' X : `````` Ralf Jung committed Mar 10, 2016 292 `````` Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (uPred_big_sepS (M:=M) X). `````` Robbert Krebbers committed Apr 11, 2016 293 `````` Proof. intros Φ1 Φ2 HΦ. apply big_sepS_proper; naive_solver. Qed. `````` Robbert Krebbers committed Feb 17, 2016 294 `````` Lemma big_sepS_mono' X : `````` Ralf Jung committed Mar 10, 2016 295 `````` Proper (pointwise_relation _ (⊢) ==> (⊢)) (uPred_big_sepS (M:=M) X). `````` Robbert Krebbers committed Feb 18, 2016 296 `````` Proof. intros Φ1 Φ2 HΦ. apply big_sepS_mono; naive_solver. Qed. `````` Robbert Krebbers committed Feb 17, 2016 297 `````` `````` Robbert Krebbers committed May 24, 2016 298 `````` Lemma big_sepS_empty Φ : ([★ set] x ∈ ∅, Φ x) ⊣⊢ True. `````` Robbert Krebbers committed Feb 17, 2016 299 `````` Proof. by rewrite /uPred_big_sepS elements_empty. Qed. `````` Robbert Krebbers committed Apr 11, 2016 300 `````` `````` Robbert Krebbers committed Feb 18, 2016 301 `````` Lemma big_sepS_insert Φ X x : `````` Robbert Krebbers committed May 24, 2016 302 `````` x ∉ X → ([★ set] y ∈ {[ x ]} ∪ X, Φ y) ⊣⊢ (Φ x ★ [★ set] y ∈ X, Φ y). `````` Robbert Krebbers committed Feb 17, 2016 303 `````` Proof. intros. by rewrite /uPred_big_sepS elements_union_singleton. Qed. `````` Robbert Krebbers committed May 30, 2016 304 `````` Lemma big_sepS_fn_insert (Ψ : A → uPred M → uPred M) Φ X x P : `````` Robbert Krebbers committed Apr 11, 2016 305 `````` x ∉ X → `````` Robbert Krebbers committed May 24, 2016 306 307 `````` ([★ set] y ∈ {[ x ]} ∪ X, Ψ y (<[x:=P]> Φ y)) ⊣⊢ (Ψ x P ★ [★ set] y ∈ X, Ψ y (Φ y)). `````` Robbert Krebbers committed Apr 11, 2016 308 309 310 311 312 `````` Proof. intros. rewrite big_sepS_insert // fn_lookup_insert. apply sep_proper, big_sepS_proper; auto=> y ??. by rewrite fn_lookup_insert_ne; last set_solver. Qed. `````` Robbert Krebbers committed May 30, 2016 313 `````` Lemma big_sepS_fn_insert' Φ X x P : `````` Robbert Krebbers committed May 24, 2016 314 `````` x ∉ X → ([★ set] y ∈ {[ x ]} ∪ X, <[x:=P]> Φ y) ⊣⊢ (P ★ [★ set] y ∈ X, Φ y). `````` Robbert Krebbers committed May 30, 2016 315 `````` Proof. apply (big_sepS_fn_insert (λ y, id)). Qed. `````` Robbert Krebbers committed Apr 11, 2016 316 `````` `````` Robbert Krebbers committed Feb 18, 2016 317 `````` Lemma big_sepS_delete Φ X x : `````` Robbert Krebbers committed May 31, 2016 318 `````` x ∈ X → ([★ set] y ∈ X, Φ y) ⊣⊢ Φ x ★ [★ set] y ∈ X ∖ {[ x ]}, Φ y. `````` Robbert Krebbers committed Feb 17, 2016 319 `````` Proof. `````` Robbert Krebbers committed Feb 17, 2016 320 321 `````` intros. rewrite -big_sepS_insert; last set_solver. by rewrite -union_difference_L; last set_solver. `````` Robbert Krebbers committed Feb 17, 2016 322 `````` Qed. `````` Robbert Krebbers committed Apr 11, 2016 323 `````` `````` Robbert Krebbers committed May 31, 2016 324 325 326 `````` Lemma big_sepS_elem_of Φ X x : x ∈ X → ([★ set] y ∈ X, Φ y) ⊢ Φ x. Proof. intros. by rewrite big_sepS_delete // sep_elim_l. Qed. `````` Robbert Krebbers committed May 24, 2016 327 `````` Lemma big_sepS_singleton Φ x : ([★ set] y ∈ {[ x ]}, Φ y) ⊣⊢ Φ x. `````` Robbert Krebbers committed Feb 17, 2016 328 `````` Proof. intros. by rewrite /uPred_big_sepS elements_singleton /= right_id. Qed. `````` Ralf Jung committed Feb 17, 2016 329 `````` `````` Robbert Krebbers committed Feb 18, 2016 330 `````` Lemma big_sepS_sepS Φ Ψ X : `````` Robbert Krebbers committed May 31, 2016 331 `````` ([★ set] y ∈ X, Φ y ★ Ψ y) ⊣⊢ ([★ set] y ∈ X, Φ y) ★ ([★ set] y ∈ X, Ψ y). `````` Ralf Jung committed Feb 17, 2016 332 `````` Proof. `````` Robbert Krebbers committed Feb 17, 2016 333 334 `````` rewrite /uPred_big_sepS. induction (elements X) as [|x l IH]; csimpl; first by rewrite ?right_id. `````` Robbert Krebbers committed Feb 18, 2016 335 `````` by rewrite IH -!assoc (assoc _ (Ψ _)) [(Ψ _ ★ _)%I]comm -!assoc. `````` Ralf Jung committed Feb 17, 2016 336 337 `````` Qed. `````` Robbert Krebbers committed May 31, 2016 338 `````` Lemma big_sepS_later Φ X : ▷ ([★ set] y ∈ X, Φ y) ⊣⊢ ([★ set] y ∈ X, ▷ Φ y). `````` Ralf Jung committed Feb 17, 2016 339 `````` Proof. `````` Robbert Krebbers committed Feb 17, 2016 340 341 342 `````` rewrite /uPred_big_sepS. induction (elements X) as [|x l IH]; csimpl; first by rewrite ?later_True. by rewrite later_sep IH. `````` Ralf Jung committed Feb 17, 2016 343 `````` Qed. `````` Robbert Krebbers committed May 31, 2016 344 `````` `````` Robbert Krebbers committed May 31, 2016 345 `````` Lemma big_sepS_always Φ X : □ ([★ set] y ∈ X, Φ y) ⊣⊢ ([★ set] y ∈ X, □ Φ y). `````` Robbert Krebbers committed May 31, 2016 346 347 348 349 350 351 352 `````` Proof. rewrite /uPred_big_sepS. induction (elements X) as [|x l IH]; csimpl; first by rewrite ?always_const. by rewrite always_sep IH. Qed. Lemma big_sepS_always_if q Φ X : `````` Robbert Krebbers committed May 31, 2016 353 `````` □?q ([★ set] y ∈ X, Φ y) ⊣⊢ ([★ set] y ∈ X, □?q Φ y). `````` Robbert Krebbers committed May 31, 2016 354 `````` Proof. destruct q; simpl; auto using big_sepS_always. Qed. `````` Robbert Krebbers committed May 31, 2016 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 `````` Lemma big_sepS_forall Φ X : (∀ x, PersistentP (Φ x)) → ([★ set] x ∈ X, Φ x) ⊣⊢ (∀ x, ■ (x ∈ X) → Φ x). Proof. intros. apply (anti_symm _). { apply forall_intro=> x. apply impl_intro_l, const_elim_l=> ?; by apply big_sepS_elem_of. } rewrite /uPred_big_sepS. setoid_rewrite <-elem_of_elements. induction (elements X) as [|x l IH]; csimpl; auto. rewrite -always_and_sep_l; apply and_intro. - rewrite (forall_elim x) const_equiv; last by left. by rewrite True_impl. - rewrite -IH. apply forall_mono=> y. apply impl_intro_l, const_elim_l=> ?. rewrite const_equiv; last by right. by rewrite True_impl. Qed. Lemma big_sepS_impl Φ Ψ X : `````` Robbert Krebbers committed May 31, 2016 372 `````` □ (∀ x, ■ (x ∈ X) → Φ x → Ψ x) ∧ ([★ set] x ∈ X, Φ x) ⊢ [★ set] x ∈ X, Ψ x. `````` Robbert Krebbers committed May 31, 2016 373 374 375 376 377 378 `````` Proof. rewrite always_and_sep_l always_forall. setoid_rewrite always_impl; setoid_rewrite always_const. rewrite -big_sepS_forall -big_sepS_sepS. apply big_sepS_mono; auto=> x ?. by rewrite -always_wand_impl always_elim wand_elim_l. Qed. `````` Robbert Krebbers committed Feb 17, 2016 379 ``````End gset. `````` Robbert Krebbers committed Feb 14, 2016 380 `````` `````` Robbert Krebbers committed Apr 08, 2016 381 ``````(** ** Persistence *) `````` Robbert Krebbers committed May 24, 2016 382 ``````Global Instance big_and_persistent Ps : PersistentL Ps → PersistentP ([∧] Ps). `````` Robbert Krebbers committed Feb 14, 2016 383 ``````Proof. induction 1; apply _. Qed. `````` Robbert Krebbers committed May 24, 2016 384 ``````Global Instance big_sep_persistent Ps : PersistentL Ps → PersistentP ([★] Ps). `````` Robbert Krebbers committed Feb 14, 2016 385 386 ``````Proof. induction 1; apply _. Qed. `````` Robbert Krebbers committed Mar 11, 2016 387 ``````Global Instance nil_persistent : PersistentL (@nil (uPred M)). `````` Robbert Krebbers committed Feb 14, 2016 388 ``````Proof. constructor. Qed. `````` Robbert Krebbers committed Mar 11, 2016 389 ``````Global Instance cons_persistent P Ps : `````` Robbert Krebbers committed Mar 15, 2016 390 `````` PersistentP P → PersistentL Ps → PersistentL (P :: Ps). `````` Robbert Krebbers committed Feb 14, 2016 391 ``````Proof. by constructor. Qed. `````` Robbert Krebbers committed Mar 11, 2016 392 393 ``````Global Instance app_persistent Ps Ps' : PersistentL Ps → PersistentL Ps' → PersistentL (Ps ++ Ps'). `````` Robbert Krebbers committed Feb 14, 2016 394 ``````Proof. apply Forall_app_2. Qed. `````` Robbert Krebbers committed Mar 11, 2016 395 ``````Global Instance zip_with_persistent {A B} (f : A → B → uPred M) xs ys : `````` Robbert Krebbers committed Mar 15, 2016 396 `````` (∀ x y, PersistentP (f x y)) → PersistentL (zip_with f xs ys). `````` Robbert Krebbers committed Mar 11, 2016 397 398 399 ``````Proof. unfold PersistentL=> ?; revert ys; induction xs=> -[|??]; constructor; auto. Qed. `````` Robbert Krebbers committed Feb 16, 2016 400 ``End big_op.``