one of my collaborators is very fond of long sequenced try
sentences, 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?
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 solve
with 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 try
sequences.
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 Hint Extern
...
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.
@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.
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: Oct 13 2024 at 01:02 UTC