feat(Logic): logical operators by fmontesi · Pull Request #607 · leanprover/cslib

fmontesi · 2026-05-29T12:56:23Z

This PR introduces typeclasses for logical operators (connectives and modalities) and refactors modal and propositional logics with appropriate instances to these.

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

benbrastmckie · 2026-06-17T21:34:59Z

Hi @fmontesi — I wanted to flag some overlap with PR #648 so we can coordinate.

PR #648 includes Connectives.lean with a single-file approach to connective typeclasses (HasBot, HasImp, HasAnd, HasOr), following @chenson2018's consolidation suggestion. A planned Modal follow-up would extend it with HasBox/ModalConnectives.

The main naming difference is HasImpl/impl here vs HasImp/imp in #648. I went with imp for consistency with FormalizedFormalLogic and the rule name prefix convention (impI/impE), but happy to align whichever way you and other reviewers prefer.

A follow-up to #648 would refactor the Modal constructors from {atom, not, and, diamond} to {atom, bot, imp, box}. The case for primitive bot is in this Zulip message (substitution invariance, free algebra property). Related reasoning favors primitive box: necessitation becomes a pure rule — ⊢ φ → ⊢ □φ — stated in terms of box alone, rather than an interaction rule requiring dia and neg, or dia, bot, and imp. This would affect how typeclass instances are written. I'd welcome your input on this issue and will post on the Modal Zulip thread.

eric-wieser · 2026-06-19T23:07:51Z

-@[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}


A little cleaner as

Suggested change

instance : HasAnd (Proposition Atom) := {and := Proposition.and}

instance : HasAnd (Proposition Atom) where and := .and

etc

I'd even use

instance : HasAnd (Proposition Atom) := ⟨.and⟩

What do you think, @eric-wieser, @thomaskwaring?

…anprover#662 on leanprover#607 Rework PR leanprover#662's modal-logic contribution to stack cleanly on PR leanprover#607 (fmontesi/connectives), whose head already provides the consolidated HasBox/HasDiamond/... operator typeclasses in Cslib/Foundations/Logic/Operators.lean. On this base, Proposition was {atom, not, and, diamond} with box derived as ¬◇¬φ. This commit adds box as a fifth primitive constructor so both modalities are primitive, and turns the interdefinability law into a derived theorem. - Basic.lean: add `| box (φ : Proposition Atom)` to the Proposition inductive; add the matching `Satisfies` clause `∀ w', m.r w w' → Satisfies m w' φ`; point HasBox at the new constructor; reduce `Satisfies.box_iff_forall` to `Iff.rfl`; prove `Satisfies.dual : ◇φ ↔ ¬□¬φ` as a genuine classical theorem from the two now-independent primitive semantic clauses (was previously definitional); add companion `Satisfies.box_iff_not_diamond_not`. - Denotation.lean: add the box denotation clause `{w | ∀ w', m.r w w' → w' ∈ φ.denotation m}`. - LogicalEquivalence.lean: add the `box` `Proposition.Context` constructor, its `fill` clause, and the matching `Congruence` induction case. No duplicate Connectives.lean exists on this branch (leanprover#607's Operators.lean is already the sole source of these typeclasses), so no deletion was needed there. Net diff vs ddc2c9b (the leanprover#607 head this branch is built on): 3 files changed, +39/-17 (net +22 LOC). Zero sorry, zero new axioms. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015tcPjCXNeSAzBxWeFYsZM5

Tasks created from the review sweep of cslib PRs leanprover#648, leanprover#607, leanprover#662 and the Propositional/Modal Logic Zulip threads. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Research how to divide overlapping PRs leanprover#607/leanprover#648/leanprover#649/leanprover#662, review leanprover#607 to help it land, and base leanprover#662 on leanprover#607's operator layer. Depends on 475. Session: sess_1783038723_6ac05b

