ClassicalUniqueChoice.v

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.

(* -*- coding: utf-8 -*- *)
(************************************************************************)
(*         *   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 unique choice; this is weaker than providing iota operator and classical logic as the definite descriptions provided by the axiom of unique choice can be used only in a propositional context (especially, they cannot be used to build functions outside the scope of a theorem proof)

Classical logic and unique choice, as shown in [ChicliPottierSimpson02], implies the double-negation of excluded-middle in Set, hence it implies a strongly classical world. Especially it conflicts with the impredicativity of Set.

[ChicliPottierSimpson02] Laurent Chicli, Loïc Pottier, Carlos Simpson, Mathematical Quotients and Quotient Types in Coq, Proceedings of TYPES 2002, Lecture Notes in Computer Science 2646, Springer Verlag.

Require Export Classical.

Axiom
  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)).

Unique choice reifies functional relations into functions

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)).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)
Proof.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)
intros A B.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 A (fun _ => B)).
Qed.

The following proof comes from [ChicliPottierSimpson02]

Require Import Setoid.

Theorem classic_set_in_prop_context :
  forall C:Prop, ((forall P:Prop, {P} + {~ P}) -> C) -> C.forall C : Prop,
((forall P : Prop, {P} + {~ P}) -> C) -> C
Proof.forall C : Prop,
((forall P : Prop, {P} + {~ P}) -> C) -> C
intros C HnotEM.C:Prop
HnotEM:(forall P : Prop, {P} + {~ P}) -> C
C
set (R := fun A b => A /\ true = b \/ ~ A /\ false = b).C:Prop
HnotEM:(forall P : Prop, {P} + {~ P}) -> C
R:=fun (A : Prop) (b : bool) =>
A /\ true = b \/ ~ A /\ false = b:Prop -> bool -> Prop
C
assert (H :  exists f : Prop -> bool, (forall A:Prop, R A (f A))).C:Prop
HnotEM:(forall P : Prop, {P} + {~ P}) -> C
R:=fun (A : Prop) (b : bool) =>
A /\ true = b \/ ~ A /\ false = b:Prop -> bool -> Prop
exists f : Prop -> bool, forall A : Prop, R A (f A)
C:Prop
HnotEM:(forall P : Prop, {P} + {~ P}) -> C
R:=fun (A : Prop) (b : bool) =>
A /\ true = b \/ ~ A /\ false = b:Prop -> bool -> Prop
H:exists f : Prop -> bool,
  forall A : Prop, R A (f A)
C
apply unique_choice.C:Prop
HnotEM:(forall P : Prop, {P} + {~ P}) -> C
R:=fun (A : Prop) (b : bool) =>
A /\ true = b \/ ~ A /\ false = b:Prop -> bool -> Prop
forall x : Prop, exists ! y : bool, R x y
C:Prop
HnotEM:(forall P : Prop, {P} + {~ P}) -> C
R:=fun (A : Prop) (b : bool) =>
A /\ true = b \/ ~ A /\ false = b:Prop -> bool -> Prop
H:exists f : Prop -> bool,
  forall A : Prop, R A (f A)
C
intro A.C:Prop
HnotEM:(forall P : Prop, {P} + {~ P}) -> C
R:=fun (A0 : Prop) (b : bool) =>
A0 /\ true = b \/ ~ A0 /\ false = b:Prop -> bool -> Prop
A:Prop
exists ! y : bool, R A y
C:Prop
HnotEM:(forall P : Prop, {P} + {~ P}) -> C
R:=fun (A : Prop) (b : bool) =>
A /\ true = b \/ ~ A /\ false = b:Prop -> bool -> Prop
H:exists f : Prop -> bool,
  forall A : Prop, R A (f A)
