upred_big_op.v 9.54 KB
 Robbert Krebbers committed Mar 10, 2016 1 2 ``````From iris.algebra Require Export upred. From iris.prelude Require Import gmap fin_collections. `````` 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 31 `````` (** * Always stability for lists *) `````` Robbert Krebbers committed Feb 14, 2016 32 33 34 35 36 37 38 39 40 41 ``````Class AlwaysStableL {M} (Ps : list (uPred M)) := always_stableL : Forall AlwaysStable Ps. Arguments always_stableL {_} _ {_}. Section big_op. Context {M : cmraT}. Implicit Types Ps Qs : list (uPred M). Implicit Types A : Type. (* Big ops *) `````` Robbert Krebbers committed Feb 16, 2016 42 ``````Global Instance big_and_proper : Proper ((≡) ==> (≡)) (@uPred_big_and M). `````` Robbert Krebbers committed Feb 14, 2016 43 ``````Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed. `````` Robbert Krebbers committed Feb 16, 2016 44 ``````Global Instance big_sep_proper : Proper ((≡) ==> (≡)) (@uPred_big_sep M). `````` Robbert Krebbers committed Feb 14, 2016 45 ``````Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed. `````` Robbert Krebbers committed Feb 17, 2016 46 47 48 49 50 51 52 53 54 55 56 57 58 `````` Global Instance big_and_ne n : Proper (Forall2 (dist n) ==> dist n) (@uPred_big_and M). Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed. Global Instance big_sep_ne n : Proper (Forall2 (dist n) ==> dist n) (@uPred_big_sep M). Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed. Global Instance big_and_mono' : Proper (Forall2 (⊑) ==> (⊑)) (@uPred_big_and M). Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed. Global Instance big_sep_mono' : Proper (Forall2 (⊑) ==> (⊑)) (@uPred_big_sep M). Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed. `````` Robbert Krebbers committed Feb 16, 2016 59 ``````Global Instance big_and_perm : Proper ((≡ₚ) ==> (≡)) (@uPred_big_and M). `````` Robbert Krebbers committed Feb 14, 2016 60 61 ``````Proof. induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto. `````` Robbert Krebbers committed Feb 17, 2016 62 63 `````` - by rewrite IH. - by rewrite !assoc (comm _ P). `````` Ralf Jung committed Feb 20, 2016 64 `````` - etrans; eauto. `````` Robbert Krebbers committed Feb 14, 2016 65 ``````Qed. `````` Robbert Krebbers committed Feb 16, 2016 66 ``````Global Instance big_sep_perm : Proper ((≡ₚ) ==> (≡)) (@uPred_big_sep M). `````` Robbert Krebbers committed Feb 14, 2016 67 68 ``````Proof. induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto. `````` Robbert Krebbers committed Feb 17, 2016 69 70 `````` - by rewrite IH. - by rewrite !assoc (comm _ P). `````` Ralf Jung committed Feb 20, 2016 71 `````` - etrans; eauto. `````` Robbert Krebbers committed Feb 14, 2016 72 ``````Qed. `````` Robbert Krebbers committed Feb 17, 2016 73 `````` `````` Robbert Krebbers committed Feb 16, 2016 74 ``````Lemma big_and_app Ps Qs : (Π∧ (Ps ++ Qs))%I ≡ (Π∧ Ps ∧ Π∧ Qs)%I. `````` Robbert Krebbers committed Feb 14, 2016 75 ``````Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed. `````` Robbert Krebbers committed Feb 16, 2016 76 ``````Lemma big_sep_app Ps Qs : (Π★ (Ps ++ Qs))%I ≡ (Π★ Ps ★ Π★ Qs)%I. `````` Robbert Krebbers committed Feb 14, 2016 77 ``````Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed. `````` Robbert Krebbers committed Feb 17, 2016 78 79 80 `````` Lemma big_and_contains Ps Qs : Qs `contains` Ps → (Π∧ Ps)%I ⊑ (Π∧ Qs)%I. Proof. `````` Ralf Jung committed Feb 17, 2016 81 `````` intros [Ps' ->]%contains_Permutation. by rewrite big_and_app and_elim_l. `````` Robbert Krebbers committed Feb 17, 2016 82 83 84 ``````Qed. Lemma big_sep_contains Ps Qs : Qs `contains` Ps → (Π★ Ps)%I ⊑ (Π★ Qs)%I. Proof. `````` Ralf Jung committed Feb 17, 2016 85 `````` intros [Ps' ->]%contains_Permutation. by rewrite big_sep_app sep_elim_l. `````` Robbert Krebbers committed Feb 17, 2016 86 87 ``````Qed. `````` Robbert Krebbers committed Feb 16, 2016 88 ``````Lemma big_sep_and Ps : (Π★ Ps) ⊑ (Π∧ Ps). `````` Robbert Krebbers committed Feb 14, 2016 89 ``````Proof. by induction Ps as [|P Ps IH]; simpl; auto with I. Qed. `````` Robbert Krebbers committed Feb 17, 2016 90 `````` `````` Robbert Krebbers committed Feb 16, 2016 91 ``````Lemma big_and_elem_of Ps P : P ∈ Ps → (Π∧ Ps) ⊑ P. `````` Robbert Krebbers committed Feb 14, 2016 92 ``````Proof. induction 1; simpl; auto with I. Qed. `````` Robbert Krebbers committed Feb 16, 2016 93 ``````Lemma big_sep_elem_of Ps P : P ∈ Ps → (Π★ Ps) ⊑ P. `````` Robbert Krebbers committed Feb 14, 2016 94 95 ``````Proof. induction 1; simpl; auto with I. Qed. `````` Robbert Krebbers committed Feb 14, 2016 96 ``````(* Big ops over finite maps *) `````` Robbert Krebbers committed Feb 17, 2016 97 98 99 ``````Section gmap. Context `{Countable K} {A : Type}. Implicit Types m : gmap K A. `````` Robbert Krebbers committed Feb 18, 2016 100 `````` Implicit Types Φ Ψ : K → A → uPred M. `````` Robbert Krebbers committed Feb 14, 2016 101 `````` `````` Robbert Krebbers committed Feb 18, 2016 102 103 104 `````` Lemma big_sepM_mono Φ Ψ m1 m2 : m2 ⊆ m1 → (∀ x k, m2 !! k = Some x → Φ k x ⊑ Ψ k x) → (Π★{map m1} Φ) ⊑ (Π★{map m2} Ψ). `````` Robbert Krebbers committed Feb 16, 2016 105 `````` Proof. `````` Ralf Jung committed Feb 20, 2016 106 `````` intros HX HΦ. trans (Π★{map m2} Φ)%I. `````` Robbert Krebbers committed Feb 17, 2016 107 108 `````` - by apply big_sep_contains, fmap_contains, map_to_list_contains. - apply big_sep_mono', Forall2_fmap, Forall2_Forall. `````` Robbert Krebbers committed Feb 18, 2016 109 `````` apply Forall_forall=> -[i x] ? /=. by apply HΦ, elem_of_map_to_list. `````` Robbert Krebbers committed Feb 16, 2016 110 `````` Qed. `````` Robbert Krebbers committed Feb 17, 2016 111 112 113 114 115 `````` 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 116 117 `````` intros Φ1 Φ2 HΦ. apply big_sep_ne, Forall2_fmap. apply Forall2_Forall, Forall_true=> -[i x]; apply HΦ. `````` Robbert Krebbers committed Feb 17, 2016 118 119 120 121 122 `````` Qed. Global Instance big_sepM_proper m : Proper (pointwise_relation _ (pointwise_relation _ (≡)) ==> (≡)) (uPred_big_sepM (M:=M) m). Proof. `````` Robbert Krebbers committed Feb 18, 2016 123 124 `````` intros Φ1 Φ2 HΦ; apply equiv_dist=> n. apply big_sepM_ne=> k x; apply equiv_dist, HΦ. `````` Robbert Krebbers committed Feb 17, 2016 125 126 127 128 `````` Qed. Global Instance big_sepM_mono' m : Proper (pointwise_relation _ (pointwise_relation _ (⊑)) ==> (⊑)) (uPred_big_sepM (M:=M) m). `````` Robbert Krebbers committed Feb 18, 2016 129 `````` Proof. intros Φ1 Φ2 HΦ. apply big_sepM_mono; intros; [done|apply HΦ]. Qed. `````` Robbert Krebbers committed Feb 17, 2016 130 `````` `````` Robbert Krebbers committed Feb 18, 2016 131 `````` Lemma big_sepM_empty Φ : (Π★{map ∅} Φ)%I ≡ True%I. `````` Robbert Krebbers committed Feb 17, 2016 132 `````` Proof. by rewrite /uPred_big_sepM map_to_list_empty. Qed. `````` Robbert Krebbers committed Feb 18, 2016 133 134 `````` Lemma big_sepM_insert Φ (m : gmap K A) i x : m !! i = None → (Π★{map <[i:=x]> m} Φ)%I ≡ (Φ i x ★ Π★{map m} Φ)%I. `````` Robbert Krebbers committed Feb 17, 2016 135 `````` Proof. intros ?; by rewrite /uPred_big_sepM map_to_list_insert. Qed. `````` Robbert Krebbers committed Feb 18, 2016 136 `````` Lemma big_sepM_singleton Φ i x : (Π★{map {[i := x]}} Φ)%I ≡ (Φ i x)%I. `````` Robbert Krebbers committed Feb 14, 2016 137 138 139 140 `````` 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 141 `````` `````` Robbert Krebbers committed Feb 18, 2016 142 143 `````` Lemma big_sepM_sepM Φ Ψ m : (Π★{map m} (λ i x, Φ i x ★ Ψ i x))%I ≡ (Π★{map m} Φ ★ Π★{map m} Ψ)%I. `````` Ralf Jung committed Feb 17, 2016 144 `````` Proof. `````` Robbert Krebbers committed Feb 17, 2016 145 146 `````` rewrite /uPred_big_sepM. induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?right_id //. `````` Robbert Krebbers committed Feb 18, 2016 147 `````` by rewrite IH -!assoc (assoc _ (Ψ _ _)) [(Ψ _ _ ★ _)%I]comm -!assoc. `````` Ralf Jung committed Feb 17, 2016 148 `````` Qed. `````` Robbert Krebbers committed Feb 18, 2016 149 `````` Lemma big_sepM_later Φ m : (▷ Π★{map m} Φ)%I ≡ (Π★{map m} (λ i x, ▷ Φ i x))%I. `````` Ralf Jung committed Feb 17, 2016 150 `````` Proof. `````` Robbert Krebbers committed Feb 17, 2016 151 152 153 `````` 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 154 `````` Qed. `````` Robbert Krebbers committed Feb 17, 2016 155 156 157 158 159 160 ``````End gmap. (* Big ops over finite sets *) Section gset. Context `{Countable A}. Implicit Types X : gset A. `````` Robbert Krebbers committed Feb 18, 2016 161 `````` Implicit Types Φ : A → uPred M. `````` Robbert Krebbers committed Feb 17, 2016 162 `````` `````` Robbert Krebbers committed Feb 18, 2016 163 164 `````` Lemma big_sepS_mono Φ Ψ X Y : Y ⊆ X → (∀ x, x ∈ Y → Φ x ⊑ Ψ x) → (Π★{set X} Φ) ⊑ (Π★{set Y} Ψ). `````` Robbert Krebbers committed Feb 17, 2016 165 `````` Proof. `````` Ralf Jung committed Feb 20, 2016 166 `````` intros HX HΦ. trans (Π★{set Y} Φ)%I. `````` Robbert Krebbers committed Feb 17, 2016 167 168 `````` - by apply big_sep_contains, fmap_contains, elements_contains. - apply big_sep_mono', Forall2_fmap, Forall2_Forall. `````` Robbert Krebbers committed Feb 18, 2016 169 `````` apply Forall_forall=> x ? /=. by apply HΦ, elem_of_elements. `````` Robbert Krebbers committed Feb 17, 2016 170 171 172 173 174 `````` Qed. 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 175 176 `````` intros Φ1 Φ2 HΦ. apply big_sep_ne, Forall2_fmap. apply Forall2_Forall, Forall_true=> x; apply HΦ. `````` Robbert Krebbers committed Feb 17, 2016 177 178 179 180 `````` Qed. Lemma big_sepS_proper X : Proper (pointwise_relation _ (≡) ==> (≡)) (uPred_big_sepS (M:=M) X). Proof. `````` Robbert Krebbers committed Feb 18, 2016 181 182 `````` intros Φ1 Φ2 HΦ; apply equiv_dist=> n. apply big_sepS_ne=> x; apply equiv_dist, HΦ. `````` Robbert Krebbers committed Feb 17, 2016 183 184 185 `````` Qed. Lemma big_sepS_mono' X : Proper (pointwise_relation _ (⊑) ==> (⊑)) (uPred_big_sepS (M:=M) X). `````` Robbert Krebbers committed Feb 18, 2016 186 `````` Proof. intros Φ1 Φ2 HΦ. apply big_sepS_mono; naive_solver. Qed. `````` Robbert Krebbers committed Feb 17, 2016 187 `````` `````` Robbert Krebbers committed Feb 18, 2016 188 `````` Lemma big_sepS_empty Φ : (Π★{set ∅} Φ)%I ≡ True%I. `````` Robbert Krebbers committed Feb 17, 2016 189 `````` Proof. by rewrite /uPred_big_sepS elements_empty. Qed. `````` Robbert Krebbers committed Feb 18, 2016 190 191 `````` Lemma big_sepS_insert Φ X x : x ∉ X → (Π★{set {[ x ]} ∪ X} Φ)%I ≡ (Φ x ★ Π★{set X} Φ)%I. `````` Robbert Krebbers committed Feb 17, 2016 192 `````` Proof. intros. by rewrite /uPred_big_sepS elements_union_singleton. Qed. `````` Robbert Krebbers committed Feb 18, 2016 193 194 `````` Lemma big_sepS_delete Φ X x : x ∈ X → (Π★{set X} Φ)%I ≡ (Φ x ★ Π★{set X ∖ {[ x ]}} Φ)%I. `````` Robbert Krebbers committed Feb 17, 2016 195 `````` Proof. `````` Robbert Krebbers committed Feb 17, 2016 196 197 `````` intros. rewrite -big_sepS_insert; last set_solver. by rewrite -union_difference_L; last set_solver. `````` Robbert Krebbers committed Feb 17, 2016 198 `````` Qed. `````` Robbert Krebbers committed Feb 18, 2016 199 `````` Lemma big_sepS_singleton Φ x : (Π★{set {[ x ]}} Φ)%I ≡ (Φ x)%I. `````` Robbert Krebbers committed Feb 17, 2016 200 `````` Proof. intros. by rewrite /uPred_big_sepS elements_singleton /= right_id. Qed. `````` Ralf Jung committed Feb 17, 2016 201 `````` `````` Robbert Krebbers committed Feb 18, 2016 202 203 `````` Lemma big_sepS_sepS Φ Ψ X : (Π★{set X} (λ x, Φ x ★ Ψ x))%I ≡ (Π★{set X} Φ ★ Π★{set X} Ψ)%I. `````` Ralf Jung committed Feb 17, 2016 204 `````` Proof. `````` Robbert Krebbers committed Feb 17, 2016 205 206 `````` rewrite /uPred_big_sepS. induction (elements X) as [|x l IH]; csimpl; first by 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 209 `````` Qed. `````` Robbert Krebbers committed Feb 18, 2016 210 `````` Lemma big_sepS_later Φ X : (▷ Π★{set X} Φ)%I ≡ (Π★{set X} (λ x, ▷ Φ x))%I. `````` Ralf Jung committed Feb 17, 2016 211 `````` Proof. `````` Robbert Krebbers committed Feb 17, 2016 212 213 214 `````` 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 215 `````` Qed. `````` Robbert Krebbers committed Feb 17, 2016 216 ``````End gset. `````` Robbert Krebbers committed Feb 14, 2016 217 `````` `````` Robbert Krebbers committed Feb 14, 2016 218 219 220 ``````(* Always stable *) Local Notation AS := AlwaysStable. Local Notation ASL := AlwaysStableL. `````` Robbert Krebbers committed Feb 16, 2016 221 ``````Global Instance big_and_always_stable Ps : ASL Ps → AS (Π∧ Ps). `````` Robbert Krebbers committed Feb 14, 2016 222 ``````Proof. induction 1; apply _. Qed. `````` Robbert Krebbers committed Feb 16, 2016 223 ``````Global Instance big_sep_always_stable Ps : ASL Ps → AS (Π★ Ps). `````` Robbert Krebbers committed Feb 14, 2016 224 225 226 227 228 229 230 231 232 233 234 ``````Proof. induction 1; apply _. Qed. Global Instance nil_always_stable : ASL (@nil (uPred M)). Proof. constructor. Qed. Global Instance cons_always_stable P Ps : AS P → ASL Ps → ASL (P :: Ps). Proof. by constructor. Qed. Global Instance app_always_stable Ps Ps' : ASL Ps → ASL Ps' → ASL (Ps ++ Ps'). Proof. apply Forall_app_2. Qed. Global Instance zip_with_always_stable {A B} (f : A → B → uPred M) xs ys : (∀ x y, AS (f x y)) → ASL (zip_with f xs ys). Proof. unfold ASL=> ?; revert ys; induction xs=> -[|??]; constructor; auto. Qed. `````` Robbert Krebbers committed Feb 16, 2016 235 ``End big_op.``