Andrej Dudenhefner (Dec 16 2020 at 09:31): 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.
Pierre-Marie Pédrot (Dec 16 2020 at 09:39):Looks like a bug in 1 and 2.
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.
Pierre-Marie Pédrot (Dec 16 2020 at 09:54):Note that try t is essentially the same as t || idtac.
Pierre-Marie Pédrot (Dec 16 2020 at 10:08):Interesting, it's not the tactic which is failing.
Pierre-Marie Pédrot (Dec 16 2020 at 10:09):It's the toplevel wrapper at proof termination.
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)
Pierre-Marie Pédrot (Dec 16 2020 at 10:13):Yes, I've commented in the issue about that function.
Fabian Kunze (Dec 16 2020 at 10:13):Ah, yes, this works:
(simple refine (eq_trans fapp_comp _);solve_constraints) || f_equal.
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.
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 +
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?
Pierre-Marie Pédrot (Dec 16 2020 at 10:16):If not a try, at least a once.
Pierre-Marie Pédrot (Dec 16 2020 at 10:16):A dot after a tactic kills backtrack.
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.
Pierre-Marie Pédrot (Dec 16 2020 at 10:17):I think it'd be more natural to implement tac. as once tac; solve.
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.
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?
Pierre-Marie Pédrot (Dec 16 2020 at 10:19):It's for backwards compat it seems.
Pierre-Marie Pédrot (Dec 16 2020 at 10:20):See https://github.com/coq/coq/issues/4763.
Pierre-Marie Pédrot (Dec 16 2020 at 10:21):... and https://github.com/coq/coq/issues/5149
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)
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.
Pierre-Marie Pédrot (Dec 16 2020 at 10:22):Just wrap any foreign tactic in a once?
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.
Pierre-Marie Pédrot (Dec 16 2020 at 10:23):Backtracking is ingrained in the evaluation model of the tactic engine.
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.
Pierre-Marie Pédrot (Dec 16 2020 at 10:25):Most tactics only backtrack internally.
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.
Fabian Kunze (Dec 16 2020 at 10:26):doesn't repeat backtrack?
Pierre-Marie Pédrot (Dec 16 2020 at 10:26):nope.
Pierre-Marie Pédrot (Dec 16 2020 at 10:27):You can see how it's implemented in Ltac2 for instance.
Fabian Kunze (Dec 16 2020 at 10:27):only "+" introduces backtracking in ltac1?
Fabian Kunze (Dec 16 2020 at 10:27):(and things like constructor)
Pierre-Marie Pédrot (Dec 16 2020 at 10:27):More or less. IIRC constructor does.
Pierre-Marie Pédrot (Dec 16 2020 at 10:28):The solver tactic above also seem to backtrack per the documentation.
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?
Pierre-Marie Pédrot (Dec 16 2020 at 10:29):You have to use multimatch to introduce explicit backtrack.
Pierre-Marie Pédrot (Dec 16 2020 at 10:29):Both match and lazymatch are not backtracking externally.
Pierre-Marie Pédrot (Dec 16 2020 at 10:29):match does backtrack but only internally (by design).
Pierre-Marie Pédrot (Dec 16 2020 at 10:30):Really, I'd recommend reading the Ltac2 implementation.
Pierre-Marie Pédrot (Dec 16 2020 at 10:31):It makes clear what does what, because everything is implemented using the basic primitives.
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.
Pierre-Marie Pédrot (Dec 16 2020 at 10:31):I think it does
Pierre-Marie Pédrot (Dec 16 2020 at 10:32):The match constructs are pretty involved semantically.
Pierre-Marie Pédrot (Dec 16 2020 at 10:33):Even lazymatch uses a shallow form of backtracking to pick the matching pattern.
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?
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.
Pierre-Marie Pédrot (Dec 16 2020 at 10:35):(and reimplement it if you wish)
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.
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?
Pierre-Marie Pédrot (Dec 16 2020 at 10:44):Not a bug, in any case not in Ltac.
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: Oct 05 2023 at 02:01 UTC