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

feat: verify insertMany method for adding lists to HashMaps #6211

Draft
wants to merge 40 commits into
base: master
Choose a base branch
from
Draft

feat: verify insertMany method for adding lists to HashMaps #6211

wants to merge 40 commits into from
+1,956 −20

Commits on Nov 27, 2024

  1. Model function for insertManyList

    @jt0202 @monsterkrampe
    jt0202 authored and monsterkrampe committed Nov 27, 2024
    Configuration menu
    Copy the full SHA
    05b86d2 View commit details
    Browse the repository at this point in the history

  2. Verified insertManyList_contains for Raw0

    @jt0202 @monsterkrampe
    jt0202 authored and monsterkrampe committed Nov 27, 2024
    Configuration menu
    Copy the full SHA
    ea17bbb View commit details
    Browse the repository at this point in the history

  3. verified InsertList together with insert/size

    @jt0202 @monsterkrampe
    jt0202 authored and monsterkrampe committed Nov 27, 2024
    Configuration menu
    Copy the full SHA
    ed56c5e View commit details
    Browse the repository at this point in the history

  4. Renamed List.insertMany to List.insertList and added Perm result for … 

    …Raw0.insertList
    @jt0202 @monsterkrampe
    jt0202 authored and monsterkrampe committed Nov 27, 2024
    Configuration menu
    Copy the full SHA
    db8a642 View commit details
    Browse the repository at this point in the history

  5. Use simp_to_model for insertList_contains

    @monsterkrampe
    monsterkrampe committed Nov 27, 2024
    Configuration menu
    Copy the full SHA
    2aecd5a View commit details
    Browse the repository at this point in the history

  6. Add get_insertList result to internal hashmap

    @monsterkrampe
    monsterkrampe committed Nov 27, 2024
    Configuration menu
    Copy the full SHA
    3845a2e View commit details
    Browse the repository at this point in the history

  7. Try to show insertMany_eq_insertList

    @monsterkrampe
    monsterkrampe committed Nov 27, 2024
    Configuration menu
    Copy the full SHA
    42d72e3 View commit details
    Browse the repository at this point in the history

  8. Add remarks from meeting

    @monsterkrampe
    monsterkrampe committed Nov 27, 2024
    Configuration menu
    Copy the full SHA
    a1d965d View commit details
    Browse the repository at this point in the history

  9. Added equality proof between insertMany & insertList by @TwoFX

    @jt0202 @monsterkrampe
    jt0202 authored and monsterkrampe committed Nov 27, 2024
    Configuration menu
    Copy the full SHA
    83b4e10 View commit details
    Browse the repository at this point in the history

  10. Simplified size_insertList

    @jt0202 @monsterkrampe
    jt0202 authored and monsterkrampe committed Nov 27, 2024
    Configuration menu
    Copy the full SHA
    ed9f63a View commit details
    Browse the repository at this point in the history

  11. Added results for isEmpty

    @jt0202 @monsterkrampe
    jt0202 authored and monsterkrampe committed Nov 27, 2024
    Configuration menu
    Copy the full SHA
    ceb23c9 View commit details
    Browse the repository at this point in the history

  12. Start get? verification

    @jt0202 @monsterkrampe
    jt0202 authored and monsterkrampe committed Nov 27, 2024
    Configuration menu
    Copy the full SHA
    a9b4847 View commit details
    Browse the repository at this point in the history

  13. WIP: verification getValueCast?

    @jt0202 @monsterkrampe
    jt0202 authored and monsterkrampe committed Nov 27, 2024
    Configuration menu
    Copy the full SHA
    da76a1d View commit details
    Browse the repository at this point in the history

  14. Finished DistinctKeys for get?

    @jt0202 @monsterkrampe
    jt0202 authored and monsterkrampe committed Nov 27, 2024
    Configuration menu
    Copy the full SHA
    9013992 View commit details
    Browse the repository at this point in the history

  15. Finish get verification

    @jt0202 @monsterkrampe
    jt0202 authored and monsterkrampe committed Nov 27, 2024
    Configuration menu
    Copy the full SHA
    1d18281 View commit details
    Browse the repository at this point in the history

  16. Some formatting

    @jt0202 @monsterkrampe
    jt0202 authored and monsterkrampe committed Nov 27, 2024
    Configuration menu
    Copy the full SHA
    f023e7f View commit details
    Browse the repository at this point in the history

  17. Pull insertList up to DHashMap

    @jt0202 @monsterkrampe
    jt0202 authored and monsterkrampe committed Nov 27, 2024
    Configuration menu
    Copy the full SHA
    fdd6bab View commit details
    Browse the repository at this point in the history

  18. Add results for getKey?_insertList

    @monsterkrampe
    monsterkrampe committed Nov 27, 2024
    Configuration menu
    Copy the full SHA
    273a0d0 View commit details
    Browse the repository at this point in the history

  19. Add results for variants of getKey_insertList

    @monsterkrampe
    monsterkrampe committed Nov 27, 2024
    Configuration menu
    Copy the full SHA
    be70b67 View commit details
    Browse the repository at this point in the history

  20. Multiple small changes

    @jt0202 @monsterkrampe
    jt0202 authored and monsterkrampe committed Nov 27, 2024
    Configuration menu
    Copy the full SHA
    a5f7e12 View commit details
    Browse the repository at this point in the history

  21. Replace insertList with insertMany in lemmas

    @jt0202 @monsterkrampe
    jt0202 authored and monsterkrampe committed Nov 27, 2024
    Configuration menu
    Copy the full SHA
    77bc339 View commit details
    Browse the repository at this point in the history

  22. Hotfix for build after rebase

    @monsterkrampe
    monsterkrampe committed Nov 27, 2024
    Configuration menu
    Copy the full SHA
    cea3723 View commit details
    Browse the repository at this point in the history

  23. Split getKey? result into two cases

    @monsterkrampe
    monsterkrampe committed Nov 27, 2024
    Configuration menu
    Copy the full SHA
    6f01fd3 View commit details
    Browse the repository at this point in the history

Commits on Nov 28, 2024

  1. Adjust remaining getKey results

    @monsterkrampe
    monsterkrampe committed Nov 28, 2024
    Configuration menu
    Copy the full SHA
    c85b156 View commit details
    Browse the repository at this point in the history

  2. Remove obsolete auxiliary result

    @monsterkrampe
    monsterkrampe committed Nov 28, 2024
    Configuration menu
    Copy the full SHA
    3a4c796 View commit details
    Browse the repository at this point in the history

Commits on Nov 29, 2024

  1. Use getKey?_of_perm for getKey?_insertList

    @monsterkrampe
    monsterkrampe committed Nov 29, 2024
    Configuration menu
    Copy the full SHA
    0cb4f2a View commit details
    Browse the repository at this point in the history

  2. Rework getValueCast? according to suggestion

    @monsterkrampe
    monsterkrampe committed Nov 29, 2024
    Configuration menu
    Copy the full SHA
    a2d70af View commit details
    Browse the repository at this point in the history

  3. Remove obsolete aux results; Fix colon spacing

    @monsterkrampe
    monsterkrampe committed Nov 29, 2024
    Configuration menu
    Copy the full SHA
    4fd84f3 View commit details
    Browse the repository at this point in the history

Commits on Nov 30, 2024

  1. constant get for insertMany

    @jt0202
    jt0202 committed Nov 30, 2024
    Configuration menu
    Copy the full SHA
    8f3eaa2 View commit details
    Browse the repository at this point in the history

  2. Verify Const.insertMany

    @jt0202
    jt0202 committed Nov 30, 2024
    Configuration menu
    Copy the full SHA
    446e801 View commit details
    Browse the repository at this point in the history

Commits on Dec 1, 2024

  1. Verify insertManyIfNewUnit

    @jt0202
    jt0202 committed Dec 1, 2024
    Configuration menu
    Copy the full SHA
    49e4a9d View commit details
    Browse the repository at this point in the history

Commits on Dec 2, 2024

  1. get results for insertManyIfNewUnit

    @jt0202
    jt0202 committed Dec 2, 2024
    Configuration menu
    Copy the full SHA
    8340caf View commit details
    Browse the repository at this point in the history

  2. Style fixes

    @jt0202
    jt0202 committed Dec 2, 2024
    Configuration menu
    Copy the full SHA
    45e3bc0 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'leanprover:master' into hashMap-insertList

    @jt0202
    jt0202 authored Dec 2, 2024
    Configuration menu
    Copy the full SHA
    7f4bc44 View commit details
    Browse the repository at this point in the history

Commits on Dec 3, 2024

  1. Adjust simp spacing

    @monsterkrampe
    monsterkrampe committed Dec 3, 2024
    Configuration menu
    Copy the full SHA
    bddf6fb View commit details
    Browse the repository at this point in the history

  2. Incorporate smaller remarks from PR

    @monsterkrampe
    monsterkrampe committed Dec 3, 2024
    Configuration menu
    Copy the full SHA
    ae25818 View commit details
    Browse the repository at this point in the history

  3. Shorten List.pairwise statements

    @monsterkrampe
    monsterkrampe committed Dec 3, 2024
    Configuration menu
    Copy the full SHA
    9bb3511 View commit details
    Browse the repository at this point in the history

  4. Fix two more small spacing issues

    @monsterkrampe
    monsterkrampe committed Dec 3, 2024
    Configuration menu
    Copy the full SHA
    3266d6c View commit details
    Browse the repository at this point in the history

Commits on Dec 4, 2024

  1. Unify getValue? proofs with getValueCast?

    @monsterkrampe
    monsterkrampe committed Dec 4, 2024
    Configuration menu
    Copy the full SHA
    422ed96 View commit details
    Browse the repository at this point in the history

  2. Simplify insertListConst

    @monsterkrampe
    monsterkrampe committed Dec 4, 2024
    Configuration menu
    Copy the full SHA
    5ce3a53 View commit details
    Browse the repository at this point in the history