Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.
(************************************************************************)
(*         *   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          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)
This file provides classical logic and functional choice; this especially provides both indefinite descriptions and choice functions but this is weaker than providing epsilon operator and classical logic as the indefinite descriptions provided by the axiom of choice can be used only in a propositional context (especially, they cannot be used to build choice functions outside the scope of a theorem proof)
This file extends ClassicalUniqueChoice.v with full choice. As ClassicalUniqueChoice.v, it implies the double-negation of excluded-middle in Set and leads to a classical world populated with non computable functions. Especially it conflicts with the impredicativity of Set, knowing that true≠false in Set. 
Require Export ClassicalUniqueChoice.
Require Export RelationalChoice.
Require Import ChoiceFacts.

Set Implicit Arguments.

Definition subset (U:Type) (P Q:U->Prop) : Prop := forall x, P x -> Q x.


forall (A : Type) (P : A -> Prop),
(exists x : A, P x) ->
exists P' : A -> Prop,
  subset P' P /\ (exists ! x : A, P' x)


forall (A : Type) (P : A -> Prop),
(exists x : A, P x) ->
exists P' : A -> Prop,
  subset P' P /\ (exists ! x : A, P' x)


A:Type
P:A -> Prop
H:exists x : A, P x
exists P' : A -> Prop,
  subset P' P /\ (exists ! x : A, P' x)


A:Type
P:A -> Prop
H:exists x : A, P x
R':unit -> A -> Prop
Hsub:subrelation R' (fun _ : unit => P)
HR':forall x : unit, exists ! y : A, R' x y
exists P' : A -> Prop,
  subset P' P /\ (exists ! x : A, P' x)

exists (R' tt); firstorder.
Qed.


forall (A B : Type) (R : A -> B -> Prop),
(forall x : A, exists y : B, R x y) ->
exists f : A -> B, forall x : A, R x (f x)


forall (A B : Type) (R : A -> B -> Prop),
(forall x : A, exists y : B, R x y) ->
exists f : A -> B, forall x : A, R x (f x)


A, B:Type
forall R : A -> B -> Prop,
(forall x : A, exists y : B, R x y) ->
exists f : A -> B, forall x : A, R x (f x)


A, B:Type
FunctionalRelReification_on A B
A, B:Type
RelationalChoice_on A B


A, B:Type
RelationalChoice_on A B

exact (relational_choice A B).
Qed.