I try to prove theorems in FSet, the finite set type theory, but my question is more general.

How deep should I go unfolding definitions with `unfolding`

? Also, what is a good strategy of including lemmas from a library theory when feeding them to Sledgehammer?

Self-answer: I proved lemmas on the main functions of FSet with `induct`

easily.

How deep should I go unfolding definitions with unfolding?

I was taught to try and unfold as little as possible. Philosophically, you've created an abstraction by introducing a definition, and it makes sense to use properties about that abstraction instead of having to reason about the lower level logic. Practically, logic becomes more complex and formulas become larger the more definitions get unfolded, and proofs can become more difficult.

That being said, I still frequently end up with proofs that are nothing but unfolding definitions and applying `auto`

/ `simp`

. And where the cutoff line should be isn't always clear. Even with a proof assistant, proving still requires creativity.

I agree with this. In particular, I tend to not follow the abstraction approach excessively: Some properties I could prove about more abstract concepts are just so simple that I don’t introduce lemmas stating these properties, because I don’t want to annoy the reader with trivialities. Instead, whenever I need such properties, I just unfold definitions and use proof methods like `simp`

. Actually, I make the defining equations of all my `definition`

specifications part of the simpset, in order to be consistent with `primrec`

, `fun`

, etc. As a result, I don’t need much manual unfolding (but sometimes I need to *prevent* unfolding).

I also agree with the point that writing Isabelle formalizations requires creativity. This is in particular because I’m of the opinion that Isabelle formalizations shouldn’t just be there to have some machine-checked proofs but should also be instructive to the human reader.

Last updated: Dec 07 2023 at 08:19 UTC