big_sepM2.

theories/bi/big_op.v

@@ -4,22 +4,7 @@ From stdpp Require Import countable fin_sets functions.
 Set Default Proof Using "Type".
 Import interface.bi derived_laws_bi.bi derived_laws_sbi.bi.
 
-(** A version of the separating big operator that ranges over two lists. This
-version also ensures that both lists have the same length. Although this version
-can be defined in terms of the unary using a [zip] (see [big_sepL2_alt]), we do
-not define it that way to get better computational behavior (for [simpl]). *)
-Fixpoint big_sepL2 {PROP : bi} {A B}
-    (Φ : nat → A → B → PROP) (l1 : list A) (l2 : list B) : PROP :=
-  match l1, l2 with
-  | [], [] => emp
-  | x1 :: l1, x2 :: l2 => Φ 0 x1 x2 ∗ big_sepL2 (λ n, Φ (S n)) l1 l2
-  | _, _ => False
-  end%I.
-Instance: Params (@big_sepL2) 3 := {}.
-Arguments big_sepL2 {PROP A B} _ !_ !_ /.
-Typeclasses Opaque big_sepL2.
-
-(* Notations *)
+(** Notations for unary variants *)
 Notation "'[∗' 'list]' k ↦ x ∈ l , P" :=
   (big_opL bi_sep (λ k x, P) l) : bi_scope.
 Notation "'[∗' 'list]' x ∈ l , P" :=
@@ -27,11 +12,6 @@ Notation "'[∗' 'list]' x ∈ l , P" :=
 
 Notation "'[∗]' Ps" := (big_opL bi_sep (λ _ x, x) Ps) : bi_scope.
 
-Notation "'[∗' 'list]' k ↦ x1 ; x2 ∈ l1 ; l2 , P" :=
-  (big_sepL2 (λ k x1 x2, P) l1 l2) : bi_scope.
-Notation "'[∗' 'list]' x1 ; x2 ∈ l1 ; l2 , P" :=
-  (big_sepL2 (λ _ x1 x2, P) l1 l2) : bi_scope.
-
 Notation "'[∧' 'list]' k ↦ x ∈ l , P" :=
   (big_opL bi_and (λ k x, P) l) : bi_scope.
 Notation "'[∧' 'list]' x ∈ l , P" :=
@@ -46,6 +26,37 @@ Notation "'[∗' 'set]' x ∈ X , P" := (big_opS bi_sep (λ x, P) X) : bi_scope.
 
 Notation "'[∗' 'mset]' x ∈ X , P" := (big_opMS bi_sep (λ x, P) X) : bi_scope.
 
+(** Definitions and notations for binary variants *)
+(** A version of the separating big operator that ranges over two lists. This
+version also ensures that both lists have the same length. Although this version
+can be defined in terms of the unary using a [zip] (see [big_sepL2_alt]), we do
+not define it that way to get better computational behavior (for [simpl]). *)
+Fixpoint big_sepL2 {PROP : bi} {A B}
+    (Φ : nat → A → B → PROP) (l1 : list A) (l2 : list B) : PROP :=
+  match l1, l2 with
+  | [], [] => emp
+  | x1 :: l1, x2 :: l2 => Φ 0 x1 x2 ∗ big_sepL2 (λ n, Φ (S n)) l1 l2
+  | _, _ => False
+  end%I.
+Instance: Params (@big_sepL2) 3 := {}.
+Arguments big_sepL2 {PROP A B} _ !_ !_ /.
+Typeclasses Opaque big_sepL2.
+Notation "'[∗' 'list]' k ↦ x1 ; x2 ∈ l1 ; l2 , P" :=
+  (big_sepL2 (λ k x1 x2, P) l1 l2) : bi_scope.
+Notation "'[∗' 'list]' x1 ; x2 ∈ l1 ; l2 , P" :=
+  (big_sepL2 (λ _ x1 x2, P) l1 l2) : bi_scope.
+
+Definition big_sepM2 {PROP : bi} `{Countable K} {A B}
+    (Φ : K → A → B → PROP) (m1 : gmap K A) (m2 : gmap K B) : PROP :=
+  (⌜ ∀ k, is_Some (m1 !! k) ↔ is_Some (m2 !! k) ⌝ ∧
+   [∗ map] k ↦ xy ∈ map_zip m1 m2, Φ k xy.1 xy.2)%I.
+Instance: Params (@big_sepM2) 6 := {}.
+Typeclasses Opaque big_sepM2.
+Notation "'[∗' 'map]' k ↦ x1 ; x2 ∈ m1 ; m2 , P" :=
+  (big_sepM2 (λ k x1 x2, P) m1 m2) : bi_scope.
+Notation "'[∗' 'map]' x1 ; x2 ∈ m1 ; m2 , P" :=
+  (big_sepM2 (λ _ x1 x2, P) m1 m2) : bi_scope.
+
 (** * Properties *)
 Section bi_big_op.
 Context {PROP : bi}.
@@ -531,7 +542,7 @@ Section and_list.
 End and_list.
 
 (** ** Big ops over finite maps *)
-Section gmap.
+Section map.
   Context `{Countable K} {A : Type}.
   Implicit Types m : gmap K A.
   Implicit Types Φ Ψ : K → A → PROP.
