The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 11/09/2014 06:28 PM, Jason Gross wrote:
> Hi,
> Is there a way to "split" evars in Coq?  I'm trying to get rewriting by
> shape to work (since it's my opinion that hypotheses should not have
> names).  I have a single rewrite working:
>
> Ltac tac_shape shape tac :=
>    match goal with
>      | [ H : ?shape' |- _ ] => unify shape' shape; tac H
>    end.
>
> Tactic Notation "shape" "rewrite" open_constr(shape) := tac_shape shape
> ltac:(fun H => rewrite H).
>
> Goal forall a b c d : Set, a = b -> b = c -> a = c.
>    intros.
>    repeat shape rewrite (_ = _); reflexivity.
>
>
> But if I try to build an equivalent of [rewrite !H], and bring the [repeat]
> inside the tactic notation, then I end up with something that (predictably)
> doesn't work:
>
> Ltac tac_shape shape tac :=
>    match goal with
>      | [ H : ?shape' |- _ ] => unify shape' shape; tac H
>    end.
>
> Tactic Notation "shape" "rewrite" open_constr(shape) := tac_shape shape
> ltac:(fun H => rewrite H).
> Tactic Notation "shape" "rewrite" "?" open_constr(shape) := repeat
> tac_shape shape ltac:(fun H => rewrite !H).
> Tactic Notation "shape" "rewrite" "!" open_constr(shape) := progress shape
> rewrite ? shape.
>
> Goal forall a b c d : Set, a = b -> b = c -> a = c.
>    intros.
>    repeat shape rewrite (_ = _); reflexivity.
>    Undo.
>    shape rewrite ! (_ = _). reflexivity.
>
>
> So my question is: is there a way to split the evars, so I can bring the
> [repeat] inside the [Tactic Notation] while keeping the pattern outside of
> it?
>
> Thanks,
> Jason

The trick I found the other day seems to handle this as well:

Ltac tac_shape shape tac :=
let e := fresh in
  refine (let e := shape in _);
  shelve_unifiable;
  let v := eval red in e in clear e;
  match goal with H : ?C |- _ =>
    unify v C; tac H
  end.


Tactic Notation "shape" "rewrite" uconstr(shape) := tac_shape shape
ltac:(fun H => rewrite H).
Tactic Notation "shape" "rewrite" "?" uconstr(shape) := repeat
tac_shape shape ltac:(fun H => rewrite !H).
Tactic Notation "shape" "rewrite" "!" uconstr(shape) := progress shape
rewrite ? shape.

Goal forall a b c d : Set, a = b -> b = c -> a = c.
  intros.
  repeat shape rewrite (_ = _); reflexivity.
  Undo.
  shape rewrite ! (_ = _). reflexivity.
Qed.

Note the use of uconstr instead of open_constr.  By the way, why isn't 
open_constr documented?

-- Jonathan