Free Monad of a Polynomial Functor

We define the free monad on a polynomial functor (PFunctor), and prove some basic properties.

def Parser.Attr.freeM_unfold_proc : Lean.ParserDescr

Simplification procedure

def Parser.Attr.freeM_unfold : Lean.ParserDescr

Simp set for structurally unfolding FreeM and displayed-family operations.

This set is reserved for one-way unfolding lemmas: constructor equations for FreeM operations, displayed-family operations, and local-hom recursion through roll. Folding and normalization lemmas should not be tagged with this attribute.

inductive PFunctor.FreeM (P : PFunctor.{uA, uB}) : Type v → Type (max uA uB v)

The free monad on a polynomial functor. This extends the W-type construction with an extra pure constructor.

• pure {P : PFunctor.{uA, uB}} {α : Type v} (x : α) : P.FreeM α
• roll {P : PFunctor.{uA, uB}} {α : Type v} (a : P.A) (r : P.B a → P.FreeM α) : P.FreeM α

@[implicit_reducible]

instance PFunctor.instInhabitedFreeM {a✝ : PFunctor.{u_1, u_2}} {a✝¹ : Type u_3} [Inhabited a✝¹] : Inhabited (a✝.FreeM a✝¹)

def PFunctor.instInhabitedFreeM.default {a✝ : PFunctor.{u_1, u_2}} {a✝¹ : Type u_3} [Inhabited a✝¹] : a✝.FreeM a✝¹

@[reducible, inline]

def PFunctor.FreeM.lift {P : PFunctor.{uA, uB}} {α : Type v} (x : ↑P α) : P.FreeM α

Lift an object of the base polynomial functor into the free monad.

@[reducible, inline]

def PFunctor.FreeM.liftA {P : PFunctor.{uA, uB}} (a : P.A) : P.FreeM (P.B a)

Lift a position of the base polynomial functor into the free monad.

@[implicit_reducible]

instance PFunctor.FreeM.instMonadLiftObj {P : PFunctor.{uA, uB}} : MonadLift (↑P) P.FreeM

@[simp]

theorem PFunctor.FreeM.lift_ne_pure {P : PFunctor.{uA, uB}} {α : Type v} (x : ↑P α) (y : α) : lift x ≠ pure y

@[simp]

theorem PFunctor.FreeM.pure_ne_lift {P : PFunctor.{uA, uB}} {α : Type v} (x : ↑P α) (y : α) : pure y ≠ lift x

theorem PFunctor.FreeM.monadLift_eq_lift {P : PFunctor.{uA, uB}} {α : Type v} (x : ↑P α) : liftM x = lift x

@[inline]

def PFunctor.FreeM.bind {P : PFunctor.{uA, uB}} {α β : Type v} : P.FreeM α → (α → P.FreeM β) → P.FreeM β

Bind operator on FreeM P operation used in the monad definition.

@[simp]

theorem PFunctor.FreeM.bind_pure {P : PFunctor.{uA, uB}} {α β : Type v} (x : α) (r : α → P.FreeM β) : (pure x).bind r = r x

@[simp]

theorem PFunctor.FreeM.bind_roll {P : PFunctor.{uA, uB}} {β γ : Type v} (a : P.A) (r : P.B a → P.FreeM β) (g : β → P.FreeM γ) : (roll a r).bind g = roll a fun (u : P.B a) => (r u).bind g

@[simp]

theorem PFunctor.FreeM.bind_lift {P : PFunctor.{uA, uB}} {α β : Type v} (x : ↑P α) (r : α → P.FreeM β) : (lift x).bind r = roll x.fst fun (a : P.B x.fst) => r (x.snd a)

@[simp]

