Stream: Coq devs & plugin devs

Topic: difference between `;` and `.`


view this post on Zulip Jason Gross (Apr 14 2022 at 16:38):

What is the difference between foo; solve_constraints; []; bar. and foo; solve_constraints; []. bar.?

view this post on Zulip Jason Gross (Apr 14 2022 at 16:42):

https://github.com/coq/coq/issues/15927

view this post on Zulip Gaëtan Gilbert (Apr 14 2022 at 16:43):

what does ;[] even do

view this post on Zulip Ali Caglayan (Apr 14 2022 at 16:46):

Unless I am reading the manual incorrectly, don't you need Unset Solve Unification Constraints to use solve_constraints?

view this post on Zulip Ali Caglayan (Apr 14 2022 at 16:47):

Or I guess that is to disable the constraints from being solved in other ltac tactics. If foo on purpose doesn't do this then maybe it is valid.

view this post on Zulip Ali Caglayan (Apr 14 2022 at 16:47):

Regarding the use of []; which I haven't seen before, is this ensuring no goals exist?

view this post on Zulip Ali Caglayan (Apr 14 2022 at 16:47):

i.e. the empty case of the [ .. | ..] syntax.

view this post on Zulip Ali Caglayan (Apr 14 2022 at 16:50):

Seems to be:

Goal nat * nat * nat.
Fail simple notypeclasses refine (_,_,_); [].

view this post on Zulip Ali Caglayan (Apr 14 2022 at 16:51):

