feat(Logic): improvements to the inference system and congruence frameworks, with associated refactorings - #753
Open
fmontesi wants to merge 48 commits into
Open
feat(Logic): improvements to the inference system and congruence frameworks, with associated refactorings#753fmontesi wants to merge 48 commits into
fmontesi wants to merge 48 commits into
Conversation
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>
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>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
9 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR introduces several improvements to the frameworks based on
InferenceSystemandCongruence.InferenceSystem.Default⇓ais now pretty-printed to⇓a(which is what users write).DefaultCongruenceclass to define the 'canonical' congruence for a type.LawfulCongruence).Contextby making the term type parameter implicit.LogicalEquivalenceinCslibTests. Both a manual proof based on contexts and one based on grind are provided. In the future, we should explore ways to plug such rewritings into Lean's and Mathlib's frameworks for congruences (perhaps by autogenerating lemmas and/or checks from inductive types).The PR also refactors CLL, HML, and Modal Logic to be in line with all these recent developments. This is a step towards the formulation of general patterns for modal logics (left to future work).
Some tests to prevent future breakage are introduced as well.
Depends on #607.