From a0bd33bdb81271025494d3f7ac7ae20bd6671579 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Oct 2016 21:30:29 +0200
Subject: Formatting references with surrounding brackets in Diaconescu.v.

---
 theories/Logic/Diaconescu.v | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v
index 23af5afc68..896be7c339 100644
--- a/theories/Logic/Diaconescu.v
+++ b/theories/Logic/Diaconescu.v
@@ -8,9 +8,9 @@
 (************************************************************************)
 
 (** 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,22 +23,22 @@
       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.
 *)
 
 (**********************************************************************)
@@ -263,7 +263,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


From 7497d4129775d15cdce862a0ac681c6400aabe54 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 6 Oct 2016 07:02:24 +0200
Subject: Logic library: Adding a characterization of excluded-middle in term
 of choice of a representative in a partition of bool.

Also move a result about propositional extensionality from
ClassicalFacts.v to PropExtensionalityFacts.v, generalizing it by
symmetry.

Also spotting typos (thanks to Théo).
---
 doc/stdlib/index-list.html.template      |   1 +
 theories/Logic/ClassicalFacts.v          |  66 ++++++++++++++++++-
 theories/Logic/PropExtensionalityFacts.v | 109 +++++++++++++++++++++++++++++++
 3 files changed, 173 insertions(+), 3 deletions(-)
 create mode 100644 theories/Logic/PropExtensionalityFacts.v

diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 9216c81fcd..4a685a3b85 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -55,6 +55,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/Logic/Description.v
     theories/Logic/Epsilon.v
     theories/Logic/IndefiniteDescription.v
+    theories/Logic/PropExtensionalityFacts.v
     theories/Logic/FunctionalExtensionality.v
     theories/Logic/ExtensionalityFacts.v
     theories/Logic/WeakFan.v
diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v
index afd64efdf8..021408a37b 100644
--- a/theories/Logic/ClassicalFacts.v
+++ b/theories/Logic/ClassicalFacts.v
@@ -34,8 +34,11 @@ Table of contents:
 
 3 3. Independence of general premises and drinker's paradox
 
-4. Classical logic and principle of unrestricted minimization
+4. Principles equivalent to classical logic
 
+4.1 Classical logic = principle of unrestricted minimization
+
+4.2 Classical logic = choice of representatives in a partition of bool
 *)
 
 (************************************************************************)
@@ -94,12 +97,14 @@ Qed.
 (** A weakest form of propositional extensionality: extensionality for
     provable propositions only *)
 
+Require Import PropExtensionalityFacts.
+
 Definition provable_prop_extensionality := forall A:Prop, A -> A = True.
 
 Lemma provable_prop_ext :
   prop_extensionality -> provable_prop_extensionality.
 Proof.
-  intros Ext A Ha; apply Ext; split; trivial.
+  exact PropExt_imp_ProvPropExt.
 Qed.
 
 (************************************************************************)
@@ -516,7 +521,7 @@ 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]]
 
    [[ChagrovZakharyaschev97]] Alexander Chagrov and Michael
    Zakharyaschev, "Modal Logic", Clarendon Press, 1997.
@@ -661,6 +666,8 @@ Proof.
     exists x0; exact Hnot.
 Qed.
 
+(** * Axioms equivalent to classical logic *)
+
 (** ** Principle of unrestricted minimization *)
 
 Require Import Coq.Arith.PeanoNat.
@@ -736,3 +743,56 @@ Section Example_of_undecidable_predicate_with_the_minimization_property.
   Qed.
 
 End Example_of_undecidable_predicate_with_the_minimization_property.
+
+(** ** Choice of representatives in a partition of bool *)
+
+(** This is similar to Bell's "weak extensional selection principle"  in [[Bell]]
+
+   [[Bell]] John L. Bell, Choice principles in intuitionistic set theory, unpublished.
+*)
+
+Require Import RelationClasses.
+
+Local Notation representative_boolean_partition :=
+  (forall R:bool->bool->Prop,
+    Equivalence R -> exists f, forall x, R x (f x) /\ forall y, R x y -> f x = f y).
+
+Theorem representative_boolean_partition_imp_excluded_middle :
+  representative_boolean_partition -> excluded_middle.
+Proof.
+  intros ReprFunChoice P.
+  pose (R (b1 b2 : bool) := b1 = b2 \/ P).
+  assert (Equivalence R).
+  { split.
+    - now left.
+    - destruct 1. now left. now right.
+    - destruct 1, 1; try now right. left; now transitivity y. }
+  destruct (ReprFunChoice R H) as (f,Hf). clear H.
+  destruct (Bool.bool_dec (f true) (f false)) as [Heq|Hneq].
+  + left.
+     destruct (Hf false) as ([Hfalse|HP],_); try easy.
+     destruct (Hf true) as ([Htrue|HP],_); try easy.
+     congruence.
+  + right. intro HP.
+     destruct (Hf true) as (_,H). apply Hneq, H. now right.
+Qed.
+
+Theorem excluded_middle_imp_representative_boolean_partition :
+  excluded_middle -> representative_boolean_partition.
+Proof.
+  intros EM R H.
+  destruct (EM (R true false)).
+  - exists (fun _ => true).
+    intros []; firstorder.
+  - exists (fun b => b).
+    intro b. split.
+    + reflexivity.
+    + destruct b, y; intros HR; easy || now symmetry in HR.
+Qed.
+
+Theorem excluded_middle_iff_representative_boolean_partition :
+  excluded_middle <-> representative_boolean_partition.
+Proof.
+  split; auto using excluded_middle_imp_representative_boolean_partition,
+                    representative_boolean_partition_imp_excluded_middle.
+Qed.
diff --git a/theories/Logic/PropExtensionalityFacts.v b/theories/Logic/PropExtensionalityFacts.v
new file mode 100644
index 0000000000..7e455dfa1e
--- /dev/null
+++ b/theories/Logic/PropExtensionalityFacts.v
@@ -0,0 +1,109 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Some facts and definitions about propositional and predicate extensionality
+
+We investigate the relations between the following extensionality principles
+
+- Proposition extensionality
+- Predicate extensionality
+- Propositional functional extensionality
+- Provable-proposition extensionality
+- Refutable-proposition extensionality
+- Extensional proposition representatives
+- Extensional predicate representatives
+- Extensional propositional function representatives
+
+Table of contents
+
+1. Definitions
+
+2.1 Predicate extensionality <-> Proposition extensionality + Propositional functional extensionality
+
+2.2 Propositional extensionality -> Provable propositional extensionality
+
+2.3 Propositional extensionality -> Refutable propositional extensionality
+
+*)
+
+Set Implicit Arguments.
+
+(**********************************************************************)
+(** * Definitions *)
+
+(** Propositional extensionality *)
+
+Local Notation PropositionalExtensionality :=
+  (forall A B : Prop, (A <-> B) -> A = B).
+
+(** Provable-proposition extensionality *)
+
+Local Notation ProvablePropositionExtensionality :=
+  (forall A:Prop, A -> A = True).
+
+(** Refutable-proposition extensionality *)
+
+Local Notation RefutablePropositionExtensionality :=
+  (forall A:Prop, ~A -> A = False).
+
+(** Predicate extensionality *)
+
+Local Notation PredicateExtensionality :=
+  (forall (A:Type) (P Q : A -> Prop), (forall x, P x <-> Q x) -> P = Q).
+
+(** Propositional functional extensionality *)
+
+Local Notation PropositionalFunctionalExtensionality :=
+  (forall (A:Type) (P Q : A -> Prop), (forall x, P x = Q x) -> P = Q).
+
+(**********************************************************************)
+(** * Propositional and predicate extensionality                      *)
+
+(**********************************************************************)
+(** ** Predicate extensionality <-> Propositional extensionality + Propositional functional extensionality *)
+
+Lemma PredExt_imp_PropExt : PredicateExtensionality -> PropositionalExtensionality.
+Proof.
+  intros Ext A B Equiv. 
+  change A with ((fun _ => A) I).
+  now rewrite Ext with (P := fun _ : True =>A) (Q := fun _ => B).
+Qed.
+
+Lemma PredExt_imp_PropFunExt : PredicateExtensionality -> PropositionalFunctionalExtensionality.
+Proof.
+  intros Ext A P Q Eq. apply Ext. intros x. now rewrite (Eq x).
+Qed.
+
+Lemma PropExt_and_PropFunExt_imp_PredExt :
+  PropositionalExtensionality -> PropositionalFunctionalExtensionality -> PredicateExtensionality.
+Proof.
+  intros Ext FunExt A P Q Equiv.
+  apply FunExt. intros x. now apply Ext.
+Qed.
+
+Theorem PropExt_and_PropFunExt_iff_PredExt :
+  PropositionalExtensionality /\ PropositionalFunctionalExtensionality <-> PredicateExtensionality.
+Proof.
+  firstorder using PredExt_imp_PropExt, PredExt_imp_PropFunExt, PropExt_and_PropFunExt_imp_PredExt.
+Qed.
+
+(**********************************************************************)
+(** ** Propositional extensionality and provable proposition extensionality *)
+
+Lemma PropExt_imp_ProvPropExt : PropositionalExtensionality -> ProvablePropositionExtensionality.
+Proof.
+  intros Ext A Ha; apply Ext; split; trivial.
+Qed.
+
+(**********************************************************************)
+(** ** Propositional extensionality and refutable proposition extensionality *)
+
+Lemma PropExt_imp_RefutPropExt : PropositionalExtensionality -> RefutablePropositionExtensionality.
+Proof.
+  intros Ext A Ha; apply Ext; split; easy.
+Qed.
-- 
cgit v1.2.3


