Theorem: LeanColls.Fold.bind_fold_pure (LeanColls/Classes/Ops/Fold.lean)

State before:
C : Type u_3
τ : Type u_4
inst✝⁵ : Fold C τ
inst✝⁴ : LeanColls.ToList C τ
inst✝³ : ToList C τ
m : Type u_1 → Type u_2
α : Type u_1
inst✝² : ToList C τ
inst✝¹ : Monad m
inst✝ : LawfulMonad m
ma : m α
c : C
f : α → τ → m α
⊢ (do
      let a ← ma
      fold c
          (fun acc t => do
            let acc ← acc
            f acc t)
          (pure a)) =
    fold c
      (fun acc t => do
        let acc ← acc
        f acc t)
      ma
Tactic:
have := ToList.fold_eq_fold_toList c
State after:
C : Type u_3
τ : Type u_4
inst✝⁵ : Fold C τ
inst✝⁴ : LeanColls.ToList C τ
inst✝³ : ToList C τ
m : Type u_1 → Type u_2
α : Type u_1
inst✝² : ToList C τ
inst✝¹ : Monad m
inst✝ : LawfulMonad m
ma : m α
c : C
f : α → τ → m α
this : ∃ L, L.Perm (toList c) ∧ ∀ {β : Type u_2} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
⊢ (do
      let a ← ma
      fold c
          (fun acc t => do
            let acc ← acc
            f acc t)
          (pure a)) =
    fold c
      (fun acc t => do
        let acc ← acc
        f acc t)
      ma

State before:
C : Type u_3
τ : Type u_4
inst✝⁵ : Fold C τ
inst✝⁴ : LeanColls.ToList C τ
inst✝³ : ToList C τ
m : Type u_1 → Type u_2
α : Type u_1
inst✝² : ToList C τ
inst✝¹ : Monad m
inst✝ : LawfulMonad m
ma : m α
c : C
f : α → τ → m α
this : ∃ L, L.Perm (toList c) ∧ ∀ {β : Type u_2} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
⊢ (do
      let a ← ma
      fold c
          (fun acc t => do
            let acc ← acc
            f acc t)
          (pure a)) =
    fold c
      (fun acc t => do
        let acc ← acc
        f acc t)
      ma
Tactic:
rcases this with ⟨L,-,h⟩
State after:
case intro.intro
C : Type u_3
τ : Type u_4
inst✝⁵ : Fold C τ
inst✝⁴ : LeanColls.ToList C τ
inst✝³ : ToList C τ
m : Type u_1 → Type u_2
α : Type u_1
inst✝² : ToList C τ
inst✝¹ : Monad m
inst✝ : LawfulMonad m
ma : m α
c : C
f : α → τ → m α
L : List τ
h : ∀ {β : Type u_2} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
⊢ (do
      let a ← ma
      fold c
          (fun acc t => do
            let acc ← acc
            f acc t)
          (pure a)) =
    fold c
      (fun acc t => do
        let acc ← acc
        f acc t)
      ma

State before:
case intro.intro
C : Type u_3
τ : Type u_4
inst✝⁵ : Fold C τ
inst✝⁴ : LeanColls.ToList C τ
inst✝³ : ToList C τ
m : Type u_1 → Type u_2
α : Type u_1
inst✝² : ToList C τ
inst✝¹ : Monad m
inst✝ : LawfulMonad m
ma : m α
c : C
f : α → τ → m α
L : List τ
h : ∀ {β : Type u_2} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
⊢ (do
      let a ← ma
      fold c
          (fun acc t => do
            let acc ← acc
            f acc t)
          (pure a)) =
    fold c
      (fun acc t => do
        let acc ← acc
        f acc t)
      ma
Tactic:
simp [h]
State after:
case intro.intro
C : Type u_3
τ : Type u_4
inst✝⁵ : Fold C τ
inst✝⁴ : LeanColls.ToList C τ
inst✝³ : ToList C τ
m : Type u_1 → Type u_2
α : Type u_1
inst✝² : ToList C τ
inst✝¹ : Monad m
inst✝ : LawfulMonad m
ma : m α
c : C
f : α → τ → m α
L : List τ
h : ∀ {β : Type u_2} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
⊢ (do
      let a ← ma
      List.foldl
          (fun acc t => do
            let acc ← acc
            f acc t)
          (pure a) L) =
    List.foldl
      (fun acc t => do
        let acc ← acc
        f acc t)
      ma L

