prove general fmap_inj lemmas

and derive the existing ones from it (and also in Iris, an equivalent one for dist)

mentioned in merge request iris!969 (merged)

added 1 commit

• d48ecad3 - prove a general option_fmap_inj lemma, and a similar one for lists

Compare with previous version

changed title from prove a general option_fmap_inj lemma to prove general fmap_inj lemmas

The equivalent lemma for maps is blocked on having map_Forall2.

added 1 commit

• c900f470 - prove a general option_fmap_inj lemma, and a similar one for lists

Compare with previous version

added 1 commit

• 9ac59018 - prove a general option_fmap_inj lemma, and a similar one for lists

Compare with previous version

added 22 commits

• 9ac59018...1ce70965 - 19 commits from branch master
• b44a2d00 - prove a general option_fmap_inj lemma, and a similar one for lists
• 415ba1b5 - Add instance `bv_unsigned_inj` and use that.
• e1a6f3cb - Tweaks.

Compare with previous version

added 1 commit

• 4c8f9418 - CHANGELOG.

Compare with previous version

added 2 commits

• 5b385655 - Tweaks.
• 2db43fb2 - CHANGELOG.

Compare with previous version

I tweaked this MR a bit.

• I noticed we already had lemmas that relate ≡ and Forall2/option_Forall2. I tried to make their statements and names consistent. See CHANGELOG for details.
• I tweaked some proofs.

LGTM, thanks!

merged

mentioned in commit b9418660

@iris-users

• Rename equiv_Forall2 → list_equiv_Forall2 and equiv_option_Forall2 → option_equiv_Forall2. Add similar lemmas list_eq_Forall2 and option_eq_Forall2 for = instead of ≡.
• Rename fmap_inj → list_fmap_eq_inj and option_fmap_inj → option_fmap_eq_inj. The new lemmas list_fmap_inj/option_fmap_inj generalize injectivity to Forall2/option_Forall2.

mentioned in commit iris@643fb0cd

mentioned in merge request iris!999 (merged)

mentioned in commit iris@608fad72

mentioned in commit iris@8515dc96