Mercurial > cpdt > repo
comparison src/InductiveTypes.v @ 417:539ed97750bb
Update for Coq trunk version intended for final 8.4 release
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Tue, 17 Jul 2012 16:37:58 -0400 |
| parents | d27c0be2c3d4 |
| children | 686cf945dd02 |
comparison
equal
deleted
inserted
replaced
| 416:ded318830bb0 | 417:539ed97750bb |
|---|---|
| 340 Qed. | 340 Qed. |
| 341 (* end thide *) | 341 (* end thide *) |
| 342 | 342 |
| 343 (** The [injection] tactic 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. | 343 (** The [injection] tactic 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. |
| 344 | 344 |
| 345 There is also a very useful tactic called %\index{tactics!congruence}%[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%\index{theory of equality and uninterpreted functions}% _complete decision procedure for the theory of equality and uninterpreted functions_, plus some smarts about inductive types. | 345 There is also a very useful tactic called %\index{tactics!congruence}%[congruence] that can prove this theorem immediately. The [congruence] tactic 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%\index{theory of equality and uninterpreted functions}% _complete decision procedure for the theory of equality and uninterpreted functions_, plus some smarts about inductive types. |
| 346 | 346 |
| 347 %\medskip% | 347 %\medskip% |
| 348 | 348 |
| 349 We can define a type of lists of natural numbers. *) | 349 We can define a type of lists of natural numbers. *) |
| 350 | 350 |