Patrick Nicodemus (Oct 30 2023 at 14:58): Patrick Nicodemus (Oct 30 2023 at 14:58):I do not want to sound too greedy in expecting too much of the magic Sledgehammer tool, I just want to understand its limitations.
It seems to me that Sledgehammer has a bias against unfolding locale definitions even when the theorem for the locale definition is explicitly passed.
have t : "category E" (* need to know that E is an instance of the locale before we can apply the definition of the locale. *)
from this have "x ∈ obj E ⟹ precategory.id E x ∈ hom E x x"
sledgehammer (add: category_def t) (* This eventually finds a proof after about 2 or 3 minutes. *)
sledgehammer (add: category_def) (* Same, doesn't matter whether we pass the proof that E is a category. *)
from this have "x ∈ obj E ⟹ precategory.id E x ∈ hom E x x"
by simp (add: category_def) (* 0ms. *)
Is my interpretation correct here, that Sledgehammer just strongly prefers to avoid unfolding locale definitions?
Why is this? Or otherwise how should I interpret these results?
Mathias Fleury (Oct 30 2023 at 15:27):In general, ATPs tend to rarely unfold definitions as you make terms much bigger
Mathias Fleury (Oct 30 2023 at 15:28):moreover, this could be one of the cases where HO provers would perform better than FO provers
Mathias Fleury (Oct 30 2023 at 15:29):but this would be related to this goal in particular
Mathias Fleury (Oct 30 2023 at 15:30):Mathias Fleury said:
In general, ATPs tend to rarely unfold definitions as you make terms much bigger
and I should add: they will never unfold many of them. Hence it makes sense to unfold + apply auto at the beginning (if this leads usually to bad proofs)
Last updated: Apr 27 2024 at 12:25 UTC