gdritter repos software-foundations / efead46
finished exercises Getty Ritter 7 years ago
1 changed file(s) with 178 addition(s) and 5 deletion(s). Collapse all Expand all
+178
-5
01-basics.v less more
1 Inductive bool : Type :=
2 | true : bool
3 | false : bool.
4
51 (* exercise nandb *)
62
73 Definition nandb (b1 : bool) (b2 : bool) : bool :=
5551
5652 (* exercise blt_nat *)
5753
58 Definition blt_nat (n m : nat) : bool. Admitted.⏎
54 Definition blt_nat (n m : nat) : bool :=
55 match m - n with
56 | 0 => false
57 | S _ => true
58 end.
59
60 Example test_blt_nat1: (blt_nat 2 2) = false.
61 Proof. simpl. reflexivity. Qed.
62 Example test_blt_nat2: (blt_nat 2 4) = true.
63 Proof. simpl. reflexivity. Qed.
64 Example test_blt_nat3: (blt_nat 4 2) = false.
65 Proof. simpl. reflexivity. Qed.
66
67 (* exercise plus_id_exercise *)
68
69 Theorem plus_id_exercise : forall n m o : nat,
70 n = m -> m = o -> n + m = m + o.
71 Proof.
72 intros n m o.
73 intros H1 H2.
74 rewrite -> H1.
75 rewrite -> H2.
76 reflexivity.
77 Qed.
78
79 (* exercise mult_S_1 *)
80
81 Theorem plus_1_l : forall n : nat, 1 + n = S n.
82 Proof. intros n. simpl. reflexivity. Qed.
83
84 Theorem mult_S_1 : forall n m : nat,
85 m = S n ->
86 m * (1 + n) = m * m.
87 Proof.
88 intros n m H.
89 rewrite plus_1_l.
90 rewrite H.
91 reflexivity.
92 Qed.
93
94 (* exercise andb_true_elim2 *)
95
96 Definition andb (b1:bool) (b2:bool) : bool :=
97 match b1 with
98 | true => b2
99 | false => false
100 end.
101
102 Theorem andb_true_elim2 : forall b c : bool,
103 andb b c = true -> c = true.
104 Proof.
105 intros b c.
106 destruct b.
107 - destruct c.
108 + reflexivity.
109 + simpl. intros H. rewrite -> H. reflexivity.
110 - destruct c.
111 + reflexivity.
112 + simpl. intros H. rewrite -> H. reflexivity.
113 Qed.
114
115 (* exercise zero_nbeq_plus_1 *)
116
117 Fixpoint beq_nat (n m : nat) : bool :=
118 match n with
119 | O => match m with
120 | O => true
121 | S m' => false
122 end
123 | S n' => match m with
124 | O => false
125 | S m' => beq_nat n' m'
126 end
127 end.
128
129 Theorem zero_nbeq_plus_1 : forall n : nat,
130 beq_nat 0 (n + 1) = false.
131 Proof.
132 intros [|n].
133 reflexivity.
134 reflexivity.
135 Qed.
136
137 (* exercise boolean functions *)
138
139 Theorem identity_fn_applied_twice :
140 forall (f : bool -> bool),
141 (forall (x: bool), f x = x) ->
142 forall (b : bool), f (f b) = b.
143 Proof.
144 intros id id_idem b.
145 rewrite id_idem. rewrite id_idem. reflexivity.
146 Qed.
147
148 (* exercise and_eq_orb *)
149
150 Lemma andb_comm : forall b c : bool, andb b c = andb c b.
151 Proof.
152 intros [] [].
153 - reflexivity.
154 - reflexivity.
155 - reflexivity.
156 - reflexivity.
157 Qed.
158
159 Lemma andb_l_false : forall b : bool, andb false b = false.
160 Proof.
161 intros [].
162 - reflexivity.
163 - reflexivity.
164 Qed.
165
166 Lemma orb_comm : forall b c : bool, orb b c = orb c b.
167 Proof.
168 intros [] [].
169 - reflexivity.
170 - reflexivity.
171 - reflexivity.
172 - reflexivity.
173 Qed.
174
175 Lemma orb_l_true : forall b : bool, orb true b = true.
176 Proof.
177 intros [].
178 - reflexivity.
179 - reflexivity.
180 Qed.
181
182 Theorem andb_eq_orb :
183 forall (b c : bool),
184 (andb b c = orb b c) ->
185 b = c.
186 Proof.
187 intros b c.
188 destruct b.
189 - destruct c.
190 + reflexivity.
191 + rewrite -> andb_comm. rewrite -> andb_l_false.
192 rewrite -> orb_l_true.
193 intros H. rewrite -> H. reflexivity.
194 - destruct c.
195 + rewrite -> andb_l_false.
196 rewrite -> orb_comm. rewrite -> orb_l_true.
197 intros H. rewrite -> H. reflexivity.
198 + reflexivity.
199 Qed.
200
201 (* exercise binary *)
202
203 Inductive bin : Type :=
204 | Z : bin
205 | DB : bin -> bin
206 | DI : bin -> bin.
207
208 Fixpoint incr (b : bin) : bin :=
209 match b with
210 | Z => DI Z
211 | DB x => DI x
212 | DI x => DB (incr x)
213 end.
214
215 Fixpoint bin_to_nat (b : bin) : nat :=
216 match b with
217 | Z => 0
218 | DB x => 2 * bin_to_nat x
219 | DI x => 1 + (2 * bin_to_nat x)
220 end.
221
222 Example text_bin_incr1: bin_to_nat (incr Z) = S (bin_to_nat Z).
223 reflexivity. Qed.
224 Example text_bin_incr2: bin_to_nat (incr (DI Z)) = S (bin_to_nat (DI Z)).
225 reflexivity. Qed.
226 Example text_bin_incr3: bin_to_nat (incr (DB Z)) = S (bin_to_nat (DB Z)).
227 reflexivity. Qed.
228 Example text_bin_incr4: bin_to_nat (incr (DI (DI Z))) = S (bin_to_nat (DI (DI Z))).
229 reflexivity. Qed.
230 Example text_bin_incr5: bin_to_nat (incr (DB (DI Z))) = S (bin_to_nat (DB (DI Z))).
231 reflexivity. Qed.