I'm trying (for automation) to understand under which circumstances for a tactic expression `t`

the variants

1) `try t.`

2) `t || idtac.`

3) `t + idtac.`

may fail resulting in a possibly unrecoverable error.

What confuses me are examples where 1 and 2 fail but 3 works, see #13639.

Looks like a bug in 1 and 2.

This is unfortunate. Could there be a workaround to get 2 to work? Even `try (t + fail).`

fails. Confusingly `try (t + idtac).`

succeeds. This throws off my understanding of ltac semantics completely.

Note that `try t`

is essentially the same as `t || idtac`

.

Interesting, it's not the tactic which is failing.

It's the toplevel wrapper at proof termination.

This might have to do with the delaying of unification delays? https://coq.inria.fr/refman/proof-engine/tactics.html#delaying-solving-unification-constraints (note that this option would nt help in any way, it is just the part from where I know that something gets delayed sometimes)

Yes, I've commented in the issue about that function.

Ah, yes, this works:

`(simple refine (eq_trans fapp_comp _);solve_constraints) || f_equal.`

I don't know whether we should try to wrap the unification solver in a try block.

The current behaviour is definitely surprising, and the fact that the solver doesn't block backtracking leads to the weird success with +

Pierre-Marie Pédrot said:

I don't know whether we should try to wrap the unification solver in a try block.

because it might not backtrack properly?

If not a try, at least a once.

A dot after a tactic kills backtrack.

So, this boils down to the question whether the solver is part of the tactic or of the command.

I think it'd be more natural to implement `tac.`

as `once tac; solve`

.

Currently we only have `tac; solve`

(disregarding the focussing issues) and this is what causes `foo + idtac.`

to succeed.

Is the decision to delay unification until the dot because of performance ? I think it is quite counterintuitive. Or is it because only that allows backtracking?

It's for backwards compat it seems.

See https://github.com/coq/coq/issues/4763.

... and https://github.com/coq/coq/issues/5149

(I personally would love a option to disable the part of backtracking all together that allows `t;t2`

with failing t2 to backtrack into t, as I have never used that on purpose in a larger context)

I most of the time only use the "raise and catch exception" aspect of fail and try/`++`

/etc.

Just wrap any foreign tactic in a `once`

?

I don't see how to do that on a large scale without breaking everything.

Backtracking is ingrained in the evaluation model of the tactic engine.

yes, i have once paranoidly wrapped a lot of things into `once`

at one point because I was not sure whether there was backtracking happening or nor.

Most tactics only backtrack internally.

That means if you don't use explicit backtrack in your proof scripts you should be fine.

doesn't repeat backtrack?

nope.

You can see how it's implemented in Ltac2 for instance.

only "+" introduces backtracking in ltac1?

(and things like `constructor`

)

More or less. IIRC `constructor`

does.

The solver tactic above also seem to backtrack per the documentation.

I once read that either `lazymatch`

or `match`

also is actually already wrapped into a `once`

, but I cant find it. So I assume the other also backtracks?

You have to use `multimatch`

to introduce explicit backtrack.

Both `match`

and `lazymatch`

are not backtracking externally.

`match`

does backtrack but only internally (by design).

Really, I'd recommend reading the Ltac2 implementation.

It makes clear what does what, because everything is implemented using the basic primitives.

so the line `match … is, in fact, shorthand for once multimatch ….`

in the ltac1 doc could probably mention that lazymatch is also not backtracking.

I think it does

The match constructs are pretty involved semantically.

Even lazymatch uses a shallow form of backtracking to pick the matching pattern.

so the semantics of ltac2-matches should mirror the semantics of ltac1-matches, but the implementation is clearer?

The implementation are observationally the same, but contrarily to Ltac1, the various Ltac2 matches are not primitive and thus you can just read the implementation.

(and reimplement it if you wish)

In Ltac1 you can read the ML implementation but it's not very user-friendly.

Having now figured out what the underlying problem is, are the initial 1) and 2) bugs, or just expected undocumented behavior? That is, is #13639 a permanent wont-fix/use-workaround?

Not a bug, in any case not in Ltac.

I'd qualify it as a surprising behaviour, and maybe we can wrap the toplevel tactic in `once`

to see whether it is backwards compatible.

Last updated: Jan 29 2023 at 06:02 UTC