Adding eassert, eset, epose, etc.

[herbelin]

This is a natural extension of the language of primitive tactics. It provides e-variants for assert, pose, set, remember, pose proof, enough, allowing to manipulate partial terms or statements, and hence to ease a way to develop proofs by refinement and unification. One can for instance see it as adding some benefits of "refine" to usual tactics (typically, I found the need for eassert when implementing functional extensionality in).

Not a commitment to the e-policy. With a translating tool, the e-prefix could eventually become the default if considered to be the good way to go. In the meantime, I however don't see other alternatives than adding specific e-variants. (See also #3872.)

Not a commitment to say that statements with free evars should be kept with unresolved evars rather than generalized over unresolved evars. For instance, Matthieu's ` could be generalized to tell "generalize" rather than "keep evars/fail", as in, say, providing assert `(_ = _) to be possibly interpreted as assert (forall A (x y : A), x = y).

Not a commitment to say that the syntax of tactics should be hard-wired in g_tactic.ml4. I followed the easy path but maybe these tactics could already be definable with TACTIC EXTEND instead.

No documentation yet.

[jonleivent]

@herbelin, you appear to have commitment issues ;)

Otherwise, cool!

As for generalizing vs. extentializing - I had a discussion with Pierre Courtieu IIRC about a tactic that was like eapply, but generalized over remaining args instead of making them holes. Point being - it would be useful to have a general method that takes something that generates holes and instead turns those into generalizations. An "unrefine"?

[JasonGross]

Shouldn't this comment be removed?

[ejgallego]

This is likely a naïve question, but why are two sets of tactics needed? Why can't the the existing set, pose, etc... gain the capability of generalizing over evars?

[JasonGross]

@ejgallego Backwards compatibility. If you make set, pose, etc more powerful in this way, automation that previously failed will now succeed, and automation that previously fully solved a goal may no longer do so, because it would take a different path.

[ejgallego]

@JasonGross umm, it looks to me that if automation would fail because of that, it would be very fragile automation to begin with.

I'm pretty convinced that supporting fragile automation is a futile goal.

[maximedenes]

@herbelin do you want this PR to be discussed for integration on the 8.7 roadmap?

[herbelin]

@maximedenes: yes, I think it is natural to have them, even if it gets eventually supersed by a new more flexible model. (And I miss them from time to time.)

[Zimmi48]

@herbelin It would be good if no new tactics were introduced without proper documentation. Not saying that this PR cannot get merged right now, but if it is then it should be on your TODO list to document the variants before the 8.7 beta release.

Another remark is that if we actually get an attribute system one day, then the e variants of tactics could instead be replaced by a uniform attribute, which could be set to emulate the behavior of the basic variant, of the e variant, or of the generalizing variant which was discussed above. And it could also be set more globally via an option...
But the fact that such attribute system is on the roadmap does not mean that we will effectively get it for 8.7 (right now no one is really working on it if I understood correctly; and there is not even a CEP), and thus, in the meantime, I support your approach.

[herbelin]

@Zimmi48: doc: I agree. To be eventually superseded by a more uniform attribute system, no objection at all, on the contrary, since it would just become a particular case of a more general mechanism.

[herbelin]

Fixed bugs and added doc. I remained vague on the specification of what a generated existential variable is, but I think it is a general issue of the documentation, if not of the system in general, to have a clearer semantics on where (dependent) existential variables go (on the shelf? at which position? etc.).

[ejgallego]

Hugo the PR is failing to build on Travis, could you fix it?

[herbelin]

@ejgallego: fix applied, now ok on travis.

Otherwise, on coqdev, @maximedenes asked about "What is the long term plan on e/not e-tactics? How is this a first step towards this long term plan?".

I answered that if the discussion is ripe for a long term plan on e-tactics I'm ok to be the one who organizes it. In particular, we can consider having an e-variant for each existing tactic, we can consider providing a modifier to stop a tactic failing on unresolved evars, or consider making stopping failing on unresolved evars to be the default (did I miss other alternatives)?

But whatever the long term plan is, a first step is to allow each individual existing tactic to be able to behave in the e-way (in the sense of allowing unresolved evars).

So, whatever long term plan we have, I don't see how to avoid having this PR as a step towards it.

Also, I'm ready to extend the implementation of e-variants to other tactics, so that these are accessible using a generic modifier or general option, or whatever, but I'm not necessarily enthousiastic to add a concrete syntax for all of them.

More precisely: I think it makes sense, by regularity, to have einversion, efix with, ecofix with, etransitivity c, eabsurd, egeneralize, estepl, estepr, especialize but I would be more encline to deprecate the following than adding a e-syntax: cut (not only it is wrongly named, but most of the time it is used in a pattern of the form cut;[intro|] which suggests that assert is to preferred), casetype and elimtype (which in practise are used in a context of the form casetype False, or elimtype False which means that exfalso is the real intent), cutrewrite (already deprecated in favor of replace). Note that more thinking is needed about the expected behavior of edestruct/einduction, and that this is not unrelated to the invert-like tactic planned in ssr 2.0.

[herbelin]

