From 1d3c90de94e1c05d42aba704a80ab1135bdc058f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 14 Oct 2019 12:37:57 +0200
Subject: Logic: Add equivalence between weak excluded-middle and classical
 Morgan's law

---
 theories/Logic/ClassicalFacts.v | 19 +++++++++++++++++--
 1 file changed, 17 insertions(+), 2 deletions(-)

diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v
index 2a9e15ab37..98dcd0d122 100644
--- a/theories/Logic/ClassicalFacts.v
+++ b/theories/Logic/ClassicalFacts.v
@@ -29,7 +29,7 @@ Table of contents:
 
 3. Weak classical axioms
 
-3.1. Weak excluded middle
+3.1. Weak excluded middle and classical de Morgan law
 
 3.2. Gödel-Dummett axiom and right distributivity of implication over
      disjunction
@@ -514,7 +514,7 @@ End Weak_proof_irrelevance_CCI.
 (** * Weak classical axioms *)
 
 (** We show the following increasing in the strength of axioms:
- - weak excluded-middle
+ - weak excluded-middle and classical De Morgan's law
  - right distributivity of implication over disjunction and Gödel-Dummett axiom
  - independence of general premises and drinker's paradox
  - excluded-middle
@@ -539,6 +539,11 @@ Definition weak_excluded_middle :=
 Definition weak_generalized_excluded_middle :=
   forall A B:Prop, ((A -> B) -> B) \/ (A -> B).
 
+(** Classical De Morgan's law *)
+
+Definition classical_de_morgan_law :=
+  forall A B:Prop, ~(A /\ B) -> ~A \/ ~B.
+
 (** ** Gödel-Dummett axiom *)
 
 (** [(A->B) \/ (B->A)] is studied in [[Dummett59]] and is based on [[Gödel33]].
@@ -590,6 +595,16 @@ Proof.
     right; intro HA; apply (HAnotA HA HA).
 Qed.
 
+(** The weak excluded middle is equivalent to the classical De Morgan's law *)
+
+Lemma weak_excluded_middle_iff_classical_de_morgan_law :
+  weak_excluded_middle <-> classical_de_morgan_law.
+Proof.
+  split; [intro WEM|intro CDML]; intros A *.
+  - destruct (WEM A); tauto.
+  - destruct (CDML A (~A)); tauto.
+Qed.
+
 (** ** Independence of general premises and drinker's paradox *)
 
 (** Independence of general premises is the unconstrained, non
-- 
cgit v1.2.3


From a8166315acaa63252f5753b71ad26d126873bbe4 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 14 Oct 2019 12:54:31 +0200
Subject: Weak excluded-middle: adding a reference.

---
 theories/Logic/ClassicalFacts.v | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v
index 98dcd0d122..9ba3db6eff 100644
--- a/theories/Logic/ClassicalFacts.v
+++ b/theories/Logic/ClassicalFacts.v
@@ -523,11 +523,15 @@ End Weak_proof_irrelevance_CCI.
 (** ** Weak excluded-middle *)
 
 (** The weak classical logic based on [~~A \/ ~A] is referred to with
-    name KC in [[ChagrovZakharyaschev97]]
+    name KC in [[ChagrovZakharyaschev97]]. See [[SorbiTerwijn11]] for
+    a short survey.
 
    [[ChagrovZakharyaschev97]] Alexander Chagrov and Michael
    Zakharyaschev, "Modal Logic", Clarendon Press, 1997.
-*)
+
+   [[SorbiTerwijn11]] Andrea Sorbi and Sebastiaan A. Terwijn,
+   "Generalizations of the weak law of the excluded-middle", Notre
+   Dame J. Formal Logic, vol 56(2), pp 321-331, 2015. *)
 
 Definition weak_excluded_middle :=
   forall A:Prop, ~~A \/ ~A.
-- 
cgit v1.2.3


From b13c438c78539040f8adf67f0b92a8f31e2e8c9f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 14 Oct 2019 12:58:26 +0200
Subject: ClassicalFacts.v: Unifying format for bibliographical references.

---
 theories/Logic/ClassicalFacts.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v
index 9ba3db6eff..8538b54c08 100644
--- a/theories/Logic/ClassicalFacts.v
+++ b/theories/Logic/ClassicalFacts.v
@@ -553,11 +553,11 @@ Definition classical_de_morgan_law :=
 (** [(A->B) \/ (B->A)] is studied in [[Dummett59]] and is based on [[Gödel33]].
 
     [[Dummett59]] Michael A. E. Dummett. "A Propositional Calculus
-    with a Denumerable Matrix", In the Journal of Symbolic Logic, Vol
-    24 No. 2(1959), pp 97-103.
+    with a Denumerable Matrix", In the Journal of Symbolic Logic, vol
+    24(2), pp 97-103, 1959.
 
     [[Gödel33]] Kurt Gödel. "Zum intuitionistischen Aussagenkalkül",
-    Ergeb. Math. Koll. 4 (1933), pp. 34-38.
+    Ergeb. Math. Koll. 4, pp. 34-38, 1933.
  *)
 
 Definition GodelDummett := forall A B:Prop, (A -> B) \/ (B -> A).
-- 
cgit v1.2.3


From 986c7b7c96d3207c64684c71aeee7cf8b5017d82 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 14 Oct 2019 13:07:24 +0200
Subject: Updating changelog

---
 .../10-standard-library/10895-master+weak-excluded-middle-de-morgan.rst  | 1 +
 1 file changed, 1 insertion(+)
 create mode 100644 doc/changelog/10-standard-library/10895-master+weak-excluded-middle-de-morgan.rst

diff --git a/doc/changelog/10-standard-library/10895-master+weak-excluded-middle-de-morgan.rst b/doc/changelog/10-standard-library/10895-master+weak-excluded-middle-de-morgan.rst
new file mode 100644
index 0000000000..6e87ff93c7
--- /dev/null
+++ b/doc/changelog/10-standard-library/10895-master+weak-excluded-middle-de-morgan.rst
@@ -0,0 +1 @@
+- ClassicalFacts: Adding the standard equivalence between weak excluded-middle and the classical instance of De Morgan's law (`#10895 <https://github.com/coq/coq/pull/10895>`_, by Hugo Herbelin).
-- 
cgit v1.2.3