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 *)