feat(category/traversable): derive traversable instances

Authors: Simon Hudon, Mario Carneiro

Author: cipher1024

category/applicative.lean

@@ -14,19 +14,41 @@ section lemmas
 
 open function
 
-variables {f : Type u → Type v}
-variables [applicative f] [is_lawful_applicative f]
+variables {F : Type u → Type v}
+variables [applicative F] [is_lawful_applicative F]
 variables {α β γ σ : Type u}
 
 attribute [functor_norm] seq_assoc pure_seq_eq_map map_pure seq_map_assoc map_seq
 
-lemma applicative.map_seq_map (g : α → β → γ) (h : σ → β) (x : f α) (y : f σ) :
-  (g <$> x) <*> (h <$> y) = (flip (∘) h ∘ g) <$> x <*> y :=
+lemma applicative.map_seq_map (f : α → β → γ) (g : σ → β) (x : F α) (y : F σ) :
+  (f <$> x) <*> (g <$> y) = (flip (∘) g ∘ f) <$> x <*> y :=
 by simp [flip] with functor_norm
 
-lemma applicative.pure_seq_eq_map' (g : α → β) :
-  (<*>) (pure g : f (α → β)) = (<$>) g :=
-by funext; simp with functor_norm
+lemma applicative.pure_seq_eq_map' (f : α → β) :
+  (<*>) (pure f : F (α → β)) = (<$>) f :=
+by ext; simp with functor_norm
+
+theorem applicative.ext {F} : ∀ {A1 : applicative F} {A2 : applicative F}
+  [@is_lawful_applicative F A1] [@is_lawful_applicative F A2]
+  (H1 : ∀ {α : Type u} (x : α),
+    @has_pure.pure _ A1.to_has_pure _ x = @has_pure.pure _ A2.to_has_pure _ x)
+  (H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α),
+    @has_seq.seq _ A1.to_has_seq _ _ f x = @has_seq.seq _ A2.to_has_seq _ _ f x),
+  A1 = A2
+| {to_functor := F1, seq := s1, pure := p1, seq_left := sl1, seq_right := sr1}
+  {to_functor := F2, seq := s2, pure := p2, seq_left := sl2, seq_right := sr2} L1 L2 H1 H2 :=
+begin
+  have : @p1 = @p2, {funext α x, apply H1}, subst this,
+  have : @s1 = @s2, {funext α β f x, apply H2}, subst this,
+  cases L1, cases L2,
+  have : F1 = F2,
+  { resetI, apply functor.ext, intros,
+    exact (L1_pure_seq_eq_map _ _).symm.trans (L2_pure_seq_eq_map _ _) },
+  subst this,
+  congr; funext α β x y,
+  { exact (L1_seq_left_eq _ _).trans (L2_seq_left_eq _ _).symm },
+  { exact (L1_seq_right_eq _ _).trans (L2_seq_right_eq _ _).symm }
+end
 
 end lemmas
 
@@ -35,63 +57,64 @@ namespace comp
 open function (hiding comp)
 open functor
 
-variables {f : Type u → Type w} {g : Type v → Type u}
+variables {F : Type u → Type w} {G : Type v → Type u}
 
-variables [applicative f] [applicative g]
+variables [applicative F] [applicative G]
 
-protected def seq  {α β : Type v} : comp f g (α → β) → comp f g α → comp f g β
-| ⟨h⟩ ⟨x⟩ := ⟨has_seq.seq <$> h <*> x⟩
+protected def seq {α β : Type v} : comp F G (α → β) → comp F G α → comp F G β
+| (comp.mk f) (comp.mk x) := comp.mk $ (<*>) <$> f <*> x
 
-instance : has_pure (comp f g) :=
-⟨λ _ x, ⟨pure $ pure x⟩⟩
+instance : has_pure (comp F G) :=
+⟨λ _ x, comp.mk $ pure $ pure x⟩
 
-instance : has_seq (comp f g) :=
+instance : has_seq (comp F G) :=
 ⟨λ _ _ f x, comp.seq f x⟩
 
