Commit 72810c5c authored by Ralf Jung's avatar Ralf Jung
Browse files

add big_sepL_sepL and big_sepS_sepS

parent f762f908
......@@ -492,12 +492,16 @@ Section gset.
Proper (pointwise_relation _ () ==> (=) ==> ()) (big_opS o (A:=A)).
Proof. intros f g Hf m ? <-. apply big_opS_proper; intros; apply Hf. Qed.
Lemma big_opS_elements f X :
([^o set] x X, f x) = [^o list] _x elements X, f x.
Proof. by rewrite big_opS_eq. Qed.
Lemma big_opS_empty f : ([^o set] x , f x) = monoid_unit.
Proof. by rewrite big_opS_eq /big_opS_def elements_empty. Qed.
Proof. by rewrite big_opS_elements elements_empty. Qed.
Lemma big_opS_insert f X x :
x X ([^o set] y {[ x ]} X, f y) (f x `o` [^o set] y X, f y).
Proof. intros. by rewrite big_opS_eq /big_opS_def elements_union_singleton. Qed.
Proof. intros. by rewrite !big_opS_elements elements_union_singleton. Qed.
Lemma big_opS_fn_insert {B} (f : A B M) h X x b :
x X
([^o set] y {[ x ]} X, f y (<[x:=b]> h y))
......@@ -529,7 +533,7 @@ Section gset.
Lemma big_opS_singleton f x : ([^o set] y {[ x ]}, f y) f x.
Proof. intros. by rewrite big_opS_eq /big_opS_def elements_singleton /= right_id. Qed.
Proof. intros. by rewrite big_opS_elements elements_singleton /= right_id. Qed.
Lemma big_opS_unit X : ([^o set] y X, monoid_unit) (monoid_unit : M).
......@@ -552,7 +556,7 @@ Section gset.
Lemma big_opS_op f g X :
([^o set] y X, f y `o` g y) ([^o set] y X, f y) `o` ([^o set] y X, g y).
Proof. by rewrite big_opS_eq /big_opS_def -big_opL_op. Qed.
Proof. by rewrite !big_opS_elements -big_opL_op. Qed.
Lemma big_opS_list_to_set f (l : list A) :
NoDup l
......@@ -357,6 +357,19 @@ Section sep_list.
End sep_list.
(* Some lemmas depend on the generalized versions of the above ones. *)
Lemma big_sepL_sepL {A B : Type} (Φ : nat A nat B PROP) (l1 : list A) (l2 : list B) :
([ list] k1x1 l1, [ list] k2x2 l2, Φ k1 x1 k2 x2)
([ list] k2x2 l2, [ list] k1x1 l1, Φ k1 x1 k2 x2).
revert Φ l2. induction l1 as [|x1 l1 IH]; intros Φ l2.
{ rewrite big_sepL_nil. setoid_rewrite big_sepL_nil.
rewrite big_sepL_emp. done. }
rewrite big_sepL_cons.
setoid_rewrite big_sepL_cons.
rewrite big_sepL_sep. f_equiv.
rewrite IH //.
Lemma big_sepL_sep_zip_with {A B C} (f : A B C) (g1 : C A) (g2 : C B)
(Φ1 : nat A PROP) (Φ2 : nat B PROP) l1 l2 :
( x y, g1 (f x y) = x)
......@@ -2010,6 +2023,10 @@ Section gset.
Proper (pointwise_relation _ () ==> (=) ==> ()) (big_opS (@bi_sep PROP) (A:=A)).
Proof. intros f g Hf m ? <-. by apply big_sepS_mono. Qed.
Lemma big_sepS_elements Φ X :
([ set] x X, Φ x) [ list] _x elements X, Φ x.
Proof. by rewrite big_opS_elements. Qed.
Lemma big_sepS_empty Φ : ([ set] x , Φ x) emp.
Proof. by rewrite big_opS_empty. Qed.
Lemma big_sepS_empty' P `{!Affine P} Φ : P [ set] x , Φ x.
......@@ -2232,6 +2249,14 @@ Section gset.
Proof. rewrite big_opS_eq /big_opS_def. apply _. Qed.
End gset.
Lemma big_sepS_sepS `{Countable A, Countable B}
(X : gset A) (Y : gset B) (Φ : A B PROP) :
([ set] x X, [ set] y Y, Φ x y) - ([ set] y Y, [ set] x X, Φ x y).
repeat setoid_rewrite big_sepS_elements.
rewrite big_sepL_sepL. done.
Lemma big_sepM_dom `{Countable K} {A} (Φ : K PROP) (m : gmap K A) :
([ map] k_ m, Φ k) ([ set] k dom _ m, Φ k).
Proof. apply big_opM_dom. Qed.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment