Library Coq.Logic.ClassicalDescription


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. Require Export Description. Require Import ChoiceFacts.


The idea for the following proof comes from ChicliPottierSimpson02

Theorem excluded_middle_informative : forall P:Prop, {P} + {~ P}.

Theorem classical_definite_description :
  forall (A : Type) (P : A->Prop), inhabited A ->
  { x : A | (exists! x : A, P x) -> P x }.

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)
Theorem dependent_unique_choice :
  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)).

Theorem unique_choice :
  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)).

Compatibility lemmas

Unset Implicit Arguments.

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