Skip to content
Snippets Groups Projects

Some lemmas about `difference` and `delete`

Merged Some lemmas about `difference` and `delete`
dfrumin/coq-stdpp:difference_lemmas into master
1 unresolved thread
Merged Dan Frumin requested to merge dfrumin/coq-stdpp:difference_lemmas into master
1 unresolved thread

Those are the lemmas I used in iris-logrel.

Merge request reports

Merged by avatar (May 2, 2025 12:13am UTC)

Loading

Pipeline #4375 passed

Stage: test

Pipeline passed for d9dd7c5e on master

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
theories/fin_maps.v
409 409 intros. apply map_eq. intros j. by destruct (decide (i = j)) as [->|?];
410 410 rewrite ?lookup_delete, ?lookup_delete_ne.
411 411 Qed.
412 Lemma delete_idem {A} (m : M A) i :
413 delete i (delete i m) = delete i m.
414 Proof. by setoid_rewrite <-partial_alter_compose. Qed.
  • Robbert Krebbers
    Robbert Krebbers @robbertkrebbers ·
    Owner

    Looks good, apart from one small nitpick! Can you change that, then I will merge.

  • Dan Frumin added 1 commit

    added 1 commit

    • 0c2f6db1 - Add some useful lemmas about difference and delete

    Compare with previous version

  • Dan Frumin
    Dan Frumin @dfrumin ·
    Author Contributor

    Done :)

  • Robbert Krebbers mentioned in commit d9dd7c5e

    mentioned in commit d9dd7c5e

  • Robbert Krebbers merged

    merged

  • Robbert Krebbers
    Robbert Krebbers @robbertkrebbers ·
    Owner

    Merged, thanks!

  • Robbert Krebbers mentioned in commit 0d0be97b

    mentioned in commit 0d0be97b

    • Please register or sign in to reply