State before:
case intro.intro
C : Type u_3
τ : Type u_4
inst✝⁵ : Fold C τ
inst✝⁴ : LeanColls.ToList C τ
inst✝³ : ToList C τ
m : Type u_1 → Type u_2
α : Type u_1
inst✝² : ToList C τ
inst✝¹ : Monad m
inst✝ : LawfulMonad m
ma : m α
c : C
f : α → τ → m α
L : List τ
h : ∀ {β : Type u_2} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
⊢ (do
      let a ← ma
      List.foldl
          (fun acc t => do
            let acc ← acc
            f acc t)
          (pure a) L) =
    List.foldl
      (fun acc t => do
        let acc ← acc
        f acc t)
      ma L
Tactic:
clear h
State after:
case intro.intro
C : Type u_3
τ : Type u_4
inst✝⁵ : Fold C τ
inst✝⁴ : LeanColls.ToList C τ
inst✝³ : ToList C τ
m : Type u_1 → Type u_2
α : Type u_1
inst✝² : ToList C τ
inst✝¹ : Monad m
inst✝ : LawfulMonad m
ma : m α
c : C
f : α → τ → m α
L : List τ
⊢ (do
      let a ← ma
      List.foldl
          (fun acc t => do
            let acc ← acc
            f acc t)
          (pure a) L) =
    List.foldl
      (fun acc t => do
        let acc ← acc
        f acc t)
      ma L

State before:
case intro.intro
C : Type u_3
τ : Type u_4
inst✝⁵ : Fold C τ
inst✝⁴ : LeanColls.ToList C τ
inst✝³ : ToList C τ
m : Type u_1 → Type u_2
α : Type u_1
inst✝² : ToList C τ
inst✝¹ : Monad m
inst✝ : LawfulMonad m
ma : m α
c : C
f : α → τ → m α
L : List τ
⊢ (do
      let a ← ma
      List.foldl
          (fun acc t => do
            let acc ← acc
            f acc t)
          (pure a) L) =
    List.foldl
      (fun acc t => do
        let acc ← acc
        f acc t)
      ma L
Tactic:
rw [← List.foldr_reverse]
State after:
case intro.intro
C : Type u_3
τ : Type u_4
inst✝⁵ : Fold C τ
inst✝⁴ : LeanColls.ToList C τ
inst✝³ : ToList C τ
m : Type u_1 → Type u_2
α : Type u_1
inst✝² : ToList C τ
inst✝¹ : Monad m
inst✝ : LawfulMonad m
ma : m α
c : C
f : α → τ → m α
L : List τ
⊢ (do
      let a ← ma
      List.foldl
          (fun acc t => do
            let acc ← acc
            f acc t)
          (pure a) L) =
    List.foldr
      (fun t acc => do
        let acc ← acc
        f acc t)
      ma L.reverse

State before:
case intro.intro
C : Type u_3
τ : Type u_4
inst✝⁵ : Fold C τ
inst✝⁴ : LeanColls.ToList C τ
inst✝³ : ToList C τ
m : Type u_1 → Type u_2
α : Type u_1
inst✝² : ToList C τ
inst✝¹ : Monad m
inst✝ : LawfulMonad m
ma : m α
c : C
f : α → τ → m α
L : List τ
⊢ (do
      let a ← ma
      List.foldl
          (fun acc t => do
            let acc ← acc
            f acc t)
          (pure a) L) =
    List.foldr
      (fun t acc => do
        let acc ← acc
        f acc t)
      ma L.reverse
Tactic:
conv => lhs; arg 2; ext; rw [← List.foldr_reverse]
State after:
case intro.intro
C : Type u_3
τ : Type u_4
inst✝⁵ : Fold C τ
inst✝⁴ : LeanColls.ToList C τ
inst✝³ : ToList C τ
m : Type u_1 → Type u_2
α : Type u_1
inst✝² : ToList C τ
inst✝¹ : Monad m
inst✝ : LawfulMonad m
ma : m α
c : C
f : α → τ → m α
L : List τ
⊢ (do
      let x ← ma
      List.foldr
          (fun t acc => do
            let acc ← acc
            f acc t)
          (pure x) L.reverse) =
    List.foldr
      (fun t acc => do
        let acc ← acc
        f acc t)
      ma L.reverse

