feat(Logic): General Modal Logic

[fmontesi]

This PR adds general modal logic (Modal/Basic.lean), formalising the approach in the reference textbook 'Modal Logic' by Blackburn et al. based on similarity types (operator signatures). The formalisation is actually a bit more general: operator signatures are formalised using polynomial functors (PFunctor), so the argument positions of different operators can be of different types, and there are no assumptions on finiteness of operator arities.

Basic modal logic, unary modal logics, dynamic modal logics, and HML are all recovered as special cases that impose assumptions on the operator signature. This allows for reusing proof infrastructure across all modal logics. All tests have been accordingly refactored to check that reuse works as intended and that abstractions do not leak too aggressively across specialisations of general modal logic.

[Shreyas4991]

It seems the unary poly functor stuff is useful even beyond modal logic and could be factored into a separate PR. This would shorten this PR.

[Shreyas4991]

This PR seems a bit large. Maybe this API for PFunctors could be a separate PR. It seems fairly straightforward merge.

[fmontesi]

Agreed in general. In this case, I've left it here primarily because I wanna make sure that this API is in sync with the modal signature development.

[XYUnknown]

I have not found anything wrong, the only technical concern is axiom T and and B in Cslib/Logics/Modal/Semantics.lean may be able to be generalised without the need of PropositionMap.const --- it is unclear to me why this restriction is needed in the first place. Though it can be a separate pr as this pr is already big.

Some concepts in the generalised frame can be explained better, sometimes it's non-trivial to figure out the exact correspondence between the Lean code and the defintion in the literature.