Skip to content

Comments

feat: Rename List.reverse_perm to List.reverse_perm_self and List.reverse_perm' to List.reverse_perm_iff#33276

Open
NicolaBernini wants to merge 5 commits intoleanprover-community:masterfrom
NicolaBernini:feat/reverse-perm-to-reverse-perm-self-rename
Open

feat: Rename List.reverse_perm to List.reverse_perm_self and List.reverse_perm' to List.reverse_perm_iff#33276
NicolaBernini wants to merge 5 commits intoleanprover-community:masterfrom
NicolaBernini:feat/reverse-perm-to-reverse-perm-self-rename

Conversation

@NicolaBernini
Copy link

@NicolaBernini NicolaBernini commented Dec 25, 2025


Open in Gitpod

@github-actions github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Dec 25, 2025
@github-actions
Copy link

github-actions bot commented Dec 25, 2025

PR summary a36c84ab82

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ reverse_perm_iff
+ reverse_perm_self
- reverse_perm'

You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.


No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

Copy link
Contributor

@Ruben-VandeVelde Ruben-VandeVelde left a comment

Choose a reason for hiding this comment

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

I'm afraid this isn't what was intended - or at least only part of it. The renaming would need to be done in the lean4 repository first.

However, I'm not convinced that would be a good change anyway. Instead, I suggest two renames below that I think make more sense. Tagging @Paul-Lez who added the TODO in #22977.

If you make this change, please make sure to update the PR title.

simp only [reverseAux_eq, map_append, map_reverse]

-- TODO: Rename `List.reverse_perm` to `List.reverse_perm_self`
@[simp] lemma reverse_perm' : l₁.reverse ~ l₂ ↔ l₁ ~ l₂ where
Copy link
Contributor

Choose a reason for hiding this comment

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

This to reverse_perm_iff

mp := l₁.reverse_perm_self.symm.trans
mpr := l₁.reverse_perm_self.trans

@[simp] lemma perm_reverse : l₁ ~ l₂.reverse ↔ l₁ ~ l₂ where
Copy link
Contributor

Choose a reason for hiding this comment

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

And this to perm_reverse_iff

@Ruben-VandeVelde
Copy link
Contributor

And most importantly: thanks for the contribution!

@Ruben-VandeVelde Ruben-VandeVelde added the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 29, 2025
…b.com:NicolaBernini/mathlib4 into feat/reverse-perm-to-reverse-perm-self-rename
@NicolaBernini NicolaBernini changed the title feat: Renaming List.reverse_perm to List.reverse_perm_self feat: Rename List.reverse_perm to List.reverse_perm_self and List.reverse_perm' to List.reverse_perm_iff Jan 2, 2026
@joneugster joneugster added the t-data Data (lists, quotients, numbers, etc) label Feb 1, 2026
@mathlib-merge-conflicts
Copy link

This pull request has conflicts, please merge master and resolve them.

@mathlib-merge-conflicts mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 18, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

awaiting-author A reviewer has asked the author a question or requested changes. merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-data Data (lists, quotients, numbers, etc)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants