## 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 |