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 |
There was a problem hiding this comment.
I'd suggest merging all these operators into a single LogicOperators file, since then you can give one docstring that summarizes the conventions of their meanings.
| @[inherit_doc] scoped infix:35 " ∨ " => Proposition.or | ||
| @[inherit_doc] scoped infix:30 " → " => Proposition.impl | ||
| @[inherit_doc] scoped prefix:40 " ¬ " => Proposition.neg | ||
| instance : HasAnd (Proposition Atom) := {and := Proposition.and} |
There was a problem hiding this comment.
A little cleaner as
| instance : HasAnd (Proposition Atom) := {and := Proposition.and} | |
| instance : HasAnd (Proposition Atom) where and := .and |
etc
| induction ctx <;> grind [= Context.fill] | ||
|
|
||
| noncomputable instance : LogicalEquivalence (Proposition Atom) (Sequent Atom) Proof where | ||
| noncomputable instance : HasLogicalEquivalence (Proposition Atom) (Sequent Atom) where |
There was a problem hiding this comment.
Note that the Has prefix is largely a Lean 3-ism.
…#648 refresh Recreates the four tasks lost during the main cleanup, aligned with Thomas Waring's closing recommendation in the CSLib Zulip "Propositional Logic" thread (606970606) and our synthesis decision: - 398 efq_nd_rule_ipl_base_keep_mpl: make IPL the base logic (efq as a primitive ND rule) while PRESERVING all completed MPL metatheory as a retained layer. Depends on 397 (green main). - 399 refresh_pr648_ipl_base_foundation: update PR leanprover#648 to the settled IPL-base foundation (refs + Zulip link), small + upstream-based cherry pick, connectives excluded. Depends on 398. - 400 reconcile_connectives_pr607: unbundle connectives, reconcile with fmontesi PR leanprover#607 (Waring flag a). - 401 polymorphic_evaluator_bool_prop_dpll: AlgEvaluate at Bool/Prop for DPLL (Doty/Waring). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01NarRy36MgZCZP7TRsrL5Df
6 participants
This PR introduces typeclasses for logical operators (connectives and modalities) and refactors modal and propositional logics with appropriate instances to these.