upred_big_op.v 13.4 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 24, 2016 86 87 88 ``````Lemma big_and_app Ps Qs : [∧] (Ps ++ Qs) ⊣⊢ ([∧] Ps ∧ [∧] Qs). Proof. induction Ps as [|?? IH]; by rewrite /= ?left_id -?assoc ?IH. Qed. 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 24, 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 Feb 18, 2016 153 `````` Lemma big_sepM_insert Φ (m : gmap K A) i x : `````` Robbert Krebbers committed May 24, 2016 154 155 `````` m !! i = None → ([★ 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 24, 2016 158 `````` Lemma big_sepM_delete Φ (m : gmap K A) i x : `````` Robbert Krebbers committed May 24, 2016 159 160 `````` m !! i = Some x → ([★ 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 24, 2016 166 `````` Lemma big_sepM_singleton Φ i x : ([★ map] k↦y ∈ {[i:=x]}, Φ k y) ⊣⊢ Φ i x. `````` Robbert Krebbers committed Feb 14, 2016 167 168 169 170 `````` 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 171 `````` `````` Robbert Krebbers committed May 31, 2016 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 `````` 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. Lemma big_sepM_insert_override (Φ : K → uPred M) (m : gmap K A) i x : m !! i = Some x → ([★ map] k↦_ ∈ <[i:=x]> m, Φ k) ⊣⊢ ([★ map] k↦_ ∈ m, Φ k). 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 201 `````` Lemma big_sepM_sepM Φ Ψ m : `````` Robbert Krebbers committed May 24, 2016 202 203 `````` ([★ map] k↦x ∈ m, Φ k x ★ Ψ k x) ⊣⊢ (([★ map] k↦x ∈ m, Φ k x) ★ ([★ map] k↦x ∈ m, Ψ k x)). `````` Ralf Jung committed Feb 17, 2016 204 `````` Proof. `````` Robbert Krebbers committed Feb 17, 2016 205 206 `````` rewrite /uPred_big_sepM. induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?right_id //. `````` Robbert Krebbers committed Feb 18, 2016 207 `````` by rewrite IH -!assoc (assoc _ (Ψ _ _)) [(Ψ _ _ ★ _)%I]comm -!assoc. `````` Ralf Jung committed Feb 17, 2016 208 `````` Qed. `````` Robbert Krebbers committed May 31, 2016 209 `````` `````` Robbert Krebbers committed May 24, 2016 210 211 `````` Lemma big_sepM_later Φ m : (▷ [★ map] k↦x ∈ m, Φ k x) ⊣⊢ ([★ map] k↦x ∈ m, ▷ Φ k x). `````` Ralf Jung committed Feb 17, 2016 212 `````` Proof. `````` Robbert Krebbers committed Feb 17, 2016 213 214 215 `````` 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 216 `````` Qed. `````` Robbert Krebbers committed Feb 17, 2016 217 218 ``````End gmap. `````` Robbert Krebbers committed Apr 08, 2016 219 ``````(** ** Big ops over finite sets *) `````` Robbert Krebbers committed Feb 17, 2016 220 221 222 ``````Section gset. Context `{Countable A}. Implicit Types X : gset A. `````` Robbert Krebbers committed Feb 18, 2016 223 `````` Implicit Types Φ : A → uPred M. `````` Robbert Krebbers committed Feb 17, 2016 224 `````` `````` Robbert Krebbers committed Feb 18, 2016 225 `````` Lemma big_sepS_mono Φ Ψ X Y : `````` Robbert Krebbers committed May 24, 2016 226 227 `````` Y ⊆ X → (∀ x, x ∈ Y → Φ x ⊢ Ψ x) → ([★ set] x ∈ X, Φ x) ⊢ ([★ set] x ∈ Y, Ψ x). `````` Robbert Krebbers committed Feb 17, 2016 228 `````` Proof. `````` Robbert Krebbers committed May 24, 2016 229 `````` intros HX HΦ. trans ([★ set] x ∈ Y, Φ x)%I. `````` Robbert Krebbers committed Feb 17, 2016 230 `````` - by apply big_sep_contains, fmap_contains, elements_contains. `````` Robbert Krebbers committed Mar 21, 2016 231 `````` - apply big_sep_mono', Forall2_fmap, Forall_Forall2. `````` Robbert Krebbers committed Feb 18, 2016 232 `````` apply Forall_forall=> x ? /=. by apply HΦ, elem_of_elements. `````` Robbert Krebbers committed Feb 17, 2016 233 `````` Qed. `````` Robbert Krebbers committed Apr 11, 2016 234 `````` Lemma big_sepS_proper Φ Ψ X Y : `````` Robbert Krebbers committed May 24, 2016 235 236 `````` X ≡ Y → (∀ x, x ∈ X → x ∈ Y → Φ x ⊣⊢ Ψ x) → ([★ set] x ∈ X, Φ x) ⊣⊢ ([★ set] x ∈ Y, Ψ x). `````` Robbert Krebbers committed Apr 11, 2016 237 238 239 240 `````` Proof. intros [??] ?; apply (anti_symm (⊢)); apply big_sepS_mono; eauto using equiv_entails, equiv_entails_sym. Qed. `````` Robbert Krebbers committed Feb 17, 2016 241 242 243 244 `````` 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 245 `````` intros Φ1 Φ2 HΦ. apply big_sep_ne, Forall2_fmap. `````` Robbert Krebbers committed Mar 21, 2016 246 `````` apply Forall_Forall2, Forall_true=> x; apply HΦ. `````` Robbert Krebbers committed Feb 17, 2016 247 `````` Qed. `````` Robbert Krebbers committed Apr 11, 2016 248 `````` Lemma big_sepS_proper' X : `````` Ralf Jung committed Mar 10, 2016 249 `````` Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (uPred_big_sepS (M:=M) X). `````` Robbert Krebbers committed Apr 11, 2016 250 `````` Proof. intros Φ1 Φ2 HΦ. apply big_sepS_proper; naive_solver. Qed. `````` Robbert Krebbers committed Feb 17, 2016 251 `````` Lemma big_sepS_mono' X : `````` Ralf Jung committed Mar 10, 2016 252 `````` Proper (pointwise_relation _ (⊢) ==> (⊢)) (uPred_big_sepS (M:=M) X). `````` Robbert Krebbers committed Feb 18, 2016 253 `````` Proof. intros Φ1 Φ2 HΦ. apply big_sepS_mono; naive_solver. Qed. `````` Robbert Krebbers committed Feb 17, 2016 254 `````` `````` Robbert Krebbers committed May 24, 2016 255 `````` Lemma big_sepS_empty Φ : ([★ set] x ∈ ∅, Φ x) ⊣⊢ True. `````` Robbert Krebbers committed Feb 17, 2016 256 `````` Proof. by rewrite /uPred_big_sepS elements_empty. Qed. `````` Robbert Krebbers committed Apr 11, 2016 257 `````` `````` Robbert Krebbers committed Feb 18, 2016 258 `````` Lemma big_sepS_insert Φ X x : `````` Robbert Krebbers committed May 24, 2016 259 `````` x ∉ X → ([★ set] y ∈ {[ x ]} ∪ X, Φ y) ⊣⊢ (Φ x ★ [★ set] y ∈ X, Φ y). `````` Robbert Krebbers committed Feb 17, 2016 260 `````` Proof. intros. by rewrite /uPred_big_sepS elements_union_singleton. Qed. `````` Robbert Krebbers committed May 30, 2016 261 `````` Lemma big_sepS_fn_insert (Ψ : A → uPred M → uPred M) Φ X x P : `````` Robbert Krebbers committed Apr 11, 2016 262 `````` x ∉ X → `````` Robbert Krebbers committed May 24, 2016 263 264 `````` ([★ set] y ∈ {[ x ]} ∪ X, Ψ y (<[x:=P]> Φ y)) ⊣⊢ (Ψ x P ★ [★ set] y ∈ X, Ψ y (Φ y)). `````` Robbert Krebbers committed Apr 11, 2016 265 266 267 268 269 `````` 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 270 `````` Lemma big_sepS_fn_insert' Φ X x P : `````` Robbert Krebbers committed May 24, 2016 271 `````` x ∉ X → ([★ set] y ∈ {[ x ]} ∪ X, <[x:=P]> Φ y) ⊣⊢ (P ★ [★ set] y ∈ X, Φ y). `````` Robbert Krebbers committed May 30, 2016 272 `````` Proof. apply (big_sepS_fn_insert (λ y, id)). Qed. `````` Robbert Krebbers committed Apr 11, 2016 273 `````` `````` Robbert Krebbers committed Feb 18, 2016 274 `````` Lemma big_sepS_delete Φ X x : `````` Robbert Krebbers committed May 24, 2016 275 `````` x ∈ X → ([★ set] y ∈ X, Φ y) ⊣⊢ (Φ x ★ [★ set] y ∈ X ∖ {[ x ]}, Φ y). `````` Robbert Krebbers committed Feb 17, 2016 276 `````` Proof. `````` Robbert Krebbers committed Feb 17, 2016 277 278 `````` intros. rewrite -big_sepS_insert; last set_solver. by rewrite -union_difference_L; last set_solver. `````` Robbert Krebbers committed Feb 17, 2016 279 `````` Qed. `````` Robbert Krebbers committed Apr 11, 2016 280 `````` `````` Robbert Krebbers committed May 24, 2016 281 `````` Lemma big_sepS_singleton Φ x : ([★ set] y ∈ {[ x ]}, Φ y) ⊣⊢ Φ x. `````` Robbert Krebbers committed Feb 17, 2016 282 `````` Proof. intros. by rewrite /uPred_big_sepS elements_singleton /= right_id. Qed. `````` Ralf Jung committed Feb 17, 2016 283 `````` `````` Robbert Krebbers committed Feb 18, 2016 284 `````` Lemma big_sepS_sepS Φ Ψ X : `````` Robbert Krebbers committed May 24, 2016 285 `````` ([★ set] y ∈ X, Φ y ★ Ψ y) ⊣⊢ (([★ set] y ∈ X, Φ y) ★ [★ set] y ∈ X, Ψ y). `````` Ralf Jung committed Feb 17, 2016 286 `````` Proof. `````` Robbert Krebbers committed Feb 17, 2016 287 288 `````` rewrite /uPred_big_sepS. induction (elements X) as [|x l IH]; csimpl; first by rewrite ?right_id. `````` Robbert Krebbers committed Feb 18, 2016 289 `````` by rewrite IH -!assoc (assoc _ (Ψ _)) [(Ψ _ ★ _)%I]comm -!assoc. `````` Ralf Jung committed Feb 17, 2016 290 291 `````` Qed. `````` Robbert Krebbers committed May 24, 2016 292 `````` Lemma big_sepS_later Φ X : (▷ [★ set] y ∈ X, Φ y) ⊣⊢ ([★ set] y ∈ X, ▷ Φ y). `````` Ralf Jung committed Feb 17, 2016 293 `````` Proof. `````` Robbert Krebbers committed Feb 17, 2016 294 295 296 `````` 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 297 `````` Qed. `````` Robbert Krebbers committed Feb 17, 2016 298 ``````End gset. `````` Robbert Krebbers committed Feb 14, 2016 299 `````` `````` Robbert Krebbers committed Apr 08, 2016 300 ``````(** ** Persistence *) `````` Robbert Krebbers committed May 24, 2016 301 ``````Global Instance big_and_persistent Ps : PersistentL Ps → PersistentP ([∧] Ps). `````` Robbert Krebbers committed Feb 14, 2016 302 ``````Proof. induction 1; apply _. Qed. `````` Robbert Krebbers committed May 24, 2016 303 ``````Global Instance big_sep_persistent Ps : PersistentL Ps → PersistentP ([★] Ps). `````` Robbert Krebbers committed Feb 14, 2016 304 305 ``````Proof. induction 1; apply _. Qed. `````` Robbert Krebbers committed Mar 11, 2016 306 ``````Global Instance nil_persistent : PersistentL (@nil (uPred M)). `````` Robbert Krebbers committed Feb 14, 2016 307 ``````Proof. constructor. Qed. `````` Robbert Krebbers committed Mar 11, 2016 308 ``````Global Instance cons_persistent P Ps : `````` Robbert Krebbers committed Mar 15, 2016 309 `````` PersistentP P → PersistentL Ps → PersistentL (P :: Ps). `````` Robbert Krebbers committed Feb 14, 2016 310 ``````Proof. by constructor. Qed. `````` Robbert Krebbers committed Mar 11, 2016 311 312 ``````Global Instance app_persistent Ps Ps' : PersistentL Ps → PersistentL Ps' → PersistentL (Ps ++ Ps'). `````` Robbert Krebbers committed Feb 14, 2016 313 ``````Proof. apply Forall_app_2. Qed. `````` Robbert Krebbers committed Mar 11, 2016 314 ``````Global Instance zip_with_persistent {A B} (f : A → B → uPred M) xs ys : `````` Robbert Krebbers committed Mar 15, 2016 315 `````` (∀ x y, PersistentP (f x y)) → PersistentL (zip_with f xs ys). `````` Robbert Krebbers committed Mar 11, 2016 316 317 318 ``````Proof. unfold PersistentL=> ?; revert ys; induction xs=> -[|??]; constructor; auto. Qed. `````` Robbert Krebbers committed Feb 16, 2016 319 ``End big_op.``