Stream: General

Topic: Narrowing the search space

Gergely Buday (Aug 28 2025 at 14:17):

You can use Sledgehammer effectively if the search space is small enough.

We can narrow the search space by

• instantiating theorems using [of ...] and [OF ...]
• unfolding theorems by [unfolded ...]
• writing calculational proofs so that the individual equations give rise to a smaller search space than the original equation
• using in-proof defines, simplifying the expressions in the proof
• giving a good using section with relevant lemmas

What else do you have in mind for this?

Yong Kiam (Aug 28 2025 at 14:46):

sometimes, apply auto before running sledgehammer could help

however, you might want to clean this up afterwards

irvin (Aug 29 2025 at 00:36):

Another useful thing. If you get theorems that keep ruining sledgehammer you can blacklist them using the no_atp attribute

Last updated: Sep 13 2025 at 12:36 UTC