@@ -718,7 +729,211 @@ Section gmap.
   Global Instance big_sepM_affine Φ m :
     (∀ k x, Affine (Φ k x)) → Affine ([∗ map] k↦x ∈ m, Φ k x).
   Proof. intros. apply big_sepL_affine=> _ [??]; apply _. Qed.
-End gmap.
+End map.
+
+(** ** Big ops over two maps *)
+Section map2.
+  Context `{Countable K} {A B : Type}.
+  Implicit Types Φ Ψ : K → A → B → PROP.
+
+  Lemma big_sepM2_empty Φ : ([∗ map] k↦y1;y2 ∈ ∅; ∅, Φ k y1 y2) ⊣⊢ emp.
+  Proof.
+    rewrite /big_sepM2 pure_True ?left_id //.
+    intros k. rewrite !lookup_empty; split; by inversion 1.
+  Qed.
+  Lemma big_sepM2_empty' `{BiAffine PROP} P Φ : P ⊢ [∗ map] k↦y1;y2 ∈ ∅;∅, Φ k y1 y2.
+  Proof. rewrite big_sepM2_empty. apply (affine _). Qed.
+
+  Lemma big_sepM2_insert Φ m1 m2 i x1 x2 :
+    (m1 !! i = None ∨ m2 !! i = None) →
+    ([∗ map] k↦y1;y2 ∈ <[i:=x1]>m1; <[i:=x2]>m2, Φ k y1 y2)
+    ⊣⊢ Φ i x1 x2 ∗ [∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2.
+  Proof.
+    intros Hm. rewrite /big_sepM2 -map_insert_zip_with.
+  Admitted.
+(*
+  Lemma big_sepM2_cons_inv_l Φ x1 m1 m2 :
+    ([∗ map] k↦y1;y2 ∈ x1 :: m1; m2, Φ k y1 y2) -∗
+    ∃ x2 m2', ⌜ m2 = x2 :: m2' ⌝ ∧
+              Φ 0 x1 x2 ∗ [∗ map] k↦y1;y2 ∈ m1;m2', Φ (S k) y1 y2.
+  Proof.
+    destruct m2 as [|x2 m2]; simpl; auto using False_elim.
+    by rewrite -(exist_intro x2) -(exist_intro m2) pure_True // left_id.
+  Qed.
+  Lemma big_sepM2_cons_inv_r Φ x2 m1 m2 :
+    ([∗ map] k↦y1;y2 ∈ m1; x2 :: m2, Φ k y1 y2) -∗
+    ∃ x1 m1', ⌜ m1 = x1 :: m1' ⌝ ∧
+              Φ 0 x1 x2 ∗ [∗ map] k↦y1;y2 ∈ m1';m2, Φ (S k) y1 y2.
+  Proof.
+    destruct m1 as [|x1 m1]; simpl; auto using False_elim.
+    by rewrite -(exist_intro x1) -(exist_intro m1) pure_True // left_id.
+  Qed.
+*)
+
+  Lemma big_sepM2_singleton Φ i x1 x2 :
+    ([∗ map] k↦y1;y2 ∈ {[ i := x1 ]}; {[ i := x2 ]}, Φ k y1 y2) ⊣⊢ Φ i x1 x2.
+  Proof. rewrite /big_sepM2. Admitted.
+
+  Lemma big_sepM2_dom Φ m1 m2 :
+    ([∗ map] k↦y1;y2 ∈ m1; m2, Φ k y1 y2) -∗ ⌜ dom (gset K) m1 = dom (gset K) m2 ⌝.
+  Proof. Admitted.
+
+(*
+  Lemma big_sepM2_app Φ m1 m2 m1' m2' :
+    ([∗ map] k↦y1;y2 ∈ m1; m1', Φ k y1 y2) -∗
+    ([∗ map] k↦y1;y2 ∈ m2; m2', Φ (length m1 + k) y1 y2) -∗
+    ([∗ map] k↦y1;y2 ∈ m1 ++ m2; m1' ++ m2', Φ k y1 y2).
+  Proof.
+    apply wand_intro_r. revert Φ m1'. induction m1 as [|x1 m1 IH]=> Φ -[|x1' m1'] /=.
+    - by rewrite left_id.
+    - rewrite left_absorb. apply False_elim.
+    - rewrite left_absorb. apply False_elim.
+    - by rewrite -assoc IH.
+  Qed.
+  Lemma big_sepM2_app_inv_l Φ m1' m1'' m2 :
+    ([∗ map] k↦y1;y2 ∈ m1' ++ m1''; m2, Φ k y1 y2) -∗
+    ∃ m2' m2'', ⌜ m2 = m2' ++ m2'' ⌝ ∧
+                ([∗ map] k↦y1;y2 ∈ m1';m2', Φ k y1 y2) ∗
+                ([∗ map] k↦y1;y2 ∈ m1'';m2'', Φ (length m1' + k) y1 y2).
+  Proof.
+    rewrite -(exist_intro (take (length m1') m2))
+      -(exist_intro (drop (length m1') m2)) take_drop pure_True // left_id.
+    revert Φ m2. induction m1' as [|x1 m1' IH]=> Φ -[|x2 m2] /=;
+       [by rewrite left_id|by rewrite left_id|apply False_elim|].
+    by rewrite IH -assoc.
+  Qed.
+  Lemma big_sepM2_app_inv_r Φ m1 m2' m2'' :
+    ([∗ map] k↦y1;y2 ∈ m1; m2' ++ m2'', Φ k y1 y2) -∗
+    ∃ m1' m1'', ⌜ m1 = m1' ++ m1'' ⌝ ∧
+                ([∗ map] k↦y1;y2 ∈ m1';m2', Φ k y1 y2) ∗
+                ([∗ map] k↦y1;y2 ∈ m1'';m2'', Φ (length m2' + k) y1 y2).
+  Proof.
+    rewrite -(exist_intro (take (length m2') m1))
+      -(exist_intro (drop (length m2') m1)) take_drop pure_True // left_id.
+    revert Φ m1. induction m2' as [|x2 m2' IH]=> Φ -[|x1 m1] /=;
+       [by rewrite left_id|by rewrite left_id|apply False_elim|].
+    by rewrite IH -assoc.
+  Qed.
+
+  Lemma big_sepM2_mono Φ Ψ m1 m2 :
+    (∀ k y1 y2, m1 !! k = Some y1 → m2 !! k = Some y2 → Φ k y1 y2 ⊢ Ψ k y1 y2) →
+    ([∗ map] k ↦ y1;y2 ∈ m1;m2, Φ k y1 y2) ⊢ [∗ map] k ↦ y1;y2 ∈ m1;m2, Ψ k y1 y2.
+  Proof.
+    intros H. rewrite !big_sepM2_alt. f_equiv. apply big_sepL_mono=> k [y1 y2].
+    rewrite lookup_zip_with=> ?; simplify_option_eq; auto.
+  Qed.
+  Lemma big_sepM2_proper Φ Ψ m1 m2 :
+    (∀ k y1 y2, m1 !! k = Some y1 → m2 !! k = Some y2 → Φ k y1 y2 ⊣⊢ Ψ k y1 y2) →
+    ([∗ map] k ↦ y1;y2 ∈ m1;m2, Φ k y1 y2) ⊣⊢ [∗ map] k ↦ y1;y2 ∈ m1;m2, Ψ k y1 y2.
+  Proof.
+    intros; apply (anti_symm _);
+      apply big_sepM2_mono; auto using equiv_entails, equiv_entails_sym.
+  Qed.
+
+  Global Instance big_sepM2_ne n :
+    Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (dist n)))
+      ==> (=) ==> (=) ==> (dist n))
+           (big_sepM2 (PROP:=PROP) (A:=A) (B:=B)).
+  Proof.
+    intros Φ1 Φ2 HΦ x1 ? <- x2 ? <-. rewrite !big_sepM2_alt. f_equiv.
+    f_equiv=> k [y1 y2]. apply HΦ.
+  Qed.
+  Global Instance big_sepM2_mono' :
+    Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (⊢)))
+      ==> (=) ==> (=) ==> (⊢))
+           (big_sepM2 (PROP:=PROP) (A:=A) (B:=B)).
+  Proof. intros f g Hf m1 ? <- m2 ? <-. apply big_sepM2_mono; intros; apply Hf. Qed.
+  Global Instance big_sepM2_proper' :
+    Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (⊣⊢)))
+      ==> (=) ==> (=) ==> (⊣⊢))
+           (big_sepM2 (PROP:=PROP) (A:=A) (B:=B)).
+  Proof. intros f g Hf m1 ? <- m2 ? <-. apply big_sepM2_proper; intros; apply Hf. Qed.
+
+  Lemma big_sepM2_lookup_acc Φ m1 m2 i x1 x2 :
+    m1 !! i = Some x1 → m2 !! i = Some x2 →
+    ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2) ⊢
+    Φ i x1 x2 ∗ (Φ i x1 x2 -∗ ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2)).
+  Proof.
+    intros Hm1 Hm2. rewrite big_sepM2_alt. apply pure_elim_l=> Hl.
+    rewrite {1}big_sepL_lookup_acc; last by rewrite lookup_zip_with; simplify_option_eq.
+    by rewrite pure_True // left_id.
+  Qed.
+
+  Lemma big_sepM2_lookup Φ m1 m2 i x1 x2 `{!Absorbing (Φ i x1 x2)} :
+    m1 !! i = Some x1 → m2 !! i = Some x2 →
+    ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2) ⊢ Φ i x1 x2.
+  Proof. intros. rewrite big_sepM2_lookup_acc //. by rewrite sep_elim_l. Qed.
+
+  Lemma big_sepM2_fmap_l {A'} (f : A → A') (Φ : nat → A' → B → PROP) m1 m2 :
+    ([∗ map] k↦y1;y2 ∈ f <$> m1; m2, Φ k y1 y2)
+    ⊣⊢ ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k (f y1) y2).
+  Proof.
+    rewrite !big_sepM2_alt fmap_length zip_with_fmap_l zip_with_zip big_sepL_fmap.
+    by f_equiv; f_equiv=> k [??].
+  Qed.
+  Lemma big_sepM2_fmap_r {B'} (g : B → B') (Φ : nat → A → B' → PROP) m1 m2 :
+    ([∗ map] k↦y1;y2 ∈ m1; g <$> m2, Φ k y1 y2)
+    ⊣⊢ ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 (g y2)).
+  Proof.
+    rewrite !big_sepM2_alt fmap_length zip_with_fmap_r zip_with_zip big_sepL_fmap.
+    by f_equiv; f_equiv=> k [??].
+  Qed.
+
+  Lemma big_sepM2_sepM2 Φ Ψ m1 m2 :
+    ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2 ∗ Ψ k y1 y2)
+    ⊣⊢ ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2) ∗ ([∗ map] k↦y1;y2 ∈ m1;m2, Ψ k y1 y2).
+  Proof.simpl
+    rewrite !big_sepM2_alt big_sepL_sepL !persistent_and_affinely_sep_l.
+    rewrite -assoc (assoc _ _ (<affine> _)%I). rewrite -(comm bi_sep (<affine> _)%I).
+    rewrite -assoc (assoc _ _ (<affine> _)%I) -!persistent_and_affinely_sep_l.
+    by rewrite affinely_and_r persistent_and_affinely_sep_l idemp.
+  Qed.
+
+  Lemma big_sepM2_and Φ Ψ m1 m2 :
+    ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2 ∧ Ψ k y1 y2)
+    ⊢ ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2) ∧ ([∗ map] k↦y1;y2 ∈ m1;m2, Ψ k y1 y2).
+  Proof. auto using and_intro, big_sepM2_mono, and_elim_l, and_elim_r. Qed.
+
+  Lemma big_sepM2_persistently `{BiAffine PROP} Φ m1 m2 :
+    <pers> ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2)
+    ⊣⊢ [∗ map] k↦y1;y2 ∈ m1;m2, <pers> (Φ k y1 y2).
+  Proof.
+    by rewrite !big_sepM2_alt persistently_and persistently_pure big_sepL_persistently.
+  Qed.
+
+  Lemma big_sepM2_impl Φ Ψ m1 m2 :
+    ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2) -∗
+    □ (∀ k x1 x2,
+      ⌜m1 !! k = Some x1⌝ → ⌜m2 !! k = Some x2⌝ → Φ k x1 x2 -∗ Ψ k x1 x2) -∗
+    [∗ map] k↦y1;y2 ∈ m1;m2, Ψ k y1 y2.
+  Proof.
+    apply wand_intro_l. revert Φ Ψ m2.
+    induction m1 as [|x1 m1 IH]=> Φ Ψ [|x2 m2] /=; [by rewrite sep_elim_r..|].
+    rewrite intuitionistically_sep_dup -assoc [(□ _ ∗ _)%I]comm -!assoc assoc.
+    apply sep_mono.
+    - rewrite (forall_elim 0) (forall_elim x1) (forall_elim x2) !pure_True // !True_impl.
+      by rewrite intuitionistically_elim wand_elim_l.
+    - rewrite comm -(IH (Φ ∘ S) (Ψ ∘ S)) /=.
+      apply sep_mono_l, affinely_mono, persistently_mono.
+      apply forall_intro=> k. by rewrite (forall_elim (S k)).
+  Qed.
+*)
+  Global Instance big_sepM2_empty_persistent Φ :
+    Persistent ([∗ map] k↦y1;y2 ∈ ∅; ∅, Φ k y1 y2).
+  Proof. rewrite big_sepM2_empty. apply _. Qed.
+  Global Instance big_sepM2_persistent Φ m1 m2 :
+    (∀ k x1 x2, Persistent (Φ k x1 x2)) →
+    Persistent ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2).
+  Proof. (* rewrite big_sepM2_alt. apply _. Qed. *) Admitted.
+
+  Global Instance big_sepM2_empty_affine Φ :
+    Affine ([∗ map] k↦y1;y2 ∈ ∅; ∅, Φ k y1 y2).
+  Proof. rewrite big_sepM2_empty. apply _. Qed.
+  Global Instance big_sepM2_affine Φ m1 m2 :
+    (∀ k x1 x2, Affine (Φ k x1 x2)) →
+    Affine ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2).
+  Proof. (* rewrite big_sepM2_alt. apply _. Qed. *) Admitted.
+End map2.
 
 (** ** Big ops over finite sets *)
 Section gset.

theories/bi/notation.v

@@ -127,6 +127,13 @@ Reserved Notation "'[∗' 'map]' x ∈ m , P"
   (at level 200, m at level 10, x at level 1, right associativity,
    format "[∗  map]  x  ∈  m ,  P").
 
+Reserved Notation "'[∗' 'map]' k ↦ x1 ; x2 ∈ m1 ; m2 , P"
+  (at level 200, m1, m2 at level 10, k, x1, x2 at level 1, right associativity,
+   format "[∗  map]  k ↦ x1 ; x2  ∈  m1 ; m2 ,  P").
+Reserved Notation "'[∗' 'map]' x1 ; x2 ∈ m1 ; m2 , P"
+  (at level 200, m1, m2 at level 10, x1, x2 at level 1, right associativity,
+   format "[∗  map]  x1 ; x2  ∈  m1 ; m2 ,  P").
+
 Reserved Notation "'[∗' 'set]' x ∈ X , P"
   (at level 200, X at level 10, x at level 1, right associativity,
    format "[∗  set]  x  ∈  X ,  P").