Commit 6b94ffb4 authored by Ralf Jung's avatar Ralf Jung
Browse files

add {fst,snd}_map_zip

parent 8eedeb59
Pipeline #49157 passed with stage
in 4 minutes and 45 seconds
......@@ -1713,6 +1713,16 @@ Lemma map_zip_diag {A} (m : M A) :
map_zip m m = (λ x, (x, x)) <$> m.
Proof. apply map_zip_with_diag. Qed.
Lemma fst_map_zip {A B} (m1 : M A) (m2 : M B) :
( k : K, is_Some (m1 !! k) is_Some (m2 !! k))
fst <$> map_zip m1 m2 = m1.
Proof. intros ?. by apply map_fmap_zip_with_l. Qed.
Lemma snd_map_zip {A B} (m1 : M A) (m2 : M B) :
( k : K, is_Some (m2 !! k) is_Some (m1 !! k))
snd <$> map_zip m1 m2 = m2.
Proof. intros ?. by apply map_fmap_zip_with_r. Qed.
(** ** Properties on the [map_relation] relation *)
Section Forall2.
Context {A B} (R : A B Prop) (P : A Prop) (Q : B Prop).
......
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