forked from tabtab777/Coq
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathBasic.v
370 lines (291 loc) · 8.69 KB
/
Basic.v
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
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
Inductive day : Type :=
| monday : day
| tuesday : day
| wednesday : day
| thursday : day
| friday : day
| saturday : day
| sunday : day.
Definition next_weekday ( d : day ) : day :=
match d with
| monday => tuesday
| tuesday => wednesday
| wednesday => thursday
| thursday => friday
| friday => monday
| saturday => monday
| sunday => monday
end.
Eval compute in ( next_weekday friday ).
Eval compute in ( next_weekday ( next_weekday friday )).
Example test_next_weekday :
( next_weekday ( next_weekday saturday )) = tuesday.
Proof. simpl. reflexivity. Qed.
Inductive bool : Type :=
| true : bool
| false : bool.
Definition negb ( b : bool ) : bool :=
match b with
| true => false
| false => true
end.
Definition andb ( x : bool ) ( y : bool ) : bool :=
match x with
| true => y
| false => false
end.
Definition orb ( x : bool ) ( y : bool ) : bool :=
match x with
| false => y
| true => true
end.
Example test_orb1 : ( orb true false ) = true.
Proof. simpl. reflexivity. Qed.
Example test_orb2 : ( orb false false ) = false.
Proof. simpl. reflexivity. Qed.
Definition nandb ( x : bool ) ( y : bool ) : bool :=
match ( x, y ) with
| ( true, true ) => false
| ( _, _ ) => true
end.
Example test_nandb1: (nandb true false) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb2: (nandb false false) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb3: (nandb false true) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb4: (nandb true true) = false.
Proof. simpl. reflexivity. Qed.
Definition andb3 ( x : bool ) ( y : bool ) ( z : bool ) : bool :=
match ( x, y, z ) with
| ( true, true, true ) => true
| ( _, _, _ ) => false
end.
Example test_andb31: (andb3 true true true) = true.
Proof. simpl. reflexivity. Qed.
Example test_andb32: (andb3 false true true) = false.
Proof. simpl. reflexivity. Qed.
Example test_andb33: (andb3 true false true) = false.
Proof. simpl. reflexivity. Qed.
Example test_andb34: (andb3 true true false) = false.
Proof. simpl. reflexivity. Qed.
Check true.
Check ( negb false ).
Check andb3.
Definition xorb ( x : bool ) ( y : bool ) : bool :=
match x, y with
| true, true => false
| false, false => false
| _, _ => true
end.
Theorem xorb_equal : forall a : bool, xorb a a = false.
Proof.
intros a. destruct a as [ | ].
reflexivity. reflexivity.
Qed.
Theorem xorb_equalleft : forall a b : bool, xorb a b = false -> a = b.
Proof.
intros a b H. destruct a. destruct b.
reflexivity. discriminate.
destruct b. discriminate. reflexivity.
Qed.
(*
Theorem xorb_notequal : forall a b : bool, xorb a b = true -> a <> b.
Proof.
intros a b H.
destruct a. destruct b.
discriminate.
rewrite <- H.
*)
Module Playground1.
Inductive nat : Type :=
| O : nat
| S : nat -> nat.
Definition pred ( n : nat ) : nat :=
match n with
| O => O
| S m => m
end.
End Playground1.
Definition minustwo ( n : nat ) : nat :=
match n with
| O => O
| S O => O
| S ( S m ) => m
end.
Check (S (S (S (S O)))).
Eval simpl in ( minustwo 4 ).
Check S.
Check pred.
Check minustwo.
Fixpoint evenb ( n : nat ) : bool :=
match n with
| O => true
| S O => false
| S ( S n' ) => evenb n'
end.
Definition oddb ( n : nat ) : bool :=
negb ( evenb n ).
Example test_oddb1: (oddb ( S ( S (S O ) ) ) ) = true.
Proof. simpl. reflexivity. Qed.
Module Playground2.
Fixpoint plus ( n : nat ) ( m : nat ) : nat :=
match n with
| O => m
| S n' => S ( plus n' m )
end.
Eval compute in plus ( S O ) ( S ( S O ) ).
Example plus_test : ( plus 3 4 ) = 7.
Proof. simpl. reflexivity. Qed.
(*
Example plus_comm : forall m n p : nat, plus m ( plus n p ) = plus ( plus m n ) p.
Proof.
intros m n p.
destruct m as [ | ].
reflexivity.
simpl.
Admitted.
*)
Fixpoint mult ( m n : nat ) : nat :=
match m with
| O => O
| S m' => plus ( mult m' n ) n
end.
Eval compute in mult 4 9.
Example test_mult : ( mult 3 3 ) = 9.
Proof. simpl. reflexivity. Qed.
Fixpoint minus ( n m : nat ) : nat :=
match n, m with
| O, _ => O
| S _, O => n
| S n', S m' => minus n' m'
end.
End Playground2.
Fixpoint exp ( base power : nat ) : nat :=
match power with
| O => S O
| S p => mult base ( exp base p )
end.
Fixpoint factorial ( n : nat ) : nat :=
match n with
| O => S O
| S n' => mult n ( factorial n' )
end.
Example test_factorial1: (factorial 3) = 6.
Proof. simpl. reflexivity. Qed.
(*
Notation "x + y" := ( plus x y ) ( at level 50, left associativity) : nat_scope.
Notation "x - y" := ( minus x y ) ( at level 50, left associativity) : nat_scope.
Notation "x * y" := ( mult x y ) ( at level 40, left associativity) : nat_scope.
Notation "x ^ y" := ( exp x y ) ( at level 30, right associativity) : nat_scope.
Eval simpl in 2^2^3.
*)
Check ( 10 + 1 + 2 ).
Check (( 0 + 1 ) + 1 ).
Fixpoint beq_nat ( n m : nat ) : bool :=
match n with
| O => match m with
| O => true
| S _ => false
end
| S n' => match m with
| O => false
| S m' => beq_nat n' m'
end
end.
Fixpoint ble_nat ( n m : nat ) : bool :=
match n with
| O => true
| S n' => match m with
| O => false
| S m' => ble_nat n' m'
end
end.
Example test_ble_nat1: (ble_nat 2 2) = true.
Proof. reflexivity. Qed.
Example test_ble_nat2: (ble_nat 2 4) = true.
Proof. reflexivity. Qed.
Example test_ble_nat3: (ble_nat 4 2) = false.
Proof. reflexivity. Qed.
Definition blt_nat ( n m : nat ) : bool :=
andb ( ble_nat n m ) ( negb ( beq_nat n m ) ).
Example test_blt_nat1 : ( blt_nat 3 3 ) = false.
Proof. simpl. reflexivity. Qed.
Example test_blt_nat2 : ( blt_nat 3 4 ) = true.
Proof. simpl. reflexivity. Qed.
Example test_blt_nat3: (blt_nat 2 2) = false.
Proof. simpl. reflexivity. Qed.
Example test_blt_nat4: (blt_nat 2 4) = true.
Proof. simpl. reflexivity. Qed.
Example test_blt_nat5: (blt_nat 4 2) = false.
Proof. simpl. reflexivity. Qed.
Theorem plus_O_n : forall n : nat, O + n = n.
Proof. intros n. reflexivity. Qed.
Theorem plus_1_n : forall n : nat, 1 + n = S n.
Proof. intros. reflexivity. Qed.
Theorem mult_O_n : forall n : nat, O * n = O.
Proof. intros. reflexivity. Qed.
Theorem plus_id_example : forall m n : nat, m = n -> n + n = m + m.
Proof. intros n m. intros H. rewrite -> H.
reflexivity. Qed.
Theorem plus_id_exercise : forall n m o : nat,
n = m -> m = o -> n + m = m + o.
Proof. intros n m o. intros H1 H2.
rewrite -> H1. rewrite -> H2.
reflexivity. Qed.
Theorem plus_id_exercise2 : forall n m o : nat,
n = m -> n + o = m + o.
Proof. intros n m o. intros H. rewrite -> H. reflexivity. Qed.
Theorem mult_O_plus : forall m n : nat, ( O + n ) * m = n * m.
Proof. intros m n. rewrite -> plus_O_n. reflexivity. Qed.
(*
Theorem mult_comm : forall m n : nat, m * n = n * m.
Proof. Admitted.
*)
Theorem mult_S_1 : forall m n : nat, m = S n -> m * ( 1 + n ) = m * m.
Proof. intros m n. intros H. rewrite -> H. reflexivity. Qed.
Theorem plus_1_neq_0_firsttry : forall n : nat, beq_nat (n + 1) 0 = false.
Proof. intros n. destruct n as [ | n']. reflexivity.
reflexivity. Qed.
Theorem negb_involuted : forall b : bool, negb ( negb b ) = b.
Proof. intros b. destruct b. reflexivity.
reflexivity. Qed.
Theorem zero_nbeq_plus_1 : forall n : nat, beq_nat 0 ( n + 1 ) = false.
Proof. intros n. destruct n as [ | n' ]. reflexivity.
reflexivity. Qed.
Theorem identity_fn_applied_twice : forall ( f : bool -> bool ),
( forall (x : bool), f x = x ) ->
forall (b : bool), f ( f b ) = b.
Proof. intros f H b. rewrite -> H. rewrite -> H. reflexivity. Qed.
Theorem negation_fn_applied_twice : forall (f : bool -> bool),
( forall (x : bool), f x = negb x ) ->
forall (b : bool), f (f b) = b.
Proof. intros f H b. rewrite -> H. rewrite -> H. destruct b.
reflexivity. reflexivity. Qed.
Theorem andb_eq_orb_rev : forall (b c : bool), b = c -> (andb b c = orb b c).
Proof. intros b c H. rewrite -> H. destruct c. reflexivity. reflexivity. Qed.
Theorem andb_eq_orb_rev1 : forall (b c : bool), b = c -> (orb b c = orb b c).
Proof. intros b c H. rewrite -> H. destruct c. reflexivity. reflexivity. Qed.
Theorem andb_eq_orb : forall ( a b : bool ), ( andb a b = orb a b ) -> a = b.
Proof.
intros a b. destruct a as [ false | true ].
simpl. intros H1. rewrite -> H1. reflexivity.
simpl. intros H2. rewrite -> H2. reflexivity.
Qed.
Inductive bin : Type :=
| O' : bin
| Twice : bin -> bin
| DPlusOne : bin -> bin.
Fixpoint inc ( b : bin ) : bin :=
match b with
| O' => DPlusOne O'
| Twice b' => DPlusOne b'
| DPlusOne b' => Twice ( inc b' )
end.
Fixpoint bintonat ( b : bin ) : nat :=
match b with
| O' => O
| Twice b' => plus ( bintonat b' ) ( bintonat b')
| DPlusOne b' => plus 1 ( plus ( bintonat b' ) ( bintonat b') )
end.
Eval compute in bintonat ( Twice ( DPlusOne ( DPlusOne O' ) )).