Strong `Proper` lemmas for `big_op{L,M}` for setoids on the lists/maps.

theories/algebra/big_op.v

@@ -155,6 +155,22 @@ Section list.
     ([^o list] k ↦ y ∈ l, f k y) ≡ ([^o list] k ↦ y ∈ l, g k y).
   Proof. apply big_opL_gen_proper; apply _. Qed.
 
+  (** The version [big_opL_proper_2] with [≡] for the list arguments can only be
+  used if there is a setoid on [A]. The version for [dist n] can be found in
+  [algebra.list]. We do not define this lemma as a [Proper] instance, since
+  [f_equiv] will then use sometimes use this one, and other times
+  [big_opL_proper'], depending on whether a setoid on [A] exists. *)
+  Lemma big_opL_proper_2 `{!Equiv A} f g l1 l2 :
+    l1 ≡ l2 →
+    (∀ k y1 y2,
+      l1 !! k = Some y1 → l2 !! k = Some y2 → y1 ≡ y2 → f k y1 ≡ g k y2) →
+    ([^o list] k ↦ y ∈ l1, f k y) ≡ ([^o list] k ↦ y ∈ l2, g k y).
+  Proof.
+    intros Hl Hf. apply big_opL_gen_proper_2; try (apply _ || done).
+    intros k. assert (l1 !! k ≡ l2 !! k) as Hlk by (by f_equiv).
+    destruct (l1 !! k) eqn:?, (l2 !! k) eqn:?; inversion Hlk; naive_solver.
+  Qed.
+
   Global Instance big_opL_ne' n :
     Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (=) ==> dist n)
            (big_opL o (A:=A)).
@@ -262,6 +278,21 @@ Section gmap.
     (∀ k x, m !! k = Some x → f k x ≡ g k x) →
     ([^o map] k ↦ x ∈ m, f k x) ≡ ([^o map] k ↦ x ∈ m, g k x).
   Proof. apply big_opM_gen_proper; apply _. Qed.
+  (** The version [big_opL_proper_2] with [≡] for the map arguments can only be
+  used if there is a setoid on [A]. The version for [dist n] can be found in
+  [algebra.gmap]. We do not define this lemma as a [Proper] instance, since
+  [f_equiv] will then use sometimes use this one, and other times
+  [big_opM_proper'], depending on whether a setoid on [A] exists. *)
+  Lemma big_opM_proper_2 `{!Equiv A} f g m1 m2 :
+    m1 ≡ m2 →
+    (∀ k y1 y2,
+      m1 !! k = Some y1 → m2 !! k = Some y2 → y1 ≡ y2 → f k y1 ≡ g k y2) →
+    ([^o map] k ↦ y ∈ m1, f k y) ≡ ([^o map] k ↦ y ∈ m2, g k y).
+  Proof.
+    intros Hl Hf. apply big_opM_gen_proper_2; try (apply _ || done).
+    intros k. assert (m1 !! k ≡ m2 !! k) as Hlk by (by f_equiv).
+    destruct (m1 !! k) eqn:?, (m2 !! k) eqn:?; inversion Hlk; naive_solver.
+  Qed.
 
   Global Instance big_opM_ne' n :
     Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (=) ==> dist n)

theories/algebra/gmap.v

@@ -119,6 +119,39 @@ Proof.
   destruct 1; destruct 1; repeat f_equiv; constructor || done.
 Qed.
 
+Lemma big_opM_ne_2 `{Monoid M o} `{Countable K} {A : ofeT} (f g : K → A → M) m1 m2 n :
+  m1 ≡{n}≡ m2 →
+  (∀ k y1 y2,
+    m1 !! k = Some y1 → m2 !! k = Some y2 → y1 ≡{n}≡ y2 → f k y1 ≡{n}≡ g k y2) →
+  ([^o map] k ↦ y ∈ m1, f k y) ≡{n}≡ ([^o map] k ↦ y ∈ m2, g k y).
+Proof.
+  intros Hl Hf. apply big_opM_gen_proper_2; try (apply _ || done).
+  { by intros ?? ->. }
+  { apply monoid_ne. }
+  intros k. assert (m1 !! k ≡{n}≡ m2 !! k) as Hlk by (by f_equiv).
+  destruct (m1 !! k) eqn:?, (m2 !! k) eqn:?; inversion Hlk; naive_solver.
+Qed.
+
+Lemma big_sepM2_ne_2 {PROP : bi} `{Countable K} (A B : ofeT)
+    (Φ Ψ : K → A → B → PROP) m1 m2 m1' m2' n :
+  m1 ≡{n}≡ m1' → m2 ≡{n}≡ m2' →
+  (∀ k y1 y1' y2 y2',
+    m1 !! k = Some y1 → m1' !! k = Some y1' → y1 ≡{n}≡ y1' →
+    m2 !! k = Some y2 → m2' !! k = Some y2' → y2 ≡{n}≡ y2' →
+    Φ k y1 y2 ≡{n}≡ Ψ k y1' y2') →
+  ([∗ map] k ↦ y1;y2 ∈ m1;m2, Φ k y1 y2)%I ≡{n}≡ ([∗ map] k ↦ y1;y2 ∈ m1';m2', Ψ k y1 y2)%I.
+Proof.
+  intros Hm1 Hm2 Hf. rewrite big_sepM2_eq /big_sepM2_def. f_equiv.
+  { f_equiv; split; intros Hm k.
+    - trans (is_Some (m1 !! k)); [symmetry; apply: is_Some_ne; by f_equiv|].
+      rewrite Hm. apply: is_Some_ne; by f_equiv.
+    - trans (is_Some (m1' !! k)); [apply: is_Some_ne; by f_equiv|].
+      rewrite Hm. symmetry. apply: is_Some_ne; by f_equiv. }
+  apply big_opM_ne_2; [by f_equiv|].
+  intros k [x1 y1] [x2 y2] (?&?&[=<- <-]&?&?)%map_lookup_zip_with_Some
+    (?&?&[=<- <-]&?&?)%map_lookup_zip_with_Some [??]; naive_solver.
+Qed.
+
 (* CMRA *)
 Section cmra.
 Context `{Countable K} {A : cmraT}.

theories/algebra/list.v

@@ -120,6 +120,34 @@ Instance zip_with_ne {A B C : ofeT} (f : A → B → C) :
   Proper (dist n ==> dist n ==> dist n) (zip_with f).
 Proof. induction 2; destruct 1; simpl; [constructor..|f_equiv; [f_equiv|]; auto]. Qed.
 
+Lemma big_opL_ne_2 `{Monoid M o} {A : ofeT} (f g : nat → A → M) l1 l2 n :
+  l1 ≡{n}≡ l2 →
+  (∀ k y1 y2,
+    l1 !! k = Some y1 → l2 !! k = Some y2 → y1 ≡{n}≡ y2 → f k y1 ≡{n}≡ g k y2) →
+  ([^o list] k ↦ y ∈ l1, f k y) ≡{n}≡ ([^o list] k ↦ y ∈ l2, g k y).
+Proof.
+  intros Hl Hf. apply big_opL_gen_proper_2; try (apply _ || done).
+  { apply monoid_ne. }
+  intros k. assert (l1 !! k ≡{n}≡ l2 !! k) as Hlk by (by f_equiv).
+  destruct (l1 !! k) eqn:?, (l2 !! k) eqn:?; inversion Hlk; naive_solver.
+Qed.
+
+Lemma big_sepL2_ne_2 {PROP : bi} {A B : ofeT}
+    (Φ Ψ : nat → A → B → PROP) l1 l2 l1' l2' n :
+  l1 ≡{n}≡ l1' → l2 ≡{n}≡ l2' →
+  (∀ k y1 y1' y2 y2',
+    l1 !! k = Some y1 → l1' !! k = Some y1' → y1 ≡{n}≡ y1' →
+    l2 !! k = Some y2 → l2' !! k = Some y2' → y2 ≡{n}≡ y2' →
+    Φ k y1 y2 ≡{n}≡ Ψ k y1' y2') →
+  ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2)%I ≡{n}≡ ([∗ list] k ↦ y1;y2 ∈ l1';l2', Ψ k y1 y2)%I.
+Proof.
+  intros Hl1 Hl2 Hf. rewrite !big_sepL2_alt. f_equiv.
+  { do 2 f_equiv; by apply: length_ne. }
+  apply big_opL_ne_2; [by f_equiv|].
+  intros k [x1 y1] [x2 y2] (?&?&[=<- <-]&?&?)%lookup_zip_with_Some
+    (?&?&[=<- <-]&?&?)%lookup_zip_with_Some [??]; naive_solver.
+Qed.
+
 (** Functor *)
 Lemma list_fmap_ext_ne {A} {B : ofeT} (f g : A → B) (l : list A) n :
   (∀ x, f x ≡{n}≡ g x) → f <$> l ≡{n}≡ g <$> l.

theories/bi/big_op.v

@@ -381,6 +381,20 @@ Section sep_list2.
     intros; apply (anti_symm _);
       apply big_sepL2_mono; auto using equiv_entails, equiv_entails_sym.
   Qed.
+  Lemma big_sepL2_proper_2 `{!Equiv A, !Equiv B} Φ Ψ l1 l2 l1' l2' :
+    l1 ≡ l1' → l2 ≡ l2' →
+    (∀ k y1 y1' y2 y2',
+      l1 !! k = Some y1 → l1' !! k = Some y1' → y1 ≡ y1' →
+      l2 !! k = Some y2 → l2' !! k = Some y2' → y2 ≡ y2' →
+      Φ k y1 y2 ⊣⊢ Ψ k y1' y2') →
+    ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2) ⊣⊢ [∗ list] k ↦ y1;y2 ∈ l1';l2', Ψ k y1 y2.
+  Proof.
+    intros Hl1 Hl2 Hf. rewrite !big_sepL2_alt. f_equiv.
+    { do 2 f_equiv; by apply length_proper. }
+    apply big_opL_proper_2; [by f_equiv|].
+    intros k [x1 y1] [x2 y2] (?&?&[=<- <-]&?&?)%lookup_zip_with_Some
+      (?&?&[=<- <-]&?&?)%lookup_zip_with_Some [??]; naive_solver.
+  Qed.
 
   Global Instance big_sepL2_ne' n :
     Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (dist n)))
