1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(*i $Id: IndefiniteDescription.v 10170 2007-10-03 14:41:25Z herbelin $ i*)
11
(** This file provides a constructive form of indefinite description that
12
allows to build choice functions; this is weaker than Hilbert's
13
epsilon operator (which implies weakly classical properties) but
14
stronger than the axiom of choice (which cannot be used outside
15
the context of a theorem proof). *)
17
Require Import ChoiceFacts.
19
Set Implicit Arguments.
21
Axiom constructive_indefinite_description :
22
forall (A : Type) (P : A->Prop),
23
(exists x, P x) -> { x : A | P x }.
25
Lemma constructive_definite_description :
26
forall (A : Type) (P : A->Prop),
27
(exists! x, P x) -> { x : A | P x }.
29
intros; apply constructive_indefinite_description; firstorder.
32
Lemma functional_choice :
33
forall (A B : Type) (R:A->B->Prop),
34
(forall x : A, exists y : B, R x y) ->
35
(exists f : A->B, forall x : A, R x (f x)).
37
apply constructive_indefinite_descr_fun_choice.
38
exact constructive_indefinite_description.