Jason Gross (Apr 14 2022 at 16:38): Jason Gross (Apr 14 2022 at 16:38):What is the difference between foo; solve_constraints; []; bar. and foo; solve_constraints; []. bar.?
Jason Gross (Apr 14 2022 at 16:42):https://github.com/coq/coq/issues/15927
Gaëtan Gilbert (Apr 14 2022 at 16:43):what does ;[] even do
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?
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.
Ali Caglayan (Apr 14 2022 at 16:47):Regarding the use of []; which I haven't seen before, is this ensuring no goals exist?
Ali Caglayan (Apr 14 2022 at 16:47):i.e. the empty case of the [ .. | ..] syntax.
Ali Caglayan (Apr 14 2022 at 16:50):Seems to be:
Goal nat * nat * nat.
Fail simple notypeclasses refine (_,_,_); [].
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).
Gaëtan Gilbert (Apr 14 2022 at 16:53):but
Goal nat.
idtac;[].
succeeds
Ali Caglayan (Apr 14 2022 at 16:54):It would because there are no new goals
Ali Caglayan (Apr 14 2022 at 16:54):Goal nat * nat * nat.
idtac "hello"; []; idtac "world".
prints
hello
world
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".
Ali Caglayan (Apr 14 2022 at 16:55):At least that is the haphazard understanding of the situation I have
Gaëtan Gilbert (Apr 14 2022 at 16:55):what is this "new goal" concept
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].
I don't know if the correct term is "new goal" but that's what it looks like to me.
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 ;?
Ali Caglayan (Apr 14 2022 at 16:58):I suppose that is it.
Ali Caglayan (Apr 14 2022 at 16:58):it seems that ; works even if there are no focused goals on the right
Ali Caglayan (Apr 14 2022 at 17:00):Which is why things like this work:
Goal True.
trivial; exact 45.
anyway removing the ;[] from the issue example changes nothing so it doesn't matter
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.
Gaëtan Gilbert (Apr 14 2022 at 17:02):no
Jason Gross (Apr 14 2022 at 17:02):; [] is "fail if the previous tactic does not leave over exactly one goal"
Ali Caglayan (Apr 14 2022 at 17:03):Is it documented in the refman?
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 ."
Gaëtan Gilbert (Apr 14 2022 at 17:04):probably the goal evar thing https://github.com/coq/coq/issues/15520
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.
Ali Caglayan (Apr 14 2022 at 17:07):Is it really the trivial case?
Ali Caglayan (Apr 14 2022 at 17:07):Goal nat.
Succeed refine (_); [].
Succeed refine (_); [idtac].
Fail refine (_); [idtac|idtac].
I would have expected the first to fail
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.
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.andfoo. bar., but I added; []andsolve_constraintsto eliminate the answers "foomight 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
Jason Gross (Apr 14 2022 at 17:10):Minimal repro case is in https://github.com/coq/coq/issues/15927, sorry for the confusion
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 elideidtacwhen 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.
@Ali Caglayan What I meant was that ; [] and ; [idtac] are the same
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.
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. :)
Guillaume Melquiond (Apr 14 2022 at 17:18):As the documentation states, "Omitting an ltac_expr leaves the corresponding goal unchanged."
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.
Ali Caglayan (Apr 14 2022 at 17:18):Thanks for explaining @Guillaume Melquiond
Jason Gross (Apr 14 2022 at 17:19):No worries
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: Dec 07 2023 at 06:38 UTC