1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id: ClassicalDescription.v,v 1.2.2.1 2004/07/16 19:31:29 herbelin Exp $ i*)
(** This file provides classical logic and definite description *)
(** Classical logic and definite description, as shown in [1],
implies the double-negation of excluded-middle in Set, hence it
implies a strongly classical world. Especially it conflicts with
impredicativity of Set, knowing that true<>false in Set.
[1] 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_description :
(A:Type;B:A->Type;R: (x:A)(B x)->Prop)
((x:A)(EX y:(B x)|(R x y)/\ ((y':(B x))(R x y') -> y=y')))
-> (EX f:(x:A)(B x) | (x:A)(R x (f x))).
(** Principle of definite descriptions (aka axiom of unique choice) *)
Theorem description :
(A:Type;B:Type;R: A->B->Prop)
((x:A)(EX y:B|(R x y)/\ ((y':B)(R x y') -> y=y')))
-> (EX f:A->B | (x:A)(R x (f x))).
Proof.
Intros A B.
Apply (dependent_description A [_]B).
Qed.
(** The followig proof comes from [1] *)
Theorem classic_set : (((P:Prop){P}+{~P}) -> False) -> False.
Proof.
Intro HnotEM.
Pose R:=[A,b]A/\true=b \/ ~A/\false=b.
Assert H:(EX f:Prop->bool|(A:Prop)(R A (f A))).
Apply description.
Intro A.
NewDestruct (classic A) as [Ha|Hnota].
Exists true; Split.
Left; Split; [Assumption|Reflexivity].
Intros y [[_ Hy]|[Hna _]].
Assumption.
Contradiction.
Exists false; Split.
Right; Split; [Assumption|Reflexivity].
Intros y [[Ha _]|[_ Hy]].
Contradiction.
Assumption.
NewDestruct H as [f Hf].
Apply HnotEM.
Intro P.
Assert HfP := (Hf P).
(* Elimination from Hf to Set is not allowed but from f to Set yes ! *)
NewDestruct (f P).
Left.
NewDestruct HfP as [[Ha _]|[_ Hfalse]].
Assumption.
Discriminate.
Right.
NewDestruct HfP as [[_ Hfalse]|[Hna _]].
Discriminate.
Assumption.
Qed.
|
