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
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].
Or rather, you'd want to replace
by, but IME (with
stdpp's done) that's not actually a safe refactoring, and I have never investigated why.
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...
I'm not an authority, but to some extent that might be a matter of style
It's not ssreflect's style, but I don't remember CPDT discouraging it
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
I've seen inline scripts there, tho not that long...
I also think such a statement would be a category error without a software engineering argument, but I've said enough
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
Instead of long sequences, I—again not an authority at all—find that using goal selectors is nicer.
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.
@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.
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.
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: Jan 29 2023 at 05:03 UTC