upred_big_op.v 11 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 Feb 16, 2016 5 6 ``````(** * Big ops over lists *) (* These are the basic building blocks for other big ops *) `````` Robbert Krebbers committed Feb 16, 2016 7 8 9 10 11 12 13 14 ``````Fixpoint uPred_big_and {M} (Ps : list (uPred M)) : uPred M:= match Ps with [] => True | P :: Ps => P ∧ uPred_big_and Ps end%I. Instance: Params (@uPred_big_and) 1. Notation "'Π∧' Ps" := (uPred_big_and Ps) (at level 20) : uPred_scope. 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. Notation "'Π★' Ps" := (uPred_big_sep Ps) (at level 20) : uPred_scope. `````` Robbert Krebbers committed Feb 14, 2016 15 `````` `````` Robbert Krebbers committed Feb 16, 2016 16 17 ``````(** * Other big ops *) (** We use a type class to obtain overloaded notations *) `````` Robbert Krebbers committed Feb 17, 2016 18 ``````Definition uPred_big_sepM {M} `{Countable K} {A} `````` Robbert Krebbers committed Feb 18, 2016 19 20 `````` (m : gmap K A) (Φ : K → A → uPred M) : uPred M := uPred_big_sep (curry Φ <\$> map_to_list m). `````` Robbert Krebbers committed Feb 17, 2016 21 ``````Instance: Params (@uPred_big_sepM) 6. `````` Robbert Krebbers committed Feb 18, 2016 22 23 ``````Notation "'Π★{map' m } Φ" := (uPred_big_sepM m Φ) (at level 20, m at level 10, format "Π★{map m } Φ") : uPred_scope. `````` Robbert Krebbers committed Feb 14, 2016 24 `````` `````` Robbert Krebbers committed Feb 17, 2016 25 ``````Definition uPred_big_sepS {M} `{Countable A} `````` Robbert Krebbers committed Feb 18, 2016 26 `````` (X : gset A) (Φ : A → uPred M) : uPred M := uPred_big_sep (Φ <\$> elements X). `````` Robbert Krebbers committed Feb 17, 2016 27 ``````Instance: Params (@uPred_big_sepS) 5. `````` Robbert Krebbers committed Feb 18, 2016 28 29 ``````Notation "'Π★{set' X } Φ" := (uPred_big_sepS X Φ) (at level 20, X at level 10, format "Π★{set X } Φ") : uPred_scope. `````` Robbert Krebbers committed Feb 16, 2016 30 `````` `````` Robbert Krebbers committed Apr 08, 2016 31 ``````(** * Persistence of lists of uPreds *) `````` Robbert Krebbers committed Mar 11, 2016 32 ``````Class PersistentL {M} (Ps : list (uPred M)) := `````` Robbert Krebbers committed Mar 15, 2016 33 `````` persistentL : Forall PersistentP Ps. `````` Robbert Krebbers committed Mar 11, 2016 34 ``````Arguments persistentL {_} _ {_}. `````` Robbert Krebbers committed Feb 14, 2016 35 `````` `````` Robbert Krebbers committed Apr 08, 2016 36 ``````(** * Properties *) `````` Robbert Krebbers committed Feb 14, 2016 37 38 39 40 41 ``````Section big_op. Context {M : cmraT}. Implicit Types Ps Qs : list (uPred M). Implicit Types A : Type. `````` Robbert Krebbers committed Apr 08, 2016 42 ``````(** ** Big ops over lists *) `````` Ralf Jung committed Mar 10, 2016 43 ``````Global Instance big_and_proper : Proper ((≡) ==> (⊣⊢)) (@uPred_big_and M). `````` Robbert Krebbers committed Feb 14, 2016 44 ``````Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed. `````` Ralf Jung committed Mar 10, 2016 45 ``````Global Instance big_sep_proper : Proper ((≡) ==> (⊣⊢)) (@uPred_big_sep M). `````` Robbert Krebbers committed Feb 14, 2016 46 ``````Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed. `````` Robbert Krebbers committed Feb 17, 2016 47 `````` `````` Robbert Krebbers committed Mar 21, 2016 48 ``````Global Instance big_and_ne n : Proper (dist n ==> dist n) (@uPred_big_and M). `````` Robbert Krebbers committed Feb 17, 2016 49 ``````Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed. `````` Robbert Krebbers committed Mar 21, 2016 50 ``````Global Instance big_sep_ne n : Proper (dist n ==> dist n) (@uPred_big_sep M). `````` Robbert Krebbers committed Feb 17, 2016 51 52 ``````Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed. `````` Ralf Jung committed Mar 10, 2016 53 ``````Global Instance big_and_mono' : Proper (Forall2 (⊢) ==> (⊢)) (@uPred_big_and M). `````` Robbert Krebbers committed Feb 17, 2016 54 ``````Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed. `````` Ralf Jung committed Mar 10, 2016 55 ``````Global Instance big_sep_mono' : Proper (Forall2 (⊢) ==> (⊢)) (@uPred_big_sep M). `````` Robbert Krebbers committed Feb 17, 2016 56 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_and_perm : Proper ((≡ₚ) ==> (⊣⊢)) (@uPred_big_and M). `````` Robbert Krebbers committed Feb 14, 2016 59 60 ``````Proof. induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto. `````` Robbert Krebbers committed Feb 17, 2016 61 62 `````` - by rewrite IH. - by rewrite !assoc (comm _ P). `````` Ralf Jung committed Feb 20, 2016 63 `````` - etrans; eauto. `````` Robbert Krebbers committed Feb 14, 2016 64 ``````Qed. `````` Ralf Jung committed Mar 10, 2016 65 ``````Global Instance big_sep_perm : Proper ((≡ₚ) ==> (⊣⊢)) (@uPred_big_sep M). `````` Robbert Krebbers committed Feb 14, 2016 66 67 ``````Proof. induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto. `````` Robbert Krebbers committed Feb 17, 2016 68 69 `````` - by rewrite IH. - by rewrite !assoc (comm _ P). `````` Ralf Jung committed Feb 20, 2016 70 `````` - etrans; eauto. `````` Robbert Krebbers committed Feb 14, 2016 71 ``````Qed. `````` Robbert Krebbers committed Feb 17, 2016 72 `````` `````` Robbert Krebbers committed Mar 21, 2016 73 ``````Lemma big_and_app Ps Qs : Π∧ (Ps ++ Qs) ⊣⊢ (Π∧ Ps ∧ Π∧ Qs). `````` Robbert Krebbers committed Feb 14, 2016 74 ``````Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed. `````` Robbert Krebbers committed Mar 21, 2016 75 ``````Lemma big_sep_app Ps Qs : Π★ (Ps ++ Qs) ⊣⊢ (Π★ Ps ★ Π★ Qs). `````` Robbert Krebbers committed Feb 14, 2016 76 ``````Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed. `````` Robbert Krebbers committed Feb 17, 2016 77 `````` `````` Robbert Krebbers committed Mar 21, 2016 78 ``````Lemma big_and_contains Ps Qs : Qs `contains` Ps → Π∧ Ps ⊢ Π∧ Qs. `````` Robbert Krebbers committed Feb 17, 2016 79 ``````Proof. `````` Ralf Jung committed Feb 17, 2016 80 `````` intros [Ps' ->]%contains_Permutation. by rewrite big_and_app and_elim_l. `````` Robbert Krebbers committed Feb 17, 2016 81 ``````Qed. `````` Robbert Krebbers committed Mar 21, 2016 82 ``````Lemma big_sep_contains Ps Qs : Qs `contains` Ps → Π★ Ps ⊢ Π★ Qs. `````` Robbert Krebbers committed Feb 17, 2016 83 ``````Proof. `````` Ralf Jung committed Feb 17, 2016 84 `````` intros [Ps' ->]%contains_Permutation. by rewrite big_sep_app sep_elim_l. `````` Robbert Krebbers committed Feb 17, 2016 85 86 ``````Qed. `````` Robbert Krebbers committed Mar 21, 2016 87 ``````Lemma big_sep_and Ps : Π★ Ps ⊢ Π∧ Ps. `````` Robbert Krebbers committed Feb 14, 2016 88 ``````Proof. by induction Ps as [|P Ps IH]; simpl; auto with I. Qed. `````` Robbert Krebbers committed Feb 17, 2016 89 `````` `````` Robbert Krebbers committed Mar 21, 2016 90 ``````Lemma big_and_elem_of Ps P : P ∈ Ps → Π∧ Ps ⊢ P. `````` Robbert Krebbers committed Feb 14, 2016 91 ``````Proof. induction 1; simpl; auto with I. Qed. `````` Robbert Krebbers committed Mar 21, 2016 92 ``````Lemma big_sep_elem_of Ps P : P ∈ Ps → Π★ Ps ⊢ P. `````` Robbert Krebbers committed Feb 14, 2016 93 94 ``````Proof. induction 1; simpl; auto with I. Qed. `````` Robbert Krebbers committed Apr 08, 2016 95 ``````(** ** Big ops over finite maps *) `````` Robbert Krebbers committed Feb 17, 2016 96 97 98 ``````Section gmap. Context `{Countable K} {A : Type}. Implicit Types m : gmap K A. `````` Robbert Krebbers committed Feb 18, 2016 99 `````` Implicit Types Φ Ψ : K → A → uPred M. `````` Robbert Krebbers committed Feb 14, 2016 100 `````` `````` Robbert Krebbers committed Feb 18, 2016 101 `````` Lemma big_sepM_mono Φ Ψ m1 m2 : `````` Ralf Jung committed Mar 10, 2016 102 `````` m2 ⊆ m1 → (∀ x k, m2 !! k = Some x → Φ k x ⊢ Ψ k x) → `````` Robbert Krebbers committed Mar 21, 2016 103 `````` Π★{map m1} Φ ⊢ Π★{map m2} Ψ. `````` Robbert Krebbers committed Feb 16, 2016 104 `````` Proof. `````` Ralf Jung committed Feb 20, 2016 105 `````` intros HX HΦ. trans (Π★{map m2} Φ)%I. `````` Robbert Krebbers committed Feb 17, 2016 106 `````` - by apply big_sep_contains, fmap_contains, map_to_list_contains. `````` Robbert Krebbers committed Mar 21, 2016 107 `````` - apply big_sep_mono', Forall2_fmap, Forall_Forall2. `````` Robbert Krebbers committed Feb 18, 2016 108 `````` apply Forall_forall=> -[i x] ? /=. by apply HΦ, elem_of_map_to_list. `````` Robbert Krebbers committed Feb 16, 2016 109 `````` Qed. `````` Robbert Krebbers committed Apr 11, 2016 110 111 112 113 `````` Lemma big_sepM_proper Φ Ψ m1 m2 : m1 ≡ m2 → (∀ x k, m1 !! k = Some x → m2 !! k = Some x → Φ k x ⊣⊢ Ψ k x) → Π★{map m1} Φ ⊣⊢ Π★{map m2} Ψ. Proof. `````` Robbert Krebbers committed Apr 18, 2016 114 115 116 `````` (* 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 117 `````` intros [??] ?; apply (anti_symm (⊢)); apply big_sepM_mono; `````` Robbert Krebbers committed Apr 18, 2016 118 `````` eauto using equiv_entails, equiv_entails_sym, @lookup_weaken. `````` Robbert Krebbers committed Apr 11, 2016 119 `````` Qed. `````` Robbert Krebbers committed Feb 17, 2016 120 121 122 123 124 `````` 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 125 `````` intros Φ1 Φ2 HΦ. apply big_sep_ne, Forall2_fmap. `````` Robbert Krebbers committed Mar 21, 2016 126 `````` apply Forall_Forall2, Forall_true=> -[i x]; apply HΦ. `````` Robbert Krebbers committed Feb 17, 2016 127 `````` Qed. `````` Robbert Krebbers committed Apr 11, 2016 128 `````` Global Instance big_sepM_proper' m : `````` Ralf Jung committed Mar 10, 2016 129 `````` Proper (pointwise_relation _ (pointwise_relation _ (⊣⊢)) ==> (⊣⊢)) `````` Robbert Krebbers committed Feb 17, 2016 130 `````` (uPred_big_sepM (M:=M) m). `````` Robbert Krebbers committed Apr 11, 2016 131 `````` Proof. intros Φ1 Φ2 HΦ. by apply big_sepM_proper; intros; last apply HΦ. Qed. `````` Robbert Krebbers committed Feb 17, 2016 132 `````` Global Instance big_sepM_mono' m : `````` Ralf Jung committed Mar 10, 2016 133 `````` Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (⊢)) `````` Robbert Krebbers committed Feb 17, 2016 134 `````` (uPred_big_sepM (M:=M) m). `````` Robbert Krebbers committed Apr 11, 2016 135 `````` Proof. intros Φ1 Φ2 HΦ. by apply big_sepM_mono; intros; last apply HΦ. Qed. `````` Robbert Krebbers committed Feb 17, 2016 136 `````` `````` Robbert Krebbers committed Mar 21, 2016 137 `````` Lemma big_sepM_empty Φ : Π★{map ∅} Φ ⊣⊢ True. `````` Robbert Krebbers committed Feb 17, 2016 138 `````` Proof. by rewrite /uPred_big_sepM map_to_list_empty. Qed. `````` Robbert Krebbers committed Feb 18, 2016 139 `````` Lemma big_sepM_insert Φ (m : gmap K A) i x : `````` Robbert Krebbers committed Mar 21, 2016 140 `````` m !! i = None → Π★{map <[i:=x]> m} Φ ⊣⊢ (Φ i x ★ Π★{map m} Φ). `````` Robbert Krebbers committed Feb 17, 2016 141 `````` Proof. intros ?; by rewrite /uPred_big_sepM map_to_list_insert. Qed. `````` Robbert Krebbers committed May 24, 2016 142 143 144 `````` Lemma big_sepM_delete Φ (m : gmap K A) i x : m !! i = Some x → Π★{map m} Φ ⊣⊢ (Φ i x ★ Π★{map delete i m} Φ). Proof. intros. by rewrite -big_sepM_insert ?lookup_delete // insert_delete. Qed. `````` Robbert Krebbers committed Mar 21, 2016 145 `````` Lemma big_sepM_singleton Φ i x : Π★{map {[i := x]}} Φ ⊣⊢ (Φ i x). `````` Robbert Krebbers committed Feb 14, 2016 146 147 148 149 `````` 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 150 `````` `````` Robbert Krebbers committed Feb 18, 2016 151 `````` Lemma big_sepM_sepM Φ Ψ m : `````` Robbert Krebbers committed Mar 21, 2016 152 `````` Π★{map m} (λ i x, Φ i x ★ Ψ i x) ⊣⊢ (Π★{map m} Φ ★ Π★{map m} Ψ). `````` Ralf Jung committed Feb 17, 2016 153 `````` Proof. `````` Robbert Krebbers committed Feb 17, 2016 154 155 `````` rewrite /uPred_big_sepM. induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?right_id //. `````` Robbert Krebbers committed Feb 18, 2016 156 `````` by rewrite IH -!assoc (assoc _ (Ψ _ _)) [(Ψ _ _ ★ _)%I]comm -!assoc. `````` Ralf Jung committed Feb 17, 2016 157 `````` Qed. `````` Robbert Krebbers committed Mar 21, 2016 158 `````` Lemma big_sepM_later Φ m : ▷ Π★{map m} Φ ⊣⊢ Π★{map m} (λ i x, ▷ Φ i x). `````` Ralf Jung committed Feb 17, 2016 159 `````` Proof. `````` Robbert Krebbers committed Feb 17, 2016 160 161 162 `````` 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 163 `````` Qed. `````` Robbert Krebbers committed Feb 17, 2016 164 165 ``````End gmap. `````` Robbert Krebbers committed Apr 08, 2016 166 ``````(** ** Big ops over finite sets *) `````` Robbert Krebbers committed Feb 17, 2016 167 168 169 ``````Section gset. Context `{Countable A}. Implicit Types X : gset A. `````` Robbert Krebbers committed Feb 18, 2016 170 `````` Implicit Types Φ : A → uPred M. `````` Robbert Krebbers committed Feb 17, 2016 171 `````` `````` Robbert Krebbers committed Feb 18, 2016 172 `````` Lemma big_sepS_mono Φ Ψ X Y : `````` Robbert Krebbers committed Mar 21, 2016 173 `````` Y ⊆ X → (∀ x, x ∈ Y → Φ x ⊢ Ψ x) → Π★{set X} Φ ⊢ Π★{set Y} Ψ. `````` Robbert Krebbers committed Feb 17, 2016 174 `````` Proof. `````` Ralf Jung committed Feb 20, 2016 175 `````` intros HX HΦ. trans (Π★{set Y} Φ)%I. `````` Robbert Krebbers committed Feb 17, 2016 176 `````` - by apply big_sep_contains, fmap_contains, elements_contains. `````` Robbert Krebbers committed Mar 21, 2016 177 `````` - apply big_sep_mono', Forall2_fmap, Forall_Forall2. `````` Robbert Krebbers committed Feb 18, 2016 178 `````` apply Forall_forall=> x ? /=. by apply HΦ, elem_of_elements. `````` Robbert Krebbers committed Feb 17, 2016 179 `````` Qed. `````` Robbert Krebbers committed Apr 11, 2016 180 181 182 183 184 185 `````` Lemma big_sepS_proper Φ Ψ X Y : X ≡ Y → (∀ x, x ∈ X → x ∈ Y → Φ x ⊣⊢ Ψ x) → Π★{set X} Φ ⊣⊢ Π★{set Y} Ψ. Proof. intros [??] ?; apply (anti_symm (⊢)); apply big_sepS_mono; eauto using equiv_entails, equiv_entails_sym. Qed. `````` Robbert Krebbers committed Feb 17, 2016 186 187 188 189 `````` 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 190 `````` intros Φ1 Φ2 HΦ. apply big_sep_ne, Forall2_fmap. `````` Robbert Krebbers committed Mar 21, 2016 191 `````` apply Forall_Forall2, Forall_true=> x; apply HΦ. `````` Robbert Krebbers committed Feb 17, 2016 192 `````` Qed. `````` Robbert Krebbers committed Apr 11, 2016 193 `````` Lemma big_sepS_proper' X : `````` Ralf Jung committed Mar 10, 2016 194 `````` Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (uPred_big_sepS (M:=M) X). `````` Robbert Krebbers committed Apr 11, 2016 195 `````` Proof. intros Φ1 Φ2 HΦ. apply big_sepS_proper; naive_solver. Qed. `````` Robbert Krebbers committed Feb 17, 2016 196 `````` Lemma big_sepS_mono' X : `````` Ralf Jung committed Mar 10, 2016 197 `````` Proper (pointwise_relation _ (⊢) ==> (⊢)) (uPred_big_sepS (M:=M) X). `````` Robbert Krebbers committed Feb 18, 2016 198 `````` Proof. intros Φ1 Φ2 HΦ. apply big_sepS_mono; naive_solver. Qed. `````` Robbert Krebbers committed Feb 17, 2016 199 `````` `````` Robbert Krebbers committed Mar 21, 2016 200 `````` Lemma big_sepS_empty Φ : Π★{set ∅} Φ ⊣⊢ True. `````` Robbert Krebbers committed Feb 17, 2016 201 `````` Proof. by rewrite /uPred_big_sepS elements_empty. Qed. `````` Robbert Krebbers committed Apr 11, 2016 202 `````` `````` Robbert Krebbers committed Feb 18, 2016 203 `````` Lemma big_sepS_insert Φ X x : `````` Robbert Krebbers committed Mar 21, 2016 204 `````` x ∉ X → Π★{set {[ x ]} ∪ X} Φ ⊣⊢ (Φ x ★ Π★{set X} Φ). `````` Robbert Krebbers committed Feb 17, 2016 205 `````` Proof. intros. by rewrite /uPred_big_sepS elements_union_singleton. Qed. `````` Robbert Krebbers committed Apr 11, 2016 206 207 208 209 210 211 212 213 214 215 216 217 218 `````` Lemma big_sepS_insert' (Ψ : A → uPred M → uPred M) Φ X x P : x ∉ X → Π★{set {[ x ]} ∪ X} (λ y, Ψ y (<[x:=P]> Φ y)) ⊣⊢ (Ψ x P ★ Π★{set X} (λ y, Ψ y (Φ y))). 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. Lemma big_sepS_insert'' Φ X x P : x ∉ X → Π★{set {[ x ]} ∪ X} (<[x:=P]> Φ) ⊣⊢ (P ★ Π★{set X} Φ). Proof. apply (big_sepS_insert' (λ y, id)). Qed. `````` Robbert Krebbers committed Feb 18, 2016 219 `````` Lemma big_sepS_delete Φ X x : `````` Robbert Krebbers committed Mar 21, 2016 220 `````` x ∈ X → Π★{set X} Φ ⊣⊢ (Φ x ★ Π★{set X ∖ {[ x ]}} Φ). `````` Robbert Krebbers committed Feb 17, 2016 221 `````` Proof. `````` Robbert Krebbers committed Feb 17, 2016 222 223 `````` intros. rewrite -big_sepS_insert; last set_solver. by rewrite -union_difference_L; last set_solver. `````` Robbert Krebbers committed Feb 17, 2016 224 `````` Qed. `````` Robbert Krebbers committed Apr 11, 2016 225 `````` `````` Robbert Krebbers committed Mar 21, 2016 226 `````` Lemma big_sepS_singleton Φ x : Π★{set {[ x ]}} Φ ⊣⊢ (Φ x). `````` Robbert Krebbers committed Feb 17, 2016 227 `````` Proof. intros. by rewrite /uPred_big_sepS elements_singleton /= right_id. Qed. `````` Ralf Jung committed Feb 17, 2016 228 `````` `````` Robbert Krebbers committed Feb 18, 2016 229 `````` Lemma big_sepS_sepS Φ Ψ X : `````` Robbert Krebbers committed Mar 21, 2016 230 `````` Π★{set X} (λ x, Φ x ★ Ψ x) ⊣⊢ (Π★{set X} Φ ★ Π★{set X} Ψ). `````` Ralf Jung committed Feb 17, 2016 231 `````` Proof. `````` Robbert Krebbers committed Feb 17, 2016 232 233 `````` rewrite /uPred_big_sepS. induction (elements X) as [|x l IH]; csimpl; first by rewrite ?right_id. `````` Robbert Krebbers committed Feb 18, 2016 234 `````` by rewrite IH -!assoc (assoc _ (Ψ _)) [(Ψ _ ★ _)%I]comm -!assoc. `````` Ralf Jung committed Feb 17, 2016 235 236 `````` Qed. `````` Robbert Krebbers committed Mar 21, 2016 237 `````` Lemma big_sepS_later Φ X : ▷ Π★{set X} Φ ⊣⊢ Π★{set X} (λ x, ▷ Φ x). `````` Ralf Jung committed Feb 17, 2016 238 `````` Proof. `````` Robbert Krebbers committed Feb 17, 2016 239 240 241 `````` 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 242 `````` Qed. `````` Robbert Krebbers committed Feb 17, 2016 243 ``````End gset. `````` Robbert Krebbers committed Feb 14, 2016 244 `````` `````` Robbert Krebbers committed Apr 08, 2016 245 ``````(** ** Persistence *) `````` Robbert Krebbers committed Mar 15, 2016 246 ``````Global Instance big_and_persistent Ps : PersistentL Ps → PersistentP (Π∧ Ps). `````` Robbert Krebbers committed Feb 14, 2016 247 ``````Proof. induction 1; apply _. Qed. `````` Robbert Krebbers committed Mar 15, 2016 248 ``````Global Instance big_sep_persistent Ps : PersistentL Ps → PersistentP (Π★ Ps). `````` Robbert Krebbers committed Feb 14, 2016 249 250 ``````Proof. induction 1; apply _. Qed. `````` Robbert Krebbers committed Mar 11, 2016 251 ``````Global Instance nil_persistent : PersistentL (@nil (uPred M)). `````` Robbert Krebbers committed Feb 14, 2016 252 ``````Proof. constructor. Qed. `````` Robbert Krebbers committed Mar 11, 2016 253 ``````Global Instance cons_persistent P Ps : `````` Robbert Krebbers committed Mar 15, 2016 254 `````` PersistentP P → PersistentL Ps → PersistentL (P :: Ps). `````` Robbert Krebbers committed Feb 14, 2016 255 ``````Proof. by constructor. Qed. `````` Robbert Krebbers committed Mar 11, 2016 256 257 ``````Global Instance app_persistent Ps Ps' : PersistentL Ps → PersistentL Ps' → PersistentL (Ps ++ Ps'). `````` Robbert Krebbers committed Feb 14, 2016 258 ``````Proof. apply Forall_app_2. Qed. `````` Robbert Krebbers committed Mar 11, 2016 259 ``````Global Instance zip_with_persistent {A B} (f : A → B → uPred M) xs ys : `````` Robbert Krebbers committed Mar 15, 2016 260 `````` (∀ x y, PersistentP (f x y)) → PersistentL (zip_with f xs ys). `````` Robbert Krebbers committed Mar 11, 2016 261 262 263 ``````Proof. unfold PersistentL=> ?; revert ys; induction xs=> -[|??]; constructor; auto. Qed. `````` Robbert Krebbers committed Feb 16, 2016 264 ``End big_op.``