## Mercurial > cpdt > repo

### comparison src/Match.v @ 484:5025a401ad9e

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

Last round of feedback from class at Penn

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

date | Sun, 06 Jan 2013 16:23:26 -0500 |

parents | 582cf453878e |

children | 31258618ef73 |

comparison

equal
deleted
inserted
replaced

483:582cf453878e | 484:5025a401ad9e |
---|---|

115 | 115 |

116 (** Since [match] patterns can share unification variables between hypothesis and conclusion patterns, it is easy to figure out when the conclusion matches a hypothesis. The %\index{tactics!exact}%[exact] tactic solves a goal completely when given a proof term of the proper type. | 116 (** Since [match] patterns can share unification variables between hypothesis and conclusion patterns, it is easy to figure out when the conclusion matches a hypothesis. The %\index{tactics!exact}%[exact] tactic solves a goal completely when given a proof term of the proper type. |

117 | 117 |

118 It is also trivial to implement the introduction rules (in the sense of %\index{natural deduction}%natural deduction%~\cite{TAPLNatDed}%) for a few of the connectives. Implementing elimination rules is only a little more work, since we must give a name for a hypothesis to [destruct]. | 118 It is also trivial to implement the introduction rules (in the sense of %\index{natural deduction}%natural deduction%~\cite{TAPLNatDed}%) for a few of the connectives. Implementing elimination rules is only a little more work, since we must give a name for a hypothesis to [destruct]. |

119 | 119 |

120 The last rule implements modus ponens, using a tactic %\index{tactics!specialize}%[specialize] which will replace a hypothesis with a version that is specialized to a provided set of arguments (for quantified variables or local hypotheses from implications). *) | 120 The last rule implements modus ponens, using a tactic %\index{tactics!specialize}%[specialize] which will replace a hypothesis with a version that is specialized to a provided set of arguments (for quantified variables or local hypotheses from implications). By convention, when the argument to [specialize] is an application of a hypothesis [H] to a set of arguments, the result of the specialization replaces [H]. For other terms, the outcome is the same as with [generalize]. *) |

121 | 121 |

122 Section propositional. | 122 Section propositional. |

123 Variables P Q R : Prop. | 123 Variables P Q R : Prop. |

124 | 124 |

125 Theorem propositional : (P \/ Q \/ False) /\ (P -> Q) -> True /\ Q. | 125 Theorem propositional : (P \/ Q \/ False) /\ (P -> Q) -> True /\ Q. |

194 notHyp t; generalize pf; intro. | 194 notHyp t; generalize pf; intro. |

195 (* end thide *) | 195 (* end thide *) |

196 | 196 |

197 (** We see the useful %\index{tactics!type of}%[type of] operator of Ltac. This operator could not be implemented in Gallina, but it is easy to support in Ltac. We end up with [t] bound to the type of [pf]. We check that [t] is not already present. If so, we use a [generalize]/[intro] combo to add a new hypothesis proved by [pf]. The tactic %\index{tactics!generalize}%[generalize] takes as input a term [t] (for instance, a proof of some proposition) and then changes the conclusion from [G] to [T -> G], where [T] is the type of [t] (for instance, the proposition proved by the proof [t]). | 197 (** We see the useful %\index{tactics!type of}%[type of] operator of Ltac. This operator could not be implemented in Gallina, but it is easy to support in Ltac. We end up with [t] bound to the type of [pf]. We check that [t] is not already present. If so, we use a [generalize]/[intro] combo to add a new hypothesis proved by [pf]. The tactic %\index{tactics!generalize}%[generalize] takes as input a term [t] (for instance, a proof of some proposition) and then changes the conclusion from [G] to [T -> G], where [T] is the type of [t] (for instance, the proposition proved by the proof [t]). |

198 | 198 |

199 With these tactics defined, we can write a tactic [completer] for adding to the context all consequences of a set of simple first-order formulas. *) | 199 With these tactics defined, we can write a tactic [completer] for, among other things, adding to the context all consequences of a set of simple first-order formulas. *) |

200 | 200 |

201 (* begin thide *) | 201 (* begin thide *) |

202 Ltac completer := | 202 Ltac completer := |

203 repeat match goal with | 203 repeat match goal with |

204 | [ |- _ /\ _ ] => constructor | 204 | [ |- _ /\ _ ] => constructor |

315 Abort. | 315 Abort. |

316 (* end thide *) | 316 (* end thide *) |

317 | 317 |

