upred_big_op.v 4.36 KB
 Robbert Krebbers committed Feb 14, 2016 1 ``````From algebra Require Export upred. `````` Robbert Krebbers committed Feb 16, 2016 2 ``````From prelude Require Import fin_maps fin_collections. `````` Robbert Krebbers committed Feb 14, 2016 3 `````` `````` Robbert Krebbers committed Feb 16, 2016 4 5 ``````(** * Big ops over lists *) (* These are the basic building blocks for other big ops *) `````` Robbert Krebbers committed Feb 16, 2016 6 7 8 9 10 11 12 13 ``````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 14 `````` `````` Robbert Krebbers committed Feb 16, 2016 15 16 ``````(** * Other big ops *) (** We use a type class to obtain overloaded notations *) `````` Robbert Krebbers committed Feb 16, 2016 17 18 19 20 ``````Definition uPred_big_sepM {M} `{FinMapToList K A MA} (m : MA) (P : K → A → uPred M) : uPred M := uPred_big_sep (curry P <\$> map_to_list m). Notation "'Π★{map' m } P" := (uPred_big_sepM m P) `````` Robbert Krebbers committed Feb 16, 2016 21 `````` (at level 20, m at level 10, format "Π★{map m } P") : uPred_scope. `````` Robbert Krebbers committed Feb 14, 2016 22 `````` `````` Robbert Krebbers committed Feb 16, 2016 23 24 25 ``````Definition uPred_big_sepS {M} `{Elements A C} (X : C) (P : A → uPred M) : uPred M := uPred_big_sep (P <\$> elements X). Notation "'Π★{set' X } P" := (uPred_big_sepS X P) `````` Robbert Krebbers committed Feb 16, 2016 26 `````` (at level 20, X at level 10, format "Π★{set X } P") : uPred_scope. `````` Robbert Krebbers committed Feb 16, 2016 27 28 `````` (** * Always stability for lists *) `````` Robbert Krebbers committed Feb 14, 2016 29 30 31 32 33 34 35 36 37 38 39 ``````Class AlwaysStableL {M} (Ps : list (uPred M)) := always_stableL : Forall AlwaysStable Ps. Arguments always_stableL {_} _ {_}. Section big_op. Context {M : cmraT}. Implicit Types P Q : uPred M. Implicit Types Ps Qs : list (uPred M). Implicit Types A : Type. (* Big ops *) `````` Robbert Krebbers committed Feb 16, 2016 40 ``````Global Instance big_and_proper : Proper ((≡) ==> (≡)) (@uPred_big_and M). `````` Robbert Krebbers committed Feb 14, 2016 41 ``````Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed. `````` Robbert Krebbers committed Feb 16, 2016 42 ``````Global Instance big_sep_proper : Proper ((≡) ==> (≡)) (@uPred_big_sep 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_and_perm : Proper ((≡ₚ) ==> (≡)) (@uPred_big_and M). `````` Robbert Krebbers committed Feb 14, 2016 45 46 47 48 49 50 ``````Proof. induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto. * by rewrite IH. * by rewrite !assoc (comm _ P). * etransitivity; eauto. Qed. `````` Robbert Krebbers committed Feb 16, 2016 51 ``````Global Instance big_sep_perm : Proper ((≡ₚ) ==> (≡)) (@uPred_big_sep M). `````` Robbert Krebbers committed Feb 14, 2016 52 53 54 55 56 57 ``````Proof. induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto. * by rewrite IH. * by rewrite !assoc (comm _ P). * etransitivity; eauto. Qed. `````` Robbert Krebbers committed Feb 16, 2016 58 ``````Lemma big_and_app Ps Qs : (Π∧ (Ps ++ Qs))%I ≡ (Π∧ Ps ∧ Π∧ Qs)%I. `````` Robbert Krebbers committed Feb 14, 2016 59 ``````Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed. `````` Robbert Krebbers committed Feb 16, 2016 60 ``````Lemma big_sep_app Ps Qs : (Π★ (Ps ++ Qs))%I ≡ (Π★ Ps ★ Π★ Qs)%I. `````` Robbert Krebbers committed Feb 14, 2016 61 ``````Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed. `````` Robbert Krebbers committed Feb 16, 2016 62 ``````Lemma big_sep_and Ps : (Π★ Ps) ⊑ (Π∧ Ps). `````` Robbert Krebbers committed Feb 14, 2016 63 ``````Proof. by induction Ps as [|P Ps IH]; simpl; auto with I. Qed. `````` Robbert Krebbers committed Feb 16, 2016 64 ``````Lemma big_and_elem_of Ps P : P ∈ Ps → (Π∧ Ps) ⊑ P. `````` Robbert Krebbers committed Feb 14, 2016 65 ``````Proof. induction 1; simpl; auto with I. Qed. `````` Robbert Krebbers committed Feb 16, 2016 66 ``````Lemma big_sep_elem_of Ps P : P ∈ Ps → (Π★ Ps) ⊑ P. `````` Robbert Krebbers committed Feb 14, 2016 67 68 ``````Proof. induction 1; simpl; auto with I. Qed. `````` Robbert Krebbers committed Feb 14, 2016 69 70 71 72 ``````(* Big ops over finite maps *) Section fin_map. Context `{FinMap K Ma} {A} (P : K → A → uPred M). `````` Robbert Krebbers committed Feb 16, 2016 73 `````` Lemma big_sepM_empty : (Π★{map ∅} P)%I ≡ True%I. `````` Robbert Krebbers committed Feb 16, 2016 74 `````` Proof. by rewrite /uPred_big_sep /uPred_big_sepM map_to_list_empty. Qed. `````` Robbert Krebbers committed Feb 14, 2016 75 `````` Lemma big_sepM_insert (m : Ma A) i x : `````` Robbert Krebbers committed Feb 16, 2016 76 `````` m !! i = None → (Π★{map <[i:=x]> m} P)%I ≡ (P i x ★ Π★{map m} P)%I. `````` Robbert Krebbers committed Feb 16, 2016 77 78 79 `````` Proof. intros ?; by rewrite /uPred_big_sep /uPred_big_sepM map_to_list_insert. Qed. `````` Robbert Krebbers committed Feb 16, 2016 80 `````` Lemma big_sepM_singleton i x : (Π★{map {[i ↦ x]}} P)%I ≡ (P i x)%I. `````` Robbert Krebbers committed Feb 14, 2016 81 82 83 84 85 86 `````` Proof. rewrite -insert_empty big_sepM_insert/=; last auto using lookup_empty. by rewrite big_sepM_empty right_id. Qed. End fin_map. `````` Robbert Krebbers committed Feb 14, 2016 87 88 89 ``````(* Always stable *) Local Notation AS := AlwaysStable. Local Notation ASL := AlwaysStableL. `````` Robbert Krebbers committed Feb 16, 2016 90 ``````Global Instance big_and_always_stable Ps : ASL Ps → AS (Π∧ Ps). `````` Robbert Krebbers committed Feb 14, 2016 91 ``````Proof. induction 1; apply _. Qed. `````` Robbert Krebbers committed Feb 16, 2016 92 ``````Global Instance big_sep_always_stable Ps : ASL Ps → AS (Π★ Ps). `````` Robbert Krebbers committed Feb 14, 2016 93 94 95 96 97 98 99 100 101 102 103 ``````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 104 ``End big_op.``