Stream: Coq users

Topic: when ltac try fails


view this post on Zulip Andrej Dudenhefner (Dec 16 2020 at 09:31):

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.

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 09:39):

Looks like a bug in 1 and 2.

view this post on Zulip Andrej Dudenhefner (Dec 16 2020 at 09:52):

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.

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 09:54):

Note that try t is essentially the same as t || idtac.

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 10:08):

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

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 10:09):

It's the toplevel wrapper at proof termination.

view this post on Zulip Fabian Kunze (Dec 16 2020 at 10:12):

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)

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 10:13):

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

view this post on Zulip Fabian Kunze (Dec 16 2020 at 10:13):

Ah, yes, this works:
(simple refine (eq_trans fapp_comp _);solve_constraints) || f_equal.

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 10:15):

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

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 10:15):

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

view this post on Zulip Fabian Kunze (Dec 16 2020 at 10:16):

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?

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 10:16):

If not a try, at least a once.

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 10:16):

A dot after a tactic kills backtrack.

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 10:16):

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

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 10:17):

I think it'd be more natural to implement tac. as once tac; solve.

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 10:18):

Currently we only have tac; solve (disregarding the focussing issues) and this is what causes foo + idtac. to succeed.

view this post on Zulip Fabian Kunze (Dec 16 2020 at 10:19):

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?

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 10:19):

It's for backwards compat it seems.

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 10:20):

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

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 10:21):

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

view this post on Zulip Fabian Kunze (Dec 16 2020 at 10:21):

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

view this post on Zulip Fabian Kunze (Dec 16 2020 at 10:22):

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

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 10:22):

Just wrap any foreign tactic in a once?

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 10:23):

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

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 10:23):

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

view this post on Zulip Fabian Kunze (Dec 16 2020 at 10:24):

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.

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 10:25):

Most tactics only backtrack internally.

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 10:25):

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

view this post on Zulip Fabian Kunze (Dec 16 2020 at 10:26):

doesn't repeat backtrack?

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 10:26):

nope.

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 10:27):

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

view this post on Zulip Fabian Kunze (Dec 16 2020 at 10:27):

only "+" introduces backtracking in ltac1?

view this post on Zulip Fabian Kunze (Dec 16 2020 at 10:27):

(and things like constructor)

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 10:27):

More or less. IIRC constructor does.

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 10:28):

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

view this post on Zulip Fabian Kunze (Dec 16 2020 at 10:28):

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?

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 10:29):

You have to use multimatch to introduce explicit backtrack.

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 10:29):

Both match and lazymatch are not backtracking externally.

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 10:29):

match does backtrack but only internally (by design).

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 10:30):

Really, I'd recommend reading the Ltac2 implementation.

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 10:31):

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

view this post on Zulip Fabian Kunze (Dec 16 2020 at 10:31):

so the line match … is, in fact, shorthand for once multimatch …. in the ltac1 doc could probably mention that lazymatch is also not backtracking.

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 10:31):

I think it does

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 10:32):

The match constructs are pretty involved semantically.

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 10:33):

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

view this post on Zulip Fabian Kunze (Dec 16 2020 at 10:33):

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

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 10:34):

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.

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 10:35):

(and reimplement it if you wish)

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 10:35):

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

view this post on Zulip Andrej Dudenhefner (Dec 16 2020 at 10:43):

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?

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 10:44):

Not a bug, in any case not in Ltac.

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 10:45):

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