State before:
case intro.intro
C : Type u_3
τ : Type u_4
inst✝⁵ : Fold C τ
inst✝⁴ : LeanColls.ToList C τ
inst✝³ : ToList C τ
m : Type u_1 → Type u_2
α : Type u_1
inst✝² : ToList C τ
inst✝¹ : Monad m
inst✝ : LawfulMonad m
ma : m α
c : C
f : α → τ → m α
L : List τ
⊢ (do
      let x ← ma
      List.foldr
          (fun t acc => do
            let acc ← acc
            f acc t)
          (pure x) L.reverse) =
    List.foldr
      (fun t acc => do
        let acc ← acc
        f acc t)
      ma L.reverse
Tactic:
generalize L.reverse = L
State after:
case intro.intro
C : Type u_3
τ : Type u_4
inst✝⁵ : Fold C τ
inst✝⁴ : LeanColls.ToList C τ
inst✝³ : ToList C τ
m : Type u_1 → Type u_2
α : Type u_1
inst✝² : ToList C τ
inst✝¹ : Monad m
inst✝ : LawfulMonad m
ma : m α
c : C
f : α → τ → m α
L✝ L : List τ
⊢ (do
      let x ← ma
      List.foldr
          (fun t acc => do
            let acc ← acc
            f acc t)
          (pure x) L) =
    List.foldr
      (fun t acc => do
        let acc ← acc
        f acc t)
      ma L

State before:
case intro.intro
C : Type u_3
τ : Type u_4
inst✝⁵ : Fold C τ
inst✝⁴ : LeanColls.ToList C τ
inst✝³ : ToList C τ
m : Type u_1 → Type u_2
α : Type u_1
inst✝² : ToList C τ
inst✝¹ : Monad m
inst✝ : LawfulMonad m
ma : m α
c : C
f : α → τ → m α
L✝ L : List τ
⊢ (do
      let x ← ma
      List.foldr
          (fun t acc => do
            let acc ← acc
            f acc t)
          (pure x) L) =
    List.foldr
      (fun t acc => do
        let acc ← acc
        f acc t)
      ma L
Tactic:
induction L with
| nil => simp
| cons hd tl ih =>
  simp; rw [← ih]
  simp
State after:
no goals

State before:
case intro.intro.nil
C : Type u_3
τ : Type u_4
inst✝⁵ : Fold C τ
inst✝⁴ : LeanColls.ToList C τ
inst✝³ : ToList C τ
m : Type u_1 → Type u_2
α : Type u_1
inst✝² : ToList C τ
inst✝¹ : Monad m
inst✝ : LawfulMonad m
ma : m α
c : C
f : α → τ → m α
L : List τ
⊢ (do
      let x ← ma
      List.foldr
          (fun t acc => do
            let acc ← acc
            f acc t)
          (pure x) []) =
    List.foldr
      (fun t acc => do
        let acc ← acc
        f acc t)
      ma []
Tactic:
simp
State after:
no goals

State before:
case intro.intro.cons
C : Type u_3
τ : Type u_4
inst✝⁵ : Fold C τ
inst✝⁴ : LeanColls.ToList C τ
inst✝³ : ToList C τ
m : Type u_1 → Type u_2
α : Type u_1
inst✝² : ToList C τ
inst✝¹ : Monad m
inst✝ : LawfulMonad m
ma : m α
c : C
f : α → τ → m α
L : List τ
hd : τ
tl : List τ
ih :
  (do
      let x ← ma
      List.foldr
          (fun t acc => do
            let acc ← acc
            f acc t)
          (pure x) tl) =
    List.foldr
      (fun t acc => do
        let acc ← acc
        f acc t)
      ma tl
⊢ (do
      let x ← ma
      List.foldr
          (fun t acc => do
            let acc ← acc
            f acc t)
          (pure x) (hd :: tl)) =
    List.foldr
      (fun t acc => do
        let acc ← acc
        f acc t)
      ma (hd :: tl)
