control.basic - mathlib docs

Simp set for functor_norm

theorem functor.map_map {α β γ : Type u} {f : Type u → Type v} [functor f] [is_lawful_functor f] (m : α → β) (g : β → γ) (x : f α) :

g <$> m <$> x = (g ∘ m) <$> x

source

@[simp]

theorem id_map' {α : Type u} {f : Type u → Type v} [functor f] [is_lawful_functor f] (x : f α) :

(λ (a : α), a) <$> x = x

source

def mzip_with {F : Type u → Type v} [applicative F] {α₁ α₂ φ : Type u} (f : α₁ → α₂ → F φ) (ma₁ : list α₁) (ma₂ : list α₂) :

F (list φ)

Equations

mzip_with f (x :: xs) (y :: ys) = (λ (_x : φ) (_y : list φ), _x :: _y) <$> f x y <*> mzip_with f xs ys
mzip_with f (hd :: tl) list.nil = pure list.nil
mzip_with f list.nil _x = pure list.nil

source

def mzip_with' {α β γ : Type u} {F : Type u → Type v} [applicative F] (f : α → β → F γ) :

list α → list β → F punit

Equations

mzip_with' f (x :: xs) (y :: ys) = f x y *> mzip_with' f xs ys
mzip_with' f (hd :: tl) list.nil = pure punit.star
mzip_with' f list.nil (hd :: tl) = pure punit.star
mzip_with' f list.nil list.nil = pure punit.star

source

@[simp]

theorem pure_id'_seq {α : Type u} {F : Type u → Type v} [applicative F] [is_lawful_applicative F] (x : F α) :

pure (λ (x : α), x) <*> x = x

source

theorem seq_map_assoc {α β γ : Type u} {F : Type u → Type v} [applicative F] [is_lawful_applicative F] (x : F (α → β)) (f : γ → α) (y : F γ) :

x <*> f <$> y = (λ (m : α → β), m ∘ f) <$> x <*> y

source

theorem map_seq {α β γ : Type u} {F : Type u → Type v} [applicative F] [is_lawful_applicative F] (f : β → γ) (x : F (α → β)) (y : F α) :

f <$> (x <*> y) = function.comp f <$> x <*> y

source

def list.mpartition {f : Type → Type} [monad f] {α : Type} (p : α → f bool) :

list α → f (list α × list α)

Equations

list.mpartition p (x :: xs) = mcond (p x) (prod.map (list.cons x) id <$> list.mpartition p xs) (prod.map id (list.cons x) <$> list.mpartition p xs)
list.mpartition p list.nil = pure (list.nil α, list.nil α)

source

theorem map_bind {α β γ : Type u} {m : Type u → Type v} [monad m] [is_lawful_monad m] (x : m α) {g : α → m β} {f : β → γ} :

f <$> (x >>= g) = x >>= λ (a : α), f <$> g a

source

theorem seq_bind_eq {α β γ : Type u} {m : Type u → Type v} [monad m] [is_lawful_monad m] (x : m α) {g : β → m γ} {f : α → β} :

f <$> x >>= g = x >>= g ∘ f

source

theorem seq_eq_bind_map {α β : Type u} {m : Type u → Type v} [monad m] [is_lawful_monad m] {x : m α} {f : m (α → β)} :

f <*> x = f >>= λ (_x : α → β), _x <$> x

source

def fish {m : Type u_1 → Type u_2} [monad m] {α : Sort u_3} {β γ : Type u_1} (f : α → m β) (g : β → m γ) (x : α) :

m γ

This is the Kleisli composition

Equations

f >=> g = λ (x : α), f x >>= g

source

theorem fish_pure {m : Type u → Type v} [monad m] [is_lawful_monad m] {α : Sort u_1} {β : Type u} (f : α → m β) :

f >=> pure = f

source

theorem fish_pipe {m : Type u → Type v} [monad m] [is_lawful_monad m] {α β : Type u} (f : α → m β) :

pure >=> f = f

source

theorem fish_assoc {m : Type u → Type v} [monad m] [is_lawful_monad m] {α : Sort u_1} {β γ φ : Type u} (f : α → m β) (g : β → m γ) (h : γ → m φ) :

