Note about Mathlib/Init/

The files in Mathlib/Init are leftovers from the port from Mathlib3. (They contain content moved from lean3 itself that Mathlib needed but was not moved to lean4.)

We intend to move all the content of these files out into the main Mathlib directory structure. Contributions assisting with this are appreciated.

#align statements without corresponding declarations (i.e. because the declaration is in Batteries or Lean) can be left here. These will be deleted soon so will not significantly delay deleting otherwise empty Init files.

Functor Laws, applicative laws, and monad Laws

def StateT.mk {σ : Type u} {m : Type u → Type v} {α : Type u} (f : σ → m (α × σ)) : StateT σ m α

Equations

• StateT.mk f = f

@[simp]

theorem StateT.run_mk {σ : Type u} {m : Type u → Type v} {α : Type u} (f : σ → m (α × σ)) (st : σ) : (StateT.mk f).run st = f st

@[simp]

theorem ExceptT.run_mk {α : Type u} {ε : Type u} {m : Type u → Type v} (x : m (Except ε α)) : (ExceptT.mk x).run = x

@[simp]

theorem ExceptT.run_monadLift {α : Type u} {ε : Type u} {m : Type u → Type v} [Monad m] {n : Type u → Type u_1} [MonadLiftT n m] (x : n α) : (monadLift x).run = Except.ok <$> monadLift x

@[simp]

theorem ExceptT.run_monadMap {α : Type u} {ε : Type u} {m : Type u → Type v} (x : ExceptT ε m α) {n : Type u → Type u_1} [MonadFunctorT n m] (f : {α : Type u} → n α → n α) : (monadMap f x).run = monadMap f x.run

def ReaderT.mk {m : Type u → Type v} {α : Type u} {σ : Type u} (f : σ → m α) : ReaderT σ m α

Equations

• ReaderT.mk f = f

@[simp]

theorem ReaderT.run_mk {m : Type u → Type v} {α : Type u} {σ : Type u} (f : σ → m α) (r : σ) : (ReaderT.mk f).run r = f r

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

@[simp]

theorem OptionT.run_mk {α : Type u} {m : Type u → Type v} (x : m (Option α)) : (OptionT.mk x).run = x

@[simp]

theorem OptionT.run_pure {α : Type u} {m : Type u → Type v} [Monad m] (a : α) : (pure a).run = pure (some a)

@[simp]

theorem OptionT.run_bind {α : Type u} {β : Type u} {m : Type u → Type v} (x : OptionT m α) [Monad m] (f : α → OptionT m β) : (x >>= f).run = do let x ← x.run match x with | some a => (f a).run | none => pure none

@[simp]

theorem OptionT.run_map {α : Type u} {β : Type u} {m : Type u → Type v} (x : OptionT m α) [Monad m] (f : α → β) [LawfulMonad m] : (f <$> x).run = Option.map f <$> x.run

@[simp]

theorem OptionT.run_monadLift {α : Type u} {m : Type u → Type v} [Monad m] {n : Type u → Type u_1} [MonadLiftT n m] (x : n α) : (monadLift x).run = do let a ← monadLift x pure (some a)

@[simp]

theorem OptionT.run_monadMap {α : Type u} {m : Type u → Type v} (x : OptionT m α) {n : Type u → Type u_1} [MonadFunctorT n m] (f : {α : Type u} → n α → n α) : (monadMap f x).run = monadMap f x.run

instance instLawfulMonadOptionT_mathlib (m : Type u → Type v) [Monad m] [LawfulMonad m] : LawfulMonad (OptionT m)

Equations

• ⋯ = ⋯

Lawfulness of IO

At some point core intends to make IO opaque, which would break these proofs As discussed in https://github.com/leanprover/std4/pull/416, it should be possible for core to expose the lawfulness of IO as part of the opaque interface, which would remove the need for these proofs anyway.

These are not in Batteries because Batteries does not want to deal with the churn from such a core refactor.

instance instLawfulMonadEIO_mathlib {ε : Type} : LawfulMonad (EIO ε)

Equations

• ⋯ = ⋯

instance instLawfulMonadBaseIO_mathlib : LawfulMonad BaseIO

Equations

• instLawfulMonadBaseIO_mathlib = ⋯

instance instLawfulMonadIO_mathlib : LawfulMonad IO

Equations

• instLawfulMonadIO_mathlib = ⋯

instance instLawfulMonadEST_mathlib {ε : Type} {σ : Type} : LawfulMonad (EST ε σ)

Equations

• ⋯ = ⋯

instance instLawfulMonadST_mathlib {ε : Type} : LawfulMonad (ST ε)

Equations

• ⋯ = ⋯