Lemmas about List.mapM and List.forM.

Monadic operations

mapM

def List.mapM' {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → m β) : List α → m (List β)

Alternate (non-tail-recursive) form of mapM for proofs.

Equations

• List.mapM' f [] = pure []
• List.mapM' f (a :: l) = do let __do_lift ← f a let __do_lift_1 ← List.mapM' f l pure (__do_lift :: __do_lift_1)

@[simp]

theorem List.mapM'_nil {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] {f : α → m β} : List.mapM' f [] = pure []

@[simp]

theorem List.mapM'_cons {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {a : α} {l : List α} [Monad m] {f : α → m β} : List.mapM' f (a :: l) = do let __do_lift ← f a let __do_lift_1 ← List.mapM' f l pure (__do_lift :: __do_lift_1)

theorem List.mapM'_eq_mapM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → m β) (l : List α) : List.mapM' f l = List.mapM f l

theorem List.mapM'_eq_mapM.go {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → m β) (l : List α) (acc : List β) : List.mapM.loop f l acc = do let __do_lift ← List.mapM' f l pure (acc.reverse ++ __do_lift)

@[simp]

theorem List.mapM_nil {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → m β) : List.mapM f [] = pure []

@[simp]

theorem List.mapM_cons {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {a : α} {l : List α} [Monad m] [LawfulMonad m] (f : α → m β) : List.mapM f (a :: l) = do let __do_lift ← f a let __do_lift_1 ← List.mapM f l pure (__do_lift :: __do_lift_1)

@[simp]

theorem List.mapM_id {α : Type u_1} {β : Type u_2} {l : List α} {f : α → Id β} : List.mapM f l = List.map f l

@[simp]

theorem List.mapM_append {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → m β) {l₁ l₂ : List α} : List.mapM f (l₁ ++ l₂) = do let __do_lift ← List.mapM f l₁ let __do_lift_1 ← List.mapM f l₂ pure (__do_lift ++ __do_lift_1)

theorem List.foldlM_cons_eq_append {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → m β) (as : List α) (b : β) (bs : List β) : List.foldlM (fun (acc : List β) (a : α) => do let __do_lift ← f a pure (__do_lift :: acc)) (b :: bs) as = (fun (x : List β) => x ++ b :: bs) <$> List.foldlM (fun (acc : List β) (a : α) => do let __do_lift ← f a pure (__do_lift :: acc)) [] as

Auxiliary lemma for mapM_eq_reverse_foldlM_cons.

theorem List.mapM_eq_reverse_foldlM_cons {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → m β) (l : List α) : List.mapM f l = List.reverse <$> List.foldlM (fun (acc : List β) (a : α) => do let __do_lift ← f a pure (__do_lift :: acc)) [] l

foldlM and foldrM

theorem List.foldlM_map {m : Type u_1 → Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {α : Type u_1} [Monad m] (f : β₁ → β₂) (g : α → β₂ → m α) (l : List β₁) (init : α) : List.foldlM g init (List.map f l) = List.foldlM (fun (x : α) (y : β₁) => g x (f y)) init l

theorem List.foldrM_map {m : Type u_1 → Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {α : Type u_1} [Monad m] [LawfulMonad m] (f : β₁ → β₂) (g : β₂ → α → m α) (l : List β₁) (init : α) : List.foldrM g init (List.map f l) = List.foldrM (fun (x : β₁) (y : α) => g (f x) y) init l

theorem List.foldlM_filterMap {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_1} [Monad m] [LawfulMonad m] (f : α → Option β) (g : γ → β → m γ) (l : List α) (init : γ) : List.foldlM g init (List.filterMap f l) = List.foldlM (fun (x : γ) (y : α) => match f y with | some b => g x b | none => pure x) init l

theorem List.foldrM_filterMap {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_1} [Monad m] [LawfulMonad m] (f : α → Option β) (g : β → γ → m γ) (l : List α) (init : γ) : List.foldrM g init (List.filterMap f l) = List.foldrM (fun (x : α) (y : γ) => match f x with | some b => g b y | none => pure y) init l

theorem List.foldlM_filter {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (p : α → Bool) (g : β → α → m β) (l : List α) (init : β) : List.foldlM g init (List.filter p l) = List.foldlM (fun (x : β) (y : α) => if p y = true then g x y else pure x) init l

theorem List.foldrM_filter {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (p : α → Bool) (g : α → β → m β) (l : List α) (init : β) : List.foldrM g init (List.filter p l) = List.foldrM (fun (x : α) (y : β) => if p x = true then g x y else pure y) init l

forM

@[simp]

theorem List.forM_nil' {m : Type u_1 → Type u_2} {α : Type u_3} {f : α → m PUnit} [Monad m] : [].forM f = pure PUnit.unit

@[simp]

theorem List.forM_cons' {m : Type u_1 → Type u_2} {α✝ : Type u_3} {a : α✝} {as : List α✝} {f : α✝ → m PUnit} [Monad m] : (a :: as).forM f = do f a as.forM f

@[simp]

theorem List.forM_append {m : Type u_1 → Type u_2} {α : Type u_3} [Monad m] [LawfulMonad m] (l₁ l₂ : List α) (f : α → m PUnit) : (l₁ ++ l₂).forM f = do l₁.forM f l₂.forM f

forIn'

theorem List.forIn'_loop_congr {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {xs : List α} [Monad m] {as bs : List α} {f : (a' : α) → a' ∈ as → β → m (ForInStep β)} {g : (a' : α) → a' ∈ bs → β → m (ForInStep β)} {b : β} (ha : ∃ (ys : List α), ys ++ xs = as) (hb : ∃ (ys : List α), ys ++ xs = bs) (h : ∀ (a : α) (m_1 : a ∈ as) (m' : a ∈ bs) (b : β), f a m_1 b = g a m' b) : List.forIn'.loop as f xs b ha = List.forIn'.loop bs g xs b hb

@[simp]

theorem List.forIn'_cons {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] {a : α} {as : List α} (f : (a' : α) → a' ∈ a :: as → β → m (ForInStep β)) (b : β) : forIn' (a :: as) b f = do let x ← f a ⋯ b match x with | ForInStep.done b => pure b | ForInStep.yield b => forIn' as b fun (a' : α) (m : a' ∈ as) (b : β) => f a' ⋯ b

@[simp]

theorem List.forIn_cons {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → β → m (ForInStep β)) (a : α) (as : List α) (b : β) : forIn (a :: as) b f = do let x ← f a b match x with | ForInStep.done b => pure b | ForInStep.yield b => forIn as b f

theorem List.forIn'_congr {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] {as bs : List α} (w : as = bs) {b b' : β} (hb : b = b') {f : (a' : α) → a' ∈ as → β → m (ForInStep β)} {g : (a' : α) → a' ∈ bs → β → m (ForInStep β)} (h : ∀ (a : α) (m_1 : a ∈ bs) (b : β), f a ⋯ b = g a m_1 b) : forIn' as b f = forIn' bs b' g