f >=> g >=> h = f >=> (g >=> h)

source

def list.mmap_accumr {α : Type u} {β' γ' : Type v} {m' : Type v → Type w} [monad m'] (f : α → β' → m' (β' × γ')) :

β' → list α → m' (β' × list γ')

Equations

list.mmap_accumr f a (x :: xs) = list.mmap_accumr f a xs >>= λ (_p : β' × list γ'), list.mmap_accumr._match_2 f x _p
list.mmap_accumr f a list.nil = pure (a, list.nil γ')
list.mmap_accumr._match_2 f x (a', ys) = f x a' >>= λ (_p : β' × γ'), list.mmap_accumr._match_1 ys _p
list.mmap_accumr._match_1 ys (a'', y) = pure (a'', y :: ys)

source

def list.mmap_accuml {α : Type u} {β' γ' : Type v} {m' : Type v → Type w} [monad m'] (f : β' → α → m' (β' × γ')) :

β' → list α → m' (β' × list γ')

Equations

list.mmap_accuml f a (x :: xs) = f a x >>= λ (_p : β' × γ'), list.mmap_accuml._match_2 (λ (a' : β'), list.mmap_accuml f a' xs) _p
list.mmap_accuml f a list.nil = pure (a, list.nil γ')
list.mmap_accuml._match_2 _f_1 (a', y) = _f_1 a' >>= λ (_p : β' × list γ'), list.mmap_accuml._match_1 y _p
list.mmap_accuml._match_1 y (a'', ys) = pure (a'', y :: ys)

source

theorem mjoin_map_map {m : Type u → Type u} [monad m] [is_lawful_monad m] {α β : Type u} (f : α → β) (a : m (m α)) :

mjoin (functor.map f <$> a) = f <$> mjoin a

source

theorem mjoin_map_mjoin {m : Type u → Type u} [monad m] [is_lawful_monad m] {α : Type u} (a : m (m (m α))) :

mjoin (mjoin <$> a) = mjoin (mjoin a)

source

@[simp]

theorem mjoin_map_pure {m : Type u → Type u} [monad m] [is_lawful_monad m] {α : Type u} (a : m α) :

mjoin (pure <$> a) = a

source

@[simp]

theorem mjoin_pure {m : Type u → Type u} [monad m] [is_lawful_monad m] {α : Type u} (a : m α) :

mjoin (pure a) = a

source

def succeeds {F : Type → Type v} [alternative F] {α : Type} (x : F α) :

F bool

Equations

succeeds x = (x $> tt <|> pure ff)

source

def mtry {F : Type → Type v} [alternative F] {α : Type} (x : F α) :

F unit

Equations

mtry x = (x $> () <|> pure ())

source

@[simp]

theorem guard_true {F : Type → Type v} [alternative F] {h : decidable true} :

guard true = pure ()

source

@[simp]

theorem guard_false {F : Type → Type v} [alternative F] {h : decidable false} :

guard false = failure

source

@[protected]

def sum.bind {e : Type v} {α : Type u_1} {β : Type u_2} :

e ⊕ α → (α → e ⊕ β) → e ⊕ β

Equations

(sum.inr x).bind f = f x
(sum.inl x).bind _x = sum.inl x

source

@[protected, instance]

def sum.monad {e : Type v} :

monad (sum e)

Equations

sum.monad = monad.mk

source

@[protected, instance]

def sum.is_lawful_functor {e : Type v} :

is_lawful_functor (sum e)

source

@[protected, instance]

def sum.is_lawful_monad {e : Type v} :

is_lawful_monad (sum e)

source

@[class]

structure is_comm_applicative (m : Type u_1 → Type u_2) [applicative m] :

Prop

to_is_lawful_applicative : is_lawful_applicative m
commutative_prod : ∀ {α β : Type ?} (a : m α) (b : m β), prod.mk <$> a <*> b = (λ (b : β) (a : α), (a, b)) <$> b <*> a

Instances

source

theorem is_comm_applicative.commutative_map {m : Type u_1 → Type u_2} [applicative m] [is_comm_applicative m] {α β γ : Type u_1} (a : m α) (b : m β) {f : α → β → γ} :

f <$> a <*> b = flip f <$> b <*> a