## Mercurial > cpdt > repo

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

line wrap: on

line diff

--- a/src/Match.v Tue Apr 07 18:59:24 2015 -0400 +++ b/src/Match.v Wed Aug 05 14:46:55 2015 -0400 @@ -1,4 +1,4 @@ -(* Copyright (c) 2008-2012, Adam Chlipala +(* Copyright (c) 2008-2012, 2015, Adam Chlipala * * This work is licensed under a * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 @@ -10,9 +10,10 @@ (* begin hide *) Require Import List. -Require Import CpdtTactics. +Require Import Cpdt.CpdtTactics. Set Implicit Arguments. +Set Asymmetric Patterns. (* end hide *) @@ -359,6 +360,9 @@ 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}% *) (* begin thide *) +(* begin hide *) +Definition red_herring := O. +(* end hide *) Ltac length ls := match ls with | nil => O @@ -383,9 +387,15 @@ Abort. Reset length. +(* begin hide *) +Reset red_herring. +(* end hide *) (** 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. *) +(* begin hide *) +Definition red_herring := O. +(* end hide *) Ltac length ls := match ls with | nil => O @@ -452,7 +462,13 @@ (* begin thide *) Reset length. +(* begin hide *) +Reset red_herring. +(* end hide *) +(* begin hide *) +Definition red_herring := O. +(* end hide *) Ltac length ls := idtac ls; match ls with @@ -484,6 +500,9 @@ 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. *) Reset length. +(* begin hide *) +Reset red_herring. +(* end hide *) Ltac length ls k := idtac ls; @@ -811,6 +830,9 @@ (** Now we can write a tactic that encapsulates the pattern we just employed, instantiating all quantifiers of a particular hypothesis. *) +(* begin hide *) +Definition red_herring := O. +(* end hide *) Ltac insterU H := repeat match type of H with | forall x : ?T, _ => @@ -923,6 +945,9 @@ End t7. Reset insterU. +(* begin hide *) +Reset red_herring. +(* end hide *) (** 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. *)