## Mercurial > cpdt > repo

### comparison src/InductiveTypes.v @ 29:add8215ec72a

Find changesets by keywords (author, files, the commit message), revision
number or hash, or revset expression.

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 ]] *) |