Introduction and proof by cases tool

Stream: new members

[William Tarver Solomon III]

Hello my name is William Solomon, but I go by Bill Solomon.
I have a bachelors in philosophy from the University of Minnesota: Twin Cities and have taken several undergraduate computer science courses as well as a graduate course in modal logic (while I was an undergrad). My senior project was also ?inventing/ discovering? a new modal logic where my supervisor was Roy T. Cook. I was interested in adding proof tools to Mathlib for complicated proofs that use proof by cases, in the least controversial modal logic K, using Kripke Semantics. It seems to me that this could help greatly reduce complexity in certain proofs by cases. Is this something that already exists in Mathlib, that I didn't find, or would it be useful?

[Kyle Miller]

Seems interesting -- I'm not familiar with these things, could you give at least a toy example of what these kinds of tools could do?