The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 01/25/2015 04:06 PM, Jason Gross wrote:
> What about making a tactic notation that takes an ident_list and a tactic,
> creates evars for all of the identifiers in the list, runs the tactic, and
> cleans them up afterwards?  You could also make a functional variant that
> returned the result of the tactic afterwards.  This would be analogous to
> needing a list of variable declarations in the code to use variables.  It's
> a bit suboptimal, perhaps, but I think it should work.  (You may need to
> play some games to actually make use of the ident_list, or might need to do
> something else that's morally equivalent to an ident_list.)

Recall the email threads titled "Splitting evars?" and "Ltac and constr 
arguments with holes" from November.  In that, we discussed the following:

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.

(Although I would now use [eval cbv delta [e] in e] instead of [eval red 
in e]).

Note that properly worked evars can appear in invocations of this 
tactic, due to the combo of uconstr and refine:

shape rewrite (f ?[E] = g ?E)

But one must always introduce the evars properly with the ?[E] form 
before using them.  Still, this is the best technique I've found. 
Luckily, if the tactic fails, the evars are of course undefined.  I 
don't recall why I thought it would leave new evars unsolved... Maybe it 
was that matching a pattern like (?[E1] /\ ?[E2]) against an already 
existing single evar hole (of type Prop in this case) using this 
technique results in evar splitting - so that E1 and E2 remain unsolved 
even though the match succeeded.

Which points out another flaw - if you have already existing evars in 
some hyps, then any attempt to match against them using unify might 
inadvertently solve them - unlike the match tactical.  You would first 
have to factor out the evars from each hyp before attempting to match 
against it to be safe - which can be done - even for evars under 
binders, using some tricks.  I guess that would fix the above case as well.

So, this is a possibility, if not too ugly.

As for functional variants - bugs 3403 and 3861 would prevent that.


> > UNSUBSCRIBE

I guess I shouldn't take the above personally.  Although it did make me 
wonder if it would be better to have a coq-hackers list separate from 
coq-club - where coq-hackers would be dedicated to (frivolous?) pursuits 
like this one, and coq-club can retain its utilitarian purity.

-- Jonathan