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

and `foo; solve_constraints; []. bar.`

?

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

what does ;[] even do

Unless I am reading the manual incorrectly, don't you need `Unset Solve Unification Constraints`

to use `solve_constraints`

?

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.

Regarding the use of `[];`

which I haven't seen before, is this ensuring no goals exist?

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

syntax.

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).

but

```
Goal nat.
idtac;[].
```

succeeds

It would because there are no new goals

```
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".

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

what is this "new goal" concept

```
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.

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

?

I suppose that is it.

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

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

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.

no

`; []`

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

Is it documented in the refman?

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 `.`

"

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

@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.

Is it really the trivial case?

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

I would have expected the first to fail

Why would it fail? As Jason just explained, the empty tactic is the same as `idtac`

. So, the first two lines are identical.

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

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

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.
```

@Ali Caglayan What I meant was that `; []`

and `; [idtac]`

are the same

No, what we mean is that `[ ]`

is the same as `[ idtac ]`

; `[ | ]`

is the same as `[ idtac | idtac ]`

; and so on.

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

As the documentation states, "Omitting an `ltac_expr`

leaves the corresponding goal unchanged."

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

Thanks for explaining @Guillaume Melquiond

No worries

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: Oct 13 2024 at 01:02 UTC