Commit ec91c14f authored by Robbert Krebbers's avatar Robbert Krebbers

Strengten `fmap_equiv_ext` lemmas.

The `Equiv` instance for the domain is not needed.
parent 436d274d
Pipeline #22876 passed with stage
in 9 minutes and 37 seconds
......@@ -643,7 +643,7 @@ Proof. apply map_eq; intros i; by rewrite lookup_fmap, option_fmap_id. Qed.
Lemma map_fmap_compose {A B C} (f : A B) (g : B C) (m : M A) :
g f <$> m = g <$> (f <$> m).
Proof. apply map_eq; intros i; by rewrite !lookup_fmap,option_fmap_compose. Qed.
Lemma map_fmap_equiv_ext `{Equiv A, Equiv B} (f1 f2 : A B) (m : M A) :
Lemma map_fmap_equiv_ext {A} `{Equiv B} (f1 f2 : A B) (m : M A) :
( i x, m !! i = Some x f1 x f2 x) f1 <$> m f2 <$> m.
Proof.
intros Hi i; rewrite !lookup_fmap.
......
......@@ -209,7 +209,7 @@ Proof. by destruct mx. Qed.
Lemma option_fmap_ext {A B} (f g : A B) mx :
( x, f x = g x) f <$> mx = g <$> mx.
Proof. intros; destruct mx; f_equal/=; auto. Qed.
Lemma option_fmap_equiv_ext `{Equiv A, Equiv B} (f g : A B) (mx : option A) :
Lemma option_fmap_equiv_ext {A} `{Equiv B} (f g : A B) (mx : option A) :
( x, f x g x) f <$> mx g <$> mx.
Proof. destruct mx; constructor; auto. Qed.
Lemma option_fmap_bind {A B C} (f : A B) (g : B option C) mx :
......
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