internlm/Lean-Github huggingface dataset:
Theorem: Insert.mem_into_iff
Proof state before:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
L : List τ
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldr (fun y x => f x y) init L.reverse
perm : L.reverse.Perm (toList c)
⊢ x ∈ fold c insert empty ↔ x ∈ c
Tactic:
generalize L.reverse = L' at perm h
Proof state after:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
L L' : List τ
perm : L'.Perm (toList c)
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldr (fun y x => f x y) init L'
⊢ x ∈ fold c insert empty ↔ x ∈ c
Theorem: Insert.mem_into_iff
Proof state before:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
L L' : List τ
perm : L'.Perm (toList c)
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldr (fun y x => f x y) init L'
⊢ x ∈ fold c insert empty ↔ x ∈ c
Tactic:
clear L
Proof state after:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
L' : List τ
perm : L'.Perm (toList c)
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldr (fun y x => f x y) init L'
⊢ x ∈ fold c insert empty ↔ x ∈ c
Theorem: Insert.mem_into_iff
Proof state before:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
L' : List τ
perm : L'.Perm (toList c)
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldr (fun y x => f x y) init L'
⊢ x ∈ fold c insert empty ↔ x ∈ c
Tactic:
conv => lhs; rw [h]
Proof state after:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
L' : List τ
perm : L'.Perm (toList c)
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldr (fun y x => f x y) init L'
⊢ x ∈ List.foldr (fun y x => insert x y) empty L' ↔ x ∈ c
Theorem: Insert.mem_into_iff
Proof state before:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
L' : List τ
perm : L'.Perm (toList c)
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldr (fun y x => f x y) init L'
⊢ x ∈ List.foldr (fun y x => insert x y) empty L' ↔ x ∈ c
Tactic:
clear h
Proof state after:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
L' : List τ
perm : L'.Perm (toList c)
⊢ x ∈ List.foldr (fun y x => insert x y) empty L' ↔ x ∈ c
Theorem: Insert.mem_into_iff
Proof state before:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
L' : List τ
perm : L'.Perm (toList c)
⊢ x ∈ List.foldr (fun y x => insert x y) empty L' ↔ x ∈ c
Tactic:
conv => rhs; rw [Mem.ToList.mem_iff_mem_toList, ← perm.mem_iff]
Proof state after:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
L' : List τ
perm : L'.Perm (toList c)
⊢ x ∈ List.foldr (fun y x => insert x y) empty L' ↔ x ∈ L'
Theorem: Insert.mem_into_iff
Proof state before:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
L' : List τ
perm : L'.Perm (toList c)
⊢ x ∈ List.foldr (fun y x => insert x y) empty L' ↔ x ∈ L'
Tactic:
clear perm
Proof state after:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
L' : List τ
⊢ x ∈ List.foldr (fun y x => insert x y) empty L' ↔ x ∈ L'
Theorem: Insert.mem_into_iff
Proof state before:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
L' : List τ
⊢ x ∈ List.foldr (fun y x => insert x y) empty L' ↔ x ∈ L'
Tactic:
induction L' with
| nil =>
  simp [Mem.mem_empty]
| cons hd tl ih =>
  simp [Mem.mem_insert, ih]
