Commit 3982e4ea authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'vsiles' into 'master'

Adding gmap_fmap_ext_ne

See merge request iris/iris!751
parents afa87d25 26be4a4b
......@@ -660,6 +660,15 @@ End unital_properties.
Global Instance gmap_fmap_ne `{Countable K} {A B : ofe} (f : A B) n :
Proper (dist n ==> dist n) f Proper (dist n ==>dist n) (fmap (M:=gmap K) f).
Proof. by intros ? m m' Hm k; rewrite !lookup_fmap; apply option_fmap_ne. Qed.
Lemma gmap_fmap_ne_ext `{Countable K}
{A : Type} {B : ofe} (f1 f2 : A B) (m : gmap K A) n :
( i x, m !! i = Some x f1 x {n} f2 x)
f1 <$> m {n} f2 <$> m.
Proof.
move => Hf i.
rewrite !lookup_fmap.
destruct (m !! i) eqn:?; constructor; by eauto.
Qed.
Global Instance gmap_fmap_cmra_morphism `{Countable K} {A B : cmra} (f : A B)
`{!CmraMorphism f} : CmraMorphism (fmap f : gmap K A gmap K B).
Proof.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment