core / init.control.lawful

source

meta def control_laws_tac :

tactic unit

source

@[class]

structure is_lawful_functor (f : Type u → Type v) [functor f] :

Prop

map_const_eq : (∀ {α β : Type ?}, functor.map_const = functor.map ∘ function.const β) . "control_laws_tac"
id_map : ∀ {α : Type ?} (x : f α), id <$> x = x
comp_map : ∀ {α β γ : Type ?} (g : α → β) (h : β → γ) (x : f α), (h ∘ g) <$> x = h <$> g <$> x

Instances

source

@[class]

structure is_lawful_applicative (f : Type u → Type v) [applicative f] :

Prop

to_is_lawful_functor : is_lawful_functor f
seq_left_eq : (∀ {α β : Type ?} (a : f α) (b : f β), a <* b = function.const β <$> a <*> b) . "control_laws_tac"
seq_right_eq : (∀ {α β : Type ?} (a : f α) (b : f β), a *> b = function.const α id <$> a <*> b) . "control_laws_tac"
pure_seq_eq_map : ∀ {α β : Type ?} (g : α → β) (x : f α), pure g <*> x = g <$> x
map_pure : ∀ {α β : Type ?} (g : α → β) (x : α), g <$> pure x = pure (g x)
seq_pure : ∀ {α β : Type ?} (g : f (α → β)) (x : α), g <*> pure x = (λ (g : α → β), g x) <$> g
seq_assoc : ∀ {α β γ : Type ?} (x : f α) (g : f (α → β)) (h : f (β → γ)), h <*> (g <*> x) = function.comp <$> h <*> g <*> x

Instances

source

@[simp]

theorem pure_id_seq {α : Type u} {f : Type u → Type v} [applicative f] [is_lawful_applicative f] (x : f α) :

pure id <*> x = x

source

@[class]

structure is_lawful_monad (m : Type u → Type v) [monad m] :

Prop

to_is_lawful_applicative : is_lawful_applicative m
bind_pure_comp_eq_map : (∀ {α β : Type ?} (f : α → β) (x : m α), x >>= pure ∘ f = f <$> x) . "control_laws_tac"
bind_map_eq_seq : (∀ {α β : Type ?} (f : m (α → β)) (x : m α), (f >>= λ (_x : α → β), _x <$> x) = f <*> x) . "control_laws_tac"
pure_bind : ∀ {α β : Type ?} (x : α) (f : α → m β), pure x >>= f = f x
bind_assoc : ∀ {α β γ : Type ?} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= λ (x : α), f x >>= g

Instances

source

@[simp]

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

x >>= pure = x

source

theorem bind_ext_congr {α β : Type u} {m : Type u → Type v} [has_bind m] {x : m α} {f g : α → m β} :

(∀ (a : α), f a = g a) → x >>= f = x >>= g

source

theorem map_ext_congr {α β : Type u} {m : Type u → Type v} [functor m] {x : m α} {f g : α → β} :

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

source

@[simp]

theorem id.map_eq {α β : Type} (x : id α) (f : α → β) :

f <$> x = f x

source

@[simp]

theorem id.bind_eq {α β : Type} (x : id α) (f : α → id β) :

x >>= f = f x

source

@[simp]

theorem id.pure_eq {α : Type} (a : α) :

pure a = a

source

@[protected, instance]

def id.is_lawful_monad :

is_lawful_monad id

source

@[ext]

theorem state_t.ext {σ : Type u} {m : Type u → Type v} {α : Type u} {x x' : state_t σ m α} (h : ∀ (st : σ), x.run st = x'.run st) :

x = x'

source

@[simp]

theorem state_t.run_pure {σ : Type u} {m : Type u → Type v} {α : Type u} (st : σ) [monad m] (a : α) :

(pure a).run st = pure (a, st)

source

@[simp]

theorem state_t.run_bind {σ : Type u} {m : Type u → Type v} {α β : Type u} (x : state_t σ m α) (st : σ) [monad m] (f : α → state_t σ m β) :

(x >>= f).run st = x.run st >>= λ (p : α × σ), (f p.fst).run p.snd

source

@[simp]

theorem state_t.run_map {σ : Type u} {m : Type u → Type v} {α β : Type u} (x : state_t σ m α) (st : σ) [monad m] (f : α → β) [is_lawful_monad m] :

(f <$> x).run st = (λ (p : α × σ), (f p.fst, p.snd)) <$> x.run st

source

@[simp]

theorem state_t.run_monad_lift {σ : Type u} {m : Type u → Type v} {α : Type u} (st : σ) [monad m] {n : Type u → Type u_1} [has_monad_lift_t n m] (x : n α) :

(monad_lift x).run st = monad_lift x >>= λ (a : α), pure (a, st)

source

@[simp]

theorem state_t.run_monad_map {σ : Type u} {m : Type u → Type v} {α : Type u} (x : state_t σ m α) (st : σ) [monad m] {m' : Type u → Type v} {n n' : Type u → Type u_1} [monad m'] [monad_functor_t n n' m m'] (f : Π {α : Type u}, n α → n' α) :

(monad_map f x).run st = monad_map f (x.run st)

source

@[simp]

theorem state_t.run_adapt {σ : Type u} {m : Type u → Type v} {α : Type u} [monad m] {σ' σ'' : Type u} (st : σ) (split : σ → σ' × σ'') (join : σ' → σ'' → σ) (x : state_t σ' m α) :

(state_t.adapt split join x).run st = (λ (_a : σ' × σ''), _a.cases_on (λ (fst : σ') (snd : σ''), id_rhs (m (α × σ)) (x.run fst >>= λ (_p : α × σ'), (λ (_a : α × σ'), _a.cases_on (λ (fst : α) (snd_1 : σ'), id_rhs (m (α × σ)) (pure (fst, join snd_1 snd)))) _p))) (split st)

source

@[simp]

theorem state_t.run_get {σ : Type u} {m : Type u → Type v} (st : σ) [monad m] :

state_t.get.run st = pure (st, st)

source

@[simp]

theorem state_t.run_put {σ : Type u} {m : Type u → Type v} (st : σ) [monad m] (st' : σ) :

(state_t.put st').run st = pure (punit.star, st')

source

@[protected, instance]

def state_t.is_lawful_monad (m : Type u → Type v) [monad m] [is_lawful_monad m] (σ : Type u) :

is_lawful_monad (state_t σ m)

source

@[ext]

theorem except_t.ext {α ε : Type u} {m : Type u → Type v} {x x' : except_t ε m α} (h : x.run = x'.run) :

x = x'

source

@[simp]

theorem except_t.run_pure {α ε : Type u} {m : Type u → Type v} [monad m] (a : α) :

(pure a).run = pure (except.ok a)

source

@[simp]

theorem except_t.run_bind {α β ε : Type u} {m : Type u → Type v} (x : except_t ε m α) [monad m] (f : α → except_t ε m β) :

(x >>= f).run = x.run >>= except_t.bind_cont f

source

@[simp]

theorem except_t.run_map {α β ε : Type u} {m : Type u → Type v} (x : except_t ε m α) [monad m] (f : α → β) [is_lawful_monad m] :

(f <$> x).run = except.map f <$> x.run

source

@[simp]

theorem except_t.run_monad_lift {α ε : Type u} {m : Type u → Type v} [monad m] {n : Type u → Type u_1} [has_monad_lift_t n m] (x : n α) :

(monad_lift x).run = except.ok <$> monad_lift x

source

@[simp]

theorem except_t.run_monad_map {α ε : Type u} {m : Type u → Type v} (x : except_t ε m α) [monad m] {m' : Type u → Type v} {n n' : Type u → Type u_1} [monad m'] [monad_functor_t n n' m m'] (f : Π {α : Type u}, n α → n' α) :

(monad_map f x).run = monad_map f x.run

source

@[protected, instance]

def except_t.is_lawful_monad (m : Type u → Type v) [monad m] [is_lawful_monad m] (ε : Type u) :

is_lawful_monad (except_t ε m)

source

@[ext]

theorem reader_t.ext {ρ : Type u} {m : Type u → Type v} {α : Type u} {x x' : reader_t ρ m α} (h : ∀ (r : ρ), x.run r = x'.run r) :

x = x'

source

@[simp]

theorem reader_t.run_pure {ρ : Type u} {m : Type u → Type v} {α : Type u} (r : ρ) [monad m] (a : α) :

(pure a).run r = pure a

source

@[simp]

theorem reader_t.run_bind {ρ : Type u} {m : Type u → Type v} {α β : Type u} (x : reader_t ρ m α) (r : ρ) [monad m] (f : α → reader_t ρ m β) :

(x >>= f).run r = x.run r >>= λ (a : α), (f a).run r

source

@[simp]

theorem reader_t.run_map {ρ : Type u} {m : Type u → Type v} {α β : Type u} (x : reader_t ρ m α) (r : ρ) [monad m] (f : α → β) [is_lawful_monad m] :

(f <$> x).run r = f <$> x.run r

source

@[simp]

theorem reader_t.run_monad_lift {ρ : Type u} {m : Type u → Type v} {α : Type u} (r : ρ) [monad m] {n : Type u → Type u_1} [has_monad_lift_t n m] (x : n α) :

(monad_lift x).run r = monad_lift x

source

@[simp]

theorem reader_t.run_monad_map {ρ : Type u} {m : Type u → Type v} {α : Type u} (x : reader_t ρ m α) (r : ρ) [monad m] {m' : Type u → Type v} {n n' : Type u → Type u_1} [monad m'] [monad_functor_t n n' m m'] (f : Π {α : Type u}, n α → n' α) :

(monad_map f x).run r = monad_map f (x.run r)

source

@[simp]

theorem reader_t.run_read {ρ : Type u} {m : Type u → Type v} (r : ρ) [monad m] :

reader_t.read.run r = pure r

source

@[protected, instance]

def reader_t.is_lawful_monad (ρ : Type u) (m : Type u → Type v) [monad m] [is_lawful_monad m] :

is_lawful_monad (reader_t ρ m)

source

@[ext]

theorem option_t.ext {α : Type u} {m : Type u → Type v} {x x' : option_t m α} (h : x.run = x'.run) :

x = x'

source

@[simp]

theorem option_t.run_pure {α : Type u} {m : Type u → Type v} [monad m] (a : α) :

(pure a).run = pure (some a)

source

@[simp]

theorem option_t.run_bind {α β : Type u} {m : Type u → Type v} (x : option_t m α) [monad m] (f : α → option_t m β) :

(x >>= f).run = x.run >>= option_t.bind_cont f

source

@[simp]

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

(f <$> x).run = option.map f <$> x.run

source

@[simp]

theorem option_t.run_monad_lift {α : Type u} {m : Type u → Type v} [monad m] {n : Type u → Type u_1} [has_monad_lift_t n m] (x : n α) :

(monad_lift x).run = some <$> monad_lift x

source

@[simp]

theorem option_t.run_monad_map {α : Type u} {m : Type u → Type v} (x : option_t m α) [monad m] {m' : Type u → Type v} {n n' : Type u → Type u_1} [monad m'] [monad_functor_t n n' m m'] (f : Π {α : Type u}, n α → n' α) :

(monad_map f x).run = monad_map f x.run

source

@[protected, instance]

def option_t.is_lawful_monad (m : Type u → Type v) [monad m] [is_lawful_monad m] :

is_lawful_monad (option_t m)