@@ -950,6 +964,24 @@ Section map2.
     intros; apply (anti_symm _);
       apply big_sepM2_mono; auto using equiv_entails, equiv_entails_sym.
   Qed.
+  Lemma big_sepM2_proper_2 `{!Equiv A, !Equiv B} Φ Ψ m1 m2 m1' m2' :
+    m1 ≡ m1' → m2 ≡ m2' →
+    (∀ k y1 y1' y2 y2',
+      m1 !! k = Some y1 → m1' !! k = Some y1' → y1 ≡ y1' →
+      m2 !! k = Some y2 → m2' !! k = Some y2' → y2 ≡ 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 Hm1 Hm2 Hf. rewrite big_sepM2_eq /big_sepM2_def. f_equiv.
+    { f_equiv; split; intros Hm k.
+      - trans (is_Some (m1 !! k)); [symmetry; apply is_Some_proper; by f_equiv|].
+        rewrite Hm. apply is_Some_proper; by f_equiv.
+      - trans (is_Some (m1' !! k)); [apply is_Some_proper; by f_equiv|].
+        rewrite Hm. symmetry. apply is_Some_proper; by f_equiv. }
+    apply big_opM_proper_2; [by f_equiv|].
+    intros k [x1 y1] [x2 y2] (?&?&[=<- <-]&?&?)%map_lookup_zip_with_Some
+      (?&?&[=<- <-]&?&?)%map_lookup_zip_with_Some [??]; naive_solver.
+  Qed.
 
   Global Instance big_sepM2_ne' n :
     Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (dist n)))