nat lists and trees
comparison
equal inserted replaced
273 injection 1; trivial. 273 injection 1; trivial.
274 Qed. 274 Qed.
275 275
276 (** [injection] refers to a premise by number, adding new equalities between the corresponding arguments of equated terms that are formed with the same constructor. We end up needing to prove [n = m -> n = m], so it is unsurprising that a tactic named [trivial] is able to finish the proof. 276 (** [injection] refers to a premise by number, adding new equalities between the corresponding arguments of equated terms that are formed with the same constructor. We end up needing to prove [n = m -> n = m], so it is unsurprising that a tactic named [trivial] is able to finish the proof.
277 277
278 There is also a very useful tactic called [congruence] that can prove this theorem immediately. [congruence] generalizes [discriminate] and [injection], and it also adds reasoning about the general properties of equality, such as that a function returns equal results on equal arguments. That is, [congruence] is a %\textit{%#<i>#complete decision procedure for the theory of equality and uninterpreted functions#</i>#%}%, plus some smarts about inductive types. *) 278 There is also a very useful tactic called [congruence] that can prove this theorem immediately. [congruence] generalizes [discriminate] and [injection], and it also adds reasoning about the general properties of equality, such as that a function returns equal results on equal arguments. That is, [congruence] is a %\textit{%#<i>#complete decision procedure for the theory of equality and uninterpreted functions#</i>#%}%, plus some smarts about inductive types.
279
280 %\medskip%
281
282 We can define a type of lists of natural numbers. *)
283
284 Inductive nat_list : Set :=
285 | NNil : nat_list
286 | NCons : nat -> nat_list -> nat_list.
287
288 (** Recursive definitions are straightforward extensions of what we have seen before. *)
289
290 Fixpoint nlength (ls : nat_list) : nat :=
291 match ls with
292 | NNil => O
293 | NCons _ ls' => S (nlength ls')
294 end.
295
296 Fixpoint napp (ls1 ls2 : nat_list) {struct ls1} : nat_list :=
297 match ls1 with
298 | NNil => ls2
299 | NCons n ls1' => NCons n (napp ls1' ls2)
300 end.
301
302 (** Inductive theorem proving can again be automated quite effectively. *)
303
304 Theorem nlength_napp : forall ls1 ls2 : nat_list, nlength (napp ls1 ls2)
305 = plus (nlength ls1) (nlength ls2).
306 induction ls1; crush.
307 Qed.
308
309 Check nat_list_ind.
310 (** [[
311
312 nat_list_ind
313 : forall P : nat_list -> Prop,
314 P NNil ->
315 (forall (n : nat) (n0 : nat_list), P n0 -> P (NCons n n0)) ->
316 forall n : nat_list, P n
317 ]]
318
319 %\medskip%
320
321 In general, we can implement any "tree" types as inductive types. For example, here are binary trees of naturals. *)
322
323 Inductive nat_btree : Set :=
324 | NLeaf : nat_btree
325 | NNode : nat_btree -> nat -> nat_btree -> nat_btree.
326
327 Fixpoint nsize (tr : nat_btree) : nat :=
328 match tr with
329 | NLeaf => O
330 | NNode tr1 _ tr2 => plus (nsize tr1) (nsize tr2)
331 end.
332
333 Fixpoint nsplice (tr1 tr2 : nat_btree) {struct tr1} : nat_btree :=
334 match tr1 with
335 | NLeaf => tr2
336 | NNode tr1' n tr2' => NNode (nsplice tr1' tr2) n tr2'
337 end.
338
339 Theorem plus_assoc : forall n1 n2 n3 : nat, plus (plus n1 n2) n3 = plus n1 (plus n2 n3).
340 induction n1; crush.
341 Qed.
342
343 Theorem nsize_nsplice : forall tr1 tr2 : nat_btree, nsize (nsplice tr1 tr2)
344 = plus (nsize tr2) (nsize tr1).
345 Hint Rewrite n_plus_O plus_assoc : cpdt.
346
347 induction tr1; crush.
348 Qed.
349
350 Check nat_btree_ind.
351 (** [[
352
353 nat_btree_ind
354 : forall P : nat_btree -> Prop,
355 P NLeaf ->
356 (forall n : nat_btree,
357 P n -> forall (n0 : nat) (n1 : nat_btree), P n1 -> P (NNode n n0 n1)) ->
358 forall n : nat_btree, P n
359 ]] *)