feat(Logic): logical operators#607
Conversation
fmontesi
changed the title
| public import Cslib.Foundations.Logic.Operators.Not | ||
| public import Cslib.Foundations.Logic.Operators.Box | ||
| public import Cslib.Foundations.Logic.Operators.Diamond | ||
| public import Cslib.Foundations.Logic.Operators.Iff |
There was a problem hiding this comment.
Would it be better to just have one file for these? If they're just notation typeclasses it seems unlikely to be heavyweight and they're likely to be used together.
There was a problem hiding this comment.
I don't know yet. We will expand these files with extended classes for expected properties about these operators, but you're right that some will require importing more than one.. I think we'll know more once we get there.
There was a problem hiding this comment.
I propose 3 files:
Modalcontaining box and diamond.Tensorby itself.Propositionalfor the reset.
BTW, do we need parameterized box and diamond for HML?
The class was intentionally uninstantiated dead code. Its neg/top rationale (minimal-logic validity) now lives in the module docstring; formula types define neg/top as abbrevs directly. Future generic abstractions should use PR leanprover#607-style HasNeg/HasTop atomic classes. Session: sess_1781312776_63c955
The class was intentionally uninstantiated dead code. Its neg/top rationale (minimal-logic validity) now lives in the module docstring; formula types define neg/top as abbrevs directly. Future generic abstractions should use PR leanprover#607-style HasNeg/HasTop atomic classes. Session: sess_1781312776_63c955
Upstream PR landscape audit for Modal/ logic. No competing signature-change PRs. PR leanprover#607 stalled with CHANGES_REQUESTED. Recommends stacking Modal PR on feat/temporal-formula-propositional. Session: sess_1781531573_4cdbb4
Diplomatic PR description for Modal/ formula primitives refactoring, stacking on PR leanprover#648. Coordinates with PRs leanprover#607, leanprover#528, leanprover#535, leanprover#649. Session: sess_1781535860_c7d8e9
|
Hi @fmontesi — I wanted to flag some overlap with PR #648 so we can coordinate. PR #648 includes The main naming difference is A follow-up to #648 would refactor the Modal constructors from |
5 participants
This PR introduces typeclasses for logical operators (connectives and modalities) and refactors modal and propositional logics with appropriate instances to these.