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
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
|
(* cf antwoorden voor laatste opgave *)
Section proplogic.
Parameters A B C : Prop.
(* exercise 1 *)
(* complete the following simply typed lambda terms *)
Definition prop1 := fun (x : C -> B -> A) (y : C -> B) (z : C) => x z (y z).
Definition prop2 := fun (x : B -> C -> A) (y : C -> B) (z : C) => x (y z) z.
Definition prop3 := fun (x : (A -> B) -> B -> C) (y : B) => x (fun z : A => y) y.
Definition prop4 := fun (x : A -> B -> C) (y : (A -> B -> C) -> A) (z : (A -> B -> C) -> B) => x (y x) (z x).
End proplogic.
Section deptypes.
(* exercise 2 *)
(* complete the following dependently typed lambda terms *)
Definition pred1 := fun (l : Set -> Set) (A : Set) (B : Set) (f : l A -> l B) (x : l A) => f x.
Definition pred2 := fun (e : nat -> nat -> Set) (n : nat) => forall m : nat, e n m.
End deptypes.
Section drinker.
(* we will prove (twice) the drinker's paradox:
in a non-empty domain there is someone such that
if he drinks then everyone drinks *)
(* use the following *)
Parameter D : Set.
Parameter d : D.
Parameter drinks : D -> Prop.
(* law of excluded middle *)
Parameter em: forall p:Prop, p \/ ~p.
(* double negation law *)
Parameter dn: forall p:Prop, ~~p -> p.
(* first proof *)
(* exercise 3 *)
(* prove the following auxiliary lemma
use dn twice, first time quite soon *)
(* With help: https://stackoverflow.com/a/4418135/1544337 *)
Lemma aux : (~ forall x:D, drinks x) -> (exists x:D, ~drinks x).
Proof.
intro F.
apply dn.
intro E.
apply F.
intro x.
assert (drinks x \/ ~drinks x).
apply em.
inversion_clear H.
exact H0.
elimtype False.
apply E.
exists x.
exact H0.
Qed.
(* exercise 4 *)
(* prove the drinker's paradox *)
(* first step: use em to distinguish two cases: everyone drinks or not *)
(* for the second case, use aux *)
Theorem drinker : exists x:D, (drinks x) -> (forall y:D, drinks y).
Proof.
assert ((forall x:D, drinks x) \/ ~(forall x:D, drinks x)).
apply em.
inversion_clear H.
exists d.
intro.
exact H0.
assert (exists x:D, ~drinks x).
apply aux.
exact H0.
elim H.
intros x H'.
exists x.
intro.
elimtype False.
apply H'.
exact H1.
Qed.
(* second proof *)
(* exercise 5 *)
(* give another proof of the drinker
using dn in the first step and then yet another time *)
Theorem drinker2 : exists x:D, (drinks x) -> (forall y:D, drinks y).
Proof.
apply dn.
intro.
(*assert (forall x:D, ~(drinks x -> forall y:D, drinks y)).*)
assert (forall x:D, drinks x /\ ~(forall y:D, drinks y)).
intro x.
split.
assert (drinks x \/ ~drinks x).
apply em.
inversion_clear H0.
exact H1.
elim H.
exists x.
intro.
elimtype False.
apply H1.
exact H0.
intro.
apply H.
exists x.
intro.
exact H0.
elim H0 with d.
intro.
intro.
apply H2.
(* Coq accepts, but prover rejects 'apply H0' here *)
intro.
elim H0 with y.
intro.
intro.
exact H3.
Qed.
End drinker.
Section barber.
(* the barber's paradox:
it is not the case that
there is someone who shaves exactly everyone who does not shave himself *)
(* setting *)
Parameter V : Set.
Parameter v : V.
Parameter shaves : V -> V -> Prop.
(* the barber's paradox *)
(* exercise 6: prove the barber's paradox
use inversion twice,
and distinguish cases using em: x shaves himself or not *)
Theorem barber : ~ exists x : V ,
(forall y:V, (shaves x y -> ~ shaves y y))
/\
(forall y:V, (~ shaves y y -> shaves x y)).
Proof.
intro.
inversion_clear H.
inversion_clear H0.
assert (shaves x x \/ ~shaves x x).
apply em.
inversion_clear H0.
assert (~shaves x x).
apply H.
exact H2.
apply H0.
exact H2.
assert (shaves x x).
apply H1.
exact H2.
apply H2.
exact H0.
Qed.
(* possible additional exercise:
prove the more elegant formulation of the barber's paradox
with the forall inside the /\ *)
Theorem barber2 : ~exists x:V,
(forall y:V, (shaves x y -> ~shaves y y) /\ (~shaves y y -> shaves x y)).
Proof.
intro.
inversion_clear H.
assert (shaves x x \/ ~shaves x x).
apply em.
inversion_clear H.
assert (~shaves x x).
apply H0.
exact H1.
contradiction.
assert (shaves x x).
apply H0.
exact H1.
contradiction.
Qed.
(* version accepted by the prover: *)
Theorem barber3 : ~exists x:V,
(forall y:V, (shaves x y -> ~shaves y y) /\ (~shaves y y -> shaves x y)).
Proof.
intro.
inversion_clear H.
elim H0 with x.
intro.
intro.
assert (shaves x x \/ ~shaves x x).
apply em.
inversion_clear H2.
apply H. exact H3. exact H3.
apply H3. apply H1. exact H3.
Qed.
End barber.
|
