Commit deebe088 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Add lemmas `merge_empty_l` and `merge_empty_r`.

parent e46cc03a
Pipeline #48710 passed with stage
in 5 minutes and 13 seconds
......@@ -1722,6 +1722,18 @@ Section more_merge.
Qed.
End more_merge.
Lemma merge_empty_l {A B C} (f : option A option B option C) (m2 : M B) :
merge f m2 = omap (f None Some) m2.
Proof.
apply map_eq; intros i. rewrite lookup_merge, lookup_omap, lookup_empty.
by destruct (m2 !! i).
Qed.
Lemma merge_empty_r {A B C} (f : option A option B option C) (m1 : M A) :
merge f m1 = omap (flip f None Some) m1.
Proof.
apply map_eq; intros i. rewrite lookup_merge, lookup_omap, lookup_empty.
by destruct (m1 !! i).
Qed.
Lemma merge_diag {A C} (f : option A option A option C) (m : M A) :
merge f m m = omap (λ x, f (Some x) (Some x)) m.
Proof.
......
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