## Mercurial > cpdt > repo

### comparison src/Large.v @ 509:21079e42b773

Find changesets by keywords (author, files, the commit message), revision
number or hash, or revset expression.

Pass through Chapter 16

author | Adam Chlipala <adam@chlipala.net> |
---|---|

date | Tue, 12 Feb 2013 11:14:52 -0500 |

parents | da576746c3ba |

children | ed829eaa91b2 |

comparison

equal
deleted
inserted
replaced

508:36428dfcde84 | 509:21079e42b773 |
---|---|

101 rewrite IHe2. | 101 rewrite IHe2. |

102 rewrite mult_plus_distr_l. | 102 rewrite mult_plus_distr_l. |

103 trivial. | 103 trivial. |

104 Qed. | 104 Qed. |

105 | 105 |

106 (** We pass %\index{tactics!induction}%[induction] an%\index{intro pattern}% _intro pattern_, using a [|] character to separate out instructions for the different inductive cases. Within a case, we write [?] to ask Coq to generate a name automatically, and we write an explicit name to assign that name to the corresponding new variable. It is apparent that, to use intro patterns to avoid proof brittleness, one needs to keep track of the seemingly unimportant facts of the orders in which variables are introduced. Thus, the script keeps working if we replace [e] by [x], but it has become more cluttered. Arguably, neither proof is particularly easy to follow. | 106 (** We pass %\index{tactics!induction}%[induction] an%\index{intro pattern}% _intro pattern_, using a [|] character to separate instructions for the different inductive cases. Within a case, we write [?] to ask Coq to generate a name automatically, and we write an explicit name to assign that name to the corresponding new variable. It is apparent that, to use intro patterns to avoid proof brittleness, one needs to keep track of the seemingly unimportant facts of the orders in which variables are introduced. Thus, the script keeps working if we replace [e] by [x], but it has become more cluttered. Arguably, neither proof is particularly easy to follow. |

107 | 107 |

108 That category of complaint has to do with understanding proofs as static artifacts. As with programming in general, with serious projects, it tends to be much more important to be able to support evolution of proofs as specifications change. Unstructured proofs like the above examples can be very hard to update in concert with theorem statements. For instance, consider how the last proof script plays out when we modify [times] to introduce a bug. *) | 108 That category of complaint has to do with understanding proofs as static artifacts. As with programming in general, with serious projects, it tends to be much more important to be able to support evolution of proofs as specifications change. Unstructured proofs like the above examples can be very hard to update in concert with theorem statements. For instance, consider how the last proof script plays out when we modify [times] to introduce a bug. *) |

109 | 109 |

110 Reset times. | 110 Reset times. |

111 | 111 |

154 induction e as [ | ? IHe1 ? IHe2 ]; [ | 154 induction e as [ | ? IHe1 ? IHe2 ]; [ |

155 trivial | 155 trivial |

156 | simpl; rewrite IHe1; rewrite IHe2; rewrite mult_plus_distr_l; trivial ]. | 156 | simpl; rewrite IHe1; rewrite IHe2; rewrite mult_plus_distr_l; trivial ]. |

157 Qed. | 157 Qed. |

158 | 158 |

159 (** We use the form of the semicolon operator that allows a different tactic to be specified for each generated subgoal. This is an improvement in robustness of the script. We no longer need to worry about tactics from one case being applied to a different case. Still, the proof script is not especially readable. Probably most readers would not find it helpful in explaining why the theorem is true. The same could be said for scripts which use the%\index{bullets}% _bullets_ or curly braces provided by Coq 8.4, which allow code like the above to be stepped through interactively, with periods in place of the semicolons, while representing proof structure in a way that is enforced by Coq. Interactive replay of scripts becomes easier, but readability is not really helped. | 159 (** We use the form of the semicolon operator that allows a different tactic to be specified for each generated subgoal. This change improves the robustness of the script: we no longer need to worry about tactics from one case being applied to a different case. Still, the proof script is not especially readable. Probably most readers would not find it helpful in explaining why the theorem is true. The same could be said for scripts using the%\index{bullets}% _bullets_ or curly braces provided by Coq 8.4, which allow code like the above to be stepped through interactively, with periods in place of the semicolons, while representing proof structure in a way that is enforced by Coq. Interactive replay of scripts becomes easier, but readability is not really helped. |

160 | 160 |

161 The situation gets worse in considering extensions to the theorem we want to prove. Let us add multiplication nodes to our [exp] type and see how the proof fares. *) | 161 The situation gets worse in considering extensions to the theorem we want to prove. Let us add multiplication nodes to our [exp] type and see how the proof fares. *) |

