Mercurial > cpdt > repo
comparison src/Match.v @ 334:386b7ad8849b
Change some template annotations
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Tue, 04 Oct 2011 13:38:21 -0400 |
| parents | 2eeb96aa0426 |
| children | 23b06f87bd30 |
comparison
equal
deleted
inserted
replaced
| 333:c27d97176c85 | 334:386b7ad8849b |
|---|---|
| 435 Abort. | 435 Abort. |
| 436 (* end thide *) | 436 (* end thide *) |
| 437 | 437 |
| 438 (** One other gotcha shows up when we want to debug our Ltac functional programs. We might expect the following code to work, to give us a version of [length] that prints a debug trace of the arguments it is called with. *) | 438 (** One other gotcha shows up when we want to debug our Ltac functional programs. We might expect the following code to work, to give us a version of [length] that prints a debug trace of the arguments it is called with. *) |
| 439 | 439 |
| 440 (* begin thide *) | |
| 440 (* begin hide *) | 441 (* begin hide *) |
| 441 Reset length. | 442 Reset length. |
| 442 (* end hide *) | 443 (* end hide *) |
| 443 (** %\noindent\coqdockw{%#<tt>#Reset#</tt>#%}% [length.] *) | 444 (** %\noindent\coqdockw{%#<tt>#Reset#</tt>#%}% [length.] *) |
| 444 | 445 |
| 479 idtac ls; | 480 idtac ls; |
| 480 match ls with | 481 match ls with |
| 481 | nil => k O | 482 | nil => k O |
| 482 | _ :: ?ls' => length ls' ltac:(fun n => k (S n)) | 483 | _ :: ?ls' => length ls' ltac:(fun n => k (S n)) |
| 483 end. | 484 end. |
| 485 (* end thide *) | |
| 484 | 486 |
| 485 (** The new [length] takes a new input: a %\emph{%#<i>#continuation#</i>#%}% [k], which is a function to be called to continue whatever proving process we were in the middle of when we called [length]. The argument passed to [k] may be thought of as the return value of [length]. *) | 487 (** The new [length] takes a new input: a %\emph{%#<i>#continuation#</i>#%}% [k], which is a function to be called to continue whatever proving process we were in the middle of when we called [length]. The argument passed to [k] may be thought of as the return value of [length]. *) |
| 486 | 488 |
| 489 (* begin thide *) | |
| 487 Goal False. | 490 Goal False. |
| 488 length (1 :: 2 :: 3 :: nil) ltac:(fun n => pose n). | 491 length (1 :: 2 :: 3 :: nil) ltac:(fun n => pose n). |
| 489 (** [[ | 492 (** [[ |
| 490 (1 :: 2 :: 3 :: nil) | 493 (1 :: 2 :: 3 :: nil) |
| 491 (2 :: 3 :: nil) | 494 (2 :: 3 :: nil) |
| 492 (3 :: nil) | 495 (3 :: nil) |
| 493 nil | 496 nil |
| 494 ]] | 497 ]] |
| 495 *) | 498 *) |
| 496 Abort. | 499 Abort. |
| 500 (* end thide *) | |
| 497 | 501 |
| 498 (** We see exactly the trace of function arguments that we expected initially, and an examination of the proof state afterward would show that variable [n] has been added with value [3]. *) | 502 (** We see exactly the trace of function arguments that we expected initially, and an examination of the proof state afterward would show that variable [n] has been added with value [3]. *) |
| 499 | 503 |
| 500 | 504 |
| 501 (** * Recursive Proof Search *) | 505 (** * Recursive Proof Search *) |
| 996 | [ |- fst ?x = 3 ] => equate x (3, 2) | 1000 | [ |- fst ?x = 3 ] => equate x (3, 2) |
| 997 end; reflexivity. | 1001 end; reflexivity. |
| 998 Qed. | 1002 Qed. |
| 999 | 1003 |
| 1000 | 1004 |
| 1005 (* begin thide *) | |
| 1001 (** * Exercises *) | 1006 (** * Exercises *) |
| 1002 | 1007 |
| 1003 (** %\begin{enumerate}%#<ol># | 1008 (** %\begin{enumerate}%#<ol># |
| 1004 | 1009 |
| 1005 %\item%#<li># An anonymous Coq fan from the Internet was excited to come up with this tactic definition shortly after getting started learning Ltac: *) | 1010 %\item%#<li># An anonymous Coq fan from the Internet was excited to come up with this tactic definition shortly after getting started learning Ltac: *) |
| 1163 In the body of the case analysis, [lemma] will be bound to the first lemma, and [more] will be bound to the remaining lemmas. There is no need to consider a case for [tt], our stand-in for [nil]. This is because lack of any matching pattern will trigger failure, which is exactly the outcome we would like upon reaching the end of the lemma list without finding one that applies. The tactic will fail, triggering backtracking to some previous [match]. | 1168 In the body of the case analysis, [lemma] will be bound to the first lemma, and [more] will be bound to the remaining lemmas. There is no need to consider a case for [tt], our stand-in for [nil]. This is because lack of any matching pattern will trigger failure, which is exactly the outcome we would like upon reaching the end of the lemma list without finding one that applies. The tactic will fail, triggering backtracking to some previous [match]. |
| 1164 | 1169 |
| 1165 There are different kinds of backtracking, corresponding to different sorts of decisions to be made. The examples considered above can be handled with backtracking that only reconsiders decisions about the order in which to apply rewriting lemmas. A full-credit solution need only handle that kind of backtracking, considering all rewriting sequences up to the length bound passed to your tactic. A good test of this level of applicability is to prove both [test1] and [test2] above. However, some theorems could only be proved using a smarter tactic that considers not only order of rewriting lemma uses, but also choice of arguments to the lemmas. That is, at some points in a proof, the same lemma may apply at multiple places within the goal formula, and some choices may lead to stuck proof states while others lead to success. For an extra challenge (without any impact on the grade for the problem), you might try beefing up your tactic to do backtracking on argument choice, too.#</li># | 1170 There are different kinds of backtracking, corresponding to different sorts of decisions to be made. The examples considered above can be handled with backtracking that only reconsiders decisions about the order in which to apply rewriting lemmas. A full-credit solution need only handle that kind of backtracking, considering all rewriting sequences up to the length bound passed to your tactic. A good test of this level of applicability is to prove both [test1] and [test2] above. However, some theorems could only be proved using a smarter tactic that considers not only order of rewriting lemma uses, but also choice of arguments to the lemmas. That is, at some points in a proof, the same lemma may apply at multiple places within the goal formula, and some choices may lead to stuck proof states while others lead to success. For an extra challenge (without any impact on the grade for the problem), you might try beefing up your tactic to do backtracking on argument choice, too.#</li># |
| 1166 | 1171 |
| 1167 #</ol>#%\end{enumerate}% *) | 1172 #</ol>#%\end{enumerate}% *) |
| 1173 (* end thide *) |