## 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 |