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
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
|
(************************************************************************)
(* 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 *)
(************************************************************************)
(** This is a proof in the pure Calculus of Construction that
classical logic in Prop + dependent elimination of disjunction entails
proof-irrelevance.
Since, dependent elimination is derivable in the Calculus of
Inductive Constructions (CCI), we get proof-irrelevance from classical
logic in the CCI.
Reference:
- [Coquand] T. Coquand, "Metamathematical Investigations of a
Calculus of Constructions", Proceedings of Logic in Computer Science
(LICS'90), 1990.
Proof skeleton: classical logic + dependent elimination of
disjunction + discrimination of proofs implies the existence of a
retract from [Prop] into [bool], hence inconsistency by encoding any
paradox of system U- (e.g. Hurkens' paradox).
*)
Require Import Hurkens.
Section Proof_irrelevance_CC.
Variable or : Prop -> Prop -> Prop.
Variable or_introl : forall A B:Prop, A -> or A B.
Variable or_intror : forall A B:Prop, B -> or A B.
Hypothesis or_elim : forall A B C:Prop, (A -> C) -> (B -> C) -> or A B -> C.
Hypothesis
or_elim_redl :
forall (A B C:Prop) (f:A -> C) (g:B -> C) (a:A),
f a = or_elim A B C f g (or_introl A B a).
Hypothesis
or_elim_redr :
forall (A B C:Prop) (f:A -> C) (g:B -> C) (b:B),
g b = or_elim A B C f g (or_intror A B b).
Hypothesis
or_dep_elim :
forall (A B:Prop) (P:or A B -> Prop),
(forall a:A, P (or_introl A B a)) ->
(forall b:B, P (or_intror A B b)) -> forall b:or A B, P b.
Hypothesis em : forall A:Prop, or A (~ A).
Variable B : Prop.
Variables b1 b2 : B.
(** [p2b] and [b2p] form a retract if [~b1=b2] *)
Definition p2b A := or_elim A (~ A) B (fun _ => b1) (fun _ => b2) (em A).
Definition b2p b := b1 = b.
Lemma p2p1 : forall A:Prop, A -> b2p (p2b A).
Proof.
unfold p2b in |- *; intro A; apply or_dep_elim with (b := em A);
unfold b2p in |- *; intros.
apply (or_elim_redl A (~ A) B (fun _ => b1) (fun _ => b2)).
destruct (b H).
Qed.
Lemma p2p2 : b1 <> b2 -> forall A:Prop, b2p (p2b A) -> A.
Proof.
intro not_eq_b1_b2.
unfold p2b in |- *; intro A; apply or_dep_elim with (b := em A);
unfold b2p in |- *; intros.
assumption.
destruct not_eq_b1_b2.
rewrite <- (or_elim_redr A (~ A) B (fun _ => b1) (fun _ => b2)) in H.
assumption.
Qed.
(** Using excluded-middle a second time, we get proof-irrelevance *)
Theorem proof_irrelevance_cc : b1 = b2.
Proof.
refine (or_elim _ _ _ _ _ (em (b1 = b2))); intro H.
trivial.
apply (paradox B p2b b2p (p2p2 H) p2p1).
Qed.
End Proof_irrelevance_CC.
(** The Calculus of Inductive Constructions (CCI) enjoys dependent
elimination, hence classical logic in CCI entails proof-irrelevance.
*)
Section Proof_irrelevance_CCI.
Hypothesis em : forall A:Prop, A \/ ~ A.
Definition or_elim_redl (A B C:Prop) (f:A -> C) (g:B -> C)
(a:A) : f a = or_ind f g (or_introl B a) := refl_equal (f a).
Definition or_elim_redr (A B C:Prop) (f:A -> C) (g:B -> C)
(b:B) : g b = or_ind f g (or_intror A b) := refl_equal (g b).
Scheme or_indd := Induction for or Sort Prop.
Theorem proof_irrelevance_cci : forall (B:Prop) (b1 b2:B), b1 = b2.
Proof
proof_irrelevance_cc or or_introl or_intror or_ind or_elim_redl
or_elim_redr or_indd em.
End Proof_irrelevance_CCI.
(** Remark: in CCI, [bool] can be taken in [Set] as well in the
paradox and since [~true=false] for [true] and [false] in
[bool], we get the inconsistency of [em : forall A:Prop, {A}+{~A}] in CCI
*)
|