162 | 162 |

163 Reset exp. | 163 Reset exp. |

164 | 164 |

286 | 286 |

287 A competing alternative to the common style of Coq tactics is the%\index{declarative proof scripts}% _declarative_ style, most frequently associated today with the %\index{Isar}%Isar%~\cite{Isar}% language. A declarative proof script is very explicit about subgoal structure and introduction of local names, aiming for human readability. The coding of proof automation is taken to be outside the scope of the proof language, an assumption related to the idea that it is not worth building new automation for each serious theorem. I have shown in this book many examples of theorem-specific automation, which I believe is crucial for scaling to significant results. Declarative proof scripts make it easier to read scripts to modify them for theorem statement changes, but the alternate%\index{adaptive proof scripts}% _adaptive_ style from this book allows use of the _same_ scripts for many versions of a theorem. | 287 A competing alternative to the common style of Coq tactics is the%\index{declarative proof scripts}% _declarative_ style, most frequently associated today with the %\index{Isar}%Isar%~\cite{Isar}% language. A declarative proof script is very explicit about subgoal structure and introduction of local names, aiming for human readability. The coding of proof automation is taken to be outside the scope of the proof language, an assumption related to the idea that it is not worth building new automation for each serious theorem. I have shown in this book many examples of theorem-specific automation, which I believe is crucial for scaling to significant results. Declarative proof scripts make it easier to read scripts to modify them for theorem statement changes, but the alternate%\index{adaptive proof scripts}% _adaptive_ style from this book allows use of the _same_ scripts for many versions of a theorem. |

288 | 288 |

289 Perhaps I am a pessimist for thinking that fully formal proofs will inevitably consist of details that are uninteresting to people, but it is my preference to focus on conveying proof-specific details through choice of lemmas. Additionally, adaptive Ltac scripts contain bits of automation that can be understood in isolation. For instance, in a big [repeat match] loop, each case can generally be digested separately, which is a big contrast from trying to understand the hierarchical structure of a script in a more common style. Adaptive scripts rely on variable binding, but generally only over very small scopes, whereas understanding a traditional script requires tracking the identities of local variables potentially across pages of code. | 289 Perhaps I am a pessimist for thinking that fully formal proofs will inevitably consist of details that are uninteresting to people, but it is my preference to focus on conveying proof-specific details through choice of lemmas. Additionally, adaptive Ltac scripts contain bits of automation that can be understood in isolation. For instance, in a big [repeat match] loop, each case can generally be digested separately, which is a big contrast from trying to understand the hierarchical structure of a script in a more common style. Adaptive scripts rely on variable binding, but generally only over very small scopes, whereas understanding a traditional script requires tracking the identities of local variables potentially across pages of code. |

290 | 290 |

291 One might also wonder why it makes sense to prove all theorems automatically (in the sense of adaptive proof scripts) but not construct all programs automatically. My view there is that _program synthesis_ is a very useful idea that deserves broader application! In practice, there are difficult obstacles in the way of finding a program automatically from its specification. A typical specification is not exhaustive in its description of program properties. For instance, details of performance on particular machine architectures are often omitted. As a result, a synthesized program may be correct in some sense while suffering from deficiencies in other senses. Program synthesis research will continue to come up with ways of dealing with this problem, but the situation for theorem proving is fundamentally different. Following mathematical practice, the only property of a formal proof that we care about is which theorem it proves, and it is trivial to check this property automatically. In other words, with a simple criterion for what makes a proof acceptable, automatic search is straightforward. Of course, in practice we also care about understandability of proofs to facilitate long-term maintenance, and that is just what the techniques outlined above are meant to support, and the next section gives some related advice. *) | 291 One might also wonder why it makes sense to prove all theorems automatically (in the sense of adaptive proof scripts) but not construct all programs automatically. My view there is that _program synthesis_ is a very useful idea that deserves broader application! In practice, there are difficult obstacles in the way of finding a program automatically from its specification. A typical specification is not exhaustive in its description of program properties. For instance, details of performance on particular machine architectures are often omitted. As a result, a synthesized program may be correct in some sense while suffering from deficiencies in other senses. Program synthesis research will continue to come up with ways of dealing with this problem, but the situation for theorem proving is fundamentally different. Following mathematical practice, the only property of a formal proof that we care about is which theorem it proves, and it is trivial to check this property automatically. In other words, with a simple criterion for what makes a proof acceptable, automatic search is straightforward. Of course, in practice we also care about understandability of proofs to facilitate long-term maintenance, which is just what motivates the techniques outlined above, and the next section gives some related advice. *) |

292 | 292 |

