The Coq mailing list

["Andrew McCreight" <continuation AT gmail.com>]

I think I have an answer to my own question now.   Russell O'Connor suggested that I could use fold to do what I wanted to do.  The following tactic does what I want, folding up all occurrences of all definitions in the hypothesis of the proof state:

  Ltac zlong :=
    repeat (match goal with
              | X : _, Y : _ |- _ => progress (fold X in Y)
            end);
    repeat (match goal with 
              | X : _ |- _ => progress (fold X)
            end).

A more direct way to write this would be:

  Ltac zlong :=
    repeat (match goal with
              | X : _ |- _ => progress (fold X in *)
            end).

...but unfortunately "fold X in *" turns "X := A : B" into "X := X : B", which is obviously something you don't want to do.  In fact, doing "unfold X in X" after that causes Coq to go into an infinite loop.  This behavior has been reported as bug 1389.

http://logical.futurs.inria.fr/coq-bugs/show_bug.cgi?id=1389

So instead a more lengthy version (and possibly slower?) is needed to prevent folding X in X.

-Andrew

On Sat, Jun 14, 2008 at 11:09 AM, Andrew McCreight <continuation AT gmail.com> wrote:

Hi,

I have many hypothesis of the form
  X := A

At some point in my proof new instances of A will occur.  Currently, what I do is "replace A with X in * |- *", which works, but is annoying when I have 5 or 6 definitions.  A silly percentage of some of my proofs are taken up by this.

What I would like to do is to have a tactic that will automatically do this for all definitions, but the obvious match goal to do this fails with a syntax error:

  Ltac unzeta :=
    match goal with
      | X := ?Y : _ => replace Y with X in *
    end.

Toplevel input, characters 66-68
Syntax error: ':' expected after [Prim.name] (in [match_hyps])

Is there some other way to do this?

More generally, is using definitions like this a bad idea?  Should I use equality instead?  I like having a syntactic distinction between a definition of a variable introduced purely to improve readability and more profound statements of equality, but maybe it isn't worth it if such definitions have a second-class status in the tactic language.

Thanks,

Andrew