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 definite description, which is equivalent to providing classical logic and Church's iota operator
Classical logic and definite descriptions implies excluded-middle in Set and leads to a classical world populated with non computable functions. It conflicts with the impredicativity of Set 
Set Implicit Arguments.

Require Export Classical.   (* Axiomatize classical reasoning *)
Require Export Description. (* Axiomatize constructive form of Church's iota *)
Require Import ChoiceFacts.

Notation inhabited A := A (only parsing).
The idea for the following proof comes from ChicliPottierSimpson02 
forall P : Prop, {P} + {~ P}


forall P : Prop, {P} + {~ P}

apply
  (constructive_definite_descr_excluded_middle
   constructive_definite_description classic).
Qed.


forall (A : Type) (P : A -> Prop),
A -> {x : A | (exists ! x0 : A, P x0) -> P x}


forall (A : Type) (P : A -> Prop),
A -> {x : A | (exists ! x0 : A, P x0) -> P x}


A:Type
P:A -> Prop
i:A
{x : A | (exists ! x0 : A, P x0) -> P x}


A:Type
P:A -> Prop
i:A
Hex:exists ! x : A, P x
{x : A | (exists ! x0 : A, P x0) -> P x}
A:Type
P:A -> Prop
i:A
HnonP:~ (exists ! x : A, P x)
{x : A | (exists ! x0 : A, P x0) -> P x}

  
A:Type
P:A -> Prop
i:A
Hex:exists ! x : A, P x
exists ! x : A, (exists ! x0 : A, P x0) -> P x
A:Type
P:A -> Prop
i:A
HnonP:~ (exists ! x : A, P x)
{x : A | (exists ! x0 : A, P x0) -> P x}

  
A:Type
P:A -> Prop
i, x:A
Hx:P x
Huni:forall x' : A, P x' -> x = x'
exists ! x0 : A, (exists ! x1 : A, P x1) -> P x0
A:Type
P:A -> Prop
i:A
HnonP:~ (exists ! x : A, P x)
{x : A | (exists ! x0 : A, P x0) -> P x}

  
A:Type
P:A -> Prop
i, x:A
Hx:P x
Huni:forall x' : A, P x' -> x = x'
(exists ! x0 : A, P x0) -> P x
A:Type
P:A -> Prop
i, x:A
Hx:P x
Huni:forall x' : A, P x' -> x = x'
forall x' : A,
((exists ! x0 : A, P x0) -> P x') -> x = x'
A:Type
P:A -> Prop
i:A
HnonP:~ (exists ! x : A, P x)
{x : A | (exists ! x0 : A, P x0) -> P x}

    
A:Type
P:A -> Prop
i, x:A
Hx:P x
Huni:forall x' : A, P x' -> x = x'
forall x' : A,
((exists ! x0 : A, P x0) -> P x') -> x = x'
A:Type
P:A -> Prop
i:A
HnonP:~ (exists ! x : A, P x)
{x : A | (exists ! x0 : A, P x0) -> P x}

    
A:Type
P:A -> Prop
i:A
HnonP:~ (exists ! x : A, P x)
{x : A | (exists ! x0 : A, P x0) -> P x}

exists i; tauto.
Qed.
Church's iota operator 
Definition iota (A : Type) (i:inhabited A) (P : A->Prop) : A
  := proj1_sig (classical_definite_description P i).

Definition iota_spec (A : Type) (i:inhabited A) (P : A->Prop) :
  (exists! x:A, P x) -> P (iota i P)
  := proj2_sig (classical_definite_description P i).
Axiom of unique "choice" (functional reification of functional relations) 
forall (A : Type) (B : A -> Type)
  (R : forall x : A, B x -> Prop),
(forall x : A, exists ! y : B x, R x y) ->
exists f : forall x : A, B x, forall x : A, R x (f x)


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


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


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

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


A:Type
B:A -> Type
R:forall x : A, B x -> Prop
H, Hexuni:forall x : A, exists ! y : B x, R x y
forall x : A,
R x
  (proj1_sig
     (constructive_definite_description 
        (R x) (Hexuni x)))


A:Type
B:A -> Type
R:forall x0 : A, B x0 -> Prop
H, Hexuni:forall x0 : A, exists ! y : B x0, R x0 y
x:A
R x
  (proj1_sig
     (constructive_definite_description 
        (R x) (Hexuni x)))

apply (proj2_sig (constructive_definite_description (R x) (Hexuni x))).
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)

apply dependent_unique_choice with (B:=fun _:A => B).
Qed.
Compatibility lemmas 
Unset Implicit Arguments.

Definition dependent_description := dependent_unique_choice.
Definition description := unique_choice.