Draft leanprover#607 review + Zulip coordination note; stopped at HOLD gate by design. Phases 3-5 gated on explicit user approval and upstream design agreement. Session: sess_1783080383_2227b3

…tribution option New gated Phase 4: prepare connectives-bundles PR (base=fmontesi/connectives, head=own in-org branch) offering HasBot + bundles; he controls the merge. Migration phases renumbered 5-6. Phases 1-2 preserved [COMPLETED]. Session: sess_1783085247_e251b8

Drop praise/over-explanation; peer-level tone for a maintainer. Session: sess_1783085247_e251b8

Session: sess_1783085247_e251b8

Drop bundling/naming duplication (carried by leanprover#607 comment); keep friendly tone. Session: sess_1783085247_e251b8

Session: sess_1783085247_e251b8

CI failure is leanprover#607's own LogicalEquivalence parametrisation breaking HML/LogicalEquivalence.lean (old signature), not main drift — so the "just rebase" claim was wrong. Point dropped; banner re-verify note corrected. Session: sess_1783085247_e251b8

…sole live gated item Posted comment 4837502740 (2026-06-29) already carries the substantive leanprover#607 coordination (verified accurate vs current leanprover#607/leanprover#648 heads). Zulip note re-verified accurate (modal constructors, CI-green, leanprover#649). Nothing posted. Session: sess_1783085247_e251b8

…tor complete, CI blocked by pre-existing leanprover#607 defect Phases 1-4 and 6 of the PR-662-stacks-on-PR-607 plan are complete on a new local branch task-477-pr662-stack-607 (based on pr607, worktree /home/benjamin/Projects/cslib-task-477-pr662-stack-607): box added as a fifth primitive Proposition constructor alongside diamond, net +49 LOC, zero sorry, zero new axioms, scoped lake build/lint-style green. Phase 5's whole-library CI gate is blocked by a pre-existing, out-of-scope defect in PR leanprover#607's own HML/LogicalEquivalence.lean (confirmed via git-stash isolation, unrelated to Modal/leanprover#662). Status set to partial pending either an upstream leanprover#607 fix or a follow-up task to migrate HML/LogicalEquivalence.lean to the new HasLogicalEquivalence API. Session: sess_1783880050_660057

Modal refactor complete on branch task-477-pr662-stack-607 (+49 LOC, zero sorry). Phase 5 whole-library CI blocked by pre-existing external defect in PR leanprover#607's HML/LogicalEquivalence.lean (not a leanprover#662 defect). Session: sess_1783880050_660057

…in Zulip draft Task 485: migrate Cslib/Logics/HML/LogicalEquivalence.lean to leanprover#607's 4-arg HasLogicalEquivalence API (blocks whole-library CI on pr607). Zulip coordination draft updated with the discovered-issue note and a collaborative heads-up clause to fmontesi. Session: sess_1783880050_660057

Ground-truth: leanprover#607 commit 059a85c parametrised the LogicalEquivalence class to 4-arg but left HML/LogicalEquivalence.lean:105 on the old 3-arg instance. Dropped the unverified 'Modal and CLL migrated' phrasing. Session: sess_1783880050_660057

Verified against live PR leanprover#607 (head ddc2c9b, branch fmontesi/connectives): CI is green and fmontesi already fixed HML (commit 77ce0c7, 2026-07-07). The 'defect' was an artifact of a STALE local pr607 branch (c2ec296), an ancestor of the live head missing 5 PR commits. leanprover#607 is blocked on code review (CHANGES_REQUESTED), not on any build failure. Session: sess_1783880050_660057

Verified against upstream: all three user PRs (leanprover#648/leanprover#662/leanprover#649) are already rebased onto latest upstream/main (056cf93, leanprover#708), 0 behind, and CI-green. leanprover#485's HML fix is redundant with fmontesi's live leanprover#607 commit 77ce0c7. Session: sess_1783880050_660057

…ed on leanprover#607 - leanprover#662 force-pushed: box primitive alongside diamond, base -> fmontesi/connectives, clean 3-file/+22 LOC diff on live leanprover#607, full build+test green. - leanprover#648/leanprover#649 kept independent on main (propositional-type design deferred to Zulip coordination: primitive-bot vs bot-via-atom). - Zulip draft revised to accurate final state + raises the propositional-type question. Session: sess_1783880050_660057

…acking to leanprover#607 direction Abandon 468/469/475 (superseded by leanprover#607 pivot in task 477), close 476 (coordination delivered), refine 486 (make leanprover#648-independence + leanprover#607 Operators typeclass-port explicit). leanprover#662 stacks on leanprover#607; leanprover#648 stays independent pending propositional-basis decision. Session: sess_1783891789_95c9f3

…on on leanprover#607 Option A delivered on worktree branch task-486-pr662-modal-package (commit 4ebdba54, off live PR head 70b7ec4): Cube.lean +69 (b/four/ five/d validity + canonicity section), references.bib +11. Zero sorry/ axioms; full lake build 2759/2759 + test 8790/8790 green. Not pushed. Research corrected the brief premise (leanprover#607 already ships the semantic cube); scope narrowed to the non-duplicative completion work. Session: sess_1783891828_7982f5

…#662 PR body 5 correspondence iffs (T/B/4/5/D) on branch task-487-pr662-bot-primitive (b041c6f7); Cube.lean +55; zero sorry/axioms; build+test green. Updated leanprover#662 PR body drafted. Final leanprover#662 diff vs leanprover#607: +233/-56, 6 files. Session: sess_1783903472_6dffde

…ne patch Zulip message proposing modal Proposition fully-primitive base to leanprover#607 (decision-his/labor-yours, semantic tradeoff acknowledged, metalogic- motivated, leanprover#648 propositional-bot tie-in). Standalone leanprover#607 patch extraction dispatched. Session: sess_1783903472_6dffde

…eanprover#607 patch) Standalone base-reshape patch off leanprover#607 (branch modal-base-reshape-onto-607, c2e37e20): +98/-56, 4 files, NO cube; leanprover#607 Cube.lean byte-identical and builds green (2759/2759); zero sorry/axioms. Zulip draft ready. Both maintainer-facing, not pushed. Session: sess_1783903472_6dffde

…r slice, CI verification Verified live PR leanprover#662/leanprover#607 state (both MERGEABLE, CI green); confirmed the native-primitive slice (Basic.lean 63-283+430-441, Denotation.lean 24-90) is sorry-free on this branch. Discovered lines 285-428 (T/B/4/5/D frame axioms) are load-bearing for Cube.lean and 8 Metalogic Soundness files on this branch, so the slice was assembled as extraction artifacts under specs/498_.../artifacts/pr-662-slice/ rather than editing the live shared Basic.lean in place. Ran the full CSLib CI pipeline (cache, scoped+full build, checkInitImports, lint, lint-style, test, mk_all, shake) plus lean_verify axiom checks on Satisfies.dual/.k and satisfies_mem_denotation: sorry_count 0, zero new axioms, all standard classical only. Session: sess_1783965646_4b3ee1

…e (native primitives) Squash-commit of the ~386 LOC foundational semantic layer slice for PR leanprover#662, built on the native 7-primitive Proposition {atom, bot, imp, and, or, box, diamond}: Satisfies/denotation, duality theorem (Satisfies.dual), per-connective decomposition (Iff.rfl), K-axiom validity (Satisfies.k), denotation bridge (satisfies_mem_denotation), and valid/logic. Extracted faithfully from Cslib/Logics/Modal/Basic.lean (lines 63-283, 430-441) and Cslib/Logics/Modal/Denotation.lean (lines 24-90) on task-441-native-refactor, EXCLUDING the T/B/4/5/D frame-correspondence axioms (Basic.lean 285-428; deferred to a later "systems" PR). sorry-free; axioms limited to propext/Classical.choice/Quot.sound (standard classical only, used by Satisfies.dual and satisfies_mem_denotation via excluded middle). Committed as extraction artifacts under specs/498_.../artifacts/pr-662-slice/ rather than directly to Cslib/Logics/Modal/ -- see Phase 1/2 plan notes: the live Basic.lean's frame-axiom lines are load-bearing for Cube.lean and 8 Metalogic Soundness files on this shared task-441-native-refactor branch, so this squash-commit is prepared content for the actual leanprover#662 head branch (feat/modal-formula-primitives), not a direct edit of the live library files. GATED: push/re-stack of the real leanprover#662 branch is deferred until PR leanprover#607 adopts the native primitive set (fmontesi back 23 July); this commit is LOCAL only, not pushed. Fallback if leanprover#607 declines: restore backup/662-pre-rework-jul13 (the pre-rework trivial box-alongside- diamond delta) or convert to a standalone non-stacked contribution. ## AI Tools Used This commit was prepared with the assistance of Claude Code (Anthropic). The AI tool was used for extracting and verifying the foundational-semantic-layer slice from the task-441 native modal refactor, running CI verification commands, and drafting this commit message. All Lean code was authored by the task-441 development (Benjamin Brast-McKie et al.) and verified to compile cleanly (sorry-free, standard classical axioms only) on this branch. Session: sess_1783965646_4b3ee1

…se zulip-coordination draft Phase 5: wrote specs/498_.../artifacts/pr-607-recommendation.md, a DRAFT comment-only recommendation that leanprover#607 adopt the native modal primitive set {atom, bot, imp, and, or, box, diamond}, with a three-point justification (per-connective Iff.rfl decomposition, IK/CK reuse, duality as theorem), typeclass instances entailed, naming-reconciliation flags (HasDia vs HasDiamond; HasBot absent in Operators.lean), and a proof-theoretic-weight reassurance. Carries a DRAFT + comment-only + user-approval + never-push-to-fmontesi/connectives banner. Not posted. Phase 6: revised specs/476_.../artifacts/zulip-coordination.md to replace the superseded box-alongside-diamond framing (~40-line delta) with the native-primitives recommendation to leanprover#607 plus a description of leanprover#662 as a substantial ~386-line foundational semantic-layer slice. Preserved the accuracy-discipline preamble and both open items (leanprover#648 propositional-base decision, imp/impl naming for task 497); added the HasDia/HasDiamond naming divergence to the same follow-up. DRAFT banner intact; not posted. Session: sess_1783965646_4b3ee1

Execution summary, final .return-meta.json, and orchestrator handoff for task 498. All 6 plan phases COMPLETED: verified live PR leanprover#607/leanprover#662 state, assembled the foundational semantic layer slice as extraction artifacts, ran the full CSLib CI pipeline (sorry_count 0, zero new axioms, standard classical axioms only), squash-committed the slice locally, prepared the comment-only leanprover#607 recommendation draft, and revised the zulip-coordination draft. No push performed anywhere; both drafts carry DRAFT + explicit-user-approval banners. Session: sess_1783965646_4b3ee1

Reworked PR leanprover#662 into a self-contained ~300 LOC native-primitive foundational semantic layer slice of the task-441 modal metalogic. Full CI green, zero-debt (0 sorries, 0 new axioms). Local squash-commit created (not pushed); push/re-stack gated on leanprover#607 adopting native primitives. leanprover#607 recommendation and revised task-476 zulip-coordination prepared as DRAFTs (not posted, await user approval). Cycles: 3/5 (research -> plan -> implement) Session: sess_1783963625_6aa0c8

Fabrizio Montesi and others added 6 commits May 21, 2026 14:48

Logical operators

31fb1ca

PL connectives, start modal

31dcc0e

fix not_def

060954e

fix modal connectives

2f4b4c9

Merge branch 'main' into fmontesi/connectives

1024345

indirection in _def lemmas

d4410e3

fmontesi requested a review from chenson2018 as a code owner May 29, 2026 12:56

fmontesi changed the title ~~feat (Logic): logical operators~~ feat(Logic): logical operators May 29, 2026

update cslib.lean

63918a2

chenson2018 requested changes May 29, 2026

View reviewed changes

Comment thread Cslib/Logics/Modal/Basic.lean Outdated

Comment thread Cslib/Logics/Modal/Basic.lean Outdated

Comment thread Cslib/Logics/Modal/Basic.lean Outdated

ctchou mentioned this pull request Jun 12, 2026

refactor: Proposition type to bot/imp primitives #635

Closed

This was referenced Jun 14, 2026

feat(Logics/Propositional): five-primitive formula type with connective typeclasses #647

Closed

feat(Logics/Propositional): five-primitive formula type with primitive bot #648

Open

Fabrizio Montesi added 3 commits June 16, 2026 08:34

merge main

500a9d9

merge main again

9669f24

fix compilationg

604ba15

fmontesi requested a review from arademaker as a code owner June 16, 2026 06:37

Fabrizio Montesi and others added 5 commits June 16, 2026 08:52

fix some proofs

20b4a92

fix simp lints

c7e5a4c

merge main

abf73e5

parametrised logical equivalence

059a85c

grind annotation for not

c2ec296

benbrastmckie mentioned this pull request Jun 19, 2026

feat(Logics/Modal): semantics for the modal metalogic, compatible with constructive modal theories #662

Draft

eric-wieser reviewed Jun 19, 2026

View reviewed changes

Comment thread Cslib/Foundations/Logic/Operators/And.lean Outdated

eric-wieser reviewed Jun 19, 2026

View reviewed changes

benbrastmckie added a commit to benbrastmckie/cslib that referenced this pull request Jul 18, 2026

task 465: draft PR leanprover#607 review comment

293d7ac

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

benbrastmckie added a commit to benbrastmckie/cslib that referenced this pull request Jul 18, 2026

task 476: tighten leanprover#607 review draft to essentials

b07155a

Drop praise/over-explanation; peer-level tone for a maintainer. Session: sess_1783085247_e251b8

benbrastmckie added a commit to benbrastmckie/cslib that referenced this pull request Jul 18, 2026

task 476: trim leanprover#607 review CI note to one line

879b418

Session: sess_1783085247_e251b8

benbrastmckie added a commit to benbrastmckie/cslib that referenced this pull request Jul 18, 2026

task 476: reorder leanprover#607 review — CI note last

12cd7af

Session: sess_1783085247_e251b8

benbrastmckie added a commit to benbrastmckie/cslib that referenced this pull request Jul 18, 2026

task 476: pare down Zulip note to split + box-vs-diamond

39b57da

Drop bundling/naming duplication (carried by leanprover#607 comment); keep friendly tone. Session: sess_1783085247_e251b8

benbrastmckie added a commit to benbrastmckie/cslib that referenced this pull request Jul 18, 2026

task 476: unwrap leanprover#607 review lines for paste-ready draft

62275c4

Session: sess_1783085247_e251b8

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

feat(Logic): logical operators#607

feat(Logic): logical operators#607
fmontesi wants to merge 23 commits into
mainfrom
fmontesi/connectives

fmontesi commented May 29, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

benbrastmckie commented Jun 17, 2026

Uh oh!

Uh oh!

eric-wieser Jun 19, 2026

Uh oh!

fmontesi Jul 7, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

	instance : HasAnd (Proposition Atom) := {and := Proposition.and}
	instance : HasAnd (Proposition Atom) where and := .and

Uh oh!

Conversation

fmontesi commented May 29, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

benbrastmckie commented Jun 17, 2026

Uh oh!

Uh oh!

eric-wieser Jun 19, 2026

Choose a reason for hiding this comment

Uh oh!

fmontesi Jul 7, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants