diff options
| -rw-r--r-- | doc/stdlib/index-list.html.template | 2 | ||||
| -rw-r--r-- | theories/Logic/ExtensionalFunctionRepresentative.v | 24 | ||||
| -rw-r--r-- | theories/Logic/SetoidChoice.v | 60 | ||||
| -rw-r--r-- | theories/Logic/vo.itarget | 4 |
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 |