Mercurial > cpdt > repo
comparison src/InductiveTypes.v @ 40:02e8e9ef2746
Spell check
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sat, 13 Sep 2008 08:58:48 -0400 |
| parents | fd18331e5c0b |
| children | d45ba7e9b266 |
comparison
equal
deleted
inserted
replaced
| 39:fd18331e5c0b | 40:02e8e9ef2746 |
|---|---|
| 1012 induction tr1 using nat_tree_ind'; crush. | 1012 induction tr1 using nat_tree_ind'; crush. |
| 1013 Qed. | 1013 Qed. |
| 1014 | 1014 |
| 1015 (** We will go into great detail on hints in a later chapter, but the only important thing to note here is that we register a pattern that describes a conclusion we expect to encounter during the proof. The pattern may contain unification variables, whose names are prefixed with question marks, and we may refer to those bound variables in a tactic that we ask to have run whenever the pattern matches. | 1015 (** We will go into great detail on hints in a later chapter, but the only important thing to note here is that we register a pattern that describes a conclusion we expect to encounter during the proof. The pattern may contain unification variables, whose names are prefixed with question marks, and we may refer to those bound variables in a tactic that we ask to have run whenever the pattern matches. |
| 1016 | 1016 |
| 1017 The advantage of using the hint is not very clear here, because the original proof was so short. However, the hint has fundamentally improved the readability of our proof. Before, the proof refered to the local variable [ls], which has an automatically-generated name. To a human reading the proof script without stepping through it interactively, it was not clear where [ls] came from. The hint explains to the reader the process for choosing which variables to case analyze on, and the hint can continue working even if the rest of the proof structure changes significantly. *) | 1017 The advantage of using the hint is not very clear here, because the original proof was so short. However, the hint has fundamentally improved the readability of our proof. Before, the proof referred to the local variable [ls], which has an automatically-generated name. To a human reading the proof script without stepping through it interactively, it was not clear where [ls] came from. The hint explains to the reader the process for choosing which variables to case analyze on, and the hint can continue working even if the rest of the proof structure changes significantly. *) |
| 1018 | 1018 |
| 1019 | 1019 |
| 1020 (** * Manual Proofs About Constructors *) | 1020 (** * Manual Proofs About Constructors *) |
| 1021 | 1021 |
| 1022 (** It can be useful to understand how tactics like [discriminate] and [injection] work, so it is worth stepping through a manual proof of each kind. We will start with a proof fit for [discriminate]. *) | 1022 (** It can be useful to understand how tactics like [discriminate] and [injection] work, so it is worth stepping through a manual proof of each kind. We will start with a proof fit for [discriminate]. *) |