C
destruct (classic A) as [Ha| Hnota].C:Prop
HnotEM:(forall P : Prop, {P} + {~ P}) -> C
R:=fun (A0 : Prop) (b : bool) =>
A0 /\ true = b \/ ~ A0 /\ false = b:Prop -> bool -> Prop
A:Prop
Ha:A
exists ! y : bool, R A y
C:Prop
HnotEM:(forall P : Prop, {P} + {~ P}) -> C
R:=fun (A0 : Prop) (b : bool) =>
A0 /\ true = b \/ ~ A0 /\ false = b:Prop -> bool -> Prop
A:Prop
Hnota:~ A
exists ! y : bool, R A y
C:Prop
HnotEM:(forall P : Prop, {P} + {~ P}) -> C
R:=fun (A : Prop) (b : bool) =>
A /\ true = b \/ ~ A /\ false = b:Prop -> bool -> Prop
H:exists f : Prop -> bool,
  forall A : Prop, R A (f A)
C
  exists true; split.C:Prop
HnotEM:(forall P : Prop, {P} + {~ P}) -> C
R:=fun (A0 : Prop) (b : bool) =>
A0 /\ true = b \/ ~ A0 /\ false = b:Prop -> bool -> Prop
A:Prop
Ha:A
R A true
C:Prop
HnotEM:(forall P : Prop, {P} + {~ P}) -> C
R:=fun (A0 : Prop) (b : bool) =>
A0 /\ true = b \/ ~ A0 /\ false = b:Prop -> bool -> Prop
A:Prop
Ha:A
forall x' : bool, R A x' -> true = x'
C:Prop
HnotEM:(forall P : Prop, {P} + {~ P}) -> C
R:=fun (A0 : Prop) (b : bool) =>
A0 /\ true = b \/ ~ A0 /\ false = b:Prop -> bool -> Prop
A:Prop
Hnota:~ A
exists ! y : bool, R A y
C:Prop
HnotEM:(forall P : Prop, {P} + {~ P}) -> C
R:=fun (A : Prop) (b : bool) =>
A /\ true = b \/ ~ A /\ false = b:Prop -> bool -> Prop
H:exists f : Prop -> bool,
  forall A : Prop, R A (f A)
C
    left; split; [ assumption | reflexivity ].C:Prop
HnotEM:(forall P : Prop, {P} + {~ P}) -> C
R:=fun (A0 : Prop) (b : bool) =>
A0 /\ true = b \/ ~ A0 /\ false = b:Prop -> bool -> Prop
A:Prop
Ha:A
forall x' : bool, R A x' -> true = x'
C:Prop
HnotEM:(forall P : Prop, {P} + {~ P}) -> C
R:=fun (A0 : Prop) (b : bool) =>
A0 /\ true = b \/ ~ A0 /\ false = b:Prop -> bool -> Prop
A:Prop
Hnota:~ A
exists ! y : bool, R A y
C:Prop
HnotEM:(forall P : Prop, {P} + {~ P}) -> C
R:=fun (A : Prop) (b : bool) =>
A /\ true = b \/ ~ A /\ false = b:Prop -> bool -> Prop
H:exists f : Prop -> bool,
  forall A : Prop, R A (f A)
C
    intros y [[_ Hy]| [Hna _]].C:Prop
HnotEM:(forall P : Prop, {P} + {~ P}) -> C
R:=fun (A0 : Prop) (b : bool) =>
A0 /\ true = b \/ ~ A0 /\ false = b:Prop -> bool -> Prop
A:Prop
Ha:A
y:bool
Hy:true = y
true = y
C:Prop
HnotEM:(forall P : Prop, {P} + {~ P}) -> C
R:=fun (A0 : Prop) (b : bool) =>
A0 /\ true = b \/ ~ A0 /\ false = b:Prop -> bool -> Prop
A:Prop
Ha:A
y:bool
Hna:~ A
true = y
C:Prop
HnotEM:(forall P : Prop, {P} + {~ P}) -> C
R:=fun (A0 : Prop) (b : bool) =>
A0 /\ true = b \/ ~ A0 /\ false = b:Prop -> bool -> Prop
A:Prop
Hnota:~ A
exists ! y : bool, R A y
C:Prop
HnotEM:(forall P : Prop, {P} + {~ P}) -> C
R:=fun (A : Prop) (b : bool) =>
A /\ true = b \/ ~ A /\ false = b:Prop -> bool -> Prop
H:exists f : Prop -> bool,
  forall A : Prop, R A (f A)
C
      assumption.C:Prop
