Merge branch 'msammler/big_op_lemmas' into 'master'

Lemmas about big op on lists for !485

See merge request iris/iris!509

opam

@@ -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}%"]

theories/algebra/big_op.v

@@ -192,6 +192,13 @@ Section list.
     ([^o list] k↦y ∈ h <$> l, f k y) ≡ ([^o list] k↦y ∈ 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] k↦x ∈ l, f k x `o` g k x)
     ≡ ([^o list] k↦x ∈ l, f k x) `o` ([^o list] k↦x ∈ 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] k↦y ∈ omap h m, f k y) ≡ [^o map] k↦y ∈ 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] k↦y ∈ <[i:=x]> m, f k y) ≡ f i x `o` [^o map] k↦y ∈ delete i m, f k y.
   Proof.

theories/bi/big_op.v

@@ -158,6 +158,10 @@ Section sep_list.
     ([∗ list] k↦y ∈ f <$> l, Φ k y) ⊣⊢ ([∗ list] k↦y ∈ 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] k↦x1;x2 ∈ replicate n x; l, Φ k x1 x2) ⊣⊢ [∗ list] k↦x2 ∈ 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] k↦x1;x2 ∈ l;replicate n x, Φ k x1 x2) ⊣⊢ [∗ list] k↦x1 ∈ l, Φ k x1 x.
+  Proof. intros <-. revert Φ. induction l as [|y l IH]=> //= Φ. by rewrite IH. Qed.
+
   Lemma big_sepL2_sep Φ Ψ l1 l2 :
     ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2 ∗ Ψ k y1 y2)
     ⊣⊢ ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) ∗ ([∗ list] k↦y1;y2 ∈ l1;l2, Ψ k y1 y2).
@@ -903,6 +916,10 @@ Section map.
     ([∗ map] k↦y ∈ f <$> m, Φ k y) ⊣⊢ ([∗ map] k↦y ∈ 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] k↦y ∈ omap f m, Φ k y) ⊣⊢ ([∗ map] k↦y ∈ 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] k↦y ∈ <[i:=x']> m, Φ k y) ⊣⊢ ([∗ map] k↦y ∈ m, Φ k y).

theories/bi/updates.v

@@ -332,6 +332,13 @@ Section fupd_derived.
   Lemma big_sepL_fupd {A} E (Φ : nat → A → PROP) l :
     ([∗ list] k↦x ∈ l, |={E}=> Φ k x) ={E}=∗ [∗ list] k↦x ∈ l, Φ k x.
   Proof. by rewrite (big_opL_commute _). Qed.
+  Lemma big_sepL2_fupd {A B} E (Φ : nat → A → B → PROP) l1 l2 :
+    ([∗ list] k↦x;y ∈ l1;l2, |={E}=> Φ k x y) ={E}=∗ [∗ list] k↦x;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] k↦x ∈ m, |={E}=> Φ k x) ={E}=∗ [∗ map] k↦x ∈ m, Φ k x.
   Proof. by rewrite (big_opM_commute _). Qed.