Skip to content

refactor: rename SN.isNormalizable to SN.normalizable - #736

Merged
chenson2018 merged 2 commits into
leanprover:mainfrom
awesome-lambda-calculus:sn_to_wn
Aug 9, 2026
Merged

refactor: rename SN.isNormalizable to SN.normalizable#736
chenson2018 merged 2 commits into
leanprover:mainfrom
awesome-lambda-calculus:sn_to_wn

Conversation

@lengyijun

@lengyijun lengyijun commented Jul 21, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

Reprove `SN.isNormalizable to move SN-related theorems adjacent

Old proof use Terminating.subtype_sn
New proof just by_cases (∃ y, r x y)

@lengyijun

lengyijun commented Jul 21, 2026

Copy link
Copy Markdown
Contributor Author

Hi @chenson2018
Thank you for reviewing my PR!
I'd like to make it easier for you to contribute changes directly. Could you please join awesome-lambda-calculus ?
Once you're a member, you'll be able to push commits directly to this PR's branch.

Our main goal is to verify the smallest basis of untyped lambda calculus.
We anticipate a large volume of code commits to the cslib infrastructure.

@chenson2018 chenson2018 self-assigned this Jul 25, 2026
chenson2018
chenson2018 reviewed Jul 25, 2026
View reviewed changes
Comment thread Cslib/Foundations/Relation/Confluence.lean Outdated
@lengyijun
lengyijun force-pushed the sn_to_wn branch 2 times, most recently from b1212c5 to e59c556 Compare July 26, 2026 00:20
@thomaskwaring

thomaskwaring commented Aug 9, 2026

Copy link
Copy Markdown
Collaborator

SN.isNormalizable already exists with precisely this signature

@lengyijun

lengyijun commented Aug 9, 2026

Copy link
Copy Markdown
Contributor Author

I have reproved SN.isNormalizable to make theorem related to sn adjacent

@chenson2018

chenson2018 commented Aug 9, 2026

Copy link
Copy Markdown
Collaborator

I have reproved SN.isNormalizable to make theorem related to sn adjacent

Can you update the title and description to reflect this?

@lengyijun lengyijun changed the title feat: Add lemma SN.to_WN: SN implies Normalizable refactor: reprove SN.isNormalizable to move SN-related theorems closer Aug 9, 2026
@lengyijun lengyijun changed the title refactor: reprove SN.isNormalizable to move SN-related theorems closer refactor: reprove SN.isNormalizable to move SN-related theorems adjacent Aug 9, 2026
@thomaskwaring

thomaskwaring commented Aug 9, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator

seems reasonable to me -- possibly the name should also be changed to SN.normalizable? (the current name is probably my mistake.) with a deprecation if that's the policy

@lengyijun lengyijun changed the title refactor: reprove SN.isNormalizable to move SN-related theorems adjacent refactor: rename SN.isNormalizable to SN.normalizable Aug 9, 2026
chenson2018
chenson2018 reviewed Aug 9, 2026
View reviewed changes
Comment thread Cslib/Foundations/Relation/Confluence.lean
thomaskwaring
thomaskwaring approved these changes Aug 9, 2026
View reviewed changes

@thomaskwaring thomaskwaring left a comment •
edited
Loading

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

minor style edits otherwise lgtm

Comment thread Cslib/Foundations/Relation/Confluence.lean
Comment thread Cslib/Foundations/Relation/Confluence.lean
@lengyijun
feat: Add lemma SN.to_WN: SN implies Normalizable
5fdc1f8 
`SN.to_WN (hx : SN r x) : Normalizable r x`

Proves that strong normalization implies weak normalization by induction
on the SN structure, constructing the normal form via the single reduction
step when a successor exists.
@chenson2018

chenson2018 commented Aug 9, 2026

Copy link
Copy Markdown
Collaborator

The rename also needs to be applied to other usages of this theorem, otherwise LGTM

@chenson2018
chenson2018 enabled auto-merge August 9, 2026 13:58
@chenson2018
chenson2018 added this pull request to the merge queue Aug 9, 2026
Merged via the queue into leanprover:main with commit 97722e0 Aug 9, 2026
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@chenson2018 chenson2018 chenson2018 approved these changes
@thomaskwaring thomaskwaring thomaskwaring approved these changes
@fmontesi fmontesi Awaiting requested review from fmontesi fmontesi is a code owner

Assignees

@chenson2018 chenson2018

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@lengyijun @thomaskwaring @chenson2018