Commit a99446f9 authored by Robbert Krebbers's avatar Robbert Krebbers

Prove `map_zip_with_singleton`.

parent fba969b6
Pipeline #14458 passed with stage
in 15 minutes and 35 seconds
......@@ -1272,10 +1272,12 @@ Qed.
Lemma map_zip_with_empty {A B C} (f : A B C) :
map_zip_with f ( : M A) ( : M B) = .
Proof. unfold map_zip_with. by rewrite merge_empty by done. Qed.
Lemma map_insert_zip_with {A B C} (f : A B C) (m1 : M A) (m2 : M B) i y z :
<[i:=f y z]>(map_zip_with f m1 m2) = map_zip_with f (<[i:=y]>m1) (<[i:=z]>m2).
Proof. unfold map_zip_with. by erewrite insert_merge by done. Qed.
Lemma map_zip_with_singleton {A B C} (f : A B C) i x y :
map_zip_with f ({[ i := x ]} : M A) ({[ i := y ]} : M B) = {[ i := f x y ]}.
Proof. unfold map_zip_with. by erewrite merge_singleton. Qed.
Lemma map_zip_with_fmap {A' A B' B C} (f : A B C)
(g1 : A' A) (g2 : B' B) (m1 : M A') (m2 : M B') :
......
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