-
Notifications
You must be signed in to change notification settings - Fork 0
/
#dayexample.v#
125 lines (108 loc) · 1.99 KB
/
#dayexample.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
Inductive day : Type :=
| sun : day
| mon : day
| tue : day
| wed : day
| thu : day
| fri : day
| sat : day.
Let next_day d :=
match d with
| sun => mon
| mon => tue
| tue => wed
| wed => thu
| thu => fri
| fri => sat
| sat => sun
end.
Definition prev_day d :=
match d with
| sun => sat
| mon => sun
| tue => mon
| wed => tue
| thu => wed
| fri => thu
| sat => fri
end.
Theorem wed_after_tue : next_day tue = wed.
Proof.
auto.
Qed.
Theorem wed_after_tue' : next_day tue = wed.
Proof.
simpl. trivial.
Qed.
Theorem day_never_repeats : forall d : day, next_day d <> d.
Proof.
intros d. destruct d.
all: discriminate.
Qed.
Theorem day_never_repeats'' : forall d : day, next_day d <> d.
Proof.
intros d. destruct d; discriminate.
Qed.
Theorem mon_preceds_tues : forall d : day,
next_day d = tue -> d = mon.
Proof.
intros d next_day_is_tue.
destruct d.
all: discriminate || trivial.
Qed.
Definition negb (b:bool) : bool :=
match b with
| true => false
| false => true
end.
Definition nandb (b1:bool) (b2:bool) : bool :=
match b1 with
| true => negb b2
| false => true
end.
Example test_nandb1: (nandb true false) = true.
Proof.
simpl.
reflexivity.
Qed.
Example test_nandb2: (nandb true true) = false.
Proof.
simpl.
reflexivity.
Qed.
Example test_nandb3: (nandb false false) = true.
Proof.
simpl.
reflexivity.
Qed.
Example test_nandb4: (nandb false true) = true.
Proof.
simpl.
reflexivity.
Qed.
Definition andb3 (b1:bool) (b2:bool) (b3:bool) : bool :=
match b1 , b2 with
| true , true => b3
| _ , _ => false
end.
Example test_andb1: (andb3 true true true) = true.
Proof.
simpl.
reflexivity.
Qed.
Example test_andb2: (andb3 true true false) = false.
Proof.
simpl.
reflexivity.
Qed.
Example test_andb3: (andb3 false false true) = false.
Proof.
simpl.
reflexivity.
Qed.
Example test_andb4: (andb3 false true true) = false.
Proof.
simpl.
reflexivity.
Qed.
(*Some more tests are there. A total of 8 tests --- skipping that for time being*)