HnotEM:(forall P : Prop, {P} + {~ P}) -> C
R:=fun (A0 : Prop) (b : bool) =>
A0 /\ true = b \/ ~ A0 /\ false = b:Prop -> bool -> Prop
A:Prop
Ha:A
y:bool
Hna:~ A
true = y
C:Prop
HnotEM:(forall P : Prop, {P} + {~ P}) -> C
R:=fun (A0 : Prop) (b : bool) =>
A0 /\ true = b \/ ~ A0 /\ false = b:Prop -> bool -> Prop
A:Prop
Hnota:~ A
exists ! y : bool, R A y
C:Prop
HnotEM:(forall P : Prop, {P} + {~ P}) -> C
R:=fun (A : Prop) (b : bool) =>
A /\ true = b \/ ~ A /\ false = b:Prop -> bool -> Prop
H:exists f : Prop -> bool,
  forall A : Prop, R A (f A)
C
      contradiction.C:Prop
HnotEM:(forall P : Prop, {P} + {~ P}) -> C
R:=fun (A0 : Prop) (b : bool) =>
A0 /\ true = b \/ ~ A0 /\ false = b:Prop -> bool -> Prop
A:Prop
Hnota:~ A
exists ! y : bool, R A y
C:Prop
HnotEM:(forall P : Prop, {P} + {~ P}) -> C
R:=fun (A : Prop) (b : bool) =>
A /\ true = b \/ ~ A /\ false = b:Prop -> bool -> Prop
H:exists f : Prop -> bool,
  forall A : Prop, R A (f A)
C
  exists false; split.C:Prop
HnotEM:(forall P : Prop, {P} + {~ P}) -> C
R:=fun (A0 : Prop) (b : bool) =>
A0 /\ true = b \/ ~ A0 /\ false = b:Prop -> bool -> Prop
A:Prop
Hnota:~ A
R A false
C:Prop
HnotEM:(forall P : Prop, {P} + {~ P}) -> C
R:=fun (A0 : Prop) (b : bool) =>
A0 /\ true = b \/ ~ A0 /\ false = b:Prop -> bool -> Prop
A:Prop
Hnota:~ A
forall x' : bool, R A x' -> false = x'
C:Prop
HnotEM:(forall P : Prop, {P} + {~ P}) -> C
R:=fun (A : Prop) (b : bool) =>
A /\ true = b \/ ~ A /\ false = b:Prop -> bool -> Prop
H:exists f : Prop -> bool,
  forall A : Prop, R A (f A)
C
    right; split; [ assumption | reflexivity ].C:Prop
HnotEM:(forall P : Prop, {P} + {~ P}) -> C
R:=fun (A0 : Prop) (b : bool) =>
A0 /\ true = b \/ ~ A0 /\ false = b:Prop -> bool -> Prop
A:Prop
Hnota:~ A
forall x' : bool, R A x' -> false = x'
C:Prop
HnotEM:(forall P : Prop, {P} + {~ P}) -> C
R:=fun (A : Prop) (b : bool) =>
A /\ true = b \/ ~ A /\ false = b:Prop -> bool -> Prop
H:exists f : Prop -> bool,
  forall A : Prop, R A (f A)
C
    intros y [[Ha _]| [_ Hy]].C:Prop
HnotEM:(forall P : Prop, {P} + {~ P}) -> C
R:=fun (A0 : Prop) (b : bool) =>
A0 /\ true = b \/ ~ A0 /\ false = b:Prop -> bool -> Prop
A:Prop
Hnota:~ A
y:bool
Ha:A
false = y
C:Prop
HnotEM:(forall P : Prop, {P} + {~ P}) -> C
R:=fun (A0 : Prop) (b : bool) =>
A0 /\ true = b \/ ~ A0 /\ false = b:Prop -> bool -> Prop
A:Prop
Hnota:~ A
y:bool
Hy:false = y
false = y
C:Prop
HnotEM:(forall P : Prop, {P} + {~ P}) -> C
R:=fun (A : Prop) (b : bool) =>
A /\ true = b \/ ~ A /\ false = b:Prop -> bool -> Prop
H:exists f : Prop -> bool,
  forall A : Prop, R A (f A)
