-
Notifications
You must be signed in to change notification settings - Fork 0
/
sample.v
147 lines (111 loc) · 2.88 KB
/
sample.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
Inductive day : Type :=
| monday
| tuesday
| wednesday
| thursday
| friday
| saturday
| sunday.
Definition next_weekday (d:day) : day :=
match d with
| monday => tuesday
| tuesday => wednesday
| wednesday => thursday
| thursday => friday
| friday => monday
| saturday => monday
| sunday => monday
end.
(* Compute (next_weekday friday). *)
Example test_next_weekday:
(next_weekday (next_weekday saturday)) = tuesday.
Proof. simpl. reflexivity. Qed.
Check monday.
Inductive bool : Type :=
| true
| false.
Definition nandb (b1:bool) (b2:bool) : bool :=
match b1, b2 with
| true, true => false
| true, false => true
| false, false => true
| false, true => 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 (b1:bool) (b2:bool) (b3:bool) : bool :=
match (b1, b2, b3) 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 andb3.
Module TuplePlayground.
Inductive bit : Type :=
| B0
| B1.
Inductive nybble : Type :=
| bits (b0 b1 b2 b3 : bit).
Check (bits B1 B0 B1 B0)
: nybble.
End TuplePlayground.
Check (S (S (S (S 0)))).
Fixpoint factorial (n:nat) : nat :=
match n with
| 0 => 1
| S x => mult n (factorial x)
end.
Example test_factorial1: (factorial 3) = 6.
Proof. simpl. reflexivity. Qed.
Example test_factorial2: (factorial 5) = (mult 10 12).
Proof. simpl. reflexivity. Qed.
Notation "x + y" := (plus x y)
(at level 50, left associativity)
: nat_scope.
Theorem plus_0_n : forall n: nat, 0 + n = n.
Proof.
intros n. simpl. 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 H.
intros H0.
rewrite -> H.
rewrite -> H0.
reflexivity.
Qed.
Check plus_id_exercise.
Notation "x * y" := (mult x y)
(at level 40, left associativity)
: nat_scope.
Theorem mult_0_l : forall n:nat, 0 * n = 0.
Proof.
intros n. simpl. reflexivity. Qed.
Theorem mult_n_0_m_0 : forall p q : nat,
(p * 0) + (q * 0) = 0.
Proof.
intros p q.
rewrite <- mult_n_O.
rewrite <- mult_n_O.
reflexivity. Qed.
Theorem mult_n_1 : forall p : nat, p * 1 = p.
Proof.
intros p.
rewrite <- mult_n_Sm.
rewrite <- mult_n_O.
reflexivity.
Qed.