Commit d253d8a1 authored by Robbert's avatar Robbert

Merge branch 'fmap_assoc' into 'master'

Make `fmap` left associative.

See merge request robbertkrebbers/coq-stdpp!16
parents 58e2c608 12e701ca
......@@ -889,7 +889,8 @@ Notation "(≫=)" := (λ m f, mbind f m) (only parsing) : stdpp_scope.
Notation "x ← y ; z" := (y = (λ x : _, z))
(at level 100, only parsing, right associativity) : stdpp_scope.
Infix "<$>" := fmap (at level 60, right associativity) : stdpp_scope.
Infix "<$>" := fmap (at level 61, left associativity) : stdpp_scope.
Notation "' ( x1 , x2 ) ← y ; z" :=
(y = (λ x : _, let ' (x1, x2) := x in z))
(at level 100, z at level 200, only parsing, right associativity) : stdpp_scope.
......
......@@ -628,7 +628,7 @@ 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.
Lemma map_fmap_compose {A B C} (f : A B) (g : B C) (m : M A) :
g f <$> m = g <$> f <$> m.
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) :
( i x, m !! i = Some x f1 x f2 x) f1 <$> m f2 <$> m.
......
......@@ -232,7 +232,7 @@ Section bijective_finite.
End bijective_finite.
Program Instance option_finite `{Finite A} : Finite (option A) :=
{| enum := None :: Some <$> enum A |}.
{| enum := None :: (Some <$> enum A) |}.
Next Obligation.
constructor.
- rewrite elem_of_list_fmap. by intros (?&?&?).
......@@ -343,7 +343,7 @@ Proof.
Qed.
Fixpoint fin_enum (n : nat) : list (fin n) :=
match n with 0 => [] | S n => 0%fin :: FS <$> fin_enum n end.
match n with 0 => [] | S n => 0%fin :: (FS <$> fin_enum n) end.
Program Instance fin_finite n : Finite (fin n) := {| enum := fin_enum n |}.
Next Obligation.
intros n. induction n; simpl; constructor.
......
......@@ -2882,7 +2882,7 @@ Section fmap.
Context {A B : Type} (f : A B).
Implicit Types l : list A.
Lemma list_fmap_compose {C} (g : B C) l : g f <$> l = g <$> f <$> l.
Lemma list_fmap_compose {C} (g : B C) l : g f <$> l = g <$> (f <$> l).
Proof. induction l; f_equal/=; auto. Qed.
Lemma list_fmap_ext (g : A B) (l1 l2 : list A) :
( x, f x = g x) l1 = l2 fmap f l1 = fmap g l2.
......@@ -2898,7 +2898,7 @@ Section fmap.
Qed.
Definition fmap_nil : f <$> [] = [] := eq_refl.
Definition fmap_cons x l : f <$> x :: l = f x :: f <$> l := eq_refl.
Definition fmap_cons x l : f <$> x :: l = f x :: (f <$> l) := eq_refl.
Lemma fmap_app l1 l2 : f <$> l1 ++ l2 = (f <$> l1) ++ (f <$> l2).
Proof. by induction l1; f_equal/=. Qed.
......
......@@ -202,7 +202,7 @@ Proof. by destruct mx. Qed.
Lemma option_fmap_id {A} (mx : option A) : id <$> mx = mx.
Proof. by destruct mx. Qed.
Lemma option_fmap_compose {A B} (f : A B) {C} (g : B C) mx :
g f <$> mx = g <$> f <$> mx.
g f <$> mx = g <$> (f <$> mx).
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.
......
......@@ -63,7 +63,7 @@ Proof.
- intros ??? [??] []; simpl; [done| |]; apply lookup_fmap.
- intros ? [o t t']; unfold map_to_list; simpl.
assert (NoDup ((prod_map Z.pos id <$> map_to_list t) ++
prod_map Z.neg id <$> map_to_list t')).
(prod_map Z.neg id <$> map_to_list t'))).
{ apply NoDup_app; split_and?.
- apply (NoDup_fmap_2 _), NoDup_map_to_list.
- intro. rewrite !elem_of_list_fmap. naive_solver.
......
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