coq-club AT inria.fr
Subject: The Coq mailing list
List archive
Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct
Chronological Thread
- From: Jonathan Leivent <jonikelee AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct
- Date: Sun, 25 Jan 2015 17:42:10 -0500
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
- [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Jason Gross, 01/24/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Jonathan Leivent, 01/24/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Emile Lunardon, 01/25/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Jason Gross, 01/25/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Jonathan Leivent, 01/25/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Jonathan Leivent, 01/26/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Jonathan Leivent, 01/26/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Jonathan Leivent, 01/26/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Jonathan Leivent, 01/27/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Jonathan Leivent, 01/26/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Jonathan Leivent, 01/26/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Jonathan Leivent, 01/25/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Jason Gross, 01/25/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Emile Lunardon, 01/25/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Jonathan Leivent, 01/24/2015
Archive powered by MHonArc 2.6.18.