Mercurial > cpdt > repo

comparison src/Large.v @ 491:da576746c3ba

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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