293 | 293 |

294 (** * Debugging and Maintaining Automation *) | 294 (** * Debugging and Maintaining Automation *) |

295 | 295 |

296 (** Fully automated proofs are desirable because they open up possibilities for automatic adaptation to changes of specification. A well-engineered script within a narrow domain can survive many changes to the formulation of the problem it solves. Still, as we are working with higher-order logic, most theorems fall within no obvious decidable theories. It is inevitable that most long-lived automated proofs will need updating. | 296 (** Fully automated proofs are desirable because they open up possibilities for automatic adaptation to changes of specification. A well-engineered script within a narrow domain can survive many changes to the formulation of the problem it solves. Still, as we are working with higher-order logic, most theorems fall within no obvious decidable theories. It is inevitable that most long-lived automated proofs will need updating. |

442 destruct E; crush | 442 destruct E; crush |

443 end. | 443 end. |

444 | 444 |

445 induction e. | 445 induction e. |

446 | 446 |

447 (** Since we see the subgoals before any simplification occurs, it is clear that this is the case for constants. Our [t] makes short work of it. *) | 447 (** Since we see the subgoals before any simplification occurs, it is clear that we are looking at the case for constants. Our [t] makes short work of it. *) |

448 | 448 |

449 t. | 449 t. |

450 | 450 |

451 (** The next subgoal, for addition, is also discharged without trouble. *) | 451 (** The next subgoal, for addition, is also discharged without trouble. *) |

452 | 452 |

671 End GROUP_THEOREMS. | 671 End GROUP_THEOREMS. |

672 | 672 |

673 (** We implement generic proofs of these theorems with a functor, whose input is an arbitrary group [M]. %\index{Vernacular commands!Module}% *) | 673 (** We implement generic proofs of these theorems with a functor, whose input is an arbitrary group [M]. %\index{Vernacular commands!Module}% *) |

674 | 674 |

675 Module GroupProofs (M : GROUP) : GROUP_THEOREMS with Module M := M. | 675 Module GroupProofs (M : GROUP) : GROUP_THEOREMS with Module M := M. |

676 | |

676 (** As in ML, Coq provides multiple options for ascribing signatures to modules. Here we use just the colon operator, which implements%\index{opaque ascription}% _opaque ascription_, hiding all details of the module not exposed by the signature. Another option is%\index{transparent ascription}% _transparent ascription_ via the [<:] operator, which checks for signature compatibility without hiding implementation details. Here we stick with opaque ascription but employ the [with] operation to add more detail to a signature, exposing just those implementation details that we need to. For instance, here we expose the underlying group representation set and operator definitions. Without such a refinement, we would get an output module proving theorems about some unknown group, which is not very useful. Also note that opaque ascription can in Coq have some undesirable consequences without analogues in ML, since not just the types but also the _definitions_ of identifiers have significance in type checking and theorem proving. *) | 677 (** As in ML, Coq provides multiple options for ascribing signatures to modules. Here we use just the colon operator, which implements%\index{opaque ascription}% _opaque ascription_, hiding all details of the module not exposed by the signature. Another option is%\index{transparent ascription}% _transparent ascription_ via the [<:] operator, which checks for signature compatibility without hiding implementation details. Here we stick with opaque ascription but employ the [with] operation to add more detail to a signature, exposing just those implementation details that we need to. For instance, here we expose the underlying group representation set and operator definitions. Without such a refinement, we would get an output module proving theorems about some unknown group, which is not very useful. Also note that opaque ascription can in Coq have some undesirable consequences without analogues in ML, since not just the types but also the _definitions_ of identifiers have significance in type checking and theorem proving. *) |

677 | 678 |

678 Module M := M. | 679 Module M := M. |

679 (** To ensure that the module we are building meets the [GROUP_THEOREMS] signature, we add an extra local name for [M], the functor argument. *) | 680 (** To ensure that the module we are building meets the [GROUP_THEOREMS] signature, we add an extra local name for [M], the functor argument. *) |

680 | 681 |

872 | 873 |

873 << | 874 << |

874 ((coq-mode . ((coq-prog-args . | 875 ((coq-mode . ((coq-prog-args . |

875 ("-emacs-U" "-R" "LIB" "Lib" "-R" "CLIENT" "Client"))))) | 876 ("-emacs-U" "-R" "LIB" "Lib" "-R" "CLIENT" "Client"))))) |

876 >> | 877 >> |

878 | |

879 A downside of this approach is that users of your code may not want to trust the arbitrary Emacs Lisp programs that you are allowed to place in such files, so that they prefer to add mappings manually. | |

877 *) | 880 *) |