Mercurial > cpdt > repo
comparison src/InductiveTypes.v @ 29:add8215ec72a
nat lists and trees
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Mon, 08 Sep 2008 15:23:04 -0400 |
| parents | 0543bbd62843 |
| children | 4887ddb1ad23 |
comparison
equal
deleted
inserted
replaced
| 28:0543bbd62843 | 29:add8215ec72a |
|---|---|
| 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 ]] *) |