From 8e3d704dac9b7c146e85dcf661ddfdb645418332 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 14 Jan 2021 13:05:54 +0900 Subject: [PATCH 1/3] iff lemmas --- CHANGELOG_UNRELEASED.md | 1 + theories/boolp.v | 6 ++++++ 2 files changed, 7 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 313ca10ebe..4c4b89dea8 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -17,6 +17,7 @@ - in `classical_sets.v`, lemmas `subset_has_lbound`, `subset_has_ubound` - in `reals.v`, lemmas `sup_setU`, `inf_setU` +- in `boolp.v`, lemmas `iff_notP`, `iff_not` ### Changed diff --git a/theories/boolp.v b/theories/boolp.v index 2bbde07dac..f62c5d0b67 100644 --- a/theories/boolp.v +++ b/theories/boolp.v @@ -366,6 +366,12 @@ Lemma notLR P Q : (P = ~ Q) -> (~ P) = Q. Proof. exact: canLR notK. Qed. Lemma notRL P Q : (~ P) = Q -> P = ~ Q. Proof. exact: canRL notK. Qed. +Lemma iff_notP (P Q : Prop) : (P <-> ~ Q) <-> (~ P <-> Q). +Proof. by split=> [/propext ->|/propext <-]; rewrite notK. Qed. + +Lemma iff_not (P Q : Prop) : (P <-> Q) <-> (~ P <-> ~ Q). +Proof. by split=> [PQ|/iff_notP]; [apply/iff_notP|]; rewrite notK. Qed. + (* -------------------------------------------------------------------- *) (* assia : let's see if we need the simplpred machinery. In any case, we sould first try definitions + appropriate Arguments setting to see whether these From c64655e98cbfb16b204cd1428ecbef1bdb38b078 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Tue, 19 Jan 2021 17:35:24 +0900 Subject: [PATCH 2/3] Update theories/boolp.v Co-authored-by: Cyril Cohen --- theories/boolp.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/theories/boolp.v b/theories/boolp.v index f62c5d0b67..c3b5a50072 100644 --- a/theories/boolp.v +++ b/theories/boolp.v @@ -366,11 +366,11 @@ Lemma notLR P Q : (P = ~ Q) -> (~ P) = Q. Proof. exact: canLR notK. Qed. Lemma notRL P Q : (~ P) = Q -> P = ~ Q. Proof. exact: canRL notK. Qed. -Lemma iff_notP (P Q : Prop) : (P <-> ~ Q) <-> (~ P <-> Q). +Lemma iff_notr (P Q : Prop) : (P <-> ~ Q) <-> (~ P <-> Q). Proof. by split=> [/propext ->|/propext <-]; rewrite notK. Qed. -Lemma iff_not (P Q : Prop) : (P <-> Q) <-> (~ P <-> ~ Q). -Proof. by split=> [PQ|/iff_notP]; [apply/iff_notP|]; rewrite notK. Qed. +Lemma iff_not2 (P Q : Prop) : (~ P <-> ~ Q) <-> (P <-> Q). +Proof. by split=> [iff_notP|PQ]; [|apply/iff_notP]; rewrite notK. Qed. (* -------------------------------------------------------------------- *) (* assia : let's see if we need the simplpred machinery. In any case, we sould From b924734834f5beb940b2eef7d6d26b41001df197 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 19 Jan 2021 17:46:47 +0900 Subject: [PATCH 3/3] fix and changelog update --- CHANGELOG_UNRELEASED.md | 2 +- theories/boolp.v | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 4c4b89dea8..30a20f3d12 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -17,7 +17,7 @@ - in `classical_sets.v`, lemmas `subset_has_lbound`, `subset_has_ubound` - in `reals.v`, lemmas `sup_setU`, `inf_setU` -- in `boolp.v`, lemmas `iff_notP`, `iff_not` +- in `boolp.v`, lemmas `iff_notr`, `iff_not2` ### Changed diff --git a/theories/boolp.v b/theories/boolp.v index c3b5a50072..3c059dc4f2 100644 --- a/theories/boolp.v +++ b/theories/boolp.v @@ -370,7 +370,7 @@ Lemma iff_notr (P Q : Prop) : (P <-> ~ Q) <-> (~ P <-> Q). Proof. by split=> [/propext ->|/propext <-]; rewrite notK. Qed. Lemma iff_not2 (P Q : Prop) : (~ P <-> ~ Q) <-> (P <-> Q). -Proof. by split=> [iff_notP|PQ]; [|apply/iff_notP]; rewrite notK. Qed. +Proof. by split=> [/iff_notr|PQ]; [|apply/iff_notr]; rewrite notK. Qed. (* -------------------------------------------------------------------- *) (* assia : let's see if we need the simplpred machinery. In any case, we sould