318 (** The problem is that unification variables may not contain locally bound variables. In this case, [?P] would need to be bound to [x = x], which contains the local quantified variable [x]. By using a wildcard in the earlier version, we avoided this restriction. To understand why this applies to the [completer] tactics, recall that, in Coq, implication is shorthand for degenerate universal quantification where the quantified variable is not used. Nonetheless, in an Ltac pattern, Coq is happy to match a wildcard implication against a universal quantification. | 318 (** The problem is that unification variables may not contain locally bound variables. In this case, [?P] would need to be bound to [x = x], which contains the local quantified variable [x]. By using a wildcard in the earlier version, we avoided this restriction. To understand why this applies to the [completer] tactics, recall that, in Coq, implication is shorthand for degenerate universal quantification where the quantified variable is not used. Nonetheless, in an Ltac pattern, Coq is happy to match a wildcard implication against a universal quantification. |

319 | 319 |

320 The Coq 8.2 release includes a special pattern form for a unification variable with an explicit set of free variables. That unification variable is then bound to a function from the free variables to the "real" value. In Coq 8.1 and earlier, there is no such workaround. We will see an example of this fancier binding form in the next chapter. | 320 The Coq 8.2 release includes a special pattern form for a unification variable with an explicit set of free variables. That unification variable is then bound to a function from the free variables to the "real" value. In Coq 8.1 and earlier, there is no such workaround. We will see an example of this fancier binding form in Section 15.5. |

321 | 321 |

322 No matter which Coq version you use, it is important to be aware of this restriction. As we have alluded to, the restriction is the culprit behind the surprising behavior of [completer']. We unintentionally match quantified facts with the modus ponens rule, circumventing the check that a suitably matching hypothesis is available and leading to different behavior, where wrong quantifier instantiations are chosen. Our earlier [completer] tactic uses a modus ponens rule that matches the implication conclusion with a variable, which blocks matching against non-trivial universal quantifiers. | 322 No matter which Coq version you use, it is important to be aware of this restriction. As we have alluded to, the restriction is the culprit behind the surprising behavior of [completer']. We unintentionally match quantified facts with the modus ponens rule, circumventing the check that a suitably matching hypothesis is available and leading to different behavior, where wrong quantifier instantiations are chosen. Our earlier [completer] tactic uses a modus ponens rule that matches the implication conclusion with a variable, which blocks matching against non-trivial universal quantifiers. |

323 | 323 |

324 Actually, the behavior demonstrated here applies to Coq version 8.4, but not 8.4pl1. The latter version will allow regular Ltac pattern variables to match terms that contain locally bound variables, but a tactic failure occurs if that variable is later used as a Gallina term. *) | 324 Actually, the behavior demonstrated here applies to Coq version 8.4, but not 8.4pl1. The latter version will allow regular Ltac pattern variables to match terms that contain locally bound variables, but a tactic failure occurs if that variable is later used as a Gallina term. *) |

325 | 325 |

476 Abort. | 476 Abort. |

477 | 477 |

478 (** What is going wrong here? The answer has to do with the dual status of Ltac as both a purely functional and an imperative programming language. The basic programming language is purely functional, but tactic scripts are one "datatype" that can be returned by such programs, and Coq will run such a script using an imperative semantics that mutates proof states. Readers familiar with %\index{monad}\index{Haskell}%monadic programming in Haskell%~\cite{Monads,IO}% may recognize a similarity. Haskell programs with side effects can be thought of as pure programs that return _the code of programs in an imperative language_, where some out-of-band mechanism takes responsibility for running these derived programs. In this way, Haskell remains pure, while supporting usual input-output side effects and more. Ltac uses the same basic mechanism, but in a dynamically typed setting. Here the embedded imperative language includes all the tactics we have been applying so far. | 478 (** What is going wrong here? The answer has to do with the dual status of Ltac as both a purely functional and an imperative programming language. The basic programming language is purely functional, but tactic scripts are one "datatype" that can be returned by such programs, and Coq will run such a script using an imperative semantics that mutates proof states. Readers familiar with %\index{monad}\index{Haskell}%monadic programming in Haskell%~\cite{Monads,IO}% may recognize a similarity. Haskell programs with side effects can be thought of as pure programs that return _the code of programs in an imperative language_, where some out-of-band mechanism takes responsibility for running these derived programs. In this way, Haskell remains pure, while supporting usual input-output side effects and more. Ltac uses the same basic mechanism, but in a dynamically typed setting. Here the embedded imperative language includes all the tactics we have been applying so far. |

479 | 479 |

480 Even basic [idtac] is an embedded imperative program, so we may not automatically mix it with purely functional code. In fact, a semicolon operator alone marks a span of Ltac code as an embedded tactic script. This makes some amount of sense, since pure functional languages have no need for sequencing: since they lack side effects, there is no reason to run an expression and then just throw away its value and move on to another expression. | 480 Even basic [idtac] is an embedded imperative program, so we may not automatically mix it with purely functional code. In fact, a semicolon operator alone marks a span of Ltac code as an embedded tactic script. This makes some amount of sense, since pure functional languages have no need for sequencing: since they lack side effects, there is no reason to run an expression and then just throw away its value and move on to another expression. |

481 | |

482 An alternate explanation that avoids an analogy to Haskell monads (admittedly a tricky concept in its own right) is: An Ltac tactic program returns a function that, when run later, will perform the desired proof modification. These functions are distinct from other types of data, like numbers or Gallina terms. The prior, correctly working version of [length] computed solely with Gallina terms, but the new one is implicitly returning a tactic function, as indicated by the use of [idtac] and semicolon. However, the new version's recursive call to [length] is structured to expect a Gallina term, not a tactic function, as output. As a result, we have a basic dynamic type error, perhaps obscured by the involvement of first-class tactic scripts. | |

481 | 483 |

482 The solution is like in Haskell: we must "monadify" our pure program to give it access to side effects. The trouble is that the embedded tactic language has no [return] construct. Proof scripts are about proving theorems, not calculating results. We can apply a somewhat awkward workaround that requires translating our program into%\index{continuation-passing style}% _continuation-passing style_ %\cite{continuations}%, a program structuring idea popular in functional programming. *) | 484 The solution is like in Haskell: we must "monadify" our pure program to give it access to side effects. The trouble is that the embedded tactic language has no [return] construct. Proof scripts are about proving theorems, not calculating results. We can apply a somewhat awkward workaround that requires translating our program into%\index{continuation-passing style}% _continuation-passing style_ %\cite{continuations}%, a program structuring idea popular in functional programming. *) |

483 | 485 |

484 Reset length. | 486 Reset length. |

485 | 487 |