1

In an interactive proof, I'm trying to extract an expression into a new variable while capturing the equality as a new proof term.

The remember tactic seems designed for this purpose. Since I like giving explicit names to introduced names, I'd prefer to use this variant:

  1. remember term as ident eqn:ident

This behaves as remember term as ident, except that the name of the generated equality is also given.

However when I attempt it (or the other remember variants), I only get this error:

> remember (prefix ++ suffix) as the_environment eqn:H_prefix_suffix.
>                                                ^^^
Syntax error: 'in' '|-' expected after [prim:ident] (in [tactic:simple_tactic]).

Heeding the error message, the only variant that actually seems to work is

remember (prefix ++ suffix) as the_environment in |-.

...which unfortunately doesn't let me choose the name of the introduced proof of equality.

Why don't the documented remember variants seem to work?

I'm using coq 8.4pl6.

1 Answer 1

2

I shot myself in the foot.

I had previously declared a tactic with that syntax:

Tactic Notation "remember" constr(c) "as" ident(x) "in" "|-" :=
  let x := fresh x in
  let H := fresh "Heq" x in
  (set (x := c); assert (H : x = c) by reflexivity; clearbody x).

It seems this explicit definition masks the built-in variants. Removing this definition makes the others visible again.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.