C
      contradiction.C:Prop
HnotEM:(forall P : Prop, {P} + {~ P}) -> C
R:=fun (A0 : Prop) (b : bool) =>
A0 /\ true = b \/ ~ A0 /\ false = b:Prop -> bool -> Prop
A:Prop
Hnota:~ A
y:bool
Hy:false = y
false = y
C:Prop
HnotEM:(forall P : Prop, {P} + {~ P}) -> C
R:=fun (A : Prop) (b : bool) =>
A /\ true = b \/ ~ A /\ false = b:Prop -> bool -> Prop
H:exists f : Prop -> bool,
  forall A : Prop, R A (f A)
C
      assumption.C:Prop
HnotEM:(forall P : Prop, {P} + {~ P}) -> C
R:=fun (A : Prop) (b : bool) =>
A /\ true = b \/ ~ A /\ false = b:Prop -> bool -> Prop
H:exists f : Prop -> bool,
  forall A : Prop, R A (f A)
C
destruct H as [f Hf].C:Prop
HnotEM:(forall P : Prop, {P} + {~ P}) -> C
R:=fun (A : Prop) (b : bool) =>
A /\ true = b \/ ~ A /\ false = b:Prop -> bool -> Prop
f:Prop -> bool
Hf:forall A : Prop, R A (f A)
C
apply HnotEM.C:Prop
HnotEM:(forall P : Prop, {P} + {~ P}) -> C
R:=fun (A : Prop) (b : bool) =>
A /\ true = b \/ ~ A /\ false = b:Prop -> bool -> Prop
f:Prop -> bool
Hf:forall A : Prop, R A (f A)
forall P : Prop, {P} + {~ P}
intro P.C:Prop
HnotEM:(forall P0 : Prop, {P0} + {~ P0}) -> C
R:=fun (A : Prop) (b : bool) =>
A /\ true = b \/ ~ A /\ false = b:Prop -> bool -> Prop
f:Prop -> bool
Hf:forall A : Prop, R A (f A)
P:Prop
{P} + {~ P}
assert (HfP := Hf P).C:Prop
HnotEM:(forall P0 : Prop, {P0} + {~ P0}) -> C
R:=fun (A : Prop) (b : bool) =>
A /\ true = b \/ ~ A /\ false = b:Prop -> bool -> Prop
f:Prop -> bool
Hf:forall A : Prop, R A (f A)
P:Prop
HfP:R P (f P)
{P} + {~ P}
(* Elimination from Hf to Set is not allowed but from f to Set yes ! *)
destruct (f P).C:Prop
HnotEM:(forall P0 : Prop, {P0} + {~ P0}) -> C
R:=fun (A : Prop) (b : bool) =>
A /\ true = b \/ ~ A /\ false = b:Prop -> bool -> Prop
f:Prop -> bool
Hf:forall A : Prop, R A (f A)
P:Prop
HfP:R P true
{P} + {~ P}
C:Prop
HnotEM:(forall P0 : Prop, {P0} + {~ P0}) -> C
R:=fun (A : Prop) (b : bool) =>
A /\ true = b \/ ~ A /\ false = b:Prop -> bool -> Prop
f:Prop -> bool
Hf:forall A : Prop, R A (f A)
P:Prop
HfP:R P false
{P} + {~ P}
  left.C:Prop
HnotEM:(forall P0 : Prop, {P0} + {~ P0}) -> C
R:=fun (A : Prop) (b : bool) =>
A /\ true = b \/ ~ A /\ false = b:Prop -> bool -> Prop
f:Prop -> bool
Hf:forall A : Prop, R A (f A)
P:Prop
HfP:R P true
P
C:Prop
HnotEM:(forall P0 : Prop, {P0} + {~ P0}) -> C
R:=fun (A : Prop) (b : bool) =>
A /\ true = b \/ ~ A /\ false = b:Prop -> bool -> Prop
f:Prop -> bool
Hf:forall A : Prop, R A (f A)
P:Prop
HfP:R P false
{P} + {~ P}
  destruct HfP as [[Ha _]| [_ Hfalse]].C:Prop
