From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 theories/Logic/Diaconescu.v | 39 ++++++++++++++++++++++-----------------
 1 file changed, 22 insertions(+), 17 deletions(-)

(limited to 'theories/Logic/Diaconescu.v')

diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v
index 23af5afc..3317766c 100644
--- a/theories/Logic/Diaconescu.v
+++ b/theories/Logic/Diaconescu.v
@@ -1,16 +1,18 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (** Diaconescu showed that the Axiom of Choice entails Excluded-Middle
-   in topoi [Diaconescu75]. Lacas and Werner adapted the proof to show
+   in topoi [[Diaconescu75]]. Lacas and Werner adapted the proof to show
    that the axiom of choice in equivalence classes entails
-   Excluded-Middle in Type Theory [LacasWerner99].
+   Excluded-Middle in Type Theory [[LacasWerner99]].
 
    Three variants of Diaconescu's result in type theory are shown below.
 
@@ -23,23 +25,24 @@
       Benjamin Werner)
 
    C. A proof that extensional Hilbert epsilon's description operator
-      entails excluded-middle (taken from Bell [Bell93])
+      entails excluded-middle (taken from Bell [[Bell93]])
 
-   See also [Carlström] for a discussion of the connection between the
+   See also [[Carlström04]] for a discussion of the connection between the
    Extensional Axiom of Choice and Excluded-Middle
 
-   [Diaconescu75] Radu Diaconescu, Axiom of Choice and Complementation,
+   [[Diaconescu75]] Radu Diaconescu, Axiom of Choice and Complementation,
    in Proceedings of AMS, vol 51, pp 176-178, 1975.
 
-   [LacasWerner99] Samuel Lacas, Benjamin Werner, Which Choices imply
+   [[LacasWerner99]] Samuel Lacas, Benjamin Werner, Which Choices imply
    the excluded middle?, preprint, 1999.
 
-   [Bell93] John L. Bell, Hilbert's epsilon operator and classical
+   [[Bell93]] John L. Bell, Hilbert's epsilon operator and classical
    logic, Journal of Philosophical Logic, 22: 1-18, 1993
 
-   [Carlström04] Jesper Carlström, EM + Ext_ + AC_int <-> AC_ext,
-   Mathematical Logic Quaterly, vol 50(3), pp 236-240, 2004.
+   [[Carlström04]] Jesper Carlström, EM + Ext_ + AC_int is equivalent
+   to AC_ext, Mathematical Logic Quaterly, vol 50(3), pp 236-240, 2004.
 *)
+Require ClassicalFacts ChoiceFacts.
 
 (**********************************************************************)
 (** * Pred. Ext. + Rel. Axiom of Choice -> Excluded-Middle       *)
@@ -54,7 +57,7 @@ Definition PredicateExtensionality :=
 (** From predicate extensionality we get propositional extensionality
    hence proof-irrelevance *)
 
-Require Import ClassicalFacts.
+Import ClassicalFacts.
 
 Variable pred_extensionality : PredicateExtensionality.
 
@@ -76,7 +79,7 @@ Qed.
 (** From proof-irrelevance and relational choice, we get guarded
    relational choice *)
 
-Require Import ChoiceFacts.
+Import ChoiceFacts.
 
 Variable rel_choice : RelationalChoice.
 
@@ -89,7 +92,7 @@ Qed.
 (** The form of choice we need: there is a functional relation which chooses
     an element in any non empty subset of bool *)
 
-Require Import Bool.
+Import Bool.
 
 Lemma AC_bool_subset_to_bool :
   exists R : (bool -> Prop) -> bool -> Prop,
@@ -161,6 +164,8 @@ End PredExt_RelChoice_imp_EM.
 
 Section ProofIrrel_RelChoice_imp_EqEM.
 
+Import ChoiceFacts.
+
 Variable rel_choice : RelationalChoice.
 
 Variable proof_irrelevance : forall P:Prop , forall x y:P, x=y.
@@ -263,7 +268,7 @@ End ProofIrrel_RelChoice_imp_EqEM.
 (**********************************************************************)
 (** * Extensional Hilbert's epsilon description operator -> Excluded-Middle *)
 
-(** Proof sketch from Bell [Bell93] (with thanks to P. Castéran) *)
+(** Proof sketch from Bell [[Bell93]] (with thanks to P. Castéran) *)
 
 Local Notation inhabited A := A (only parsing).
 
-- 
cgit v1.2.3