Mercurial > cpdt > repo
comparison src/Large.v @ 491:da576746c3ba
Fix one reported grammatical error and make my own final pass over Chapter 1
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Fri, 18 Jan 2013 13:45:00 -0500 |
parents | 1fd4109f7b31 |
children | 21079e42b773 |
comparison
equal
deleted
inserted
replaced
490:c8a3cb24bae9 | 491:da576746c3ba |
---|---|
215 eval (times k e) = k * eval e. | 215 eval (times k e) = k * eval e. |
216 induction e; crush. | 216 induction e; crush. |
217 Qed. | 217 Qed. |
218 (* end thide *) | 218 (* end thide *) |
219 | 219 |
220 (** This style is motivated by a hard truth: one person's manual proof script is almost always mostly inscrutable to most everyone else. I claim that step-by-step formal proofs are a poor way of conveying information. Thus, we had might as well cut out the steps and automate as much as possible. | 220 (** This style is motivated by a hard truth: one person's manual proof script is almost always mostly inscrutable to most everyone else. I claim that step-by-step formal proofs are a poor way of conveying information. Thus, we might as well cut out the steps and automate as much as possible. |
221 | 221 |
222 What about the illustrative value of proofs? Most informal proofs are read to convey the big ideas of proofs. How can reading [induction e; crush] convey any big ideas? My position is that any ideas that standard automation can find are not very big after all, and the _real_ big ideas should be expressed through lemmas that are added as hints. | 222 What about the illustrative value of proofs? Most informal proofs are read to convey the big ideas of proofs. How can reading [induction e; crush] convey any big ideas? My position is that any ideas that standard automation can find are not very big after all, and the _real_ big ideas should be expressed through lemmas that are added as hints. |
223 | 223 |
224 An example should help illustrate what I mean. Consider this function, which rewrites an expression using associativity of addition and multiplication. *) | 224 An example should help illustrate what I mean. Consider this function, which rewrites an expression using associativity of addition and multiplication. *) |
225 | 225 |