Then to answer your original question, the first is different than the second since bar is being bound to a new empty set of goals (I don't know if those are the right words).

view this post on Zulip Gaëtan Gilbert (Apr 14 2022 at 16:53):

but

Goal nat.
  idtac;[].

succeeds

view this post on Zulip Ali Caglayan (Apr 14 2022 at 16:54):

It would because there are no new goals

view this post on Zulip Ali Caglayan (Apr 14 2022 at 16:54):

Goal nat * nat * nat.
idtac "hello"; []; idtac "world".

prints

hello
world

view this post on Zulip Ali Caglayan (Apr 14 2022 at 16:55):

But if idtac "world" was replaced with a tactic that actually did anything, then the latter bar would do something in the original goal, whilsts the former bar would do it in the "empty set of goals".

view this post on Zulip Ali Caglayan (Apr 14 2022 at 16:55):

At least that is the haphazard understanding of the situation I have

view this post on Zulip Gaëtan Gilbert (Apr 14 2022 at 16:55):

what is this "new goal" concept

view this post on Zulip Ali Caglayan (Apr 14 2022 at 16:56):

Goal nat * nat * nat.
Fail refine (_,_,_); [].
Fail refine (_,_,_); [idtac].
Fail refine (_,_,_); [idtac|idtac].
Succeed refine (_,_,_); [idtac|idtac|idtac].

view this post on Zulip Ali Caglayan (Apr 14 2022 at 16:57):

I don't know if the correct term is "new goal" but that's what it looks like to me.

view this post on Zulip Gaëtan Gilbert (Apr 14 2022 at 16:57):

do you mean the goals which are focused after the tactic on the left of the ;?

view this post on Zulip Ali Caglayan (Apr 14 2022 at 16:58):

I suppose that is it.

view this post on Zulip Ali Caglayan (Apr 14 2022 at 16:58):

it seems that ; works even if there are no focused goals on the right

view this post on Zulip Ali Caglayan (Apr 14 2022 at 17:00):

Which is why things like this work:

Goal True.
trivial; exact 45.

view this post on Zulip Gaëtan Gilbert (Apr 14 2022 at 17:00):

anyway removing the ;[] from the issue example changes nothing so it doesn't matter

view this post on Zulip Ali Caglayan (Apr 14 2022 at 17:01):

The answer to Jason's question is then, bar does nothing in the first example since there are no focused goals, but something in the second example since there is one goal focused.

view this post on Zulip Gaëtan Gilbert (Apr 14 2022 at 17:02):

no

view this post on Zulip Jason Gross (Apr 14 2022 at 17:02):

; [] is "fail if the previous tactic does not leave over exactly one goal"

view this post on Zulip Ali Caglayan (Apr 14 2022 at 17:03):

Is it documented in the refman?

view this post on Zulip Jason Gross (Apr 14 2022 at 17:04):

I mean, really my question is "what is the difference between foo; bar. and foo. bar., but I added ; [] and solve_constraints to eliminate the answers "foo might not leave over exactly one goal" and "some constraints are only solved at ."

view this post on Zulip Gaëtan Gilbert (Apr 14 2022 at 17:04):

probably the goal evar thing https://github.com/coq/coq/issues/15520

view this post on Zulip Jason Gross (Apr 14 2022 at 17:05):

@Ali Caglayan It should be? It's the trivial case of things like foo; [ bar | baz | qux ] where you only have one goal you're delegating to. Note that you can elide idtac when you don't want to do something in the branch.

view this post on Zulip Ali Caglayan (Apr 14 2022 at 17:07):

Is it really the trivial case?

view this post on Zulip Ali Caglayan (Apr 14 2022 at 17:07):

Goal nat.
Succeed refine (_); [].
Succeed refine (_); [idtac].
Fail refine (_); [idtac|idtac].

view this post on Zulip Ali Caglayan (Apr 14 2022 at 17:07):

I would have expected the first to fail

view this post on Zulip Guillaume Melquiond (Apr 14 2022 at 17:08):

Why would it fail? As Jason just explained, the empty tactic is the same as idtac. So, the first two lines are identical.

view this post on Zulip Gaëtan Gilbert (Apr 14 2022 at 17:08):

Jason Gross said:

I mean, really my question is "what is the difference between foo; bar. and foo. bar., but I added ; [] and solve_constraints to eliminate the answers "foo might not leave over exactly one goal" and "some constraints are only solved at ."

I thought it was a minimal repro case so this was confusing

view this post on Zulip Jason Gross (Apr 14 2022 at 17:10):

Minimal repro case is in https://github.com/coq/coq/issues/15927, sorry for the confusion

view this post on Zulip Ali Caglayan (Apr 14 2022 at 17:14):

What is confusing me is what Jason said here:
Jason Gross said:

Ali Caglayan It should be? It's the trivial case of things like foo; [ bar | baz | qux ] where you only have one goal you're delegating to. Note that you can elide idtac when you don't want to do something in the branch.

Guillaume Melquiond said:

Why would it fail? As Jason just explained, the empty tactic is the same as idtac. So, the first two lines are identical.

How is it the same as idtac?

Goal nat * nat * nat.
Fail refine (_,_,_); [].
Succeed refine (_,_,_); idtac.

view this post on Zulip Jason Gross (Apr 14 2022 at 17:15):

@Ali Caglayan What I meant was that ; [] and ; [idtac] are the same

view this post on Zulip Guillaume Melquiond (Apr 14 2022 at 17:15):

No, what we mean is that [ ] is the same as [ idtac ]; [ | ] is the same as [ idtac | idtac ]; and so on.

view this post on Zulip Ali Caglayan (Apr 14 2022 at 17:17):

It took me a while to realize that the semi colon there was not part of the code. :)

view this post on Zulip Guillaume Melquiond (Apr 14 2022 at 17:18):

As the documentation states, "Omitting an ltac_expr leaves the corresponding goal unchanged."

view this post on Zulip Ali Caglayan (Apr 14 2022 at 17:18):

Sorry @Jason Gross I didn't mean to hijack your thread, I guess I still don't understand some things here.

view this post on Zulip Ali Caglayan (Apr 14 2022 at 17:18):

Thanks for explaining @Guillaume Melquiond

view this post on Zulip Jason Gross (Apr 14 2022 at 17:19):

No worries

view this post on Zulip Jason Gross (Apr 14 2022 at 17:20):

I'm still baffled by the behavior I posted though (I don't see how it can be pattern_of_constr as @Gaëtan Gilbert suggests on the issue...)


Last updated: Feb 01 2023 at 15:04 UTC