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
|
(* cf antwoorden voor laatste opgave *)
Section proplogic.
Parameters A B C : Prop.
(* exercise 1 *)
(* complete the following simply typed lambda terms *)
Definition prop1 := (*! term *)
(* fun (x : ?) (y : ?) (z : ?) => x z (y z). *)
.
Definition prop2 := (*! term *)
(* fun (x : ?) (y : ?) (z : ?) => x (y z) z. *)
.
Definition prop3 := (*! term *)
(* fun (x : ?) (y : ?) => x (fun z : A => y) y. *)
.
Definition prop4 := (*! term *)
(* fun (x : ?) (y : ?) (z : ?) => x (y x) (z x). *)
.
End proplogic.
Section deptypes.
(* exercise 2 *)
(* complete the following dependently typed lambda terms *)
Definition pred1 := (*! term *)
(* fun (l : Set -> Set) (A : ?) (B : ?) (f : l A -> l B) (x : ?) => f x. *)
.
Definition pred2 := (*! term *)
(* fun (e : nat -> nat -> ?) (n : ?) => forall m : ?, 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 *)
Lemma aux : (~ forall x:D, drinks x) -> (exists x:D, ~drinks x).
Proof.
(*! proof *)
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.
(*! proof *)
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.
(*! proof *)
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.
(*! proof *)
Qed.
(* possible additional exercise:
prove the more elegant formulation of the barber's paradox
with the forall inside the /\ *)
Theorem barber2 : (*! term *)
.
Proof.
(*! proof *)
Qed.
End barber.
|