-@[simp]
-protected lemma run_pure {α : Type v} :
-  ∀ x : α, (pure x : comp f g α).run = pure (pure x)
+@[simp] protected lemma run_pure {α : Type v} :
+  ∀ x : α, (pure x : comp F G α).run = pure (pure x)
 | _ := rfl
 
-@[simp]
-protected lemma run_seq {α β : Type v} :
-  ∀ (h : comp f g (α → β)) (x : comp f g α),
-  (h <*> x).run = (<*>) <$> h.run <*> x.run
-| ⟨_⟩ ⟨_⟩ := rfl
+@[simp] protected lemma run_seq {α β : Type v} (f : comp F G (α → β)) (x : comp F G α) :
+  (f <*> x).run = (<*>) <$> f.run <*> x.run := rfl
 
-variables [is_lawful_applicative f] [is_lawful_applicative g]
+instance : applicative (comp F G) :=
+{ map := @comp.map F G _ _,
+  seq := @comp.seq F G _ _,
+  ..comp.has_pure }
+
+variables [is_lawful_applicative F] [is_lawful_applicative G]
 variables {α β γ : Type v}
 
-lemma map_pure (h : α → β) (x : α) : (h <$> pure x : comp f g β) = pure (h x) :=
-by ext; simp
+lemma map_pure (f : α → β) (x : α) : (f <$> pure x : comp F G β) = pure (f x) :=
+comp.ext $ by simp
 
-lemma seq_pure (h : comp f g (α → β)) (x : α) :
-  h <*> pure x = (λ g : α → β, g x) <$> h :=
-by ext; simp [(∘)] with functor_norm
+lemma seq_pure (f : comp F G (α → β)) (x : α) :
+  f <*> pure x = (λ g : α → β, g x) <$> f :=
+comp.ext $ by simp [(∘)] with functor_norm
 
-lemma seq_assoc (x : comp f g α) (h₀ : comp f g (α → β)) (h₁ : comp f g (β → γ)) :
-   h₁ <*> (h₀ <*> x) = (@function.comp α β γ <$> h₁) <*> h₀ <*> x :=
-by ext; simp [(∘)] with functor_norm
+lemma seq_assoc (x : comp F G α) (f : comp F G (α → β)) (g : comp F G (β → γ)) :
+   g <*> (f <*> x) = (@function.comp α β γ <$> g) <*> f <*> x :=
+comp.ext $ by simp [(∘)] with functor_norm
 