theorem List.forIn'_eq_foldlM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (l : List α) (f : (a : α) → a ∈ l → β → m (ForInStep β)) (init : β) : forIn' l init f = ForInStep.value <$> List.foldlM (fun (b : ForInStep β) (x : { x : α // x ∈ l }) => match x with | ⟨a, m_1⟩ => match b with | ForInStep.yield b => f a m_1 b | ForInStep.done b => pure (ForInStep.done b)) (ForInStep.yield init) l.attach

We can express a for loop over a list as a fold, in which whenever we reach .done b we keep that value through the rest of the fold.

@[simp]

theorem List.forIn'_yield_eq_foldlM {m : Type u_1 → Type u_2} {α : Type u_3} {β γ : Type u_1} [Monad m] [LawfulMonad m] (l : List α) (f : (a : α) → a ∈ l → β → m γ) (g : (a : α) → a ∈ l → β → γ → β) (init : β) : (forIn' l init fun (a : α) (m_1 : a ∈ l) (b : β) => (fun (c : γ) => ForInStep.yield (g a m_1 b c)) <$> f a m_1 b) = List.foldlM (fun (b : β) (x : { x : α // x ∈ l }) => match x with | ⟨a, m_1⟩ => g a m_1 b <$> f a m_1 b) init l.attach

We can express a for loop over a list which always yields as a fold.

theorem List.forIn'_pure_yield_eq_foldl {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (l : List α) (f : (a : α) → a ∈ l → β → β) (init : β) : (forIn' l init fun (a : α) (m_1 : a ∈ l) (b : β) => pure (ForInStep.yield (f a m_1 b))) = pure (List.foldl (fun (b : β) (x : { x : α // x ∈ l }) => match x with | ⟨a, h⟩ => f a h b) init l.attach)

@[simp]

theorem List.forIn'_yield_eq_foldl {α : Type u_1} {β : Type u_2} (l : List α) (f : (a : α) → a ∈ l → β → β) (init : β) : (forIn' l init fun (a : α) (m : a ∈ l) (b : β) => ForInStep.yield (f a m b)) = List.foldl (fun (b : β) (x : { x : α // x ∈ l }) => match x with | ⟨a, h⟩ => f a h b) init l.attach

theorem List.forIn_eq_foldlM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → β → m (ForInStep β)) (init : β) (l : List α) : forIn l init f = ForInStep.value <$> List.foldlM (fun (b : ForInStep β) (a : α) => match b with | ForInStep.yield b => f a b | ForInStep.done b => pure (ForInStep.done b)) (ForInStep.yield init) l

We can express a for loop over a list as a fold, in which whenever we reach .done b we keep that value through the rest of the fold.

@[simp]

theorem List.forIn_yield_eq_foldlM {m : Type u_1 → Type u_2} {α : Type u_3} {β γ : Type u_1} [Monad m] [LawfulMonad m] (l : List α) (f : α → β → m γ) (g : α → β → γ → β) (init : β) : (forIn l init fun (a : α) (b : β) => (fun (c : γ) => ForInStep.yield (g a b c)) <$> f a b) = List.foldlM (fun (b : β) (a : α) => g a b <$> f a b) init l

We can express a for loop over a list which always yields as a fold.

theorem List.forIn_pure_yield_eq_foldl {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (l : List α) (f : α → β → β) (init : β) : (forIn l init fun (a : α) (b : β) => pure (ForInStep.yield (f a b))) = pure (List.foldl (fun (b : β) (a : α) => f a b) init l)

@[simp]

theorem List.forIn_yield_eq_foldl {α : Type u_1} {β : Type u_2} (l : List α) (f : α → β → β) (init : β) : (forIn l init fun (a : α) (b : β) => ForInStep.yield (f a b)) = List.foldl (fun (b : β) (a : α) => f a b) init l

allM

theorem List.allM_eq_not_anyM_not {m : Type → Type u_1} {α : Type u_2} [Monad m] [LawfulMonad m] (p : α → m Bool) (as : List α) : List.allM p as = (fun (x : Bool) => !x) <$> List.anyM (fun (x : α) => (fun (x : Bool) => !x) <$> p x) as