Karl Palmskog (Jul 28 2020 at 16:21): Karl Palmskog (Jul 28 2020 at 16:21):one of my collaborators is very fond of long sequenced trysentences, as in try lia; try eapply some_lemma; try auto with arith; try .... Since I tend to use SSReflect and by everywhere, our styles don't mesh well. Is there a "canonical" expert source stating something like "sequenced trys are harmful" to use when persuading someone to come over to the by side?
Paolo Giarrusso (Jul 28 2020 at 16:38):that's a verbose way to write first [lia | eapply some_lemma | auto with arith]. It sounds like you want solve [lia | eapply some_lemma | auto with arith].
Paolo Giarrusso (Jul 28 2020 at 16:39):Or rather, you'd want to replace solve with by, but IME (with stdpp's done) that's not actually a safe refactoring, and I have never investigated why.
Karl Palmskog (Jul 28 2020 at 16:39):ah, sure, but think of proof scripts with say, 30+ of these sequenced try, and each can solve multiple goals. I guess what I'm asking is for a statement from authority that this is a code smell...
Paolo Giarrusso (Jul 28 2020 at 16:40):I'm not an authority, but to some extent that might be a matter of style
Paolo Giarrusso (Jul 28 2020 at 16:41):It's not ssreflect's style, but I don't remember CPDT discouraging it
Karl Palmskog (Jul 28 2020 at 16:42):I think CPDT is a different in that the actual custom tactics are typically recursive, and in my view it basically encourages "one custom recursive tactic per proof". This is to me at least somewhat more maintainable than long ad-hoc try sequences.
Paolo Giarrusso (Jul 28 2020 at 16:43):I've seen inline scripts there, tho not that long...
Paolo Giarrusso (Jul 28 2020 at 16:43):I also think such a statement would be a category error without a software engineering argument, but I've said enough
Paolo Giarrusso (Jul 28 2020 at 16:48):last: I've also written similar (shorter) scripts, on gnarly syntactic proofs, but it seems some improvements are possible — that particular example sounds like it warrants Hint Extern...
Théo Winterhalter (Jul 28 2020 at 17:03):Instead of long sequences, I—again not an authority at all—find that using goal selectors is nicer.
Like
all: try lia.
all: try solve [ auto with arith ].
...
This way you can see what happens, and it is more robust as you can see if the number of goal doesn't decrease.
Karl Palmskog (Jul 28 2020 at 17:05):@Théo Winterhalter thanks, in this case it would at least be much easier to debug indeed, e.g., if one uses the convention that any all: ... is supposed to decrease the goal count by at least one.
Théo Winterhalter (Jul 28 2020 at 17:11):Yes, that is what I had in mind. I usually couple this with
Set Default Goal Selector "!"
so that when I stop with the all: then I have only one goal left (or none) and Coq will complain if it is no longer the case.
Paolo Giarrusso (Jul 28 2020 at 17:46):Using all: also avoids backtracking among goals, which might be a feature for this script. Using backtracking in a 30-tactic-chain sounds too evil even for me.
Last updated: Apr 19 2024 at 02:02 UTC