Commit bd11cf26 authored by Michael Sammler's avatar Michael Sammler
Browse files

Lemmas about big op on lists for !485

parent 19ba2bc0
......@@ -11,7 +11,7 @@ synopsis: "Iris is a Higher-Order Concurrent Separation Logic Framework with sup
depends: [
"coq" { (>= "8.10.2" & < "8.13~") | (= "dev") }
"coq-stdpp" { (= "dev.2020-09-15.0.f4a2763b") | (= "dev") }
"coq-stdpp" { (= "dev.2020-09-29.3.e80f1433") | (= "dev") }
]
build: [make "-j%{jobs}%"]
......
......@@ -192,6 +192,13 @@ Section list.
([^o list] ky h <$> l, f k y) ([^o list] ky l, f k (h y)).
Proof. revert f. induction l as [|x l IH]=> f; csimpl=> //. by rewrite IH. Qed.
Lemma big_opL_omap {B} (h : A option B) (f : B M) l :
([^o list] y omap h l, f y) ([^o list] y l, from_option f monoid_unit (h y)).
Proof.
revert f. induction l as [|x l IH]=> f //; csimpl.
case_match; csimpl; by rewrite IH // left_id.
Qed.
Lemma big_opL_op f g l :
([^o list] kx l, f k x `o` g k x)
([^o list] kx l, f k x) `o` ([^o list] kx l, g k x).
......@@ -323,6 +330,18 @@ Section gmap.
by apply big_opL_proper=> ? [??].
Qed.
Lemma big_opM_omap {B} (h : A option B) (f : K B M) m :
([^o map] ky omap h m, f k y) [^o map] ky m, from_option (f k) monoid_unit (h y).
Proof.
revert f. induction m as [|i x m Hmi IH] using map_ind=> f.
{ by rewrite omap_empty !big_opM_empty. }
assert (omap h m !! i = None) by (by rewrite lookup_omap Hmi).
destruct (h x) as [y|] eqn:Hhx.
- by rewrite (omap_insert _ _ _ _ y) // !big_opM_insert // IH Hhx.
- rewrite omap_insert_None // delete_notin // big_opM_insert //.
by rewrite Hhx /= left_id.
Qed.
Lemma big_opM_insert_delete `{Countable K} {B} (f : K B M) (m : gmap K B) i x :
([^o map] ky <[i:=x]> m, f k y) f i x `o` [^o map] ky delete i m, f k y.
Proof.
......
......@@ -158,6 +158,10 @@ Section sep_list.
([ list] ky f <$> l, Φ k y) ([ list] ky l, Φ k (f y)).
Proof. by rewrite big_opL_fmap. Qed.
Lemma big_sepL_omap {B} (f : A option B) (Φ : B PROP) l :
([ list] y omap f l, Φ y) ([ list] y l, from_option Φ emp (f y)).
Proof. by rewrite big_opL_omap. Qed.
Lemma big_sepL_bind {B} (f : A list B) (Φ : B PROP) l :
([ list] y l = f, Φ y) ([ list] x l, [ list] y f x, Φ y).
Proof. by rewrite big_opL_bind. Qed.
......@@ -513,6 +517,15 @@ Section sep_list2.
([ list] y1;y2 reverse l1;reverse l2, Φ y1 y2) ([ list] y1;y2 l1;l2, Φ y1 y2).
Proof. apply (anti_symm _); by rewrite big_sepL2_reverse_2 ?reverse_involutive. Qed.
Lemma big_sepL2_replicate_l l x Φ n :
length l = n
([ list] kx1;x2 replicate n x; l, Φ k x1 x2) [ list] kx2 l, Φ k x x2.
Proof. intros <-. revert Φ. induction l as [|y l IH]=> //= Φ. by rewrite IH. Qed.
Lemma big_sepL2_replicate_r l x Φ n :
length l = n
([ list] kx1;x2 l;replicate n x, Φ k x1 x2) [ list] kx1 l, Φ k x1 x.
Proof. intros <-. revert Φ. induction l as [|y l IH]=> //= Φ. by rewrite IH. Qed.
Lemma big_sepL2_sep Φ Ψ l1 l2 :
([ list] ky1;y2 l1;l2, Φ k y1 y2 Ψ k y1 y2)
([ list] ky1;y2 l1;l2, Φ k y1 y2) ([ list] ky1;y2 l1;l2, Ψ k y1 y2).
......@@ -903,6 +916,10 @@ Section map.
([ map] ky f <$> m, Φ k y) ([ map] ky m, Φ k (f y)).
Proof. by rewrite big_opM_fmap. Qed.
Lemma big_sepM_omap {B} (f : A option B) (Φ : K B PROP) m :
([ map] ky omap f m, Φ k y) ([ map] ky m, from_option (Φ k) emp (f y)).
Proof. by rewrite big_opM_omap. Qed.
Lemma big_sepM_insert_override Φ m i x x' :
m !! i = Some x (Φ i x Φ i x')
([ map] ky <[i:=x']> m, Φ k y) ([ map] ky m, Φ k y).
......
......@@ -332,6 +332,13 @@ Section fupd_derived.
Lemma big_sepL_fupd {A} E (Φ : nat A PROP) l :
([ list] kx l, |={E}=> Φ k x) ={E}= [ list] kx l, Φ k x.
Proof. by rewrite (big_opL_commute _). Qed.
Lemma big_sepL2_fupd {A B} E (Φ : nat A B PROP) l1 l2 :
([ list] kx;y l1;l2, |={E}=> Φ k x y) ={E}= [ list] kx;y l1;l2, Φ k x y.
Proof.
rewrite !big_sepL2_alt !persistent_and_affinely_sep_l.
etrans; [| by apply fupd_frame_l]. apply sep_mono_r. apply big_sepL_fupd.
Qed.
Lemma big_sepM_fupd `{Countable K} {A} E (Φ : K A PROP) m :
([ map] kx m, |={E}=> Φ k x) ={E}= [ map] kx m, Φ k x.
Proof. by rewrite (big_opM_commute _). 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