HnotEM:(forall P0 : Prop, {P0} + {~ P0}) -> C
R:=fun (A : Prop) (b : bool) =>
A /\ true = b \/ ~ A /\ false = b:Prop -> bool -> Prop
f:Prop -> bool
Hf:forall A : Prop, R A (f A)
P:Prop
Ha:P
P
C:Prop
HnotEM:(forall P0 : Prop, {P0} + {~ P0}) -> C
R:=fun (A : Prop) (b : bool) =>
A /\ true = b \/ ~ A /\ false = b:Prop -> bool -> Prop
f:Prop -> bool
Hf:forall A : Prop, R A (f A)
P:Prop
Hfalse:false = true
P
C:Prop
HnotEM:(forall P0 : Prop, {P0} + {~ P0}) -> C
R:=fun (A : Prop) (b : bool) =>
A /\ true = b \/ ~ A /\ false = b:Prop -> bool -> Prop
f:Prop -> bool
Hf:forall A : Prop, R A (f A)
P:Prop
HfP:R P false
{P} + {~ P}
    assumption.C:Prop
HnotEM:(forall P0 : Prop, {P0} + {~ P0}) -> C
R:=fun (A : Prop) (b : bool) =>
A /\ true = b \/ ~ A /\ false = b:Prop -> bool -> Prop
f:Prop -> bool
Hf:forall A : Prop, R A (f A)
P:Prop
Hfalse:false = true
P
C:Prop
HnotEM:(forall P0 : Prop, {P0} + {~ P0}) -> C
R:=fun (A : Prop) (b : bool) =>
A /\ true = b \/ ~ A /\ false = b:Prop -> bool -> Prop
f:Prop -> bool
Hf:forall A : Prop, R A (f A)
P:Prop
HfP:R P false
{P} + {~ P}
    discriminate.C:Prop
HnotEM:(forall P0 : Prop, {P0} + {~ P0}) -> C
R:=fun (A : Prop) (b : bool) =>
A /\ true = b \/ ~ A /\ false = b:Prop -> bool -> Prop
f:Prop -> bool
Hf:forall A : Prop, R A (f A)
P:Prop
HfP:R P false
{P} + {~ P}
  right.C:Prop
HnotEM:(forall P0 : Prop, {P0} + {~ P0}) -> C
R:=fun (A : Prop) (b : bool) =>
A /\ true = b \/ ~ A /\ false = b:Prop -> bool -> Prop
f:Prop -> bool
Hf:forall A : Prop, R A (f A)
P:Prop
HfP:R P false
~ P
  destruct HfP as [[_ Hfalse]| [Hna _]].C:Prop
HnotEM:(forall P0 : Prop, {P0} + {~ P0}) -> C
R:=fun (A : Prop) (b : bool) =>
A /\ true = b \/ ~ A /\ false = b:Prop -> bool -> Prop
f:Prop -> bool
Hf:forall A : Prop, R A (f A)
P:Prop
Hfalse:true = false
~ P
C:Prop
HnotEM:(forall P0 : Prop, {P0} + {~ P0}) -> C
R:=fun (A : Prop) (b : bool) =>
A /\ true = b \/ ~ A /\ false = b:Prop -> bool -> Prop
f:Prop -> bool
Hf:forall A : Prop, R A (f A)
P:Prop
Hna:~ P
~ P
    discriminate.C:Prop
HnotEM:(forall P0 : Prop, {P0} + {~ P0}) -> C
R:=fun (A : Prop) (b : bool) =>
A /\ true = b \/ ~ A /\ false = b:Prop -> bool -> Prop
f:Prop -> bool
Hf:forall A : Prop, R A (f A)
P:Prop
Hna:~ P
~ P
    assumption. 
Qed.

Corollary not_not_classic_set :
  ((forall P:Prop, {P} + {~ P}) -> False) -> False.((forall P : Prop, {P} + {~ P}) -> False) -> False
Proof.((forall P : Prop, {P} + {~ P}) -> False) -> False
apply classic_set_in_prop_context.
Qed.

(* Compatibility *)
Notation classic_set := not_not_classic_set (only parsing).