From 92b4913fbc28fc375cc056830de292af8db5e8d8 Mon Sep 17 00:00:00 2001 From: Hoang-Hai Dang 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 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 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 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