cmra_big_op.v 1.55 KB
 Robbert Krebbers committed Mar 24, 2017 1 ``````From stdpp Require Import gmap gmultiset. `````` Jacques-Henri Jourdan committed Sep 13, 2019 2 ``````From iris.algebra Require Export big_op cmra. `````` Robbert Krebbers committed Mar 24, 2017 3 ``````Set Default Proof Using "Type*". `````` Robbert Krebbers committed Sep 28, 2016 4 `````` `````` Robbert Krebbers committed Oct 02, 2016 5 6 ``````(** Option *) Lemma big_opL_None {M : cmraT} {A} (f : nat → A → option M) l : `````` Robbert Krebbers committed Mar 24, 2017 7 `````` ([^op list] k↦x ∈ l, f k x) = None ↔ ∀ k x, l !! k = Some x → f k x = None. `````` Robbert Krebbers committed Oct 02, 2016 8 ``````Proof. `````` Robbert Krebbers committed Mar 24, 2017 9 `````` revert f. induction l as [|x l IH]=> f //=. rewrite op_None IH. split. `````` Robbert Krebbers committed Oct 02, 2016 10 11 12 13 `````` - intros [??] [|k] y ?; naive_solver. - intros Hl. split. by apply (Hl 0). intros k. apply (Hl (S k)). Qed. Lemma big_opM_None {M : cmraT} `{Countable K} {A} (f : K → A → option M) m : `````` Robbert Krebbers committed Mar 24, 2017 14 `````` ([^op map] k↦x ∈ m, f k x) = None ↔ ∀ k x, m !! k = Some x → f k x = None. `````` Robbert Krebbers committed Oct 02, 2016 15 16 17 18 19 20 21 22 23 ``````Proof. induction m as [|i x m ? IH] using map_ind=> //=. rewrite -equiv_None big_opM_insert // equiv_None op_None IH. split. { intros [??] k y. rewrite lookup_insert_Some; naive_solver. } intros Hm; split. - apply (Hm i). by simplify_map_eq. - intros k y ?. apply (Hm k). by simplify_map_eq. Qed. Lemma big_opS_None {M : cmraT} `{Countable A} (f : A → option M) X : `````` Robbert Krebbers committed Mar 24, 2017 24 `````` ([^op set] x ∈ X, f x) = None ↔ ∀ x, x ∈ X → f x = None. `````` Robbert Krebbers committed Oct 02, 2016 25 ``````Proof. `````` Robbert Krebbers committed Feb 20, 2019 26 `````` induction X as [|x X ? IH] using set_ind_L; [done|]. `````` Robbert Krebbers committed Oct 02, 2016 27 28 `````` rewrite -equiv_None big_opS_insert // equiv_None op_None IH. set_solver. Qed. `````` Robbert Krebbers committed Nov 19, 2016 29 ``````Lemma big_opMS_None {M : cmraT} `{Countable A} (f : A → option M) X : `````` Robbert Krebbers committed Mar 24, 2017 30 `````` ([^op mset] x ∈ X, f x) = None ↔ ∀ x, x ∈ X → f x = None. `````` Robbert Krebbers committed Nov 19, 2016 31 32 33 ``````Proof. induction X as [|x X IH] using gmultiset_ind. { rewrite big_opMS_empty. set_solver. } `````` Robbert Krebbers committed Feb 21, 2019 34 `````` rewrite -equiv_None big_opMS_disj_union big_opMS_singleton equiv_None op_None IH. `````` Robbert Krebbers committed Nov 19, 2016 35 `````` set_solver. `````` Jacques-Henri Jourdan committed Sep 13, 2019 36 ``Qed.``