@maximedenes: did you take time to study my answer? To improve the fluidity of development, I really think that we should make progress on the PRs pending for a long time (congratulations in passing for today's efficiency!), and, unless I missed something in the discussion, this one is blocking on your answer.

[ejgallego]

No strong opinion on this one, however as a user it doesn't feel great to have so many versions of tactics. In particular I was discussing with @Zimmi48 today how ssr have is versatile enough that replaces 4 (or in the case of this patch 8) tactics.

[Zimmi48]

There was some related discussion in #449 (comment) (where I remarked in particular that pose proof and specialize can basically be used to do exactly the same thing, however people seemed reluctant to merge these two) and some threads on coqdev as well.

@ejgallego have replaces assert, pose proof and specialize but I'm missing the fourth one.
Incidentally, all of these tactics are listed as "variants" of assert in the refman. See https://coq.inria.fr/refman/Reference-Manual010.html#hevea_tactic52. From what I can see in the code pose proof is a true variant of assert in terms of implementation, while specialize is distinct.

Now, I'd be interested to hear how this also replaces the e-variants proposed by Hugo here.
I tried using have H : _ = _. but this does not compare at all to eassert (H : _ = _). The first one generalizes each of the holes as a distinct variable while the second creates (as expected) one existential variable for each of the holes.

[herbelin]

@ejgallego: It is certain that we can reduce the number of tactics, but

• Tactics that do not exists with the e-option do not support the e-semantics, so, implementing the e-semantics, even without giving it a syntax is a necessary preliminary step to eventually reduce the number of tactics, isn't it?
• We have to do with tactics as they are. We cannot change the semantics of non e-variants without breaking the compatibility. Even if versioning tactics allows to support more semantics change of tactics, we should limit them so that users willing to upgrade can do it, shouldn't we?
• In my opinion, having tactic foo and tactic efoo has the drawback of blocking two entries in the parser but it is not so bad in terms of regularity and style compared to having foo and, say, a prefixwith_evar to modify in the e-way the semantics of foo.

But, maybe are you actually talking about the number of tactics in general, independently of the existence of an e-variant?

In particular, when you say that ssr is versatile enough to replace 4 tactics, I guess that you are referring to rewrite? If so, wouldn't it be fairer to say that ssr has symbolic notations for 4 tactics which all use the same rewrite keyword? My experience with symbolic notations is that it allows compactness and easy chaining but that it does not make a tactic call necessarily clearer, especially for a beginner, so even in the presence of symbolic notations, I think it makes sense to keep appealing clearly identified keywords that any reader, even if non-Coq user, can have an intuition about.

Also, we tried several times in the past to support in vanilla rewrite the possibilities of symbolic chaining that ssr rewrite provides but at the end, we were never really satisfied with the resulting syntax (- vs <-, the absence of commas in ssr's notation, etc.). So, it seems that to merge ssr rewrite and vanilla rewrite, some compromise at the syntax level is needed.

But if you think that such a merge of ssr rewrite within vanilla rewrite is possible, that would be interesting.

[Zimmi48]

@herbelin You misread a bit of @ejgallego comment. He's talking about the ssr tactic have.

[maximedenes]

I think adding new tactics has some risk because of the number of already existing tactics, but is an ok compromise as a step towards a model that factors them using attributes for instance.

@herbelin Can you rebase this PR so that we merge it? Thanks!

[herbelin]

@Zimmi48: Ah, sorry, I indeed misread @ejgallego's comment.

It happens that vanilla assert do have the syntax assert (H:=foo) which does pose proof!

Actually, it is even the other way round, pose proof has been introduced because the syntax assert (H:=foo) was considered to be too ad hoc and a bit unappropriate.

So, maybe, ssr, which roughly derived from vanilla Coq as it was at the beginning of the 2000's, just kept vanilla's assert as it was at this time ("pose proof" is from 2006).

[herbelin]

@Zimmi48, @ejgallego: By the way, it is a long time that I wonder about the user feedback wrt the
"generalization over holes as distinct variables" feature. It looks interesting and I would be happy to know more about the use cases.

[Zimmi48]

@herbelin From what Georges Gonthier told me yesterday, have was introduced when Coq had only cut, thus before vanilla assert.

[herbelin]

@Zimmi48: The tactic assert was introduced in 2001. I suspect that the name have came after assert was implemented since my memories is that this was precisely one of the reasons of friction between Georges and the Coq developers at this time, that he renamed assert into have without a strong motivation (I vaguely remember that he wanted to get rid of the Coq's constraint that terms arguments of tactics are always surrounded by parentheses; maybe he also found have more appealing that assert, I don't know; the motivation for the divergence is still unclear to me as of today.)

Maybe it is time that Georges and the Coq developers from the 2000's meet and get beyond the syntactic quarrel from this period of time, concentrating on how to work together rather than maintaining a futile "schism", as P. C. called it.

[Zimmi48]

Thanks! This now looks great to me.

[maximedenes]

@herbelin Travis passed. Could you isolate the commits that are really implementing what the title of this PR suggests? We could then merge it. Thanks!

[herbelin]

@maximedenes: I made #693 for the fix.

If we want to nitpick, there is also "Support for using type information to infer more precise evar sources." which, in rare circumstances, changes the name the user sees for evars whose name is generated by Coq (typically evars associated to a dependent _ are named after the name of the variable they are bound to rather than ?Goal). I can make a different PR for it if someone wants to specifically comment on that.

[maximedenes]

@herbelin Thanks!

As for "Support for using type information to infer more precise evar sources.", if everyone is ok with it (@ppedrot?), we can leave it here. What I'd like to avoid is that the entire PR gets delayed if a bit of discussion is needed on one item.

[maximedenes]

Something is wrong, the test-suite does not pass.

[ppedrot]

LGTM.

[herbelin]

@maximedenes: Just a shift in evar ID for emacs. Fixed.

By the way, there is another problem with test-suite on MacOS X since #687: readlink -f does not work on MacOS X. Setting BIN := $(shell cd ../bin; pwd)/ is a way e.g. to make it works. @SkySkimmer: would you be ok to do something for it?

[SkySkimmer]

@herbelin see #701

[herbelin]

@SkySkimmer: thanks.