Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add list lemmas and shorten some other proofs using them #721

Merged
merged 1 commit into from
Feb 20, 2025
Merged

Conversation

MM45
Copy link
Contributor

@MM45 MM45 commented Feb 20, 2025

I needed some of these lemmas for a recent project and thought I would add them + try to shorten other proofs using them where possible.
The main result here that is useful to me is the uniq_le_perm_eq lemma, which seems to encompass the other lemmas that are there currently, provided you also have the perm_eq_uniq_impl lemma. I know that these are derivable from the present lemmas, but this is not directly obvious (at least it wasn't to me). And I would say this is especially so since the lemma that currently comes closest to uniq_le_perm_eq, which is uniq_perm_eq_size, uses more and stronger hypotheses than necessary (see the new proof, which clears one of the hypotheses and does not much more than directly applying a lemma with weaker hypothesis).
The other, smaller lemmas on drop and behead I included have simply been annoying me in proofs (their absence, that is).

@strub
Copy link
Member

strub commented Feb 20, 2025

Hi. Squash your commits and we are good to go.

@MM45 MM45 enabled auto-merge (squash) February 20, 2025 13:32
@fdupress
Copy link
Member

Nah, squash by hand and force push, please.

This gives you the opportunity to check that the squashing happened right—and more importantly to pick the commit message for the squashed commit!

@MM45
Copy link
Contributor Author

MM45 commented Feb 20, 2025

Alrighty, will do. But this auto-merging also lets you pick the commit message!

@MM45 MM45 disabled auto-merge February 20, 2025 13:52
@fdupress fdupress self-requested a review February 20, 2025 14:08
@MM45 MM45 merged commit b91e29c into main Feb 20, 2025
15 checks passed
@MM45 MM45 deleted the add-list-lemmas branch February 20, 2025 14:34
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants