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.

Co-authored-by: Thomas Waring thomas.waring99@gmail.com

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.

…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

This PR proves the standardization theorem: if `M` beta-reduces to `N` in any number of steps, then `N` is reachable from `M` by a standard reduction. Builds on #671. --------- Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com> Co-authored-by: Chris Henson <chrishenson.net@gmail.com>

If a term is locally closed at level `i` and `i ≤ j`, then it is also locally closed at level `j`. --------- Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>

This PR refactors the cslib bench suite so it closely resembles mathlib's again, following leanprover-community/mathlib4#41587.

- Redefine `multiApp` as right-recursive (`multiApp (app f a) as`) instead of left. - Switch several inductions to `List.reverseRecOn` for compatibility with the new recursion. - Add `listFullBeta_cons_r`/`listFullBeta_cons_l`/`multiApp_tail` helpers. - Update related proofs Fixes #706 --------- Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>

… fairness properties (#612) This PR contains some technical machineries for reasoning about diamond and fairness properties about the distributed algorithms introduced in #556: * `CanReachVia.lean` defines the notion of reachability via a subset of processes and proves some of its properties, including some diamond properties. * `FairScheduler.lean` contains a technical machinery for constructing fair executions, which will be used in formalizing some arguments which were either only hinted at or completely glossed over in Völzer's paper. Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/513188-CSLib/topic/Impossibility.20of.20distributed.20consensus/with/592462001

This tweak brings the bench suite more in line with the other repos. It should not affect functionality. Follow-up to #707.

Addresses #638. Converts the global well-formed notation to a macro with a `noWs` whitespace guard. This explicitly prevents the postfix parser from greedily consuming the `✓` token across line breaks, resolving the syntax collision with TimeM's prefix tick notation when both modules are imported simultaneously. --------- Co-authored-by: Sean Stoneburner <litholight@gmail.com> Co-authored-by: Chris Henson <chrishenson.net@gmail.com>

… are regular (#720) Prove languages matching regular expressions are regular in IsRegular.regex. The proof uses existing theorems IsRegular.add, IsRegular.mul, and IsRegular.kstar. Prove remaining key ingredient that the language containing only the one character string is regular in IsRegular.char. Implemented collaboratively by Brooke Gill and Chi-Yun Hsu --------- Co-authored-by: Chi-Yun Hsu <chiyunhsu@users.noreply.github.com> Co-authored-by: Brooke Gill <96643991+brooke-gill@users.noreply.github.com>

… OmegaLanguage (#722) This PR proves some consequences of an empty alphabet type (denoted by `Symbol`) on Language and OmegaLanguage: (1) The only possible languages over an empty alphabet are {} and {[]}. (2) The only possible omega-language over an empty alphabet is {}. Furthermore, (1) enables the assumption `[Inhabited Symbol]` to be removed from the regular language closure properties `IsRegular.mul` and `IsRegular.kstar`. Now no closure property for regular languages has that assumption.

Co-authored-by: mathlib-nightly-testing[bot] <258991302+mathlib-nightly-testing[bot]@users.noreply.github.com> Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: leanprover-community-mathlib4-bot <129911861+leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: Chris Henson <chrishenson.net@gmail.com> Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com> Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com> Co-authored-by: Ching-Tsun Chou <chingtsun.chou@gmail.com> Co-authored-by: Alexandre Rademaker <arademaker@gmail.com> Co-authored-by: Fabrizio Montesi <famontesi@gmail.com>

This PR adds README files to some of the main source code directories, covering explanations on principles and vision for CSLib that I've found myself repeating often in private and public conversations. --------- Co-authored-by: Fabrizio Montesi <fabrizio.montesi@pm.me>

Bump `mathlib` dependency to [d99d52c](leanprover-community/mathlib4@d99d52c): chore(Data): rename `setOf` to `Set.ofPred` (#41507) (2026-07-17) Previously at: [79d0395](leanprover-community/mathlib4@79d0395): chore: bump toolchain to v4.33.0-rc1 (#41779) (2026-07-16) Closes #727 Failure log from the validation run: [download](https://github.com/leanprover-community/downstream-reports/actions/runs/29592162806/artifacts/8412435005) _(link expires after 1 year)_ --- This PR bumps `mathlib` to an identified incompatible (first-known-bad) commit (`d99d52c`) so you can reproduce and fix the incompatibility locally by checking out this branch. _Opened automatically by [downstream-reports/track-incompatibility](https://github.com/leanprover-community/downstream-reports) via [this workflow run](https://github.com/leanprover/cslib/actions/runs/29610863999)._ --------- Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com> Co-authored-by: Chris Henson <chrishenson.net@gmail.com>

)

Bump `mathlib` dependency to [169c26b](leanprover-community/mathlib4@169c26b): refactor: rename restrict to domRestrict (#25980) (2026-07-20) Previously at: [d99d52c](leanprover-community/mathlib4@d99d52c): chore(Data): rename `setOf` to `Set.ofPred` (#41507) (2026-07-17) Closes #732 Failure log from the validation run: [download](https://github.com/leanprover-community/downstream-reports/actions/runs/29755881109/artifacts/8467297013) _(link expires after 1 year)_ --- This PR bumps `mathlib` to an identified incompatible (first-known-bad) commit (`169c26b`) so you can reproduce and fix the incompatibility locally by checking out this branch. _Opened automatically by [downstream-reports/track-incompatibility](https://github.com/leanprover-community/downstream-reports) via [this workflow run](https://github.com/leanprover/cslib/actions/runs/29776447755)._ --------- Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com> Co-authored-by: Chris Henson <chrishenson.net@gmail.com>

…cceeded) Tasks completed: 393, 449 Tasks failed: 2 (535 partial 2/5 phases, 425 blocked plan-revision; see multi-state log) Tasks skipped: 1 (497 blocked by failed predecessors + external PR leanprover#607) Session: sess_1784888487_837ef1 Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Fa6AeJ7Df9zCQ5hRFy5qPk

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

Comment thread Cslib/Logics/Propositional/Defs.lean Outdated

m-ow and others added 17 commits July 22, 2026 14:06

feat(LocallyNameless/Untyped): new theorem lcAt_le (#699)

6d1e639

If a term is locally closed at level `i` and `i ≤ j`, then it is also locally closed at level `j`. --------- Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>

chore: update bench suite (#707)

8db7536

This PR refactors the cslib bench suite so it closely resembles mathlib's again, following leanprover-community/mathlib4#41587.

chore: bump toolchain to v4.32.0 (#717)

19f6420

chore: tweak bench suite (#715)

da9c47c

This tweak brings the bench suite more in line with the other repos. It should not affect functionality. Follow-up to #707.

chore: fix (all) backward.isDefEq.respectTransparency exceptions (#729

bb3fc4c

)

fix grind? issue

b5a1ef6

instance refactor

8cbaec9

fmontesi requested review from kim-em and sorrachai as code owners July 22, 2026 12:23

fmontesi added 2 commits July 22, 2026 14:29

Merge branch 'main' into fmontesi/connectives

36b9f80

dynamic syntax docstring fix

552d40e

fmontesi mentioned this pull request Jul 29, 2026

feat(Logic): improvements to the inference system and congruence frameworks, with associated refactorings #753

Open

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 42 commits into
mainfrom
fmontesi/connectives

fmontesi commented May 29, 2026 •

edited

Loading

Uh oh!

Uh oh!

Uh oh!

Uh oh!

benbrastmckie commented Jun 17, 2026

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

12 participants

Uh oh!

Conversation

fmontesi commented May 29, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

benbrastmckie commented Jun 17, 2026

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

12 participants

fmontesi commented May 29, 2026 •

edited

Loading