Commit 12e701ca authored by Robbert Krebbers's avatar Robbert Krebbers

Make `fmap` left associative.

This follows the associativity in Haskell. So, something like

  f <$> g <$> h

Is now parsed as:

  (f <$> g) <$> h

Since the functor is a generalized form of function application, this also now
also corresponds with the associativity of function application, which is also
left associative.
parent 58e2c608
...@@ -889,7 +889,8 @@ Notation "(≫=)" := (λ m f, mbind f m) (only parsing) : stdpp_scope. ...@@ -889,7 +889,8 @@ Notation "(≫=)" := (λ m f, mbind f m) (only parsing) : stdpp_scope.
Notation "x ← y ; z" := (y = (λ x : _, z)) Notation "x ← y ; z" := (y = (λ x : _, z))
(at level 100, only parsing, right associativity) : stdpp_scope. (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" := Notation "' ( x1 , x2 ) ← y ; z" :=
(y = (λ x : _, let ' (x1, x2) := x in z)) (y = (λ x : _, let ' (x1, x2) := x in z))
(at level 100, z at level 200, only parsing, right associativity) : stdpp_scope. (at level 100, z at level 200, only parsing, right associativity) : stdpp_scope.
......
...@@ -628,7 +628,7 @@ Qed. ...@@ -628,7 +628,7 @@ Qed.
Lemma map_fmap_id {A} (m : M A) : id <$> m = m. 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. 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) : 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. 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 `{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. ( i x, m !! i = Some x f1 x f2 x) f1 <$> m f2 <$> m.
......
...@@ -232,7 +232,7 @@ Section bijective_finite. ...@@ -232,7 +232,7 @@ Section bijective_finite.
End bijective_finite. End bijective_finite.
Program Instance option_finite `{Finite A} : Finite (option A) := Program Instance option_finite `{Finite A} : Finite (option A) :=
{| enum := None :: Some <$> enum A |}. {| enum := None :: (Some <$> enum A) |}.
Next Obligation. Next Obligation.
constructor. constructor.
- rewrite elem_of_list_fmap. by intros (?&?&?). - rewrite elem_of_list_fmap. by intros (?&?&?).
...@@ -343,7 +343,7 @@ Proof. ...@@ -343,7 +343,7 @@ Proof.
Qed. Qed.
Fixpoint fin_enum (n : nat) : list (fin n) := 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 |}. Program Instance fin_finite n : Finite (fin n) := {| enum := fin_enum n |}.
Next Obligation. Next Obligation.
intros n. induction n; simpl; constructor. intros n. induction n; simpl; constructor.
......
...@@ -2882,7 +2882,7 @@ Section fmap. ...@@ -2882,7 +2882,7 @@ Section fmap.
Context {A B : Type} (f : A B). Context {A B : Type} (f : A B).
Implicit Types l : list A. 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. Proof. induction l; f_equal/=; auto. Qed.
Lemma list_fmap_ext (g : A B) (l1 l2 : list A) : Lemma list_fmap_ext (g : A B) (l1 l2 : list A) :
( x, f x = g x) l1 = l2 fmap f l1 = fmap g l2. ( x, f x = g x) l1 = l2 fmap f l1 = fmap g l2.
...@@ -2898,7 +2898,7 @@ Section fmap. ...@@ -2898,7 +2898,7 @@ Section fmap.
Qed. Qed.
Definition fmap_nil : f <$> [] = [] := eq_refl. 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). Lemma fmap_app l1 l2 : f <$> l1 ++ l2 = (f <$> l1) ++ (f <$> l2).
Proof. by induction l1; f_equal/=. Qed. Proof. by induction l1; f_equal/=. Qed.
......
...@@ -202,7 +202,7 @@ Proof. by destruct mx. Qed. ...@@ -202,7 +202,7 @@ Proof. by destruct mx. Qed.
Lemma option_fmap_id {A} (mx : option A) : id <$> mx = mx. Lemma option_fmap_id {A} (mx : option A) : id <$> mx = mx.
Proof. by destruct mx. Qed. Proof. by destruct mx. Qed.
Lemma option_fmap_compose {A B} (f : A B) {C} (g : B C) mx : 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. Proof. by destruct mx. Qed.
Lemma option_fmap_ext {A B} (f g : A B) mx : Lemma option_fmap_ext {A B} (f g : A B) mx :
( x, f x = g x) f <$> mx = g <$> mx. ( x, f x = g x) f <$> mx = g <$> mx.
......
...@@ -63,7 +63,7 @@ Proof. ...@@ -63,7 +63,7 @@ Proof.
- intros ??? [??] []; simpl; [done| |]; apply lookup_fmap. - intros ??? [??] []; simpl; [done| |]; apply lookup_fmap.
- intros ? [o t t']; unfold map_to_list; simpl. - intros ? [o t t']; unfold map_to_list; simpl.
assert (NoDup ((prod_map Z.pos id <$> map_to_list t) ++ 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_app; split_and?.
- apply (NoDup_fmap_2 _), NoDup_map_to_list. - apply (NoDup_fmap_2 _), NoDup_map_to_list.
- intro. rewrite !elem_of_list_fmap. naive_solver. - 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