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.

Sign up for GitHub

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

Jump to bottom

Add some multiset-related lemmas #1329

Open
wants to merge 4 commits into
base: main
Choose a base branch
from
Open

Add some multiset-related lemmas #1329

wants to merge 4 commits into from

Commits on Oct 30, 2024

  1. prove theorem about fold_right over permutations 

    For a commutative fold_right operator, any folding order (i.e., folding
over any permutation of a sequence) produces the same result.
    @zeldovich
    zeldovich committed Oct 30, 2024
    Configuration menu
    Copy the full SHA
    4e67ff6 View commit details
    Browse the repository at this point in the history

  2. add the converse of lemma_multiset_has_no_duplicates

    @zeldovich
    zeldovich committed Oct 30, 2024
    Configuration menu
    Copy the full SHA
    3d3028e View commit details
    Browse the repository at this point in the history

  3. make verusfmt happy

    @zeldovich
    zeldovich committed Oct 30, 2024
    Configuration menu
    Copy the full SHA
    bb7ec6b View commit details
    Browse the repository at this point in the history

  4. make some more seq lemmas public 

    lemma_fold_right_split (formerly aux_lemma_fold_right_alt) is a useful
lemma in its own right about how fold_right distributes over splitting
a sequence into two parts using subrange.

lemma_fold_right_commute_one is also useful for proofs that need to
commute the order of operations in fold_right, in a way that's not quite
about permutations.
    @zeldovich
    zeldovich committed Oct 30, 2024
    Configuration menu
    Copy the full SHA
    2e7ddb1 View commit details
    Browse the repository at this point in the history