Generalize `map_relation` and `map_included` / Add `map_Forall2`.

map_Forall and the big ops in Iris also take the key, so this makes map_relation consistent with that.

This also allowed me to add map_Forall2 (defined using map_relation) in a way that is consistent with map_Forall.

This change is not backwards compatible, but I expect little breakage. map_relation is mostly used internally to define (⊆), map_disjoint, map_agree. And aside from a Decision instance there is very little theory about map_relation.

added 2 commits

• d85efa39 - Add `map_Forall2` and some basic lemmas inspired by `map_Forall`.
• 3d8a8363 - CHANGELOG.

Compare with previous version

changed title from Generalize map_relation and map_included. to Generalize map_relation and map_included{+ / Add map_Forall2+}.

changed the description

added 2 commits

• 45a533bd - Add `map_Forall2` and some basic lemmas inspired by `map_Forall`.
• ea5fa7ce - CHANGELOG.

Compare with previous version

I wonder if map_included is used anywhere at all. Maybe we should just inline it in map_subseteq. Especially since we barely have any theory about it.

added 1 commit

• 510a20da - Code style.

Compare with previous version

added 2 commits

• 94f92518 - Add law `map_fold_foldr` to `FinMap` interface.
• 54ba3dcf - Remove `map_Forall2_insert_1_*`.

Compare with previous version

mentioned in issue #214

resolved all threads

added 1 commit

• b72cf5f9 - Remove `map_Forall2_insert_1_*`.

Compare with previous version

I think this is ready to be merged.

added 1 commit

• 48420e2f - Code style.

Compare with previous version

mentioned in commit 6cb5c0f2

merged

@iris-users this MR includes breaking changes.

• Generalize map_relation R P Q to have the key (extra argument K) in the predicates R, P and Q.
• Generalize map_included R to a predicate R : K → A → B → Prop, i.e., (a) to have the key, and (b) to have different types A and B.
• Rename map_not_Forall2 into map_not_relation.

mentioned in merge request !575 (merged)