Clean up `empty{',_inv,_iff}` lemmas.

Write them all using ↔ and consistently use the _iff suffix.

Also:

• Make map_empty a biimplication
• Add lemma map_filter_empty_iff

Sometimes biimplications work less well than one-directional ones, in particular with typeclasses such as dom or empty... might be good to also still have a one-directional version?

I think the lemma is used about three times in Iris, and that's it.

Let me check if the bidirectional version causes problems there.

The iff lemmas seem to work just fine in Iris.

Okay :)

@tchajed reports that this is quite painful in Perennial because rewriting with these lemmas no longer works.

In particular Perennial uses fmap_empty_inv and dom_empty_inv_L that way.

We can either restore the _inv lemma for this case, or add a _2 lemma. The former probably makes more sense.

Probably we should have all these _inv lemmas then though, or at least the ones that conceivably one can rewrite with?

The ones that "conceivably one can rewrite with" makes sense.

For what it's worth I changed the style in Perennial to generally assert (m = \empty) and prove this assertion by applying dom_empty_iff_L. I think this is clearer than the rewrite even if the _inv lemma were still around.

I agree with @tchajed. If either one of you want to add the _inv lemmas, though, please make an MR :)

Why do you think it is clearer?

The rewrites in Perennial were already specifying the map involved in many cases (since the goal had more than one map), so they weren't any less verbose, while the assertion says exactly what's going on. It's also more general because the map is substituted everywhere rather than just the goal.

We also had an anti-pattern of using replace, which requires annotating the \empty with the right type and produces a goal \empty = m which dom_empty_iff_L doesn't apply to. Using assert instead solves both problems.

No fundamental objection, but a full list of renames would be useful (and will be needed for the changelog anyway).

added 13 commits

• 82362145...cbd68767 - 9 commits from branch master
• 1b3a09b4 - Make `map_empty` a biimplication.
• ead373e4 - Clean up `empty_{inv,iff}` lemmas.
• 953658b1 - Add lemma `map_filter_empty_iff`.
• 255e2a6e - CHANGELOG.

Compare with previous version

resolved all threads

I have added a CHANGELOG entry.

changed title from Clean up empty{-_-}{inv,iff} lemmas. to Clean up empty{{+',_+}inv,{+_+}iff} lemmas.

added 1 commit

• b47d3b36 - CHANGELOG.

Compare with previous version

added 1 commit

• 54efa2cd - CHANGELOG.

Compare with previous version

And updated the CHANGELOG, since I forgot some lemmas...

mentioned in merge request !245 (merged)

added 1 commit

• 47bd9469 - Tweak CHANGELOG.

Compare with previous version

I assume you tested that sed script?

LGTM!

added 1 commit

• e50a5b09 - Apply 1 suggestion(s) to 1 file(s)

Compare with previous version

added 1 commit

• 7de04696 - Properly escape ' in sed script.

Compare with previous version

resolved all threads

I tested it now, turns out I fucked up escaping '... My current solution is ugly, but it seems to work.

added 1 commit

• d8ad1852 - Properly escape ' in sed script.

Compare with previous version

resolved all threads