From 92b4913fbc28fc375cc056830de292af8db5e8d8 Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Wed, 21 Oct 2020 13:13:47 +0200
Subject: [PATCH 1/4] add commutativity lemmas for bi exist and forall

---
 theories/bi/derived_laws.v | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index e9191e134..50c884b75 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -249,6 +249,27 @@ Proof.
   - rewrite -(exist_intro ()). done.
 Qed.
 
+Lemma exist_comm {A B} (Ψ : A → B → PROP) :
+  (∃ (x : A) (y : B), Ψ x y) ⊣⊢ (∃ (y : B) (x : A), Ψ x y).
+Proof.
+  apply (anti_symm (⊢));
+    do 2 apply exist_elim => ?;
+    do 2 rewrite -exist_intro; eauto.
+Qed.
+Lemma forall_comm {A B} (Ψ : A → B → PROP) :
+  (∀ (x : A) (y : B), Ψ x y) ⊣⊢ (∀ (y : B) (x : A), Ψ x y).
+Proof.
+  apply (anti_symm (⊢));
+    do 2 apply forall_intro=>?;
+    do 2 rewrite forall_elim; eauto.
+Qed.
+Lemma exist_forall_comm {A B} (Ψ : A → B → PROP) :
+  (∃ (x : A), ∀ (y : B), Ψ x y) ⊢ (∀ (y : B), ∃ (x : A), Ψ x y).
+Proof.
+  apply forall_intro=>?. apply exist_elim=>?.
+  rewrite -exist_intro forall_elim ; eauto.
+Qed.
+
 Lemma impl_curry P Q R : (P → Q → R) ⊣⊢ (P ∧ Q → R).
 Proof.
   apply (anti_symm _).
-- 
GitLab


From 8d11b41c93993006eadc8e37ae39fb4478312f2b Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Wed, 21 Oct 2020 13:24:52 +0200
Subject: [PATCH 2/4] rename exist/forall_comm to exist/forall_swap; reformat
 proof

---
 theories/bi/derived_laws.v | 12 +++++-------
 1 file changed, 5 insertions(+), 7 deletions(-)

diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index 50c884b75..4dd18468b 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -249,21 +249,19 @@ Proof.
   - rewrite -(exist_intro ()). done.
 Qed.
 
-Lemma exist_comm {A B} (Ψ : A → B → PROP) :
+Lemma exist_swap {A B} (Ψ : A → B → PROP) :
   (∃ (x : A) (y : B), Ψ x y) ⊣⊢ (∃ (y : B) (x : A), Ψ x y).
 Proof.
   apply (anti_symm (⊢));
-    do 2 apply exist_elim => ?;
-    do 2 rewrite -exist_intro; eauto.
+    do 2 (apply exist_elim=>?); rewrite -2!exist_intro; eauto.
 Qed.
-Lemma forall_comm {A B} (Ψ : A → B → PROP) :
+Lemma forall_swap {A B} (Ψ : A → B → PROP) :
   (∀ (x : A) (y : B), Ψ x y) ⊣⊢ (∀ (y : B) (x : A), Ψ x y).
 Proof.
   apply (anti_symm (⊢));
-    do 2 apply forall_intro=>?;
-    do 2 rewrite forall_elim; eauto.
+    do 2 (apply forall_intro=>?); rewrite 2!forall_elim; eauto.
 Qed.
-Lemma exist_forall_comm {A B} (Ψ : A → B → PROP) :
+Lemma exist_forall_swap {A B} (Ψ : A → B → PROP) :
   (∃ (x : A), ∀ (y : B), Ψ x y) ⊢ (∀ (y : B), ∃ (x : A), Ψ x y).
 Proof.
   apply forall_intro=>?. apply exist_elim=>?.
-- 
GitLab


From d8bcd73c6ba6051f8f34c33c3c0bd48cb64d9027 Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Wed, 21 Oct 2020 13:45:18 +0200
Subject: [PATCH 3/4] address more comments

---
 theories/bi/derived_laws.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index 4dd18468b..7bbed3948 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -250,19 +250,19 @@ Proof.
 Qed.
 
 Lemma exist_swap {A B} (Ψ : A → B → PROP) :
-  (∃ (x : A) (y : B), Ψ x y) ⊣⊢ (∃ (y : B) (x : A), Ψ x y).
+  (∃ x y, Ψ x y) ⊣⊢ (∃ y x, Ψ x y).
 Proof.
   apply (anti_symm (⊢));
     do 2 (apply exist_elim=>?); rewrite -2!exist_intro; eauto.
 Qed.
 Lemma forall_swap {A B} (Ψ : A → B → PROP) :
-  (∀ (x : A) (y : B), Ψ x y) ⊣⊢ (∀ (y : B) (x : A), Ψ x y).
+  (∀ x y, Ψ x y) ⊣⊢ (∀ y x, Ψ x y).
 Proof.
   apply (anti_symm (⊢));
     do 2 (apply forall_intro=>?); rewrite 2!forall_elim; eauto.
 Qed.
-Lemma exist_forall_swap {A B} (Ψ : A → B → PROP) :
-  (∃ (x : A), ∀ (y : B), Ψ x y) ⊢ (∀ (y : B), ∃ (x : A), Ψ x y).
+Lemma exist_forall {A B} (Ψ : A → B → PROP) :
+  (∃ x, ∀ y, Ψ x y) ⊢ (∀ y, ∃ x, Ψ x y).
 Proof.
   apply forall_intro=>?. apply exist_elim=>?.
   rewrite -exist_intro forall_elim ; eauto.
-- 
GitLab


From 6c3914cf81c78e598857236e6a55eb146e679b69 Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Wed, 21 Oct 2020 16:42:30 +0200
Subject: [PATCH 4/4] rename lemmas

---
 theories/bi/derived_laws.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index 7bbed3948..b8170151a 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -249,13 +249,13 @@ Proof.
   - rewrite -(exist_intro ()). done.
 Qed.
 
-Lemma exist_swap {A B} (Ψ : A → B → PROP) :
+Lemma exist_exist {A B} (Ψ : A → B → PROP) :
   (∃ x y, Ψ x y) ⊣⊢ (∃ y x, Ψ x y).
 Proof.
   apply (anti_symm (⊢));
     do 2 (apply exist_elim=>?); rewrite -2!exist_intro; eauto.
 Qed.
-Lemma forall_swap {A B} (Ψ : A → B → PROP) :
+Lemma forall_forall {A B} (Ψ : A → B → PROP) :
   (∀ x y, Ψ x y) ⊣⊢ (∀ y x, Ψ x y).
 Proof.
   apply (anti_symm (⊢));
-- 
GitLab