Mercurial > cpdt > repo

comparison src/Match.v @ 534:ed829eaa91b2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Builds with Coq 8.5beta2
author Adam Chlipala <adam@chlipala.net>
date Wed, 05 Aug 2015 14:46:55 -0400
parents 49f3b2d70302
children 4f6e7bab0d45
comparison
equal deleted inserted replaced
533:8921cfa2f503 534:ed829eaa91b2
1 (* Copyright (c) 2008-2012, Adam Chlipala 1 (* Copyright (c) 2008-2012, 2015, Adam Chlipala
2 * 2 *
3 * This work is licensed under a 3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License. 5 * Unported License.
6 * The license text is available at: 6 * The license text is available at:
8 *) 8 *)
9 9
10 (* begin hide *) 10 (* begin hide *)
11 Require Import List. 11 Require Import List.
12 12
13 Require Import CpdtTactics. 13 Require Import Cpdt.CpdtTactics.
14 14
15 Set Implicit Arguments. 15 Set Implicit Arguments.
16 Set Asymmetric Patterns.
16 (* end hide *) 17 (* end hide *)
17 18
18 19
19 (** %\chapter{Proof Search in Ltac}% *) 20 (** %\chapter{Proof Search in Ltac}% *)
20 21
357 >> 358 >>
358 359
359 The problem is that Ltac treats the expression [S (length ls')] as an invocation of a tactic [S] with argument [length ls']. We need to use a special annotation to "escape into" the Gallina parsing nonterminal.%\index{tactics!constr}% *) 360 The problem is that Ltac treats the expression [S (length ls')] as an invocation of a tactic [S] with argument [length ls']. We need to use a special annotation to "escape into" the Gallina parsing nonterminal.%\index{tactics!constr}% *)
360 361
361 (* begin thide *) 362 (* begin thide *)
363 (* begin hide *)
364 Definition red_herring := O.
365 (* end hide *)
362 Ltac length ls := 366 Ltac length ls :=
363 match ls with 367 match ls with
364 | nil => O 368 | nil => O
365 | _ :: ?ls' => constr:(S (length ls')) 369 | _ :: ?ls' => constr:(S (length ls'))
366 end. 370 end.
381 The value of [n] only has the length calculation unrolled one step. What has happened here is that, by escaping into the [constr] nonterminal, we referred to the [length] function of Gallina, rather than the [length] Ltac function that we are defining. *) 385 The value of [n] only has the length calculation unrolled one step. What has happened here is that, by escaping into the [constr] nonterminal, we referred to the [length] function of Gallina, rather than the [length] Ltac function that we are defining. *)
382 386
383 Abort. 387 Abort.
384 388
385 Reset length. 389 Reset length.
390 (* begin hide *)
391 Reset red_herring.
392 (* end hide *)
386 393
387 (** The thing to remember is that Gallina terms built by tactics must be bound explicitly via [let] or a similar technique, rather than inserting Ltac calls directly in other Gallina terms. *) 394 (** The thing to remember is that Gallina terms built by tactics must be bound explicitly via [let] or a similar technique, rather than inserting Ltac calls directly in other Gallina terms. *)
388 395
396 (* begin hide *)
397 Definition red_herring := O.
398 (* end hide *)
389 Ltac length ls := 399 Ltac length ls :=
390 match ls with 400 match ls with
391 | nil => O 401 | nil => O
392 | _ :: ?ls' => 402 | _ :: ?ls' =>
393 let ls'' := length ls' in 403 let ls'' := length ls' in
450 460
451 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 %\coqdocvar{%#<tt>#length#</tt>#%}% that prints a debug trace of the arguments it is called with. *) 461 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 %\coqdocvar{%#<tt>#length#</tt>#%}% that prints a debug trace of the arguments it is called with. *)
452 462
453 (* begin thide *) 463 (* begin thide *)
454 Reset length. 464 Reset length.
455 465 (* begin hide *)
466 Reset red_herring.
467 (* end hide *)
468
469 (* begin hide *)
470 Definition red_herring := O.
471 (* end hide *)
456 Ltac length ls := 472 Ltac length ls :=
457 idtac ls; 473 idtac ls;
458 match ls with 474 match ls with
459 | nil => O 475 | nil => O
460 | _ :: ?ls' => 476 | _ :: ?ls' =>
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. 498 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.
483 499
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. *) 500 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. *)
485 501
486 Reset length. 502 Reset length.
503 (* begin hide *)
504 Reset red_herring.
505 (* end hide *)
487 506
488 Ltac length ls k := 507 Ltac length ls k :=
489 idtac ls; 508 idtac ls;
490 match ls with 509 match ls with
491 | nil => k O 510 | nil => k O
809 apply H. 828 apply H.
810 Qed. 829 Qed.
811 830
812 (** Now we can write a tactic that encapsulates the pattern we just employed, instantiating all quantifiers of a particular hypothesis. *) 831 (** Now we can write a tactic that encapsulates the pattern we just employed, instantiating all quantifiers of a particular hypothesis. *)
813 832
833 (* begin hide *)
834 Definition red_herring := O.
835 (* end hide *)
814 Ltac insterU H := 836 Ltac insterU H :=
815 repeat match type of H with 837 repeat match type of H with
816 | forall x : ?T, _ => 838 | forall x : ?T, _ =>
817 let x := fresh "x" in 839 let x := fresh "x" in
818 evar (x : T); 840 evar (x : T);
921 943
922 Abort. 944 Abort.
923 End t7. 945 End t7.
924 946
925 Reset insterU. 947 Reset insterU.
948 (* begin hide *)
949 Reset red_herring.
950 (* end hide *)
926 951
927 (** We can redefine [insterU] to treat implications differently. In particular, we pattern-match on the type of the type [T] in [forall x : ?T, ...]. If [T] has type [Prop], then [x]'s instantiation should be thought of as a proof. Thus, instead of picking a new unification variable for it, we instead apply a user-supplied tactic [tac]. It is important that we end this special [Prop] case with [|| fail 1], so that, if [tac] fails to prove [T], we abort the instantiation, rather than continuing on to the default quantifier handling. Also recall that the tactic form %\index{tactics!solve}%[solve [ t ]] fails if [t] does not completely solve the goal. *) 952 (** We can redefine [insterU] to treat implications differently. In particular, we pattern-match on the type of the type [T] in [forall x : ?T, ...]. If [T] has type [Prop], then [x]'s instantiation should be thought of as a proof. Thus, instead of picking a new unification variable for it, we instead apply a user-supplied tactic [tac]. It is important that we end this special [Prop] case with [|| fail 1], so that, if [tac] fails to prove [T], we abort the instantiation, rather than continuing on to the default quantifier handling. Also recall that the tactic form %\index{tactics!solve}%[solve [ t ]] fails if [t] does not completely solve the goal. *)
928 953
929 Ltac insterU tac H := 954 Ltac insterU tac H :=
930 repeat match type of H with 955 repeat match type of H with