Tactic:
simp
State after:
case intro.intro.cons
C : Type u_3
τ : Type u_4
inst✝⁵ : Fold C τ
inst✝⁴ : LeanColls.ToList C τ
inst✝³ : ToList C τ
m : Type u_1 → Type u_2
α : Type u_1
inst✝² : ToList C τ
inst✝¹ : Monad m
inst✝ : LawfulMonad m
ma : m α
c : C
f : α → τ → m α
L : List τ
hd : τ
tl : List τ
ih :
  (do
      let x ← ma
      List.foldr
          (fun t acc => do
            let acc ← acc
            f acc t)
          (pure x) tl) =
    List.foldr
      (fun t acc => do
        let acc ← acc
        f acc t)
      ma tl
⊢ (do
      let x ← ma
      let acc ←
        List.foldr
            (fun t acc => do
              let acc ← acc
              f acc t)
            (pure x) tl
      f acc hd) =
    do
    let acc ←
      List.foldr
          (fun t acc => do
            let acc ← acc
            f acc t)
          ma tl
    f acc hd

State before:
case intro.intro.cons
C : Type u_3
τ : Type u_4
inst✝⁵ : Fold C τ
inst✝⁴ : LeanColls.ToList C τ
inst✝³ : ToList C τ
m : Type u_1 → Type u_2
α : Type u_1
inst✝² : ToList C τ
inst✝¹ : Monad m
inst✝ : LawfulMonad m
ma : m α
c : C
f : α → τ → m α
L : List τ
hd : τ
tl : List τ
ih :
  (do
      let x ← ma
      List.foldr
          (fun t acc => do
            let acc ← acc
            f acc t)
          (pure x) tl) =
    List.foldr
      (fun t acc => do
        let acc ← acc
        f acc t)
      ma tl
⊢ (do
      let x ← ma
      let acc ←
        List.foldr
            (fun t acc => do
              let acc ← acc
              f acc t)
            (pure x) tl
      f acc hd) =
    do
    let acc ←
      List.foldr
          (fun t acc => do
            let acc ← acc
            f acc t)
          ma tl
    f acc hd
Tactic:
rw [← ih]
State after:
case intro.intro.cons
C : Type u_3
τ : Type u_4
inst✝⁵ : Fold C τ
inst✝⁴ : LeanColls.ToList C τ
inst✝³ : ToList C τ
m : Type u_1 → Type u_2
α : Type u_1
inst✝² : ToList C τ
inst✝¹ : Monad m
inst✝ : LawfulMonad m
ma : m α
c : C
f : α → τ → m α
L : List τ
hd : τ
tl : List τ
ih :
  (do
      let x ← ma
      List.foldr
          (fun t acc => do
            let acc ← acc
            f acc t)
          (pure x) tl) =
    List.foldr
      (fun t acc => do
        let acc ← acc
        f acc t)
      ma tl
⊢ (do
      let x ← ma
      let acc ←
        List.foldr
            (fun t acc => do
              let acc ← acc
              f acc t)
            (pure x) tl
      f acc hd) =
    do
    let acc ←
      do
        let x ← ma
        List.foldr
            (fun t acc => do
              let acc ← acc
              f acc t)
            (pure x) tl
    f acc hd

State before:
case intro.intro.cons
C : Type u_3
τ : Type u_4
inst✝⁵ : Fold C τ
inst✝⁴ : LeanColls.ToList C τ
inst✝³ : ToList C τ
m : Type u_1 → Type u_2
α : Type u_1
inst✝² : ToList C τ
inst✝¹ : Monad m
inst✝ : LawfulMonad m
ma : m α
c : C
f : α → τ → m α
L : List τ
hd : τ
tl : List τ
ih :
  (do
      let x ← ma
      List.foldr
          (fun t acc => do
            let acc ← acc
            f acc t)
          (pure x) tl) =
    List.foldr
      (fun t acc => do
        let acc ← acc
        f acc t)
      ma tl
⊢ (do
      let x ← ma
      let acc ←
        List.foldr
            (fun t acc => do
              let acc ← acc
              f acc t)
            (pure x) tl
      f acc hd) =
    do
    let acc ←
      do
        let x ← ma
        List.foldr
            (fun t acc => do
              let acc ← acc
              f acc t)
            (pure x) tl
    f acc hd
Tactic:
simp
State after:
no goals