aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--doc/stdlib/index-list.html.template2
-rw-r--r--theories/Logic/ExtensionalFunctionRepresentative.v24
-rw-r--r--theories/Logic/SetoidChoice.v60
-rw-r--r--theories/Logic/vo.itarget4
4 files changed, 89 insertions, 1 deletions
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 4a685a3b8..4ffdbb115 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 000000000..a9da68e16
--- /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 000000000..84432dda1
--- /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 323597395..71d01c1fb 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