Commit 9ca1e7b2 authored by Robbert Krebbers's avatar Robbert Krebbers

More consistent fmap and omap properties for fin_maps.

parent 7d393c2b
......@@ -162,7 +162,7 @@ Section setoid.
Proof.
intros ?? Hf ?? Hm1 ?? Hm2 i; apply (merge_ext _ _); auto.
by do 2 destruct 1; first [apply Hf | constructor].
Qed.
Qed.
Global Instance map_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (M A).
Proof.
intros m1 m2 Hm; apply map_eq; intros i.
......@@ -480,13 +480,6 @@ Proof.
* eauto using insert_delete_subset.
* by rewrite lookup_delete.
Qed.
Lemma fmap_insert {A B} (f : A B) (m : M A) i x :
f <$> <[i:=x]>m = <[i:=f x]>(f <$> m).
Proof.
apply map_eq; intros i'; destruct (decide (i' = i)) as [->|].
* by rewrite lookup_fmap, !lookup_insert.
* by rewrite lookup_fmap, !lookup_insert_ne, lookup_fmap by done.
Qed.
Lemma insert_empty {A} i (x : A) : <[i:=x]> = {[i x]}.
Proof. done. Qed.
......@@ -524,22 +517,34 @@ Proof.
intros. apply map_eq; intros i'. by destruct (decide (i = i')) as [->|?];
rewrite ?lookup_alter, ?lookup_singleton_ne, ?lookup_alter_ne by done.
Qed.
Lemma map_fmap_singleton {A B} (f : A B) i x : f <$> {[i x]} = {[i f x]}.
Proof.
by unfold singletonM, map_singleton; rewrite fmap_insert, map_fmap_empty.
Qed.
(** ** Properties of the map operations *)
Lemma fmap_empty {A B} (f : A B) : f <$> = .
Proof. apply map_empty; intros i. by rewrite lookup_fmap, lookup_empty. Qed.
Lemma omap_empty {A B} (f : A option B) : omap f = .
Proof. apply map_empty; intros i. by rewrite lookup_omap, lookup_empty. Qed.
Lemma fmap_insert {A B} (f: A B) m i x: f <$> <[i:=x]>m = <[i:=f x]>(f <$> m).
Proof.
apply map_eq; intros i'; destruct (decide (i' = i)) as [->|].
* by rewrite lookup_fmap, !lookup_insert.
* by rewrite lookup_fmap, !lookup_insert_ne, lookup_fmap by done.
Qed.
Lemma omap_insert {A B} (f : A option B) m i x y :
f x = Some y omap f (<[i:=x]>m) = <[i:=y]>(omap f m).
Proof.
intros; apply map_eq; intros i'; destruct (decide (i' = i)) as [->|].
* by rewrite lookup_omap, !lookup_insert.
* by rewrite lookup_omap, !lookup_insert_ne, lookup_omap by done.
Qed.
Lemma map_fmap_singleton {A B} (f : A B) i x : f <$> {[i x]} = {[i f x]}.
Proof.
by unfold singletonM, map_singleton; rewrite fmap_insert, map_fmap_empty.
Qed.
Lemma omap_singleton {A B} (f : A option B) i x y :
f x = Some y omap f {[ i x ]} = {[ i y ]}.
Proof.
intros; apply map_eq; intros j; destruct (decide (i = j)) as [->|].
* by rewrite lookup_omap, !lookup_singleton.
* by rewrite lookup_omap, !lookup_singleton_ne.
intros. unfold singletonM, map_singleton.
by erewrite omap_insert, omap_empty by eauto.
Qed.
Lemma map_fmap_id {A} (m : M A) : id <$> m = m.
Proof. apply map_eq; intros i; by rewrite lookup_fmap, option_fmap_id. Qed.
......
Markdown is supported
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