[WIP] new traversable type class

category/basic.lean

@@ -15,6 +15,54 @@ variables {f : Type u → Type v} [applicative f]
 lemma pure_seq_eq_map : ∀ {α β : Type u} (g : α → β) (x : f α), pure g <*> x = g <$> x :=
 @applicative.pure_seq_eq_map f _
 
+def mmap₂
+  {α₁ α₂ φ : Type u}
+  (g : α₁ → α₂ → f φ)
+: Π (ma₁ : list α₁) (ma₂: list α₂), f (list φ)
+ | (x :: xs) (y :: ys) := (::) <$> g x y <*> mmap₂ xs ys
+ | _ _ := pure []
+
+def mmap₂'  (g : α → β → f γ) : list α → list β → f punit
+| (x :: xs) (y :: ys) := g x y *> mmap₂' xs ys
+| [] _ := pure punit.star
+| _ [] := pure punit.star
+
+private def mpartition_aux (x : α) : ulift bool → list α × list α → list α × list α
+ | ⟨ tt ⟩ (xs,ys) := (x::xs,ys)
+ | ⟨ ff ⟩ (xs,ys) := (xs,x::ys)
+
+def list.mpartition' (g : α → f (ulift bool)) : list α → f (list α × list α)
+ | [] := pure ([],[])
+ | (x :: xs) := mpartition_aux x <$> g x <*> list.mpartition' xs
+
+def list.mpartition {α : Type} {f : Type → Type v} [applicative f] (g : α → f bool) :=
+list.mpartition' (λ x, ulift.up <$> g x)
+
+variables {m : Type u → Type v} [applicative m]
+def lift₂
+  {α₁ α₂ φ : Type u}
+  (f : α₁ → α₂ → φ)
+  (ma₁ : m α₁) (ma₂: m α₂) : m φ :=
+f <$> ma₁ <*> ma₂
+
+def lift₃
+  {α₁ α₂ α₃ φ : Type u}
+  (f : α₁ → α₂ → α₃ → φ)
+  (ma₁ : m α₁) (ma₂: m α₂) (ma₃ : m α₃) : m φ :=
+f <$> ma₁ <*> ma₂ <*> ma₃
+
+def lift₄
+  {α₁ α₂ α₃ α₄ φ : Type u}
+  (f : α₁ → α₂ → α₃ → α₄ → φ)
+  (ma₁ : m α₁) (ma₂: m α₂) (ma₃ : m α₃) (ma₄ : m α₄) : m φ :=
+f <$> ma₁ <*> ma₂ <*> ma₃ <*> ma₄
+
+def lift₅
+  {α₁ α₂ α₃ α₄ α₅ φ : Type u}
+  (f : α₁ → α₂ → α₃ → α₄ → α₅ → φ)
+  (ma₁ : m α₁) (ma₂: m α₂) (ma₃ : m α₃) (ma₄ : m α₄) (ma₅ : m α₅) : m φ :=
+f <$> ma₁ <*> ma₂ <*> ma₃ <*> ma₄ <*> ma₅
+
 end applicative
 
 section monad

control/applicative.lean

@@ -0,0 +1,174 @@
+
+import data.functor
+
+universe variables u v w u' v' w'
+
+section lemmas
+
+open function applicative
+
+variables {α β γ : Type u}
+variables {f : Type u → Type v}
+variables [applicative f]
+variables (g : β → γ)
+
+lemma applicative.map_seq_assoc
+  (x : f (α → β)) (y : f α)
+: @has_map.map f _ _ _ g (x <*> y) = comp g <$> x <*> y :=
+by rw [← applicative.pure_seq_eq_map
+      ,seq_assoc
+      ,map_pure
+      ,applicative.pure_seq_eq_map]
+
+lemma applicative.seq_map_comm
+  (x : f (γ → α)) (y : f β)
+: x <*> g <$> y = flip comp g <$> x <*> y :=
+begin
+  rw [← pure_seq_eq_map _ y,seq_assoc,seq_pure,← functor.map_comp],
+  refl,
+end
+
+end lemmas
+
+namespace identity
+
+open function
+
+variables {α : Type u} {β : Type v} {γ : Type u'}
+
+def pure : α → identity α := identity.mk
+
+def seq : identity (α → β) → identity α → identity β
+  | ⟨ f ⟩ ⟨ x ⟩ := ⟨ f x ⟩
+
+local infix <$> := map
+local infix <*> := seq
+
+lemma pure_seq_eq_map (g : α → β) : ∀ (x : identity α), pure g <*> x = g <$> x
+  | ⟨ x ⟩ := rfl
+
+lemma map_pure (g : α → β) (x : α)
+: g <$> pure x = pure (g x) :=
+rfl
+
+lemma seq_pure : ∀ (g : identity (α → β)) (x : α),
+  g <*> pure x = (λ g : α → β, g x) <$> g
+  | ⟨ g ⟩ x := rfl
+
+lemma seq_assoc : ∀ (x : identity α) (g : identity (α → β)) (h : identity (β → γ)),
+  h <*> (g <*> x) = (@comp α β γ <$> h) <*> g <*> x
+| ⟨ x ⟩ ⟨ g ⟩ ⟨ h ⟩ := rfl
+
+end identity
+
+instance applicative_identity : applicative identity :=
+{ map := @identity.map
+, id_map := @identity.id_map
+, pure := @identity.pure
+, seq := @identity.seq
+, pure_seq_eq_map := @identity.pure_seq_eq_map
+, map_pure := @identity.map_pure
+, seq_pure := @identity.seq_pure
+, seq_assoc := @identity.seq_assoc }
+
+lemma identity.seq_mk {α β : Type v}  (f : α → β) (x : α)
+: identity.mk f <*> identity.mk x = identity.mk (f x) := rfl
+
+namespace compose
+
+open function
+
+variables {f : Type u → Type u'} {g : Type v → Type u}
+
+variables [applicative f] [applicative g]
+variables {α β γ : Type v}
+
+def seq : compose f g (α → β) → compose f g α → compose f g β
+  | ⟨ h ⟩ ⟨ x ⟩ := ⟨ has_seq.seq <$> h <*> x ⟩
+
+def pure (x : α) : compose f g α :=
+⟨ pure $ pure x ⟩
+
+local infix ` <$> ` := map
+local infix ` <*> ` := seq
+
+lemma map_pure (h : α → β) (x : α) : (h <$> pure x : compose f g β) = pure (h x) :=
+begin
+  unfold compose.pure comp compose.map,
+  apply congr_arg,
+  rw [applicative.map_pure,applicative.map_pure],
+end
+
+lemma seq_pure (h : compose f g (α → β)) (x : α)
+: h <*> pure x = (λ g : α → β, g x) <$> h :=
+begin
+  cases h with h,
+  unfold compose.map compose.pure compose.seq comp,
+  apply congr_arg,
+  rw [applicative.seq_pure,← functor.map_comp],
+  apply congr_fun, apply congr_arg,
+  apply funext, intro y,
+  unfold comp,
+  apply applicative.seq_pure
+end
+
+lemma seq_assoc : ∀ (x : compose f g α) (h₀ : compose f g (α → β)) (h₁ : compose f g (β → γ)),
+   h₁ <*> (h₀ <*> x) = (@comp α β γ <$> h₁) <*> h₀ <*> x
+| ⟨ x ⟩ ⟨ h₀ ⟩ ⟨ h₁ ⟩ :=
+begin
+  unfold compose.seq compose.map,
+  apply congr_arg,
+  repeat { rw [applicative.seq_assoc] },
+  apply congr_fun,
+  apply congr_arg,
+  rw [← functor.map_comp],
+  rw [← functor.map_comp],
+  rw [← applicative.pure_seq_eq_map has_seq.seq
+     ,applicative.seq_assoc
+     ,applicative.seq_pure _ has_seq.seq],
+  repeat { rw [← functor.map_comp] },
+  rw [applicative.map_seq_assoc has_seq.seq,← functor.map_comp],
+  apply congr_fun,
+  apply congr_arg,
+  apply congr_fun,
+  apply congr_arg,
+  { apply funext, intro i,
+    unfold comp,
+    apply funext, intro j,
+    apply funext, intro k,
+    rw [applicative.seq_assoc] },
+end
+
+lemma pure_seq_eq_map (h : α → β) : ∀ (x : compose f g α), pure h <*> x = h <$> x
+  | ⟨ x ⟩ :=
+begin
+  unfold compose.pure compose.seq compose.map comp,
+  apply congr_arg,
+  rw [applicative.map_pure,applicative.pure_seq_eq_map],
+  apply congr_fun,
+  apply congr_arg,
+  apply funext, clear x, intro x,
+  apply applicative.pure_seq_eq_map
+end
+
+instance applicative_compose
+  {f : Type u → Type u'} {g : Type v → Type u}
+  [applicative f] [applicative g]
+: applicative (compose f g) :=
+{ map := @compose.map f g _ _
+, id_map := @compose.id_map f g _ _
+, map_comp := @compose.map_comp f g _ _
+, seq := @compose.seq f g _ _
+, pure := @compose.pure f g _ _
+, pure_seq_eq_map := @compose.pure_seq_eq_map f g _ _
+, map_pure := @compose.map_pure f g _ _
+, seq_pure := @compose.seq_pure f g _ _
+, seq_assoc := @compose.seq_assoc f g _ _ }
+
+end compose
+
+lemma compose.seq_mk {α β : Type u'}
+  {f : Type u → Type v} {g : Type u' → Type u}
+  [applicative f] [applicative g]
+  (h : f (g (α → β))) (x : f (g α))
+: compose.mk h <*> compose.mk x = compose.mk (has_seq.seq <$> h <*> x) := rfl

data/functor.lean

@@ -0,0 +1,94 @@
+
+universe variables u v w u' v' w'
+
+section functor
+
+variables {F : Type u → Type v}
+variables {α β γ : Type u}
+variables [functor F]
+
+lemma functor.id_map' : has_map.map id = (id : F α → F α) :=
+by { apply funext, apply functor.id_map }
+
+lemma functor.map_comp' (f : α → β) (g : β → γ)
+: has_map.map (g ∘ f) = (has_map.map g ∘ has_map.map f : F α → F γ) :=
+by { apply funext, intro, apply functor.map_comp }
+
+end functor
+
+structure identity (α : Type u) : Type u :=
+  (run_identity : α)
+
+structure compose (f : Type u → Type u') (g : Type v → Type u) (α : Type v) : Type u' :=
+  (run : f $ g α)
+
+namespace identity
+
+open function
+
+variables {α : Type u} {β : Type v} {γ : Type u'}
+
+def map (f : α → β) : identity α → identity β
+  | ⟨ x ⟩ := ⟨ f x ⟩
+
+local infixr <$> := map
+
+lemma id_map : ∀ (x : identity α), map id x = x
+ | ⟨ x ⟩ := rfl
+
+lemma map_comp (f : α → β) (g : β → γ)
+: ∀ (x : identity α), map (g ∘ f) x = g <$> f <$> x
+ | ⟨ x ⟩ := rfl
+
+end identity
+
+instance identity_functor : functor identity :=
+{ map := @identity.map
+, id_map := @identity.id_map
+, map_comp := @identity.map_comp }
+
+lemma identity.map_mk {α β : Type v}  (f : α → β) (x : α)
+: f <$> identity.mk x = identity.mk (f x) := rfl
+
+namespace compose
+
+variables {f : Type u → Type u'} {g : Type v → Type u}
+
+variables [functor f] [functor g]
+variables {α β γ : Type v}
+
+def map (h : α → β) : compose f g α → compose f g β
+  | ⟨ x ⟩ := ⟨ has_map.map h <$> x ⟩
+
+local infix ` <$> ` := map
+
+lemma id_map : ∀ (x : compose f g α), map id x = x
+  | ⟨ x ⟩ :=
+by { unfold map, rw [functor.id_map',functor.id_map], }
+
+lemma map_comp (g_1 : α → β) (h : β → γ) : ∀ (x : compose f g α),
+           map (h ∘ g_1) x = map h (map g_1 x)
+  | ⟨ x ⟩ :=
+by { unfold map, rw [functor.map_comp' g_1 h,functor.map_comp], }
+
+end compose
+
+instance functor_compose {f : Type u → Type u'} {g : Type v → Type u}
+  [functor f] [functor g]
+: functor (compose f g) :=
+{ map := @compose.map f g _ _
+, id_map := @compose.id_map f g _ _
+, map_comp := @compose.map_comp f g _ _ }
+
+lemma compose.map_mk {α β : Type u'}
+  {f : Type u → Type v} {g : Type u' → Type u}
+  [functor f] [functor g]
+  (h : α → β) (x : f (g α))
+: h <$> compose.mk x = compose.mk (has_map.map h <$> x) := rfl
+
+namespace ulift
+
+instance : has_map ulift :=
+{ map := λ α β f, up ∘ f ∘ down }
+
+end ulift