Proof state after:
no goals
Theorem: Insert.mem_into_iff
Proof state before:
case nil
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
⊢ x ∈ List.foldr (fun y x => insert x y) empty [] ↔ x ∈ []
Tactic:
simp [Mem.mem_empty]
Proof state after:
no goals
Theorem: Insert.mem_into_iff
Proof state before:
case cons
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
hd : τ
tl : List τ
ih : x ∈ List.foldr (fun y x => insert x y) empty tl ↔ x ∈ tl
⊢ x ∈ List.foldr (fun y x => insert x y) empty (hd :: tl) ↔ x ∈ hd :: tl
Tactic:
simp [Mem.mem_insert, ih]
Proof state after:
no goals
Theorem: LeanColls.Fold.foldM_eq_foldM_toList
Proof state before:
C : Type u_3
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
m : Type u_1 → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
c : C
⊢ ∃ L, L.Perm (toList c) ∧ ∀ {β : Type u_1} (f : β → τ → m β) (init : β), foldM c f init = List.foldlM f init L
Tactic:
have ⟨L,perm,h⟩ := ToList.fold_eq_fold_toList c
Proof state after:
C : Type u_3
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
m : Type u_1 → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
c : C
L : List τ
perm : L.Perm (toList c)
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
⊢ ∃ L, L.Perm (toList c) ∧ ∀ {β : Type u_1} (f : β → τ → m β) (init : β), foldM c f init = List.foldlM f init L
Theorem: LeanColls.Fold.foldM_eq_foldM_toList
Proof state before:
C : Type u_3
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
m : Type u_1 → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
c : C
L : List τ
perm : L.Perm (toList c)
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
⊢ ∃ L, L.Perm (toList c) ∧ ∀ {β : Type u_1} (f : β → τ → m β) (init : β), foldM c f init = List.foldlM f init L
Tactic:
use L
Proof state after:
case h
C : Type u_3
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
m : Type u_1 → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
c : C
L : List τ
perm : L.Perm (toList c)
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
⊢ L.Perm (toList c) ∧ ∀ {β : Type u_1} (f : β → τ → m β) (init : β), foldM c f init = List.foldlM f init L
Theorem: LeanColls.Fold.foldM_eq_foldM_toList
Proof state before:
case h
C : Type u_3
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
m : Type u_1 → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
c : C
L : List τ
perm : L.Perm (toList c)
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
⊢ L.Perm (toList c) ∧ ∀ {β : Type u_1} (f : β → τ → m β) (init : β), foldM c f init = List.foldlM f init L
Tactic:
refine ⟨perm,?_⟩
Proof state after:
case h
C : Type u_3
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
m : Type u_1 → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
c : C
L : List τ
perm : L.Perm (toList c)
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
⊢ ∀ {β : Type u_1} (f : β → τ → m β) (init : β), foldM c f init = List.foldlM f init L
Theorem: LeanColls.Fold.foldM_eq_foldM_toList
Proof state before:
case h
C : Type u_3
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
m : Type u_1 → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
c : C
L : List τ
perm : L.Perm (toList c)
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
⊢ ∀ {β : Type u_1} (f : β → τ → m β) (init : β), foldM c f init = List.foldlM f init L
Tactic:
clear perm
Proof state after:
case h
C : Type u_3
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
m : Type u_1 → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
c : C
L : List τ
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
⊢ ∀ {β : Type u_1} (f : β → τ → m β) (init : β), foldM c f init = List.foldlM f init L
Theorem: LeanColls.Fold.foldM_eq_foldM_toList
Proof state before:
case h
C : Type u_3
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
m : Type u_1 → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
c : C
L : List τ
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
⊢ ∀ {β : Type u_1} (f : β → τ → m β) (init : β), foldM c f init = List.foldlM f init L
Tactic:
intro β f init
Proof state after:
case h
C : Type u_3
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
m : Type u_1 → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
c : C
L : List τ
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
β : Type u_1
f : β → τ → m β
init : β
⊢ foldM c f init = List.foldlM f init L
Theorem: LeanColls.Fold.foldM_eq_foldM_toList
Proof state before:
case h
C : Type u_3
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
m : Type u_1 → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
c : C
L : List τ
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
β : Type u_1
f : β → τ → m β
init : β
⊢ foldM c f init = List.foldlM f init L
Tactic:
rw [ToList.foldM_eq_fold, h, List.foldlM_eq_foldl]
Proof state after:
no goals
Theorem: LeanColls.Fold.bind_fold_pure
Proof 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
Proof 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
Theorem: LeanColls.Fold.bind_fold_pure
Proof 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⟩
Proof 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
Theorem: LeanColls.Fold.bind_fold_pure
Proof 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]
Proof 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
Theorem: LeanColls.Fold.bind_fold_pure
Proof 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
Proof 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
Theorem: LeanColls.Fold.bind_fold_pure
Proof 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]
Proof 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
Theorem: LeanColls.Fold.bind_fold_pure
Proof 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]
Proof 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
Theorem: LeanColls.Fold.bind_fold_pure
Proof 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
Proof 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
Theorem: LeanColls.Fold.bind_fold_pure
Proof 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
Proof state after:
no goals
Theorem: LeanColls.Fold.bind_fold_pure
Proof 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
Proof state after:
no goals
Theorem: LeanColls.Fold.bind_fold_pure
Proof 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
Proof 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
Theorem: LeanColls.Fold.bind_fold_pure
Proof 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]
Proof 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