-lemma pure_seq_eq_map (h : α → β)  (x : comp f g α) :
-  pure h <*> x = h <$> x :=
-by ext; simp [applicative.pure_seq_eq_map'] with functor_norm
+lemma pure_seq_eq_map (f : α → β) (x : comp F G α) :
+  pure f <*> x = f <$> x :=
+comp.ext $ by simp [applicative.pure_seq_eq_map'] with functor_norm
 
-instance {f : Type u → Type w} {g : Type v → Type u}
-  [applicative f] [applicative g] :
-  applicative (comp f g) :=
-{ map := @comp.map f g _ _,
-  seq := @comp.seq f g _ _,
-  ..comp.has_pure }
+instance : is_lawful_applicative (comp F G) :=
+{ pure_seq_eq_map := @comp.pure_seq_eq_map F G _ _ _ _,
+  map_pure := @comp.map_pure F G _ _ _ _,
+  seq_pure := @comp.seq_pure F G _ _ _ _,
+  seq_assoc := @comp.seq_assoc F G _ _ _ _ }
 
-instance {f : Type u → Type w} {g : Type v → Type u}
-  [applicative f] [applicative g]
-  [is_lawful_applicative f] [is_lawful_applicative g] :
-  is_lawful_applicative (comp f g) :=
-{ pure_seq_eq_map := @comp.pure_seq_eq_map f g _ _ _ _,
-  map_pure := @comp.map_pure f g _ _ _ _,
-  seq_pure := @comp.seq_pure f g _ _ _ _,
-  seq_assoc := @comp.seq_assoc f g _ _ _ _ }
+theorem applicative_id_comp {F} [AF : applicative F] [LF : is_lawful_applicative F] :
+  @comp.applicative id F _ _ = AF :=
+@applicative.ext F _ _ (@comp.is_lawful_applicative id F _ _ _ _) _
+  (λ α x, rfl) (λ α β f x, rfl)
+
+theorem applicative_comp_id {F} [AF : applicative F] [LF : is_lawful_applicative F] :
+  @comp.applicative F id _ _ = AF :=
+@applicative.ext F _ _ (@comp.is_lawful_applicative F id _ _ _ _) _
+  (λ α x, rfl) (λ α β f x, show id <$> f <*> x = f <*> x, by rw id_map)
 
 end comp
 open functor

category/basic.lean

@@ -25,49 +25,49 @@ run_cmd mk_simp_attr `functor_norm
 end functor
 
 section applicative
-variables {f : Type u → Type v} [applicative f]
+variables {F : Type u → Type v} [applicative F]
 
 def mzip_with
   {α₁ α₂ φ : Type u}
-  (g : α₁ → α₂ → f φ) :
-  Π (ma₁ : list α₁) (ma₂: list α₂), f (list φ)
-| (x :: xs) (y :: ys) := (::) <$> g x y <*> mzip_with xs ys
+  (f : α₁ → α₂ → F φ) :
+  Π (ma₁ : list α₁) (ma₂: list α₂), F (list φ)
+| (x :: xs) (y :: ys) := (::) <$> f x y <*> mzip_with xs ys
 | _ _ := pure []
 
-def mzip_with'  (g : α → β → f γ) : list α → list β → f punit
-| (x :: xs) (y :: ys) := g x y *> mzip_with' xs ys
+def mzip_with'  (f : α → β → F γ) : list α → list β → F punit
+| (x :: xs) (y :: ys) := f x y *> mzip_with' xs ys
 | [] _ := pure punit.star
 | _ [] := pure punit.star
 
-protected def option.traverse {α β : Type*} (g : α → f β) : option α → f (option β)
+protected def option.traverse {α β : Type*} (f : α → F β) : option α → F (option β)
 | none := pure none
-| (some x) := some <$> g x
+| (some x) := some <$> f x
 
-protected def list.traverse {α β : Type*} (g : α → f β) : list α → f (list β)
+protected def list.traverse {α β : Type*} (f : α → F β) : list α → F (list β)
 | [] := pure []
-| (x :: xs) := list.cons <$> g x <*> list.traverse xs
+| (x :: xs) := list.cons <$> f x <*> list.traverse xs
 
-variables [is_lawful_applicative f]
+variables [is_lawful_applicative F]
 
 attribute [functor_norm] seq_assoc pure_seq_eq_map
 
-@[simp] theorem pure_id'_seq (x : f α) : pure (λx, x) <*> x = x :=
+@[simp] theorem pure_id'_seq (x : F α) : pure (λx, x) <*> x = x :=
 pure_id_seq x
 
-variables  [is_lawful_applicative f]
+variables  [is_lawful_applicative F]
 
 attribute [functor_norm] seq_assoc pure_seq_eq_map
 
-@[functor_norm] theorem seq_map_assoc (x : f (α → β)) (g : γ → α) (y : f γ) :
-  (x <*> (g <$> y)) = (λ(m:α→β), m ∘ g) <$> x <*> y :=
+@[functor_norm] theorem seq_map_assoc (x : F (α → β)) (f : γ → α) (y : F γ) :
+  (x <*> (f <$> y)) = (λ(m:α→β), m ∘ f) <$> x <*> y :=
 begin
   simp [(pure_seq_eq_map _ _).symm],
   simp [seq_assoc, (comp_map _ _ _).symm, (∘)],
   simp [pure_seq_eq_map]
 end
 
-@[functor_norm] theorem map_seq (g : β → γ) (x : f (α → β)) (y : f α) :
-  (g <$> (x <*> y)) = ((∘) g) <$> x <*> y :=
+@[functor_norm] theorem map_seq (f : β → γ) (x : F (α → β)) (y : F α) :
+  (f <$> (x <*> y)) = ((∘) f) <$> x <*> y :=
 by simp [(pure_seq_eq_map _ _).symm]; simp [seq_assoc]
 
 end applicative
@@ -76,6 +76,15 @@ end applicative
 section monad
 variables {m : Type u → Type v} [monad m] [is_lawful_monad m]
 
+open list
+
+def list.mpartition {f : Type → Type} [monad f] {α : Type} (p : α → f bool) :
+  list α → f (list α × list α)
+| [] := pure ([],[])
+| (x :: xs) :=
+mcond (p x) (prod.map (cons x) id <$> list.mpartition xs)
+            (prod.map id (cons x) <$> list.mpartition xs)
+
 lemma map_bind (x : m α) {g : α → m β} {f : β → γ} : f <$> (x >>= g) = (x >>= λa, f <$> g a) :=
 by rw [← bind_pure_comp_eq_map,bind_assoc]; simp [bind_pure_comp_eq_map]
 
@@ -89,17 +98,17 @@ lemma seq_eq_bind_map {x : m α} {f : m (α → β)} : f <*> x = (f >>= (<$> x))
 end monad
 
 section alternative
-variables {f : Type → Type v} [alternative f]
+variables {F : Type → Type v} [alternative F]
 
-def succeeds {α} (x : f α) : f bool := (x $> tt) <|> pure ff
+def succeeds {α} (x : F α) : F bool := (x $> tt) <|> pure ff
 
-def mtry {α} (x : f α) : f unit := (x $> ()) <|> pure ()
+def mtry {α} (x : F α) : F unit := (x $> ()) <|> pure ()
 
 @[simp] theorem guard_true {h : decidable true} :
-  @guard f _ true h = pure () := by simp [guard]
+  @guard F _ true h = pure () := by simp [guard]
 
 @[simp] theorem guard_false {h : decidable false} :
-  @guard f _ false h = failure := by simp [guard]
+  @guard F _ false h = failure := by simp [guard]
 
 end alternative
 

category/functor.lean

@@ -5,8 +5,7 @@ Author: Simon Hudon
 
 Standard identity and composition functors
 -/
-import tactic.ext
-import category.basic
+import tactic.ext tactic.cache category.basic
 
 universe variables u v w
 
@@ -23,6 +22,20 @@ lemma functor.map_comp_map (f : α → β) (g : β → γ) :
   ((<$>) g ∘ (<$>) f : F α → F γ) = (<$>) (g ∘ f) :=
 by apply funext; intro; rw comp_map
 
+theorem functor.ext {F} : ∀ {F1 : functor F} {F2 : functor F}
+  [@is_lawful_functor F F1] [@is_lawful_functor F F2]
+  (H : ∀ α β (f : α → β) (x : F α),
+    @functor.map _ F1 _ _ f x = @functor.map _ F2 _ _ f x),
+  F1 = F2
+| ⟨m, mc⟩ ⟨m', mc'⟩ H1 H2 H :=
+begin
+  cases show @m = @m', by funext α β f x; apply H,
+  congr, funext α β,
+  have E1 := @map_const_eq _ ⟨@m, @mc⟩ H1,
+  have E2 := @map_const_eq _ ⟨@m, @mc'⟩ H2,
+  exact E1.trans E2.symm
+end
+
 end functor
 
 def id.mk {α : Sort u} : α → id α := id
@@ -31,61 +44,59 @@ namespace functor
 
 /-- `functor.comp` is a wrapper around `function.comp` for types.
     It prevents Lean's type class resolution mechanism from trying
-    a `functor (comp f id)` when `functor f` would do. -/
-structure comp (f : Type u → Type w) (g : Type v → Type u) (α : Type v) : Type w :=
-(run : f $ g α)
+    a `functor (comp F id)` when `functor F` would do. -/
+def comp (F : Type u → Type w) (G : Type v → Type u) (α : Type v) : Type w :=
+F $ G α
+
+@[pattern] def comp.mk {F : Type u → Type w} {G : Type v → Type u} {α : Type v}
+  (x : F (G α)) : comp F G α := x
 
-@[extensionality]
-protected lemma comp.ext {f : Type u → Type w} {g : Type v → Type u} {α : Type v} :
-  ∀ {x y : comp f g α}, x.run = y.run → x = y
-| ⟨x⟩ ⟨._⟩ rfl := rfl
+def comp.run {F : Type u → Type w} {G : Type v → Type u} {α : Type v}
+  (x : comp F G α) : F (G α) := x
 
 namespace comp
 
-variables {f : Type u → Type w} {g : Type v → Type u}
+variables {F : Type u → Type w} {G : Type v → Type u}
+
+protected lemma ext
+  {α} {x y : comp F G α} : x.run = y.run → x = y := id
 
-variables [functor f] [functor g]
+variables [functor F] [functor G]
 
-protected def map {α β : Type v} (h : α → β) : comp f g α → comp f g β
-| ⟨x⟩ := ⟨(<$>) h <$> x⟩
+protected def map {α β : Type v} (h : α → β) : comp F G α → comp F G β
+| (comp.mk x) := comp.mk ((<$>) h <$> x)
 
-variables [is_lawful_functor f] [is_lawful_functor g]
+instance : functor (comp F G) := { map := @comp.map F G _ _ }
+
+@[functor_norm] lemma map_mk {α β} (h : α → β) (x : F (G α)) :
+  h <$> comp.mk x = comp.mk ((<$>) h <$> x) := rfl
+
+variables [is_lawful_functor F] [is_lawful_functor G]
 variables {α β γ : Type v}
 
-protected lemma id_map : ∀ (x : comp f g α), comp.map id x = x
-| ⟨x⟩ :=
-by simp [comp.map,functor.map_id]
+protected lemma id_map : ∀ (x : comp F G α), comp.map id x = x
+| (comp.mk x) := by simp [comp.map, functor.map_id]
 
-protected lemma comp_map (g_1 : α → β) (h : β → γ) : ∀ (x : comp f g α),
-           comp.map (h ∘ g_1) x = comp.map h (comp.map g_1 x)
-| ⟨x⟩ :=
-by simp [comp.map,functor.map_comp_map g_1 h] with functor_norm
+protected lemma comp_map (g' : α → β) (h : β → γ) : ∀ (x : comp F G α),
+           comp.map (h ∘ g') x = comp.map h (comp.map g' x)
+| (comp.mk x) := by simp [comp.map, functor.map_comp_map g' h] with functor_norm
 
-instance {f : Type u → Type w} {g : Type v → Type u}
-  [functor f] [functor g] :
-  functor (comp f g) :=
-{ map := @comp.map f g _ _ }
+@[simp] protected lemma run_map (h : α → β) (x : comp F G α) :
+  (h <$> x).run = (<$>) h <$> x.run := rfl
 
-@[simp]
-protected lemma run_map {α β : Type v} (h : α → β) :
-  ∀ x : comp f g α, (h <$> x).run = (<$>) h <$> x.run
-| ⟨_⟩ := rfl
+instance : is_lawful_functor (comp F G) :=
+{ id_map := @comp.id_map F G _ _ _ _,
+  comp_map := @comp.comp_map F G _ _ _ _ }
 
-instance {f : Type u → Type w} {g : Type v → Type u}
-  [functor f] [functor g]
-  [is_lawful_functor f] [is_lawful_functor g] :
-  is_lawful_functor (comp f g) :=
-{ id_map := @comp.id_map f g _ _ _ _,
-  comp_map := @comp.comp_map f g _ _ _ _ }
+theorem functor_comp_id {F} [AF : functor F] [is_lawful_functor F] :
+  @comp.functor F id _ _ = AF :=
+@functor.ext F _ AF (@comp.is_lawful_functor F id _ _ _ _) _ (λ α β f x, rfl)
 
-end comp
+theorem functor_id_comp {F} [AF : functor F] [is_lawful_functor F] :
+  @comp.functor id F _ _ = AF :=
+@functor.ext F _ AF (@comp.is_lawful_functor id F _ _ _ _) _ (λ α β f x, rfl)
 
-@[functor_norm]
-lemma comp.map_mk {α β : Type w}
-  {f : Type u → Type v} {g : Type w → Type u}
-  [functor f] [functor g]
-  (h : α → β) (x : f (g α)) :
-  h <$> comp.mk x = comp.mk ((<$>) h <$> x) := rfl
+end comp
 
 end functor