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
226
227
228
229
230
231
232
233
|
(* ************************************************************** *)
Section pred1.
Variable Terms : Set.
Variable M : Terms.
(* predicates *)
Variable A : Prop.
Variable P : Terms -> Prop.
Variable Q : Terms -> Prop.
Variable R : Terms -> Terms -> Prop.
(* example *)
Theorem example0 : (forall x:Terms, (P x)) -> (P M).
Proof.
intro u.
apply u.
Qed.
Print example0.
(* \u: Pi x:Terms. Px. (u M) *)
(* example *)
Theorem example1 : forall x:Terms, (P x) -> (forall y:Terms, (P y) -> A) -> A.
Proof.
intro x.
intro h.
intro i.
apply i with x.
assumption.
Qed.
Print example1.
(* \x:Terms. \h:(P x). \i:(Pi y:Terms. Py -> A). (i x h) *)
(* example, see slide 35 of week 6 *)
Theorem example2 :
(forall x : Terms , P x -> Q x)
->
(forall x : Terms , P x)
->
forall y : Terms , Q y.
Proof.
intro h.
intro i.
intro y.
apply h.
apply i.
Qed.
Print example2.
(* \h: (Pi x:Terms. Px -> Qx). \i: (Pi x:Terms Px). \y: Terms. h y (i y) *)
(* exercise 1: prove the lemma and inspect the proof term *)
Lemma one : (forall x : Terms, P x) -> P M.
Proof.
intro H.
apply H.
Qed.
Print one.
(* exercise 2: prove the lemma and inspect the proof term *)
Lemma two : (A -> forall x : Terms, P x) -> forall y : Terms, A -> P y.
Proof.
intros H y HA.
apply H.
assumption.
Qed.
Print two.
(* exercise 3: prove the lemma and inspect the proof term *)
Lemma three : A -> forall x : Terms, A.
Proof.
intros H _.
exact H.
Qed.
Print three.
(* example, see slides 13-14-15 of week 7 *)
Definition AS :=
forall x y : Terms, (R x y) -> ~(R y x).
Definition IR :=
forall x:Terms, ~(R x x).
Theorem AS_implies_IR : AS -> IR.
Proof.
unfold AS.
unfold IR.
intro h.
intro x.
intro i.
apply h with x x.
(* alternative: apply (h x x ) *)
exact i.
exact i.
Qed.
Print AS_implies_IR.
(* given *)
Definition reflif := forall x : Terms, (exists y : Terms, R x y) -> R x x.
(* exercise 4:
define sym as the proposition stating that
R is symmetric, that is,
if x and y are related via R, then y and x are related via R *)
Definition sym := forall x y : Terms, R x y -> R y x.
(* exercise 5:
define trans as the proposition stating that
R is transitive, that is,
if x and y are related via R, and y and z are related via R,
then x and z are related via R *)
Definition trans := forall x y z : Terms, R x y /\ R y z -> R x z.
(* exercise 6: prove the following Lemma *)
Lemma str : sym -> trans -> reflif.
Proof.
unfold sym.
unfold trans.
unfold reflif.
intros Hsym Htrans x Hy.
inversion Hy.
apply Htrans with x0.
split.
assumption.
apply Hsym.
assumption.
Qed.
End pred1.
(* ************************************************************** *)
Section logical_framework.
(* we encode propositional logic
source: webpage Herman Geuvers
handbook article Henk Barendregt *)
(* prop representing the propositions is declared as a Set *)
Parameter prop : Set.
(* implication on prop is a binary operator *)
Parameter imp : prop -> prop -> prop.
(* we can use infix notation => for imp *)
Infix "=>" := imp (right associativity, at level 85).
(* T expresses if a proposion in prop is valid
if (T p) is inhabited then p is valid
if (T p) is not inhabited then p is not valid *)
Parameter T : prop -> Prop.
(* the variable imp_introduction models the introduction rule for imp *)
Parameter imp_introduction : forall p q : prop, (T p -> T q) -> T (p => q).
(* the variable imp_elimination models the elimination rule for imp *)
Parameter imp_elimination : forall p q : prop, T (p => q) -> T p -> T q.
(* exercise 7 : prove the following lemma *)
Lemma I : forall p : prop, T (p => p).
Proof.
intro p.
apply imp_introduction.
intro.
assumption.
Qed.
(* exercise 8 : prove the following lemma *)
Lemma transitivity :
forall p q r : prop, T (p => q) -> T (q => r) -> T (p => r).
Proof.
intros p q r.
intros H1 H2.
apply imp_introduction.
intro H3.
apply imp_elimination with q.
assumption.
apply imp_elimination with p ; assumption.
Qed.
Parameter conjunction : prop -> prop -> prop.
Infix "X" := conjunction (no associativity, at level 90).
(* exercise 9 : define variables that model the introduction
rule for conjuction on prop, and both elimination rules *)
Parameter conjunction_introduction : forall p q : prop, T p -> T q -> T (p X q).
Parameter conjunction_elimination_l : forall p q : prop, T (p X q) -> T p.
Parameter conjunction_elimination_r : forall p q : prop, T (p X q) -> T q.
(* exercise 10: prove the following lemma *)
Lemma weak : forall a b c : prop, T (a => c) -> T ((a X b) => c).
Proof.
intros a b c.
intro.
apply imp_introduction.
intro.
apply imp_elimination with a.
assumption.
apply conjunction_elimination_l with b.
assumption.
Qed.
(* the remainder is not obligatory *)
(* bot represents falsum in prop *)
Parameter bot : prop.
(* not represents negation in prop *)
Definition not (p : prop) := p => bot.
(* not obligatory *)
(* exercise 11 : prove the following lemma *)
Lemma contrapositive : forall p q : prop, T (p => q) -> T (not q => not p).
Proof.
intros p q.
intro.
unfold not.
apply imp_introduction.
intro.
apply imp_introduction.
intro.
apply imp_elimination with q.
assumption.
apply imp_elimination with p ; assumption.
Qed.
End logical_framework.
|
