Class 20: Sledgehammer in the Wild

This class, we are going to look at Sledgehammer in the wild! The paper we read on Tuesday was about Sledgehammer in practice. One of the coolest things about Sledgehammer is its extremely wide adoption in the Isabelle/HOL community. So we are going to look at some other people's proof developments, and how they use Sledgehammer or any of the automatic solvers it calls.

This exercise is going to be a bit more open-ended than what we've seen so far. Isabelle/HOL has an archive of proof developments; we will go through this archive to find developments that we like, and see how they use this automation. We'll also play around with modifying and understanding the development. We'll discuss in groups, then post on the board as usual. More below.

Installation Instructions

1. Install the Isabelle/HOL proof assistant following these instructions.
2. Download the Isabelle/HOL Archive of Formal Proofs here.
3. Browse the Archive of Formal Proofs here, and identify a project that looks interesting to you.
4. Open the interesting project in Isabelle/HOL, and make sure the proofs go through.

If you have any trouble, please post your questions in this thread. Please also drop any installation tips you have in that thread.

If installation fails, and the class forums are no help, do not panic; we will try to match you with someone in class for whom installation worked.

You can find the exercise we will do together in class below.

During class, we will again divide up into groups. We will open up Isabelle/HOL, and click on the Sledgehammer tutorial link to keep that reference available throughout the exercise. We will then step through the steps below:

1. Open any of the proof developments from the Archive of Formal Proofs that one of the members of your group chose.
2. Does the proof development use Sledgehammer or any of the automated solvers that the Sledgehammer tactic invokes (for example, `metis`, `smt`, or `meson`)? To what degree?
3. Spend a few minutes trying to understand one of the proofs that invokes one of these, if applicable.
4. Try using Sledgehammer yourself instead of `metis`, `smt`, `meson`, or something similar, if applicable. Does it produce the same proof?
5. Does checking the Isar proofs box work? If so, what are the tradeoffs between the original proof and the proof it produces with Isar proofs enabled?
6. If you feel comfortable trying an Isabelle/HOL proof, try to complete one of the proofs that calls an automated solver manually, using simpler automation. (There are several tutorials you can refer to in order to help you with this, all of which are linked to within the Isabelle/HOL IDE.) How hard is this?
7. What are the tradeoffs of the different kinds of automation you've tried so far for this proof?
8. Try using Sledgehammer yourself instead of some manual proof, if applicable. Does it work? (It's OK if it doesn't.) Do you have a sense of what Sledgehammer is good at versus bad at so far?
9. Repeat for other proof developments as time allows.

You can do this on your own if you cannot make it to class, or enter a Zoom breakout if you're remote. Let me know if you can't attend, but would like me to find you a partner or make an exception.

If you have extra time at the end, I recommend playing around with new theorems that you define, and how Sledgehammer handles them.

As usual, the only graded part will be a discussion question: Based on your experiences with the proof development(s) you tried, what did you learn about Sledgehammer? When would you use Sledgehammer versus other automation? What did you like about using Sledgehammer? And what do you think would improve the experience of using automation like Sledgehammer?

Please have your group post your answers in the class forum thread (coming soon), listing all group members in your response.