Email Gateway (Oct 13 2022 at 08:53): Email Gateway (Oct 13 2022 at 08:53):From: Jørgen Villadsen <cl-isabelle-users@lists.cam.ac.uk>
Hi,
Method auto is the same as (auto 4 2). I have a proof where auto does not work but (auto 5 2) works. Should I just use (auto 5 2) or is it problematic?
I also wonder if it has been considered to change the default to (auto 5 2).
Regards, Jørgen
Email Gateway (Oct 13 2022 at 09:10):From: Dmitriy Traytel <traytel@di.ku.dk>
Hi Jørgen,
In the AFP I get the below histogram using:
export Isabelle getenv AFP; grep "auto [0-9][0-9]* [0-9][0-9]" $AFP -roh --include='.thy' | sort | uniq -c | sort -n
This suggests that it is fine to use the arguments I guess. But note that 4 3 is the far more popular alternative than 5 2. ;) Still given that there are around 300 000 invocations of auto in the AFP, either is still an outlier. I’m sure that changing the default will create more problems than it will solve.
Best wishes,
Dmitriy
1 auto 1 3
1 auto 1 4
1 auto 11 0
1 auto 2 0
1 auto 2 1
1 auto 2 4
1 auto 3 3
1 auto 4 10
1 auto 6 5
1 auto 7 0
1 auto 7 2
1 auto 9 2
1 auto 9 3
2 auto 10 10
2 auto 2 3
2 auto 3 0
2 auto 4 7
2 auto 5 3
2 auto 5 4
2 auto 5 5
2 auto 9 0
3 auto 5 0
3 auto 6 4
3 auto 6 6
4 auto 0 2
4 auto 13 2
4 auto 6 2
4 auto 8 0
5 auto 0 6
5 auto 4 0
6 auto 0 1
6 auto 6 0
7 auto 0 5
7 auto 10 0
7 auto 4 6
8 auto 5 2
13 auto 4 5
17 auto 0 0
62 auto 3 4
80 auto 0 4
131 auto 0 3
219 auto 4 4
325 auto 4 3
Email Gateway (Oct 13 2022 at 09:20):From: Thomas Sewell <tals4@cam.ac.uk>
You might already realise this. The numeric arguments control the search depth of auto's standard proof search and the search depth of blast as called at each step. I forget which is which. It's no surprise that turning the numbers up from 4 to 5 finds a new proof, that just means that the necessary proof is exactly 5 steps long in some eccentric sense.
Setting the default higher would make auto take longer to terminate when it isn't making progress, and many proofs do actually use auto in this way. The branching factor of the search is variable, so the effect of changing the limits might be quite different from place to place. It would also break some existing proofs for silly reasons. That's probably not a good option.
There's a bigger question floating around, is there some way to add more information to the interface? Is there some reasonable time to tell the user "by the way, the auto you just typed would make more progress if given a longer leash"?
Best regards,
Thomas.
Email Gateway (Oct 13 2022 at 09:53):From: Lawrence Paulson <lp15@cam.ac.uk>
As the author of this method, I quite forgot that those options existed :-)
But it’s important to remember what auto is for: to remove the trivial (quickly) and leave behind the difficult. It’s chiefly intended for exploration. With the trivial proofs disposed of, you can focus on the difficult proofs. Then ideally you should restructure your proof with the difficult parts proved first so that auto leaves nothing behind. Making auto work harder and for longer would defeat its main purpose, and we have other tactics such as force that might do what you need.
Larry
Last updated: Apr 26 2024 at 01:06 UTC