From 834c66e0582a92bc8e42c5499e2120519ed14ef3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 30 Sep 2016 09:55:14 +0200
Subject: [PATCH] Extensionality (for Leibniz equality) of big ops.

---
 algebra/cmra_big_op.v  | 26 +++++++++++++++++---------
 algebra/upred_big_op.v | 13 +++++--------
 2 files changed, 22 insertions(+), 17 deletions(-)

diff --git a/algebra/cmra_big_op.v b/algebra/cmra_big_op.v
index 7bc069d25..6fe6cda19 100644
--- a/algebra/cmra_big_op.v
+++ b/algebra/cmra_big_op.v
@@ -138,6 +138,10 @@ Section list.
     (∀ k y, l !! k = Some y → f k y ≼ g k y) →
     ([⋅ list] k ↦ y ∈ l, f k y) ≼ [⋅ list] k ↦ y ∈ l, g k y.
   Proof. apply big_opL_forall; apply _. Qed.
+  Lemma big_opL_ext f g l :
+    (∀ k y, l !! k = Some y → f k y = g k y) →
+    ([⋅ list] k ↦ y ∈ l, f k y) = [⋅ list] k ↦ y ∈ l, g k y.
+  Proof. apply big_opL_forall; apply _. Qed.
   Lemma big_opL_proper f g l :
     (∀ k y, l !! k = Some y → f k y ≡ g k y) →
     ([⋅ list] k ↦ y ∈ l, f k y) ≡ ([⋅ list] k ↦ y ∈ l, g k y).
@@ -207,6 +211,10 @@ Section gmap.
     - by apply big_op_contains, fmap_contains, map_to_list_contains.
     - apply big_opM_forall; apply _ || auto.
   Qed.
+  Lemma big_opM_ext f g m :
+    (∀ k x, m !! k = Some x → f k x = g k x) →
+    ([⋅ map] k ↦ x ∈ m, f k x) = ([⋅ map] k ↦ x ∈ m, g k x).
+  Proof. apply big_opM_forall; apply _. Qed.
   Lemma big_opM_proper f g m :
     (∀ k x, m !! k = Some x → f k x ≡ g k x) →
     ([⋅ map] k ↦ x ∈ m, f k x) ≡ ([⋅ map] k ↦ x ∈ m, g k x).
@@ -314,14 +322,14 @@ Section gset.
     - by apply big_op_contains, fmap_contains, elements_contains.
     - apply big_opS_forall; apply _ || auto.
   Qed.
-  Lemma big_opS_proper f g X Y :
-    X ≡ Y → (∀ x, x ∈ X → x ∈ Y → f x ≡ g x) →
-    ([⋅ set] x ∈ X, f x) ≡ ([⋅ set] x ∈ Y, g x).
-  Proof.
-    intros HX Hf. trans ([⋅ set] x ∈ Y, f x).
-    - apply big_op_permutation. by rewrite HX.
-    - apply big_opS_forall; try apply _ || set_solver.
-  Qed.
+  Lemma big_opS_ext f g X :
+    (∀ x, x ∈ X → f x = g x) →
+    ([⋅ set] x ∈ X, f x) = ([⋅ set] x ∈ X, g x).
+  Proof. apply big_opS_forall; apply _. Qed.
+  Lemma big_opS_proper f g X :
+    (∀ x, x ∈ X → f x ≡ g x) →
+    ([⋅ set] x ∈ X, f x) ≡ ([⋅ set] x ∈ X, g x).
+  Proof. apply big_opS_forall; apply _. Qed.
 
   Lemma big_opS_ne X n :
     Proper (pointwise_relation _ (dist n) ==> dist n) (big_opS (M:=M) X).
@@ -345,7 +353,7 @@ Section gset.
     ≡ (f x b ⋅ [⋅ set] y ∈ X, f y (h y)).
   Proof.
     intros. rewrite big_opS_insert // fn_lookup_insert.
-    apply cmra_op_proper', big_opS_proper; auto=> y ??.
+    apply cmra_op_proper', big_opS_proper; auto=> y ?.
     by rewrite fn_lookup_insert_ne; last set_solver.
   Qed.
   Lemma big_opS_fn_insert' f X x P :
diff --git a/algebra/upred_big_op.v b/algebra/upred_big_op.v
index 8571558e8..9f2dded3d 100644
--- a/algebra/upred_big_op.v
+++ b/algebra/upred_big_op.v
@@ -125,7 +125,6 @@ Section list.
     (∀ k y, l !! k = Some y → Φ k y ⊢ Ψ k y) →
     ([★ list] k ↦ y ∈ l, Φ k y) ⊢ [★ list] k ↦ y ∈ l, Ψ k y.
   Proof. apply big_opL_forall; apply _. Qed.
-
   Lemma big_sepL_proper Φ Ψ l :
     (∀ k y, l !! k = Some y → Φ k y ⊣⊢ Ψ k y) →
     ([★ list] k ↦ y ∈ l, Φ k y) ⊣⊢ ([★ list] k ↦ y ∈ l, Ψ k y).
@@ -219,7 +218,6 @@ Section gmap.
       by apply fmap_contains, map_to_list_contains.
     - apply big_opM_forall; apply _ || auto.
   Qed.
-
   Lemma big_sepM_proper Φ Ψ m :
     (∀ k x, m !! k = Some x → Φ k x ⊣⊢ Ψ k x) →
     ([★ map] k ↦ x ∈ m, Φ k x) ⊣⊢ ([★ map] k ↦ x ∈ m, Ψ k x).
@@ -344,16 +342,15 @@ Section gset.
       by apply fmap_contains, elements_contains.
     - apply big_opS_forall; apply _ || auto.
   Qed.
+  Lemma big_sepS_proper Φ Ψ X :
+    (∀ x, x ∈ X → Φ x ⊣⊢ Ψ x) →
+    ([★ set] x ∈ X, Φ x) ⊣⊢ ([★ set] x ∈ X, Ψ x).
+  Proof. apply: big_opS_proper. Qed.
 
-  Lemma big_sepS_mono' X :
+  Global Instance big_sepS_mono' X :
      Proper (pointwise_relation _ (⊢) ==> (⊢)) (big_opS (M:=uPredUR M) X).
   Proof. intros f g Hf. apply big_opS_forall; apply _ || intros; apply Hf. Qed.
 
-  Lemma big_sepS_proper Φ Ψ X Y :
-    X ≡ Y → (∀ x, x ∈ X → x ∈ Y → Φ x ⊣⊢ Ψ x) →
-    ([★ set] x ∈ X, Φ x) ⊣⊢ ([★ set] x ∈ Y, Ψ x).
-  Proof. apply: big_opS_proper. Qed.
-
   Lemma big_sepS_empty Φ : ([★ set] x ∈ ∅, Φ x) ⊣⊢ True.
   Proof. by rewrite big_opS_empty. Qed.
 
-- 
GitLab