Strengthen `map_filter_strong_ext` and `map_filter_ext`.

I just added it as another lemma, but it is also possible to change "implies" to "iff" in the map_filter_strong_ext itself.

Wouldn't it make more sense to turn map_filter_strong_ext into a ↔? The only problem is that we don't have any other _ext lemma that are an ↔, I think.

We usually use lem_1 and lem_2 for → versions of a ↔ lemma lem. So here the naming is off, since lem is one direction, and lem_2 the other.

An alternative is to call this lemma map_filter_strong_ext_inv or something else.

PS: Here's a short proof for the ↔:

  Lemma map_filter_strong_ext (m1 m2 : M A) :
    filter P m1 = filter Q m2 ↔
    (∀ i x, (P (i, x) ∧ m1 !! i = Some x) ↔ (Q (i, x) ∧ m2 !! i = Some x)).
  Proof.
    intros. rewrite map_eq_iff. setoid_rewrite option_eq.
    setoid_rewrite map_filter_lookup_Some. naive_solver.
  Qed.
  Lemma map_filter_ext (m : M A) :
    filter P m = filter Q m ↔
    (∀ i x, m !! i = Some x → P (i, x) ↔ Q (i, x)).
  Proof. rewrite map_filter_strong_ext. naive_solver. Qed.

setoid_rewrite! that's what i needed

I will update the PR

added 1 commit

• c3ef745a - Better naming

Compare with previous version

Please update the MR title, and add a changelog entry.

changed title from Add map_filter_strong_ext{-_2-}. to Strengthen map_filter_strong_ext{+ and map_filter_ext+}.

added 2 commits

• 44b864a9 - Better naming
• b3efe8dd - Update changelog

Compare with previous version

Updated!

added 40 commits

• b3efe8dd...29af30c2 - 37 commits from branch iris:master
• 6058134f - Add `map_filter_strong_ext_2`.
• 8396f122 - Better naming
• 4100164d - Update changelog

Compare with previous version

resolved all threads

Thanks.

merged

mentioned in commit 86e53498

@iris-users This is a breaking change:

Make `map_filter_strong_ext` and `map_filter_ext` bidirectional.

mentioned in merge request !290 (merged)