theorem PFunctor.FreeM.bind_eq_pure_iff {P : PFunctor.{uA, uB}} {α β : Type v} (x : P.FreeM α) (y : α → P.FreeM β) (y' : β) : x.bind y = pure y' ↔ ∃ (x' : α), x = pure x' ∧ y x' = pure y'

@[simp]

theorem PFunctor.FreeM.pure_eq_bind_iff {P : PFunctor.{uA, uB}} {α β : Type v} (x : P.FreeM α) (y : α → P.FreeM β) (y' : β) : pure y' = x.bind y ↔ ∃ (x' : α), x = pure x' ∧ pure y' = y x'

@[implicit_reducible]

instance PFunctor.FreeM.instMonad {P : PFunctor.{uA, uB}} : Monad P.FreeM

theorem PFunctor.FreeM.monad_pure_def {P : PFunctor.{uA, uB}} {α : Type v} (x : α) : pure x = pure x

theorem PFunctor.FreeM.monad_bind_def {P : PFunctor.{uA, uB}} {α β : Type v} (x : P.FreeM α) (g : α → P.FreeM β) : x >>= g = x.bind g

instance PFunctor.FreeM.instLawfulMonad {P : PFunctor.{uA, uB}} : LawfulMonad P.FreeM

theorem PFunctor.FreeM.pure_inj {P : PFunctor.{uA, uB}} {α : Type v} (x y : α) : pure x = pure y ↔ x = y

@[simp]

theorem PFunctor.FreeM.roll_inj {P : PFunctor.{uA, uB}} {α : Type v} (x x' : P.A) (y : P.B x → P.FreeM α) (y' : P.B x' → P.FreeM α) : roll x y = roll x' y' ↔ ∃ (h : x = x'), Eq.rec (motive := fun (x_1 : P.A) (h : x = x_1) => P.B x_1 → P.FreeM α) y h = y'

def PFunctor.FreeM.mapLens {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} (l : P.Lens Q) : P.FreeM α → Q.FreeM α

Transport a free polynomial tree along a polynomial lens.

The source polynomial P is the abstract/control interface. The target polynomial Q is the concrete/runtime interface. At each P-node, the lens chooses a Q-position by toFunA; when runtime supplies a Q-direction, toFunB maps it back to the corresponding P-direction selecting the control continuation.

@[simp]

theorem PFunctor.FreeM.mapLens_pure {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} (l : P.Lens Q) (x : α) : FreeM.mapLens l (pure x) = pure x

@[simp]

theorem PFunctor.FreeM.mapLens_roll {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} (l : P.Lens Q) (a : P.A) (rest : P.B a → P.FreeM α) : FreeM.mapLens l (roll a rest) = roll (l.toFunA a) fun (d : Q.B (l.toFunA a)) => FreeM.mapLens l (rest (l.toFunB a d))

@[simp]

theorem PFunctor.FreeM.mapLens_id {P : PFunctor.{uA, uB}} {α : Type v} (x : P.FreeM α) : FreeM.mapLens (Lens.id P) x = x

@[simp]

theorem PFunctor.FreeM.mapLens_comp {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} (l₂ : Q.Lens R) (l₁ : P.Lens Q) (x : P.FreeM α) : FreeM.mapLens l₂ (FreeM.mapLens l₁ x) = FreeM.mapLens (l₂ ∘ₗ l₁) x

@[simp]

theorem PFunctor.FreeM.mapLens_bind {P : PFunctor.{uA, uB}} {α β : Type v} {Q : PFunctor.{uA₂, uB₂}} (l : P.Lens Q) (x : P.FreeM α) (f : α → P.FreeM β) : FreeM.mapLens l (x.bind f) = (FreeM.mapLens l x).bind fun (a : α) => FreeM.mapLens l (f a)

@[simp]

theorem PFunctor.FreeM.mapLens_bind' {P : PFunctor.{uA, uB}} {α β : Type v} {Q : PFunctor.{uA₂, uB₂}} (l : P.Lens Q) (x : P.FreeM α) (f : α → P.FreeM β) : FreeM.mapLens l (x >>= f) = do let a ← FreeM.mapLens l x FreeM.mapLens l (f a)

def PFunctor.FreeM.inductionOn {P : PFunctor.{uA, uB}} {α : Type v} {C : P.FreeM α → Prop} (pure : ∀ (x : α), C (pure x)) (roll : ∀ (x : P.A) (r : P.B x → P.FreeM α), (∀ (y : P.B x), C (r y)) → C (roll x r)) (oa : P.FreeM α) : C oa

Proving a predicate C of FreeM P α requires two cases:

• pure x for some x : α
• roll x r h for some x : P.A, r : P.B x → FreeM P α, and h : ∀ y, C (r y) Note that we can't use Sort v instead of Prop due to universe levels.

def PFunctor.FreeM.construct {P : PFunctor.{uA, uB}} {α : Type v} {C : P.FreeM α → Type u_1} (pure : (x : α) → C (pure x)) (roll : (x : P.A) → (r : P.B x → P.FreeM α) → ((y : P.B x) → C (r y)) → C (roll x r)) (oa : P.FreeM α) : C oa

Shoulde be possible to unify with the above

@[simp]

theorem PFunctor.FreeM.construct_pure {P : PFunctor.{uA, uB}} {α : Type v} {C : P.FreeM α → Type u_1} (h_pure : (x : α) → C (pure x)) (h_roll : (x : P.A) → (r : P.B x → P.FreeM α) → ((y : P.B x) → C (r y)) → C (roll x r)) (y : α) : FreeM.construct h_pure h_roll (pure y) = h_pure y

@[simp]

theorem PFunctor.FreeM.construct_roll {P : PFunctor.{uA, uB}} {α : Type v} {C : P.FreeM α → Type u_1} (h_pure : (x : α) → C (pure x)) (h_roll : (x : P.A) → (r : P.B x → P.FreeM α) → ((y : P.B x) → C (r y)) → C (roll x r)) (x : P.A) (r : P.B x → P.FreeM α) : FreeM.construct h_pure h_roll (roll x r) = h_roll x r fun (u : P.B x) => FreeM.construct h_pure h_roll (r u)

def PFunctor.FreeM.mapM {P : PFunctor.{uA, uB}} {m : Type uB → Type v} {α : Type uB} [Pure m] [Bind m] (s : (a : P.A) → m (P.B a)) : P.FreeM α → m α

Canonical mapping of FreeM P into any other monad, given a map s : (a : P.A) → m (P.B a).

@[simp]

theorem PFunctor.FreeM.mapM_pure' {P : PFunctor.{uA, uB}} {m : Type uB → Type v} {α : Type uB} [Monad m] (s : (a : P.A) → m (P.B a)) (x : α) : FreeM.mapM s (pure x) = Pure.pure x

@[simp]

theorem PFunctor.FreeM.mapM_roll {P : PFunctor.{uA, uB}} {m : Type uB → Type v} {α : Type uB} [Monad m] (s : (a : P.A) → m (P.B a)) (x : P.A) (r : P.B x → P.FreeM α) : FreeM.mapM s (roll x r) = do let u ← s x FreeM.mapM s (r u)

@[simp]

theorem PFunctor.FreeM.mapM_pure {P : PFunctor.{uA, uB}} {m : Type uB → Type v} {α : Type uB} [Monad m] (s : (a : P.A) → m (P.B a)) (x : α) : FreeM.mapM s (Pure.pure x) = Pure.pure x

@[simp]

theorem PFunctor.FreeM.mapM_bind {P : PFunctor.{uA, uB}} {m : Type uB → Type v} [Monad m] (s : (a : P.A) → m (P.B a)) [LawfulMonad m] {α β : Type uB} (x : P.FreeM α) (y : α → P.FreeM β) : FreeM.mapM s (x.bind y) = do let u ← FreeM.mapM s x FreeM.mapM s (y u)

@[simp]

theorem PFunctor.FreeM.mapM_bind' {P : PFunctor.{uA, uB}} {m : Type uB → Type v} [Monad m] (s : (a : P.A) → m (P.B a)) [LawfulMonad m] {α β : Type uB} (x : P.FreeM α) (y : α → P.FreeM β) : FreeM.mapM s (x >>= y) = do let u ← FreeM.mapM s x FreeM.mapM s (y u)

@[simp]

theorem PFunctor.FreeM.mapM_map {P : PFunctor.{uA, uB}} {m : Type uB → Type v} [Monad m] (s : (a : P.A) → m (P.B a)) [LawfulMonad m] {α β : Type uB} (x : P.FreeM α) (f : α → β) : FreeM.mapM s (f <$> x) = f <$> FreeM.mapM s x

@[simp]

theorem PFunctor.FreeM.mapM_seq {P : PFunctor.{uA, uB}} {m : Type uB → Type v} [Monad m] [LawfulMonad m] {α β : Type uB} (s : (a : P.A) → m (P.B a)) (x : P.FreeM (α → β)) (y : P.FreeM α) : FreeM.mapM s (x <*> y) = FreeM.mapM s x <*> FreeM.mapM s y

@[simp]

theorem PFunctor.FreeM.mapM_lift {P : PFunctor.{uA, uB}} {m : Type uB → Type v} {α : Type uB} [Monad m] [LawfulMonad m] (s : (a : P.A) → m (P.B a)) (x : ↑P α) : FreeM.mapM s (lift x) = do let u ← s x.fst FreeM.mapM s (pure (x.snd u))

@[simp]

theorem PFunctor.FreeM.mapM_liftA {P : PFunctor.{uA, uB}} {m : Type uB → Type v} [Monad m] [LawfulMonad m] (s : (a : P.A) → m (P.B a)) (x : P.A) : FreeM.mapM s (liftA x) = s x

def PFunctor.FreeM.mapMHom {P : PFunctor.{uA, uB}} {m : Type uB → Type v} [Monad m] [LawfulMonad m] (s : (a : P.A) → m (P.B a)) : P.FreeM →ᵐ m

FreeM.mapM as a monad homomorphism.

@[simp]

theorem PFunctor.FreeM.mapMHom_toFun_eq {P : PFunctor.{uA, uB}} {m : Type uB → Type v} {α : Type uB} [Monad m] [LawfulMonad m] (s : (a : P.A) → m (P.B a)) : (FreeM.mapMHom s).toFun α = FreeM.mapM s

def PFunctor.FreeM.mapMHom' {P : PFunctor.{uA, uB}} {m : Type uB → Type v} [Monad m] [LawfulMonad m] (s : NatHom (↑P) m) : P.FreeM →ᵐ m

@[simp]

theorem PFunctor.FreeM.mapMHom'_toFun_eq {P : PFunctor.{uA, uB}} {m : Type uB → Type v} {α : Type uB} [Monad m] [LawfulMonad m] (s : NatHom (↑P) m) : (FreeM.mapMHom' s).toFun α = FreeM.mapM fun (t : P.A) => (fun {α : Type uB} (x : ↑P α) => s.toFun α x) ⟨t, id⟩