From 12e701cae8724bfb6d13c777d8e136a6eb1fdfa0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 8 Nov 2017 10:43:57 +0100
Subject: [PATCH] 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.
---
 theories/base.v     | 3 ++-
 theories/fin_maps.v | 2 +-
 theories/finite.v   | 4 ++--
 theories/list.v     | 4 ++--
 theories/option.v   | 2 +-
 theories/zmap.v     | 2 +-
 6 files changed, 9 insertions(+), 8 deletions(-)

diff --git a/theories/base.v b/theories/base.v
index d6f95cd4..b74ca055 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -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.
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 91af5b33..37a9b4d7 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -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.
diff --git a/theories/finite.v b/theories/finite.v
index a44bfe75..b64b94f0 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -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.
diff --git a/theories/list.v b/theories/list.v
index 532224f0..c685c985 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -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.
diff --git a/theories/option.v b/theories/option.v
index f149f442..59b6b7b3 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -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.
diff --git a/theories/zmap.v b/theories/zmap.v
index 90c87f5c..241b1d3c 100644
--- a/theories/zmap.v
+++ b/theories/zmap.v
@@ -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.
-- 
GitLab