Stream: General

Topic: Strategy for proving FSet theorems

Gergely Buday (Sep 19 2023 at 13:17):

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?

Gergely Buday (Sep 19 2023 at 13:46):

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

Alex Weisberger (Sep 19 2023 at 20:19):

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.

Wolfgang Jeltsch (Sep 19 2023 at 20:29):

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).

Wolfgang Jeltsch (Sep 19 2023 at 20:31):

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 21 2024 at 12:33 UTC