From b453d0281db6de0c36cbd9f2c0a094946f4fcfd6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 10 Oct 2016 12:12:33 +0200
Subject: Slightly unifying renaming in ChoiceFacts.v.

---
 theories/Logic/ChoiceFacts.v | 23 ++++++++++++++++-------
 1 file changed, 16 insertions(+), 7 deletions(-)

diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index 1420a000b6..2ab851e297 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -284,7 +284,7 @@ Definition SmallDrinker'sParadox :=
    relational formulation) without known inconsistency with classical logic,
    though functional relation reification conflicts with classical logic *)
 
-Lemma description_rel_choice_imp_funct_choice :
+Lemma functional_rel_reification_and_rel_choice_imp_fun_choice :
   forall A B : Type,
     FunctionalRelReification_on A B -> RelationalChoice_on A B -> FunctionalChoice_on A B.
 Proof.
@@ -298,7 +298,10 @@ Proof.
   apply HR'R; assumption.
 Qed.
 
-Lemma funct_choice_imp_rel_choice :
+Notation description_rel_choice_imp_funct_choice :=
+  functional_rel_reification_and_rel_choice_imp_fun_choice (compat "8.6").
+
+Lemma fun_choice_imp_rel_choice :
   forall A B : Type, FunctionalChoice_on A B -> RelationalChoice_on A B.
 Proof.
   intros A B FunCh R H.
@@ -311,7 +314,9 @@ Proof.
     trivial.
 Qed.
 
-Lemma funct_choice_imp_description :
+Notation funct_choice_imp_rel_choice := fun_choice_imp_rel_choice (compat "8.6").
+
+Lemma fun_choice_imp_functional_rel_reification :
   forall A B : Type, FunctionalChoice_on A B -> FunctionalRelReification_on A B.
 Proof.
   intros A B FunCh R H.
@@ -324,17 +329,21 @@ Proof.
   exists f; exact H0.
 Qed.
 
-Corollary FunChoice_Equiv_RelChoice_and_ParamDefinDescr :
+Notation funct_choice_imp_description := fun_choice_imp_functional_rel_reification (compat "8.6").
+
+Corollary fun_choice_iff_rel_choice_and_functional_rel_reification :
   forall A B : Type, FunctionalChoice_on A B <->
     RelationalChoice_on A B /\ FunctionalRelReification_on A B.
 Proof.
   intros A B. split.
   intro H; split;
-    [ exact (funct_choice_imp_rel_choice H)
-      | exact (funct_choice_imp_description H) ].
-  intros [H H0]; exact (description_rel_choice_imp_funct_choice H0 H).
+    [ exact (fun_choice_imp_rel_choice H)
+      | exact (fun_choice_imp_functional_rel_reification H) ].
+  intros [H H0]; exact (functional_rel_reification_and_rel_choice_imp_fun_choice H0 H).
 Qed.
 
+Notation FunChoice_Equiv_RelChoice_and_ParamDefinDescr :=
+ fun_choice_iff_rel_choice_and_functional_rel_reification (compat "8.6").
 (**********************************************************************)
 (** * Connection between the guarded, non guarded and omniscient choices *)
 
-- 
cgit v1.2.3


From 62ed11de4c528a496e0ece70a07062a1b6d4f7d8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Oct 2016 21:48:52 +0200
Subject: Adding various properties and characterization of the extensional
 axiom of choice (i.e. choice on setoids) and of the axiom selecting
 representatives in classes of equivalence.

Also integrating suggestions from Théo.
---
 theories/Logic/ChoiceFacts.v | 425 ++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 422 insertions(+), 3 deletions(-)

diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index 2ab851e297..3f17ba5a95 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -22,7 +22,14 @@ description principles
 - AC!     = functional relation reification
             (known as axiom of unique choice in topos theory,
              sometimes called principle of definite description in
-             the context of constructive type theory)
+             the context of constructive type theory, sometimes
+             called axiom of no choice)
+
+- AC_fun_repr       = functional choice of a representative in an equivalence class
+- AC_fun_setoid_gen = functional form of the general form of the (so-called
+                      extensional) axiom of choice over setoids
+- AC_fun_setoid     = functional form of the (so-called extensional) axiom of
+                      choice from setoids
 
 - GAC_rel = guarded relational form of the (non extensional) axiom of choice
 - GAC_fun = guarded functional form of the (non extensional) axiom of choice
@@ -45,6 +52,11 @@ description principles
              independence of premises)
 - Drinker = drinker's paradox (small form)
             (called Ex in Bell [[Bell]])
