cmra_big_op.v 3 KB
Newer Older
 Robbert Krebbers committed Mar 21, 2016 1 ``````From iris.algebra Require Export cmra list. `````` Robbert Krebbers committed Mar 10, 2016 2 ``````From iris.prelude Require Import gmap. `````` Robbert Krebbers committed Feb 01, 2016 3 `````` `````` Robbert Krebbers committed May 27, 2016 4 ``````Fixpoint big_op {A : ucmraT} (xs : list A) : A := `````` Robbert Krebbers committed Feb 01, 2016 5 `````` match xs with [] => ∅ | x :: xs => x ⋅ big_op xs end. `````` Robbert Krebbers committed May 27, 2016 6 7 8 ``````Arguments big_op _ !_ /. Instance: Params (@big_op) 1. Definition big_opM `{Countable K} {A : ucmraT} (m : gmap K A) : A := `````` Robbert Krebbers committed Feb 01, 2016 9 `````` big_op (snd <\$> map_to_list m). `````` Robbert Krebbers committed May 27, 2016 10 ``````Instance: Params (@big_opM) 4. `````` Robbert Krebbers committed Feb 01, 2016 11 12 13 `````` (** * Properties about big ops *) Section big_op. `````` Robbert Krebbers committed May 27, 2016 14 15 ``````Context {A : ucmraT}. Implicit Types xs : list A. `````` Robbert Krebbers committed Feb 01, 2016 16 17 18 19 20 21 `````` (** * Big ops *) Lemma big_op_nil : big_op (@nil A) = ∅. Proof. done. Qed. Lemma big_op_cons x xs : big_op (x :: xs) = x ⋅ big_op xs. Proof. done. Qed. `````` Robbert Krebbers committed May 27, 2016 22 ``````Global Instance big_op_permutation : Proper ((≡ₚ) ==> (≡)) (@big_op A). `````` Robbert Krebbers committed Feb 01, 2016 23 24 ``````Proof. induction 1 as [|x xs1 xs2 ? IH|x y xs|xs1 xs2 xs3]; simpl; auto. `````` Robbert Krebbers committed Feb 17, 2016 25 26 `````` - by rewrite IH. - by rewrite !assoc (comm _ x). `````` Ralf Jung committed Feb 20, 2016 27 `````` - by trans (big_op xs2). `````` Robbert Krebbers committed Feb 01, 2016 28 ``````Qed. `````` Robbert Krebbers committed May 27, 2016 29 ``````Global Instance big_op_ne n : Proper (dist n ==> dist n) (@big_op A). `````` Robbert Krebbers committed Feb 01, 2016 30 ``````Proof. by induction 1; simpl; repeat apply (_ : Proper (_ ==> _ ==> _) op). Qed. `````` Robbert Krebbers committed Mar 21, 2016 31 ``````Global Instance big_op_proper : Proper ((≡) ==> (≡)) big_op := ne_proper _. `````` Robbert Krebbers committed Feb 01, 2016 32 33 ``````Lemma big_op_app xs ys : big_op (xs ++ ys) ≡ big_op xs ⋅ big_op ys. Proof. `````` Robbert Krebbers committed Feb 11, 2016 34 35 `````` induction xs as [|x xs IH]; simpl; first by rewrite ?left_id. by rewrite IH assoc. `````` Robbert Krebbers committed Feb 01, 2016 36 37 38 ``````Qed. Lemma big_op_contains xs ys : xs `contains` ys → big_op xs ≼ big_op ys. Proof. `````` Robbert Krebbers committed Feb 17, 2016 39 40 `````` intros [xs' ->]%contains_Permutation. rewrite big_op_app; apply cmra_included_l. `````` Robbert Krebbers committed Feb 01, 2016 41 42 43 44 45 ``````Qed. Lemma big_op_delete xs i x : xs !! i = Some x → x ⋅ big_op (delete i xs) ≡ big_op xs. Proof. by intros; rewrite {2}(delete_Permutation xs i x). Qed. `````` Robbert Krebbers committed Feb 17, 2016 46 47 48 ``````Context `{Countable K}. Implicit Types m : gmap K A. Lemma big_opM_empty : big_opM (∅ : gmap K A) ≡ ∅. `````` Robbert Krebbers committed Feb 01, 2016 49 ``````Proof. unfold big_opM. by rewrite map_to_list_empty. Qed. `````` Robbert Krebbers committed Feb 17, 2016 50 ``````Lemma big_opM_insert m i x : `````` Robbert Krebbers committed Feb 01, 2016 51 52 `````` m !! i = None → big_opM (<[i:=x]> m) ≡ x ⋅ big_opM m. Proof. intros ?; by rewrite /big_opM map_to_list_insert. Qed. `````` Robbert Krebbers committed Feb 17, 2016 53 ``````Lemma big_opM_delete m i x : `````` Robbert Krebbers committed Feb 01, 2016 54 55 `````` m !! i = Some x → x ⋅ big_opM (delete i m) ≡ big_opM m. Proof. `````` Robbert Krebbers committed May 31, 2016 56 57 `````` intros. rewrite -{2}(insert_id m i x) // -insert_delete. by rewrite big_opM_insert ?lookup_delete. `````` Robbert Krebbers committed Feb 01, 2016 58 ``````Qed. `````` Robbert Krebbers committed Feb 17, 2016 59 ``````Lemma big_opM_singleton i x : big_opM ({[i := x]} : gmap K A) ≡ x. `````` Robbert Krebbers committed Feb 01, 2016 60 61 ``````Proof. rewrite -insert_empty big_opM_insert /=; last auto using lookup_empty. `````` Robbert Krebbers committed Feb 11, 2016 62 `````` by rewrite big_opM_empty right_id. `````` Robbert Krebbers committed Feb 01, 2016 63 ``````Qed. `````` Robbert Krebbers committed Feb 17, 2016 64 ``````Global Instance big_opM_proper : Proper ((≡) ==> (≡)) (big_opM : gmap K A → _). `````` Robbert Krebbers committed Feb 01, 2016 65 66 67 68 69 ``````Proof. intros m1; induction m1 as [|i x m1 ? IH] using map_ind. { by intros m2; rewrite (symmetry_iff (≡)) map_equiv_empty; intros ->. } intros m2 Hm2; rewrite big_opM_insert //. rewrite (IH (delete i m2)); last by rewrite -Hm2 delete_insert. `````` Robbert Krebbers committed Mar 21, 2016 70 `````` destruct (map_equiv_lookup_l (<[i:=x]> m1) m2 i x) `````` Robbert Krebbers committed Feb 01, 2016 71 72 `````` as (y&?&Hxy); auto using lookup_insert. rewrite Hxy -big_opM_insert; last auto using lookup_delete. `````` Robbert Krebbers committed May 31, 2016 73 `````` by rewrite insert_delete insert_id. `````` Robbert Krebbers committed Feb 01, 2016 74 ``````Qed. `````` Robbert Krebbers committed Feb 11, 2016 75 ``````Lemma big_opM_lookup_valid n m i x : ✓{n} big_opM m → m !! i = Some x → ✓{n} x. `````` Robbert Krebbers committed Feb 01, 2016 76 77 78 79 80 ``````Proof. intros Hm ?; revert Hm; rewrite -(big_opM_delete _ i x) //. apply cmra_validN_op_l. Qed. End big_op.``````