Skip to content
Snippets Groups Projects

Misc setoids lemmas and tweaks for maps and option

Merged Misc setoids lemmas and tweaks for maps and option
robbert/map_setoid into master
1 unresolved thread
Merged Robbert Krebbers requested to merge robbert/map_setoid into master
1 unresolved thread
  • Add lemmas map_singleton_equiv_inj and map_fmap_equiv_inj.
  • Add lemma option_fmap_equiv_inj.
  • Add Propers for maps, and generalize existing ones. Add tests to check that the old ones can be derived.
  • Add lemma map_equiv_lookup_r.
  • Add lemma map_equiv_iff.

Also, rename instances option_mbind_proper → option_bind_proper and option_mjoin_proper → option_join_proper to be consistent with similar instances for sets and lists.

Merge request reports

Loading
Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
  • Ralf Jung
  • Ralf Jung
  • Robbert Krebbers added 1 commit

    added 1 commit

    • 1a8aac47 - Renamed tests/solve_proper.v -> tests/proper.v since it tests more Proper related stuff.

    Compare with previous version

  • Robbert Krebbers added 1 commit

    added 1 commit

    • 84a727e6 - Spell out function names in `Proper`s instead of using notations.

    Compare with previous version

  • Robbert Krebbers added 2 commits

    added 2 commits

    • 8f93d6e3 - Renamed tests/solve_proper.v -> tests/proper.v since it tests more Proper related stuff.
    • 379014ec - Spell out function names in `Proper`s instead of using notations.

    Compare with previous version

  • Ralf Jung resolved all threads

    resolved all threads

  • Robbert Krebbers resolved all threads

    resolved all threads

  • Robbert Krebbers merged

    merged

  • Robbert Krebbers mentioned in commit 8c6f2e63

    mentioned in commit 8c6f2e63

  • Robbert Krebbers
    Robbert Krebbers @robbertkrebbers
    Author Owner

    Oops, I forgot the CHANGELOG. Let me fix that...

  • Robbert Krebbers mentioned in commit 7f76f0e2

    mentioned in commit 7f76f0e2

  • Robbert Krebbers
    Robbert Krebbers @robbertkrebbers
    Author Owner

    CHANGELOG: 7f76f0e2

  • Robbert Krebbers
    Robbert Krebbers @robbertkrebbers
    Author Owner

    @iris-users This is a breaking change (in the unlikely event that you are using instances explicitly):

    Rename instances `option_mbind_proper` → `option_bind_proper` and `option_mjoin_proper` → `option_join_proper` to be consistent with similar instances for sets and lists.
  • Ralf Jung
    Ralf Jung @jung started a thread on the diff
    • theories/option.v
    145 145
    146 146 Global Instance is_Some_proper : Proper ((≡@{option A}) ==> iff) is_Some.
    147 147 Proof. inversion_clear 1; split; eauto. Qed.
    148 Global Instance from_option_proper {B} (R : relation B) (f : A → B) :
    149 Proper ((≡) ==> R) f → Proper (R ==> (≡) ==> R) (from_option f).
    148 Global Instance from_option_proper {B} (R : relation B) :
    149 Proper (((≡@{A}) ==> R) ==> R ==> (≡) ==> R) from_option.
  • Robbert Krebbers mentioned in commit ca70af1d

    mentioned in commit ca70af1d

  • Robbert Krebbers mentioned in merge request !407 (merged)

    mentioned in merge request !407 (merged)

    • Please register or sign in to reply