+- EM      = excluded-middle
+
+- Ext_pred_repr     = choice of a representative among extensional predicates
+- Ext_pred          = extensionality of predicates
+- Ext_fun_prop_repr = choice of a representative among extensional functions to Prop
 
 We let also
 
@@ -76,6 +88,10 @@ Table of contents
 
 8. Choice -> Dependent choice -> Countable choice
 
+9.1. AC_fun_ext = AC_fun + Ext_fun_repr + EM
+
+9.2. AC_fun_ext = AC_fun + Ext_prop_fun_repr + PI
+
 References:
 
 [[Bell]] John L. Bell, Choice principles in intuitionistic set theory,
@@ -84,8 +100,13 @@ unpublished.
 [[Bell93]] John L. Bell, Hilbert's Epsilon Operator in Intuitionistic
 Type Theories, Mathematical Logic Quarterly, volume 39, 1993.
 
+[[Carlström04]] Jesper Carlström, EM + Ext_ + AC_int is equivalent to
+AC_ext, Mathematical Logic Quaterly, vol 50(3), pp 236-240, 2004.
+
 [[Carlström05]] Jesper Carlström, Interpreting descriptions in
 intentional type theory, Journal of Symbolic Logic 70(2):488-514, 2005.
+
+[[Werner97]] Benjamin Werner, Sets in Types, Types in Sets, TACS, 1997.
 *)
 
 Set Implicit Arguments.
@@ -108,8 +129,6 @@ Variables A B :Type.
 
 Variable P:A->Prop.
 
-Variable R:A->B->Prop.
-
 (** ** Constructive choice and description *)
 
 (** AC_rel *)
@@ -121,6 +140,10 @@ Definition RelationalChoice_on :=
 
 (** AC_fun *)
 
+(* Note: This is called Type-Theoretic Description Axiom (TTDA) in
+   [[Werner97]] (using a non-standard meaning of "description"). This
+   is called intensional axiom of choice (AC_int) in [[Carlström04]] *)
+
 Definition FunctionalChoice_on :=
   forall R:A->B->Prop,
     (forall x : A, exists y : B, R x y) ->
@@ -148,6 +171,55 @@ Definition FunctionalRelReification_on :=
     (forall x : A, exists! y : B, R x y) ->
     (exists f : A->B, forall x : A, R x (f x)).
 
+(** AC_fun_repr *)
+
+(* Note: This is called Type-Theoretic Choice Axiom (TTCA) in
+   [[Werner97]] (by reference to the extensional set-theoretic
+   formulation of choice); Note also a typo in its intended
+   formulation in [[Werner97]]. *)
+
+Require Import RelationClasses Logic.
+
+Definition RepresentativeFunctionalChoice_on :=
+  forall R:A->A->Prop,
+    (Equivalence R) ->
+    (exists f : A->A, forall x : A, (R x (f x)) /\ forall y, R x y -> f x = f y).
+
+(** AC_fun_ext *)
+
+Definition SetoidFunctionalChoice_on :=
+  forall R : A -> A -> Prop,
+  forall T : A -> B -> Prop,
+  Equivalence R ->
+  (forall x x' y, R x x' -> T x y -> T x' y) ->
+  (forall x, exists y, T x y) ->
+  exists f : A -> B, forall x : A, T x (f x) /\ (forall y : A, R x y -> f x = f y).
+
+(** AC_fun_ext_gen *)
+
+(* Note: This is called extensional axiom of choice (AC_ext) in
+   [[Carlström04]]. *)
+
+Definition GeneralizedSetoidFunctionalChoice_on :=
+  forall R : A -> A -> Prop,
+  forall S : B -> B -> Prop,
+  forall T : A -> B -> Prop,
+  Equivalence R ->
+  Equivalence S ->
+  (forall x x' y y', R x x' -> S y y' -> T x y -> T x' y') ->
+  (forall x, exists y, T x y) ->
+  exists f : A -> B,
+    forall x : A, T x (f x) /\ (forall y : A, R x y -> S (f x) (f y)).
+
+(** AC_fun_ext_simple *)
+
+Definition SimpleSetoidFunctionalChoice_on A B :=
+  forall R : A -> A -> Prop,
+  forall T : A -> B -> Prop,
+  Equivalence R ->
+  (forall x, exists y, forall x', R x x' -> T x' y) ->
+  exists f : A -> B, forall x : A, T x (f x) /\ (forall x' : A, R x x' -> f x = f x').
+
 (** ID_epsilon (constructive version of indefinite description;
     combined with proof-irrelevance, it may be connected to
     Carlström's type theory with a constructive indefinite description
@@ -234,6 +306,14 @@ Notation FunctionalChoiceOnInhabitedSet :=
   (forall A B : Type, inhabited B -> FunctionalChoice_on A B).
 Notation FunctionalRelReification :=
   (forall A B : Type, FunctionalRelReification_on A B).
+Notation RepresentativeFunctionalChoice :=
+  (forall A : Type, RepresentativeFunctionalChoice_on A).
+Notation SetoidFunctionalChoice :=
+  (forall A  B: Type, SetoidFunctionalChoice_on A B).
+Notation GeneralizedSetoidFunctionalChoice :=
+  (forall A B : Type, GeneralizedSetoidFunctionalChoice_on A B).
+Notation SimpleSetoidFunctionalChoice :=
+  (forall A B : Type, SimpleSetoidFunctionalChoice_on A B).
 
 Notation GuardedRelationalChoice :=
   (forall A B : Type, GuardedRelationalChoice_on A B).
@@ -271,6 +351,26 @@ Definition SmallDrinker'sParadox :=
   forall (A:Type) (P:A -> Prop), inhabited A ->
     exists x, (exists x, P x) -> P x.
 
+Definition ExcludedMiddle :=
+  forall P:Prop, P \/ ~ P.
+
+(** Extensional schemes *)
+
+Local Notation ExtensionalPropositionRepresentative :=
+  (forall (A:Type),
+   exists h : Prop -> Prop,
+   forall P : Prop, (P <-> h P) /\ forall Q, (P <-> Q) -> h P = h Q).
+
+Local Notation ExtensionalPredicateRepresentative :=
+  (forall (A:Type),
+   exists h : (A->Prop) -> (A->Prop),
+   forall (P : A -> Prop), (forall x, P x <-> h P x) /\ forall Q, (forall x, P x <-> Q x) -> h P = h Q).
+
+Local Notation ExtensionalFunctionRepresentative :=
+  (forall (A B:Type),
+   exists h : (A->B) -> (A->B),
+   forall (f : A -> B), (forall x, f x = h f x) /\ forall g, (forall x, f x = g x) -> h f = h g).
+
 (**********************************************************************)
 (** * AC_rel + AC! = AC_fun
 
@@ -871,3 +971,322 @@ Proof.
   rewrite Heq in HR.
   assumption.
 Qed.
+
+(**********************************************************************)
+(** * About the axiom of choice over setoids                          *)
+
+Require Import ClassicalFacts PropExtensionalityFacts.
+
+(**********************************************************************)
+(** ** Consequences of the choice of a representative in an equivalence class *)
+
+Theorem repr_fun_choice_imp_ext_prop_repr :
+  RepresentativeFunctionalChoice -> ExtensionalPropositionRepresentative.
+Proof.
+  intros ReprFunChoice A.
+  pose (R P Q := P <-> Q).
+  assert (Hequiv:Equivalence R) by (split; firstorder).
+  apply (ReprFunChoice _ R Hequiv).
+Qed.
+
+Theorem repr_fun_choice_imp_ext_pred_repr :
+  RepresentativeFunctionalChoice -> ExtensionalPredicateRepresentative.
+Proof.
+  intros ReprFunChoice A.
+  pose (R P Q := forall x : A, P x <-> Q x).
+  assert (Hequiv:Equivalence R) by (split; firstorder).
+  apply (ReprFunChoice _ R Hequiv).
+Qed.
+
+Theorem repr_fun_choice_imp_ext_function_repr :
+  RepresentativeFunctionalChoice -> ExtensionalFunctionRepresentative.
+Proof.
+  intros ReprFunChoice A B.
+  pose (R (f g : A -> B) := forall x : A, f x = g x).
+  assert (Hequiv:Equivalence R).
+  { split; try easy. firstorder using eq_trans. }
+  apply (ReprFunChoice _ R Hequiv).
+Qed.
+
+(** *** This is a variant of Diaconescu and Goodman-Myhill theorems *)
+
+Theorem repr_fun_choice_imp_excluded_middle :
+  RepresentativeFunctionalChoice -> ExcludedMiddle.
+Proof.
+  intros ReprFunChoice.
+  apply representative_boolean_partition_imp_excluded_middle, ReprFunChoice.
+Qed.
+
+Theorem repr_fun_choice_imp_relational_choice :
+  RepresentativeFunctionalChoice -> RelationalChoice.
+Proof.
+  intros ReprFunChoice A B T Hexists.
+  pose (D := (A*B)%type).
+  pose (R (z z':D) :=
+    let x := fst z in
+    let x' := fst z' in
+    let y := snd z in
+    let y' := snd z' in
+    x = x' /\ (T x y -> y = y' \/ T x y') /\ (T x y' -> y = y' \/ T x y)).
+  assert (Hequiv : Equivalence R).
+  { split.
+    - split. easy. firstorder.
+    - intros (x,y) (x',y') (H1,(H2,H2')). split. easy. simpl fst in *. simpl snd in *.
+      subst x'. split; intro H.
+      + destruct (H2' H); firstorder.
+      + destruct (H2 H); firstorder.
+    - intros (x,y) (x',y') (x'',y'') (H1,(H2,H2')) (H3,(H4,H4')).
+      simpl fst in *. simpl snd in *. subst x'' x'. split. easy. split; intro H.
+      + simpl fst in *. simpl snd in *. destruct (H2 H) as [<-|H0].
+        * destruct (H4 H); firstorder.
+        * destruct (H2' H0), (H4 H0); try subst y'; try subst y''; try firstorder.
+      + simpl fst in *. simpl snd in *. destruct (H4' H) as [<-|H0].
+        * destruct (H2' H); firstorder.
+        * destruct (H2' H0), (H4 H0); try subst y'; try subst y''; try firstorder. }
+  destruct (ReprFunChoice D R Hequiv) as (g,Hg).
+  set (T' x y := T x y /\ exists y', T x y' /\ g (x,y') = (x,y)).
+  exists T'. split.
+  - intros x y (H,_); easy.
+  - intro x. destruct (Hexists x) as (y,Hy).
+    exists (snd (g (x,y))).
+    destruct (Hg (x,y)) as ((Heq1,(H',H'')),Hgxyuniq); clear Hg.
+    destruct (H' Hy) as [Heq2|Hgy]; clear H'.
+    + split. split.
+      * rewrite <- Heq2. assumption.
+      * exists y. destruct (g (x,y)) as (x',y'). simpl in Heq1, Heq2. subst; easy.
+      * intros y' (Hy',(y'',(Hy'',Heq))).
+        rewrite (Hgxyuniq (x,y'')), Heq. easy. split. easy.
+        split; right; easy.
+    + split. split.
+      * assumption.
+      * exists y. destruct (g (x,y)) as (x',y'). simpl in Heq1. subst x'; easy.
+      * intros y' (Hy',(y'',(Hy'',Heq))).
+        rewrite (Hgxyuniq (x,y'')), Heq. easy. split. easy.
+        split; right; easy.
+Qed.
+
+(**********************************************************************)
+(** ** AC_fun_setoid = AC_fun_setoid_gen                              *)
+
+Theorem gen_setoid_fun_choice_imp_setoid_fun_choice  :
+   GeneralizedSetoidFunctionalChoice -> SetoidFunctionalChoice.
+Proof.
+  intros GenSetoidFunChoice A B R T Hequiv Hcompat Hex.
+  apply GenSetoidFunChoice; try easy.
+  apply eq_equivalence.
+  intros * H <-. firstorder.
+Qed.
+
+Theorem setoid_fun_choice_imp_gen_setoid_fun_choice :
+  SetoidFunctionalChoice -> GeneralizedSetoidFunctionalChoice.
+Proof.
+  intros SetoidFunChoice A B R S T HequivR HequivS Hcompat Hex.
+  destruct SetoidFunChoice with (R:=R) (T:=T) as (f,Hf); try easy.
+  { intros; apply (Hcompat x x' y y); try easy. }
+  exists f. intros x; specialize Hf with x as (Hf,Huniq). intuition. now erewrite Huniq.
+Qed.
+
+Theorem setoid_fun_choice_imp_simple_setoid_fun_choice  :
+   SetoidFunctionalChoice -> SimpleSetoidFunctionalChoice.
+Proof.
+  intros SetoidFunChoice A B R T Hequiv Hexists.
+  pose (T' x y := forall x', R x x' -> T x' y).
+  assert (Hcompat : forall (x x' : A) (y : B), R x x' -> T' x y -> T' x' y) by firstorder.
+  destruct (SetoidFunChoice A B R T' Hequiv Hcompat Hexists) as (f,Hf).
+  exists f. firstorder.
+Qed.
+
+Theorem simple_setoid_fun_choice_imp_setoid_fun_choice :
+  SimpleSetoidFunctionalChoice -> SetoidFunctionalChoice.
+Proof.
+  intros SimpleSetoidFunChoice A B R T Hequiv Hcompat Hexists.
+  destruct (SimpleSetoidFunChoice A B R T Hequiv) as (f,Hf); firstorder.
+Qed.
+
+(**********************************************************************)
+(** ** AC_fun_setoid = AC! + AC_fun_repr                              *)
+
+Theorem setoid_fun_choice_imp_fun_choice :
+  SetoidFunctionalChoice -> FunctionalChoice.
+Proof.
+  intros SetoidFunChoice A B T Hexists.
+  destruct SetoidFunChoice with (R:=@eq A) (T:=T) as (f,Hf).
+  - apply eq_equivalence.
+  - now intros * ->.
+  - assumption.
+  - exists f. firstorder.
+Qed.
+
+Corollary setoid_fun_choice_imp_functional_rel_reification :
+  SetoidFunctionalChoice -> FunctionalRelReification.
+Proof.
+  intro SetoidFunChoice.
+  intros A B; apply fun_choice_imp_functional_rel_reification.
+  now apply setoid_fun_choice_imp_fun_choice.
+Qed.
+
+Theorem setoid_fun_choice_imp_repr_fun_choice :
+  SetoidFunctionalChoice -> RepresentativeFunctionalChoice.
+Proof.
+  intros SetoidFunChoice A R Hequiv.
+  apply SetoidFunChoice; firstorder.
+Qed.
+
+Theorem functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice :
+  FunctionalRelReification -> RepresentativeFunctionalChoice -> SetoidFunctionalChoice.
+Proof.
+  intros FunRelReify ReprFunChoice A B R T Hequiv Hcompat Hexists.
+  assert (FunChoice : FunctionalChoice).
+  { intros A' B'. apply functional_rel_reification_and_rel_choice_imp_fun_choice.
+    - apply FunRelReify.
+    - now apply repr_fun_choice_imp_relational_choice. }
+  destruct (FunChoice _ _ T Hexists) as (f,Hf).
+  destruct (ReprFunChoice A R Hequiv) as (g,Hg).
+  exists (fun a => f (g a)).
+  intro x. destruct (Hg x) as (Hgx,HRuniq).
+  split.
+  - eapply Hcompat. symmetry. apply Hgx. apply Hf.
+  - intros y Hxy. f_equal. auto.
+Qed.
+
+Theorem functional_rel_reification_and_repr_fun_choice_iff_setoid_fun_choice :
+  FunctionalRelReification /\ RepresentativeFunctionalChoice <-> SetoidFunctionalChoice.
+Proof.
+  split; intros.
+  - now apply functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice.
+  - split.
+    + now apply setoid_fun_choice_imp_functional_rel_reification.
+    + now apply setoid_fun_choice_imp_repr_fun_choice.
+Qed.
+
+(** Note: What characterization to give of
+RepresentativeFunctionalChoice? A formulation of it as a functional
+relation would certainly be equivalent to the formulation of
+SetoidFunctionalChoice as a functional relation, but in their
+functional forms, SetoidFunctionalChoice seems strictly stronger *)
+
+(**********************************************************************)
+(** * AC_fun_setoid = AC_fun + Ext_fun_repr + EM                      *)
+
+Import EqNotations.
+
+(** ** This is the main theorem in [[Carlström04]] *)
+
+(** Note: all ingredients have a computational meaning when taken in
+  separation. However, to compute with the functional choice,
+  existential quantification has to be thought as a strong
+  existential, which is incompatible with the computational content of
+  excluded-middle *)
+
+Theorem fun_choice_and_ext_functions_repr_and_excluded_middle_imp_setoid_fun_choice :
+  FunctionalChoice -> ExtensionalFunctionRepresentative -> ExcludedMiddle -> RepresentativeFunctionalChoice.
+Proof.
+  intros FunChoice SetoidFunRepr EM A R (Hrefl,Hsym,Htrans).
+  assert (H:forall P:Prop, exists b, b = true <-> P).
+  { intros P. destruct (EM P).
+    - exists true; firstorder.
+    - exists false; easy. }
+  destruct (FunChoice _ _ _ H) as (c,Hc).
+  pose (class_of a y := c (R a y)).
+  pose (isclass f := exists x:A, f x = true).
+  pose (class := {f:A -> bool | isclass f}).
+  pose (contains (c:class) (a:A) := proj1_sig c a = true).
+  destruct (FunChoice class A contains) as (f,Hf).
+  - intros f. destruct (proj2_sig f) as (x,Hx).
+    exists x. easy.
+  - destruct (SetoidFunRepr A bool) as (h,Hh).
+    assert (Hisclass:forall a, isclass (h (class_of a))).
+    { intro a. exists a. destruct (Hh (class_of a)) as (Ha,Huniqa).
+      rewrite <- Ha. apply Hc. apply Hrefl. }
+   pose (f':= fun a => exist _ (h (class_of a)) (Hisclass a) : class).
+    exists (fun a => f (f' a)).
+    intros x. destruct (Hh (class_of x)) as (Hx,Huniqx). split.
+    + specialize Hf with (f' x). unfold contains in Hf. simpl in Hf. rewrite <- Hx in Hf. apply Hc. assumption.
+    + intros y Hxy.
+       f_equal.
+       assert (Heq1: h (class_of x) = h (class_of y)).
+       { apply Huniqx. intro z. unfold class_of.
+         destruct (c (R x z)) eqn:Hxz.
+         - symmetry. apply Hc. apply -> Hc in Hxz. firstorder.
+         - destruct (c (R y z)) eqn:Hyz.
+           + apply -> Hc in Hyz. rewrite <- Hxz. apply Hc. firstorder.
+           + easy. }
+       assert (Heq2:rew Heq1 in Hisclass x = Hisclass y).
+       { apply proof_irrelevance_cci, EM. }
+       unfold f'.
+       rewrite <- Heq2.
+       rewrite <- Heq1.
+       reflexivity.
+Qed.
+
+Theorem setoid_functional_choice_first_characterization :
+  FunctionalChoice /\ ExtensionalFunctionRepresentative /\ ExcludedMiddle <-> SetoidFunctionalChoice.
+Proof.
+  split.
+  - intros (FunChoice & SetoidFunRepr & EM).
+    apply functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice.
+    + intros A B. apply fun_choice_imp_functional_rel_reification, FunChoice.
+    + now apply fun_choice_and_ext_functions_repr_and_excluded_middle_imp_setoid_fun_choice.
+  - intro SetoidFunChoice. repeat split.
+    + now apply setoid_fun_choice_imp_fun_choice.
+    + apply repr_fun_choice_imp_ext_function_repr.
+       now apply setoid_fun_choice_imp_repr_fun_choice.
+    + apply repr_fun_choice_imp_excluded_middle.
+       now apply setoid_fun_choice_imp_repr_fun_choice.
+Qed.
+
+(**********************************************************************)
+(** ** AC_fun_setoid = AC_fun + Ext_pred_repr + PI                    *)
+
+(** Note: all ingredients have a computational meaning when taken in
+  separation. However, to compute with the functional choice,
+  existential quantification has to be thought as a strong
+  existential, which is incompatible with proof-irrelevance which
+  requires existential quantification to be truncated *)
+
+Theorem fun_choice_and_ext_pred_ext_and_proof_irrel_imp_setoid_fun_choice :
+  FunctionalChoice -> ExtensionalPredicateRepresentative -> ProofIrrelevance -> RepresentativeFunctionalChoice.
+Proof.
+  intros FunChoice PredExtRepr PI A R (Hrefl,Hsym,Htrans).
+  pose (isclass P := exists x:A, P x).
+  pose (class := {P:A -> Prop | isclass P}).
+  pose (contains (c:class) (a:A) := proj1_sig c a).
+  pose (class_of a := R a).
+  destruct (FunChoice class A contains) as (f,Hf).
+  - intros c. apply proj2_sig.
+  - destruct (PredExtRepr A) as (h,Hh).
+    assert (Hisclass:forall a, isclass (h (class_of a))).
+    { intro a. exists a. destruct (Hh (class_of a)) as (Ha,Huniqa).
+      rewrite <- Ha; apply Hrefl. }
+    pose (f':= fun a => exist _ (h (class_of a)) (Hisclass a) : class).
+    exists (fun a => f (f' a)).
+    intros x. destruct (Hh (class_of x)) as (Hx,Huniqx). split.
+    + specialize Hf with (f' x). simpl in Hf. rewrite <- Hx in Hf. assumption.
+    + intros y Hxy.
+       f_equal.
+       assert (Heq1: h (class_of x) = h (class_of y)).
+       { apply Huniqx. intro z. unfold class_of. firstorder. }
+       assert (Heq2:rew Heq1 in Hisclass x = Hisclass y).
+       { apply PI. }
+       unfold f'.
+       rewrite <- Heq2.
+       rewrite <- Heq1.
+       reflexivity.
+Qed.
+
+Theorem setoid_functional_choice_second_characterization :
+  FunctionalChoice /\ ExtensionalPredicateRepresentative /\ ProofIrrelevance <-> SetoidFunctionalChoice.
+Proof.
+  split.
+  - intros (FunChoice & ExtPredRepr & PI).
+    apply functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice.
+    + intros A B. now apply fun_choice_imp_functional_rel_reification.
+    + now apply fun_choice_and_ext_pred_ext_and_proof_irrel_imp_setoid_fun_choice.
+  - intro SetoidFunChoice. repeat split.
+    + now apply setoid_fun_choice_imp_fun_choice.
+    + apply repr_fun_choice_imp_ext_pred_repr.
+       now apply setoid_fun_choice_imp_repr_fun_choice.
+    + red. apply proof_irrelevance_cci.
+       apply repr_fun_choice_imp_excluded_middle.
+       now apply setoid_fun_choice_imp_repr_fun_choice.
+Qed.
-- 
cgit v1.2.3


From 9c21392c7957a0a1a66e5269022d5991649a38b5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Oct 2016 22:02:52 +0200
Subject: Adding a file providing extensional choice (i.e. choice over
 setoids).

Also integrating suggestions from Théo.
---
 doc/stdlib/index-list.html.template                |  2 +
 theories/Logic/ExtensionalFunctionRepresentative.v | 24 +++++++++
 theories/Logic/SetoidChoice.v                      | 60 ++++++++++++++++++++++
 theories/Logic/vo.itarget                          |  4 +-
 4 files changed, 89 insertions(+), 1 deletion(-)
 create mode 100644 theories/Logic/ExtensionalFunctionRepresentative.v
 create mode 100644 theories/Logic/SetoidChoice.v

diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 4a685a3b85..4ffdbb1152 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -46,6 +46,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/Logic/ClassicalDescription.v
     theories/Logic/ClassicalEpsilon.v
     theories/Logic/ClassicalUniqueChoice.v
+    theories/Logic/SetoidChoice.v
     theories/Logic/Berardi.v
     theories/Logic/Diaconescu.v
     theories/Logic/Hurkens.v
@@ -57,6 +58,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/Logic/IndefiniteDescription.v
     theories/Logic/PropExtensionalityFacts.v
     theories/Logic/FunctionalExtensionality.v
+    theories/Logic/ExtensionalFunctionRepresentative.v
     theories/Logic/ExtensionalityFacts.v
     theories/Logic/WeakFan.v
     theories/Logic/WKL.v
diff --git a/theories/Logic/ExtensionalFunctionRepresentative.v b/theories/Logic/ExtensionalFunctionRepresentative.v
new file mode 100644
index 0000000000..a9da68e165
--- /dev/null
+++ b/theories/Logic/ExtensionalFunctionRepresentative.v
@@ -0,0 +1,24 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** This module states a limited form axiom of functional
+    extensionality which selects a canonical representative in each
+    class of extensional functions *)
+
+(** Its main interest is that it is the needed ingredient to provide
+    axiom of choice on setoids (a.k.a. axiom of extensional choice)
+    when combined with classical logic and axiom of (intensonal)
+    choice *)
+
+(** It provides extensionality of functions while still supporting (a
+    priori) an intensional interpretation of equality *)
+
+Axiom extensional_function_representative :
+  forall A B, exists repr, forall (f : A -> B),
+  (forall x, f x = repr f x) /\
+  (forall g, (forall x, f x = g x) -> repr f = repr g).
diff --git a/theories/Logic/SetoidChoice.v b/theories/Logic/SetoidChoice.v
new file mode 100644
index 0000000000..84432dda1b
--- /dev/null
+++ b/theories/Logic/SetoidChoice.v
@@ -0,0 +1,60 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** This module states the functional form of the axiom of choice over
+  setoids, commonly called extensional axiom of choice [[Carlström04]],
+  [[Martin-Löf05]]. This is obtained by a decomposition of the axiom
+  into the following components:
+
+  - classical logic
+  - relational axiom of choice
+  - axiom of unique choice
+  - a limited form of functional extensionality
+
+  Among other results, it entails:
+  - proof irrelevance
+  - choice of a representative in equivalence classes
+
+  [[Carlström04]] Jesper Carlström, EM + Ext_ + AC_int is equivalent to
+  AC_ext, Mathematical Logic Quaterly, vol 50(3), pp 236-240, 2004.
+
+  [[Martin-Löf05] Per Martin-Löf, 100 years of Zermelo’s axiom of
+  choice: what was the problem with it?, lecture notes for KTH/SU
+  colloquium, 2005.
+
+*)
+
+Require Export ClassicalChoice. (* classical logic, relational choice, unique choice *)
+Require Export ExtensionalFunctionRepresentative.
+
+Require Import ChoiceFacts.
+Require Import ClassicalFacts.
+Require Import RelationClasses.
+
+Theorem setoid_choice :
+  forall A B,
+  forall R : A -> A -> Prop,
+  forall T : A -> B -> Prop,
+  Equivalence R ->
+  (forall x x' y, R x x' -> T x y -> T x' y) ->
+  (forall x, exists y, T x y) ->
+  exists f : A -> B, forall x : A, T x (f x) /\ (forall x' : A, R x x' -> f x = f x').
+Proof.
+  apply setoid_functional_choice_first_characterization. split; [|split].
+  - exact choice.
+  - exact extensional_function_representative.
+  - exact classic.
+Qed.
+
+Theorem representative_choice :
+  forall A (R:A->A->Prop), (Equivalence R) ->
+  exists f : A->A, forall x : A, R x (f x) /\ forall x', R x x' -> f x = f x'.
+Proof.
+  apply setoid_fun_choice_imp_repr_fun_choice.
+  exact setoid_choice.
+Qed.
diff --git a/theories/Logic/vo.itarget b/theories/Logic/vo.itarget
index 323597395f..71d01c1fb1 100644
--- a/theories/Logic/vo.itarget
+++ b/theories/Logic/vo.itarget
@@ -20,6 +20,7 @@ WeakFan.vo
 WKL.vo
 FunctionalExtensionality.vo
 ExtensionalityFacts.vo
+ExtensionalFunctionRepresentative.vo
 Hurkens.vo
 IndefiniteDescription.vo
 JMeq.vo
@@ -27,4 +28,5 @@ ProofIrrelevanceFacts.vo
 ProofIrrelevance.vo
 RelationalChoice.vo
 SetIsType.vo
-FinFun.vo
\ No newline at end of file
+SetoidChoice.vo
+FinFun.vo
-- 
cgit v1.2.3


From 4e85cc6e9792da116f1b20e484b2ce629c6f6865 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Oct 2016 20:27:59 +0200
Subject: Adding explicitly a file to work in the context of propositional
 extensionality.

---
 doc/stdlib/index-list.html.template |  1 +
 theories/Logic/PropExtensionality.v | 22 ++++++++++++++++++++++
 theories/Logic/vo.itarget           |  1 +
 3 files changed, 24 insertions(+)
 create mode 100644 theories/Logic/PropExtensionality.v

diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 4ffdbb1152..aeb0de48a3 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -56,6 +56,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/Logic/Description.v
     theories/Logic/Epsilon.v
     theories/Logic/IndefiniteDescription.v
+    theories/Logic/PropExtensionality.v
     theories/Logic/PropExtensionalityFacts.v
     theories/Logic/FunctionalExtensionality.v
     theories/Logic/ExtensionalFunctionRepresentative.v
diff --git a/theories/Logic/PropExtensionality.v b/theories/Logic/PropExtensionality.v
new file mode 100644
index 0000000000..796c602734
--- /dev/null
+++ b/theories/Logic/PropExtensionality.v
@@ -0,0 +1,22 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** This module states propositional extensionality and draws
+    consequences of it *)
+
+Axiom propositional_extensionality :
+  forall (P Q : Prop), (P <-> Q) -> P = Q.
+
+Require Import ClassicalFacts.
+
+Theorem proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2.
+Proof.
+  apply ext_prop_dep_proof_irrel_cic.
+  exact propositional_extensionality.
+Qed.
+
diff --git a/theories/Logic/vo.itarget b/theories/Logic/vo.itarget
index 71d01c1fb1..ef2709b472 100644
--- a/theories/Logic/vo.itarget
+++ b/theories/Logic/vo.itarget
@@ -26,6 +26,7 @@ IndefiniteDescription.vo
 JMeq.vo
 ProofIrrelevanceFacts.vo
 ProofIrrelevance.vo
+PropExtensionality.vo
 RelationalChoice.vo
 SetIsType.vo
 SetoidChoice.vo
-- 
cgit v1.2.3


From 620f1918452b898d6663cabb5e0f341c7e767017 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 12 Oct 2016 18:58:41 +0200
Subject: Strengthening some of the results in ChoiceFacts.v.

Further highlighting when the correspondence between variants of
choice is independent of the domain and codomain of the function, as
was done already done in the beginning of the file (suggestion from
Jason).

Adding some corollaries.
---
 theories/Logic/ChoiceFacts.v | 76 ++++++++++++++++++++++++++------------------
 1 file changed, 45 insertions(+), 31 deletions(-)

diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index 3f17ba5a95..07e8b6ef8d 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -25,11 +25,13 @@ description principles
              the context of constructive type theory, sometimes
              called axiom of no choice)
 
-- AC_fun_repr       = functional choice of a representative in an equivalence class
-- AC_fun_setoid_gen = functional form of the general form of the (so-called
-                      extensional) axiom of choice over setoids
-- AC_fun_setoid     = functional form of the (so-called extensional) axiom of
-                      choice from setoids
+- AC_fun_repr          = functional choice of a representative in an equivalence class
+- AC_fun_setoid_gen    = functional form of the general form of the (so-called
+                          extensional) axiom of choice over setoids
+- AC_fun_setoid        = functional form of the (so-called extensional) axiom of
+                         choice from setoids
+- AC_fun_setoid_simple = functional form of the (so-called extensional) axiom of
+                         choice from setoids on locally compatible relations
 
 - GAC_rel = guarded relational form of the (non extensional) axiom of choice
 - GAC_fun = guarded functional form of the (non extensional) axiom of choice
@@ -183,9 +185,9 @@ Require Import RelationClasses Logic.
 Definition RepresentativeFunctionalChoice_on :=
   forall R:A->A->Prop,
     (Equivalence R) ->
-    (exists f : A->A, forall x : A, (R x (f x)) /\ forall y, R x y -> f x = f y).
+    (exists f : A->A, forall x : A, (R x (f x)) /\ forall x', R x x' -> f x = f x').
 
-(** AC_fun_ext *)
+(** AC_fun_setoid *)
 
 Definition SetoidFunctionalChoice_on :=
   forall R : A -> A -> Prop,
@@ -193,9 +195,9 @@ Definition SetoidFunctionalChoice_on :=
   Equivalence R ->
   (forall x x' y, R x x' -> T x y -> T x' y) ->
   (forall x, exists y, T x y) ->
-  exists f : A -> B, forall x : A, T x (f x) /\ (forall y : A, R x y -> f x = f y).
+  exists f : A -> B, forall x : A, T x (f x) /\ (forall x' : A, R x x' -> f x = f x').
 
-(** AC_fun_ext_gen *)
+(** AC_fun_setoid_gen *)
 
 (* Note: This is called extensional axiom of choice (AC_ext) in
    [[Carlström04]]. *)
@@ -209,9 +211,9 @@ Definition GeneralizedSetoidFunctionalChoice_on :=
   (forall x x' y y', R x x' -> S y y' -> T x y -> T x' y') ->
   (forall x, exists y, T x y) ->
   exists f : A -> B,
-    forall x : A, T x (f x) /\ (forall y : A, R x y -> S (f x) (f y)).
+    forall x : A, T x (f x) /\ (forall x' : A, R x x' -> S (f x) (f x')).
 
-(** AC_fun_ext_simple *)
+(** AC_fun_setoid_simple *)
 
 Definition SimpleSetoidFunctionalChoice_on A B :=
   forall R : A -> A -> Prop,
@@ -1066,50 +1068,62 @@ Proof.
 Qed.
 
 (**********************************************************************)
-(** ** AC_fun_setoid = AC_fun_setoid_gen                              *)
+(** ** AC_fun_setoid = AC_fun_setoid_gen = AC_fun_setoid_simple       *)
 
 Theorem gen_setoid_fun_choice_imp_setoid_fun_choice  :
-   GeneralizedSetoidFunctionalChoice -> SetoidFunctionalChoice.
+  forall A B, GeneralizedSetoidFunctionalChoice_on A B -> SetoidFunctionalChoice_on A B.
 Proof.
-  intros GenSetoidFunChoice A B R T Hequiv Hcompat Hex.
+  intros A B GenSetoidFunChoice R T Hequiv Hcompat Hex.
   apply GenSetoidFunChoice; try easy.
   apply eq_equivalence.
   intros * H <-. firstorder.
 Qed.
 
 Theorem setoid_fun_choice_imp_gen_setoid_fun_choice :
-  SetoidFunctionalChoice -> GeneralizedSetoidFunctionalChoice.
+  forall A B, SetoidFunctionalChoice_on A B -> GeneralizedSetoidFunctionalChoice_on A B.
 Proof.
-  intros SetoidFunChoice A B R S T HequivR HequivS Hcompat Hex.
+  intros A B SetoidFunChoice R S T HequivR HequivS Hcompat Hex.
   destruct SetoidFunChoice with (R:=R) (T:=T) as (f,Hf); try easy.
   { intros; apply (Hcompat x x' y y); try easy. }
   exists f. intros x; specialize Hf with x as (Hf,Huniq). intuition. now erewrite Huniq.
 Qed.
 
+Corollary setoid_fun_choice_iff_gen_setoid_fun_choice :
+  forall A B, SetoidFunctionalChoice_on A B <-> GeneralizedSetoidFunctionalChoice_on A B.
+Proof.
+  split; auto using gen_setoid_fun_choice_imp_setoid_fun_choice, setoid_fun_choice_imp_gen_setoid_fun_choice.
+Qed.
+
 Theorem setoid_fun_choice_imp_simple_setoid_fun_choice  :
-   SetoidFunctionalChoice -> SimpleSetoidFunctionalChoice.
+   forall A B, SetoidFunctionalChoice_on A B -> SimpleSetoidFunctionalChoice_on A B.
 Proof.
-  intros SetoidFunChoice A B R T Hequiv Hexists.
+  intros A B SetoidFunChoice R T Hequiv Hexists.
   pose (T' x y := forall x', R x x' -> T x' y).
   assert (Hcompat : forall (x x' : A) (y : B), R x x' -> T' x y -> T' x' y) by firstorder.
-  destruct (SetoidFunChoice A B R T' Hequiv Hcompat Hexists) as (f,Hf).
+  destruct (SetoidFunChoice R T' Hequiv Hcompat Hexists) as (f,Hf).
   exists f. firstorder.
 Qed.
 
 Theorem simple_setoid_fun_choice_imp_setoid_fun_choice :
-  SimpleSetoidFunctionalChoice -> SetoidFunctionalChoice.
+  forall A B, SimpleSetoidFunctionalChoice_on A B -> SetoidFunctionalChoice_on A B.
+Proof.
+  intros A B SimpleSetoidFunChoice R T Hequiv Hcompat Hexists.
+  destruct (SimpleSetoidFunChoice R T Hequiv) as (f,Hf); firstorder.
+Qed.
+
+Corollary setoid_fun_choice_iff_simple_setoid_fun_choice :
+  forall A B, SetoidFunctionalChoice_on A B <-> SimpleSetoidFunctionalChoice_on A B.
 Proof.
-  intros SimpleSetoidFunChoice A B R T Hequiv Hcompat Hexists.
-  destruct (SimpleSetoidFunChoice A B R T Hequiv) as (f,Hf); firstorder.
+  split; auto using simple_setoid_fun_choice_imp_setoid_fun_choice, setoid_fun_choice_imp_simple_setoid_fun_choice.
 Qed.
 
 (**********************************************************************)
 (** ** AC_fun_setoid = AC! + AC_fun_repr                              *)
 
 Theorem setoid_fun_choice_imp_fun_choice :
-  SetoidFunctionalChoice -> FunctionalChoice.
+  forall A B, SetoidFunctionalChoice_on A B -> FunctionalChoice_on A B.
 Proof.
-  intros SetoidFunChoice A B T Hexists.
+  intros A B SetoidFunChoice T Hexists.
   destruct SetoidFunChoice with (R:=@eq A) (T:=T) as (f,Hf).
   - apply eq_equivalence.
   - now intros * ->.
@@ -1118,15 +1132,15 @@ Proof.
 Qed.
 
 Corollary setoid_fun_choice_imp_functional_rel_reification :
-  SetoidFunctionalChoice -> FunctionalRelReification.
+  forall A B, SetoidFunctionalChoice_on A B -> FunctionalRelReification_on A B.
 Proof.
-  intro SetoidFunChoice.
-  intros A B; apply fun_choice_imp_functional_rel_reification.
+  intros A B SetoidFunChoice.
+  apply fun_choice_imp_functional_rel_reification.
   now apply setoid_fun_choice_imp_fun_choice.
 Qed.
 
 Theorem setoid_fun_choice_imp_repr_fun_choice :
-  SetoidFunctionalChoice -> RepresentativeFunctionalChoice.
+  SetoidFunctionalChoice -> RepresentativeFunctionalChoice .
 Proof.
   intros SetoidFunChoice A R Hequiv.
   apply SetoidFunChoice; firstorder.
@@ -1155,7 +1169,7 @@ Proof.
   split; intros.
   - now apply functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice.
   - split.
-    + now apply setoid_fun_choice_imp_functional_rel_reification.
+    + now intros A B; apply setoid_fun_choice_imp_functional_rel_reification.
     + now apply setoid_fun_choice_imp_repr_fun_choice.
 Qed.
 
@@ -1228,7 +1242,7 @@ Proof.
     + intros A B. apply fun_choice_imp_functional_rel_reification, FunChoice.
     + now apply fun_choice_and_ext_functions_repr_and_excluded_middle_imp_setoid_fun_choice.
   - intro SetoidFunChoice. repeat split.
-    + now apply setoid_fun_choice_imp_fun_choice.
+    + now intros A B; apply setoid_fun_choice_imp_fun_choice.
     + apply repr_fun_choice_imp_ext_function_repr.
        now apply setoid_fun_choice_imp_repr_fun_choice.
     + apply repr_fun_choice_imp_excluded_middle.
@@ -1283,7 +1297,7 @@ Proof.
     + intros A B. now apply fun_choice_imp_functional_rel_reification.
     + now apply fun_choice_and_ext_pred_ext_and_proof_irrel_imp_setoid_fun_choice.
   - intro SetoidFunChoice. repeat split.
-    + now apply setoid_fun_choice_imp_fun_choice.
+    + now intros A B; apply setoid_fun_choice_imp_fun_choice.
     + apply repr_fun_choice_imp_ext_pred_repr.
        now apply setoid_fun_choice_imp_repr_fun_choice.
     + red. apply proof_irrelevance_cci.
-- 
cgit v1.2.3


From 9133d6faece4feb675fdc9c66cebcb2bba9246a9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 3 Mar 2017 14:43:00 +0100
Subject: CHANGES: choice over setoids and prop. ext.

---
 CHANGES | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/CHANGES b/CHANGES
index 4a7cb8c45e..a7cba9aa4f 100644
--- a/CHANGES
+++ b/CHANGES
@@ -7,6 +7,15 @@ Tactics
   functional extensionality in H supposed to be a quantified equality
   until giving a bare equality.
 
+Libraries
+
+- New file PropExtensionality.v to explicitly work in the axiomatic
+  context of propositional extensionality.
+- New file SetoidChoice.v axiomatically providing choice over setoids,
+  and, consequently, choice of representatives in equivalence classes.
+  Various proof-theoretic characterizations of choice over setoids in
+  file ChoiceFacts.v.
+
 Changes from V8.6beta1 to V8.6
 ==============================
 
-- 
cgit v1.2.3