internlm/Lean-Github huggingface dataset:
Theorem: Fin.foldlM_eq_foldl
Proof state before:
case zero
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
i : ℕ
macc : m β
hj : i = n
⊢ (do
      let acc ← macc
      foldlM.aux n f i acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      macc i
Tactic:
cases hj
Proof state after:
case zero.refl
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
macc : m β
⊢ (do
      let acc ← macc
      foldlM.aux n f n acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      macc n
Theorem: Fin.foldlM_eq_foldl
Proof state before:
case zero.refl
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
macc : m β
⊢ (do
      let acc ← macc
      foldlM.aux n f n acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      macc n
Tactic:
unfold foldl.loop
Proof state after:
case zero.refl
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
macc : m β
⊢ (do
      let acc ← macc
      foldlM.aux n f n acc) =
    if h : n < n then
      foldl.loop n
        (fun macc i => do
          let acc ← macc
          f i acc)
        (do
          let acc ← macc
          f ⟨n, h⟩ acc)
        (n + 1)
    else macc
Theorem: Fin.foldlM_eq_foldl
Proof state before:
case zero.refl
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
macc : m β
⊢ (do
      let acc ← macc
      foldlM.aux n f n acc) =
    if h : n < n then
      foldl.loop n
        (fun macc i => do
          let acc ← macc
          f i acc)
        (do
          let acc ← macc
          f ⟨n, h⟩ acc)
        (n + 1)
    else macc
Tactic:
unfold foldlM.aux
Proof state after:
case zero.refl
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
macc : m β
⊢ (do
      let acc ← macc
      if h' : n < n then do
          let acc ← f ⟨n, h'⟩ acc
          foldlM.aux n f (n + 1) acc
        else pure acc) =
    if h : n < n then
      foldl.loop n
        (fun macc i => do
          let acc ← macc
          f i acc)
        (do
          let acc ← macc
          f ⟨n, h⟩ acc)
        (n + 1)
    else macc
Theorem: Fin.foldlM_eq_foldl
Proof state before:
case zero.refl
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
macc : m β
⊢ (do
      let acc ← macc
      if h' : n < n then do
          let acc ← f ⟨n, h'⟩ acc
          foldlM.aux n f (n + 1) acc
        else pure acc) =
    if h : n < n then
      foldl.loop n
        (fun macc i => do
          let acc ← macc
          f i acc)
        (do
          let acc ← macc
          f ⟨n, h⟩ acc)
        (n + 1)
    else macc
Tactic:
simp
Proof state after:
no goals
Theorem: Fin.foldlM_eq_foldl
Proof state before:
case succ
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
j' : ℕ
ih :
  ∀ (i : ℕ),
    i + j' = n →
      ∀ (macc : m β),
        (do
            let acc ← macc
            foldlM.aux n f i acc) =
          foldl.loop n
            (fun macc i => do
              let acc ← macc
              f i acc)
            macc i
i : ℕ
hj : i + (j' + 1) = n
⊢ ∀ (macc : m β),
    (do
        let acc ← macc
        foldlM.aux n f i acc) =
      foldl.loop n
        (fun macc i => do
          let acc ← macc
          f i acc)
        macc i
Tactic:
intro macc
Proof state after:
case succ
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
j' : ℕ
ih :
  ∀ (i : ℕ),
    i + j' = n →
      ∀ (macc : m β),
        (do
            let acc ← macc
            foldlM.aux n f i acc) =
          foldl.loop n
            (fun macc i => do
              let acc ← macc
              f i acc)
            macc i
i : ℕ
hj : i + (j' + 1) = n
macc : m β
⊢ (do
      let acc ← macc
      foldlM.aux n f i acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      macc i
Theorem: Fin.foldlM_eq_foldl
Proof state before:
case succ
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
j' : ℕ
ih :
  ∀ (i : ℕ),
    i + j' = n →
      ∀ (macc : m β),
        (do
            let acc ← macc
            foldlM.aux n f i acc) =
          foldl.loop n
            (fun macc i => do
              let acc ← macc
              f i acc)
            macc i
i : ℕ
hj : i + (j' + 1) = n
macc : m β
⊢ (do
      let acc ← macc
      foldlM.aux n f i acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      macc i
Tactic:
rw [Nat.add_succ, ← Nat.succ_add] at hj
Proof state after:
case succ
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
j' : ℕ
ih :
  ∀ (i : ℕ),
    i + j' = n →
      ∀ (macc : m β),
        (do
            let acc ← macc
            foldlM.aux n f i acc) =
          foldl.loop n
            (fun macc i => do
              let acc ← macc
              f i acc)
            macc i
i : ℕ
hj : i.succ + j' = n
macc : m β
⊢ (do
      let acc ← macc
      foldlM.aux n f i acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      macc i
Theorem: Fin.foldlM_eq_foldl
Proof state before:
case succ
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
j' : ℕ
ih :
  ∀ (i : ℕ),
    i + j' = n →
      ∀ (macc : m β),
        (do
            let acc ← macc
            foldlM.aux n f i acc) =
          foldl.loop n
            (fun macc i => do
              let acc ← macc
              f i acc)
            macc i
i : ℕ
hj : i.succ + j' = n
macc : m β
⊢ (do
      let acc ← macc
      foldlM.aux n f i acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      macc i
Tactic:
have hi : i < n := by calc
  _ ≤ Nat.succ i + j' := Nat.le_add_right _ _
  _ = n := hj
Proof state after:
case succ
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
j' : ℕ
ih :
  ∀ (i : ℕ),
    i + j' = n →
      ∀ (macc : m β),
        (do
            let acc ← macc
            foldlM.aux n f i acc) =
          foldl.loop n
            (fun macc i => do
              let acc ← macc
              f i acc)
            macc i
i : ℕ
hj : i.succ + j' = n
macc : m β
hi : i < n
⊢ (do
      let acc ← macc
      foldlM.aux n f i acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      macc i
Theorem: Fin.foldlM_eq_foldl
Proof state before:
case succ
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
j' : ℕ
ih :
  ∀ (i : ℕ),
    i + j' = n →
      ∀ (macc : m β),
        (do
            let acc ← macc
            foldlM.aux n f i acc) =
          foldl.loop n
            (fun macc i => do
              let acc ← macc
              f i acc)
            macc i
i : ℕ
hj : i.succ + j' = n
macc : m β
hi : i < n
⊢ (do
      let acc ← macc
      foldlM.aux n f i acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      macc i
Tactic:
have := ih (i+1) hj (macc >>= fun acc => f ⟨i,hi⟩ acc)
Proof state after:
case succ
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
j' : ℕ
ih :
  ∀ (i : ℕ),
    i + j' = n →
      ∀ (macc : m β),
        (do
            let acc ← macc
            foldlM.aux n f i acc) =
          foldl.loop n
            (fun macc i => do
              let acc ← macc
              f i acc)
            macc i
i : ℕ
hj : i.succ + j' = n
macc : m β
hi : i < n
this :
  (do
      let acc ←
        do
          let acc ← macc
          f ⟨i, hi⟩ acc
      foldlM.aux n f (i + 1) acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      (do
        let acc ← macc
        f ⟨i, hi⟩ acc)
      (i + 1)
⊢ (do
      let acc ← macc
      foldlM.aux n f i acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      macc i
Theorem: Fin.foldlM_eq_foldl
Proof state before:
case succ
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
j' : ℕ
ih :
  ∀ (i : ℕ),
    i + j' = n →
      ∀ (macc : m β),
        (do
            let acc ← macc
            foldlM.aux n f i acc) =
          foldl.loop n
            (fun macc i => do
              let acc ← macc
              f i acc)
            macc i
i : ℕ
hj : i.succ + j' = n
macc : m β
hi : i < n
this :
  (do
      let acc ←
        do
          let acc ← macc
          f ⟨i, hi⟩ acc
      foldlM.aux n f (i + 1) acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      (do
        let acc ← macc
        f ⟨i, hi⟩ acc)
      (i + 1)
⊢ (do
      let acc ← macc
      foldlM.aux n f i acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      macc i
Tactic:
clear ih
Proof state after:
case succ
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
j' i : ℕ
hj : i.succ + j' = n
macc : m β
hi : i < n
this :
  (do
      let acc ←
        do
          let acc ← macc
          f ⟨i, hi⟩ acc
      foldlM.aux n f (i + 1) acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      (do
        let acc ← macc
        f ⟨i, hi⟩ acc)
      (i + 1)
⊢ (do
      let acc ← macc
      foldlM.aux n f i acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      macc i
Theorem: Fin.foldlM_eq_foldl
Proof state before:
case succ
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
j' i : ℕ
hj : i.succ + j' = n
macc : m β
hi : i < n
this :
  (do
      let acc ←
        do
          let acc ← macc
          f ⟨i, hi⟩ acc
      foldlM.aux n f (i + 1) acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      (do
        let acc ← macc
        f ⟨i, hi⟩ acc)
      (i + 1)
⊢ (do
      let acc ← macc
      foldlM.aux n f i acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      macc i
Tactic:
unfold foldl.loop
Proof state after:
case succ
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
j' i : ℕ
hj : i.succ + j' = n
macc : m β
hi : i < n
this :
  (do
      let acc ←
        do
          let acc ← macc
          f ⟨i, hi⟩ acc
      foldlM.aux n f (i + 1) acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      (do
        let acc ← macc
        f ⟨i, hi⟩ acc)
      (i + 1)
⊢ (do
      let acc ← macc
      foldlM.aux n f i acc) =
    if h : i < n then
      foldl.loop n
        (fun macc i => do
          let acc ← macc
          f i acc)
        (do
          let acc ← macc
          f ⟨i, h⟩ acc)
        (i + 1)
    else macc
Theorem: Fin.foldlM_eq_foldl
Proof state before:
case succ
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
j' i : ℕ
hj : i.succ + j' = n
macc : m β
hi : i < n
this :
  (do
      let acc ←
        do
          let acc ← macc
          f ⟨i, hi⟩ acc
      foldlM.aux n f (i + 1) acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      (do
        let acc ← macc
        f ⟨i, hi⟩ acc)
      (i + 1)
⊢ (do
      let acc ← macc
      foldlM.aux n f i acc) =
    if h : i < n then
      foldl.loop n
        (fun macc i => do
          let acc ← macc
          f i acc)
        (do
          let acc ← macc
          f ⟨i, h⟩ acc)
        (i + 1)
    else macc
Tactic:
unfold foldlM.aux
Proof state after:
case succ
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
j' i : ℕ
hj : i.succ + j' = n
macc : m β
hi : i < n
this :
  (do
      let acc ←
        do
          let acc ← macc
          f ⟨i, hi⟩ acc
      foldlM.aux n f (i + 1) acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      (do
        let acc ← macc
        f ⟨i, hi⟩ acc)
      (i + 1)
⊢ (do
      let acc ← macc
      if h' : i < n then do
          let acc ← f ⟨i, h'⟩ acc
          foldlM.aux n f (i + 1) acc
        else pure acc) =
    if h : i < n then
      foldl.loop n
        (fun macc i => do
          let acc ← macc
          f i acc)
        (do
          let acc ← macc
          f ⟨i, h⟩ acc)
        (i + 1)
    else macc
Theorem: Fin.foldlM_eq_foldl
Proof state before:
case succ
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
j' i : ℕ
hj : i.succ + j' = n
macc : m β
hi : i < n
this :
  (do
      let acc ←
        do
          let acc ← macc
          f ⟨i, hi⟩ acc
      foldlM.aux n f (i + 1) acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      (do
        let acc ← macc
        f ⟨i, hi⟩ acc)
      (i + 1)
⊢ (do
      let acc ← macc
      if h' : i < n then do
          let acc ← f ⟨i, h'⟩ acc
          foldlM.aux n f (i + 1) acc
        else pure acc) =
    if h : i < n then
      foldl.loop n
        (fun macc i => do
          let acc ← macc
          f i acc)
        (do
          let acc ← macc
          f ⟨i, h⟩ acc)
        (i + 1)
    else macc
Tactic:
simp_all
Proof state after:
no goals
Theorem: Fin.foldlM_eq_foldl
Proof state before:
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
j' : ℕ
ih :
  ∀ (i : ℕ),
    i + j' = n →
      ∀ (macc : m β),
        (do
            let acc ← macc
            foldlM.aux n f i acc) =
          foldl.loop n
            (fun macc i => do
              let acc ← macc
              f i acc)
            macc i
i : ℕ
hj : i.succ + j' = n
macc : m β
⊢ i < n
Tactic:
calc
_ ≤ Nat.succ i + j' := Nat.le_add_right _ _
_ = n := hj
Proof state after:
no goals
Theorem: Fin.foldl_eq_foldl_ofFn
Proof state before:
α : Type u_1
n : ℕ
f : α → Fin n → α
init : α
⊢ foldl n f init = List.foldl f init (List.ofFn id)
Tactic:
unfold foldl
Proof state after:
α : Type u_1
n : ℕ
f : α → Fin n → α
init : α
⊢ foldl.loop n f init 0 = List.foldl f init (List.ofFn id)
Theorem: Fin.foldl_eq_foldl_ofFn
Proof state before:
α : Type u_1
n : ℕ
f : α → Fin n → α
init : α
⊢ foldl.loop n f init 0 = List.foldl f init (List.ofFn id)
Tactic:
suffices ∀ init i j (h : i + j = n),
  foldl.loop n f init i =
    List.foldl f init (List.ofFn (n := j) (fun x => Fin.natAdd i x |>.cast h))
  by
    have := this init 0 n (by simp)
    simp at this; rw [this]; rfl
Proof state after:
α : Type u_1
n : ℕ
f : α → Fin n → α
init : α
⊢ ∀ (init : α) (i j : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
Theorem: Fin.foldl_eq_foldl_ofFn
Proof state before:
α : Type u_1
n : ℕ
f : α → Fin n → α
init : α
⊢ ∀ (init : α) (i j : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
Tactic:
intro init i j h
Proof state after:
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ init : α
i j : ℕ
h : i + j = n
⊢ foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
Theorem: Fin.foldl_eq_foldl_ofFn
Proof state before:
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ init : α
i j : ℕ
h : i + j = n
⊢ foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
Tactic:
induction j generalizing init i with
| zero =>
  unfold foldl.loop
  simp at h
  simp [List.drop_eq_nil_of_le, h]
| succ j ih =>
  unfold foldl.loop
  have : i < n := by omega
  simp [this, cast]
  generalize f init _ = init'
  have : (i+1) + j = n := by omega
  specialize ih init' (i+1) this
  rw [ih]; clear ih
  congr
  funext ⟨x,hx⟩; simp; omega
Proof state after:
no goals
Theorem: Fin.foldl_eq_foldl_ofFn
Proof state before:
α : Type u_1
n : ℕ
f : α → Fin n → α
init : α
this :
  ∀ (init : α) (i j : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
⊢ foldl.loop n f init 0 = List.foldl f init (List.ofFn id)
Tactic:
have := this init 0 n (by simp)
Proof state after:
α : Type u_1
n : ℕ
f : α → Fin n → α
init : α
this✝ :
  ∀ (init : α) (i j : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
this : foldl.loop n f init 0 = List.foldl f init (List.ofFn fun x => cast ⋯ (natAdd 0 x))
⊢ foldl.loop n f init 0 = List.foldl f init (List.ofFn id)
Theorem: Fin.foldl_eq_foldl_ofFn
Proof state before:
α : Type u_1
n : ℕ
f : α → Fin n → α
init : α
this✝ :
  ∀ (init : α) (i j : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
this : foldl.loop n f init 0 = List.foldl f init (List.ofFn fun x => cast ⋯ (natAdd 0 x))
⊢ foldl.loop n f init 0 = List.foldl f init (List.ofFn id)
Tactic:
simp at this
Proof state after:
α : Type u_1
n : ℕ
f : α → Fin n → α
init : α
this✝ :
  ∀ (init : α) (i j : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
this : foldl.loop n f init 0 = List.foldl f init (List.ofFn fun x => x.addNat 0)
⊢ foldl.loop n f init 0 = List.foldl f init (List.ofFn id)
Theorem: Fin.foldl_eq_foldl_ofFn
Proof state before:
α : Type u_1
n : ℕ
f : α → Fin n → α
init : α
this✝ :
  ∀ (init : α) (i j : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
this : foldl.loop n f init 0 = List.foldl f init (List.ofFn fun x => x.addNat 0)
⊢ foldl.loop n f init 0 = List.foldl f init (List.ofFn id)
Tactic:
rw [this]
Proof state after:
α : Type u_1
n : ℕ
f : α → Fin n → α
init : α
this✝ :
  ∀ (init : α) (i j : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
this : foldl.loop n f init 0 = List.foldl f init (List.ofFn fun x => x.addNat 0)
⊢ List.foldl f init (List.ofFn fun x => x.addNat 0) = List.foldl f init (List.ofFn id)
Theorem: Fin.foldl_eq_foldl_ofFn
Proof state before:
α : Type u_1
n : ℕ
f : α → Fin n → α
init : α
this✝ :
  ∀ (init : α) (i j : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
this : foldl.loop n f init 0 = List.foldl f init (List.ofFn fun x => x.addNat 0)
⊢ List.foldl f init (List.ofFn fun x => x.addNat 0) = List.foldl f init (List.ofFn id)
Tactic:
rfl
Proof state after:
no goals
Theorem: Fin.foldl_eq_foldl_ofFn
Proof state before:
α : Type u_1
n : ℕ
f : α → Fin n → α
init : α
this :
  ∀ (init : α) (i j : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
⊢ 0 + n = n
Tactic:
simp
Proof state after:
no goals
Theorem: Fin.foldl_eq_foldl_ofFn
Proof state before:
case zero
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ init : α
i : ℕ
h : i + 0 = n
⊢ foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
Tactic:
unfold foldl.loop
Proof state after:
case zero
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ init : α
i : ℕ
h : i + 0 = n
⊢ (if h : i < n then foldl.loop n f (f init ⟨i, h⟩) (i + 1) else init) =
    List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
Theorem: Fin.foldl_eq_foldl_ofFn
Proof state before:
case zero
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ init : α
i : ℕ
h : i + 0 = n
⊢ (if h : i < n then foldl.loop n f (f init ⟨i, h⟩) (i + 1) else init) =
    List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
Tactic:
simp at h
Proof state after:
case zero
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ init : α
i : ℕ
h✝ : i + 0 = n
h : i = n
⊢ (if h : i < n then foldl.loop n f (f init ⟨i, h⟩) (i + 1) else init) =
    List.foldl f init (List.ofFn fun x => cast h✝ (natAdd i x))
Theorem: Fin.foldl_eq_foldl_ofFn
Proof state before:
case zero
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ init : α
i : ℕ
h✝ : i + 0 = n
h : i = n
⊢ (if h : i < n then foldl.loop n f (f init ⟨i, h⟩) (i + 1) else init) =
    List.foldl f init (List.ofFn fun x => cast h✝ (natAdd i x))
Tactic:
simp [List.drop_eq_nil_of_le, h]
Proof state after:
no goals
Theorem: Fin.foldl_eq_foldl_ofFn
Proof state before:
case succ
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
ih :
  ∀ (init : α) (i : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
init : α
i : ℕ
h : i + (j + 1) = n
⊢ foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
Tactic:
unfold foldl.loop
Proof state after:
case succ
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
ih :
  ∀ (init : α) (i : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
init : α
i : ℕ
h : i + (j + 1) = n
⊢ (if h : i < n then foldl.loop n f (f init ⟨i, h⟩) (i + 1) else init) =
    List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
Theorem: Fin.foldl_eq_foldl_ofFn
Proof state before:
case succ
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
ih :
  ∀ (init : α) (i : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
init : α
i : ℕ
h : i + (j + 1) = n
⊢ (if h : i < n then foldl.loop n f (f init ⟨i, h⟩) (i + 1) else init) =
    List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
Tactic:
have : i < n := by omega
Proof state after:
case succ
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
ih :
  ∀ (init : α) (i : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
init : α
i : ℕ
h : i + (j + 1) = n
this : i < n
⊢ (if h : i < n then foldl.loop n f (f init ⟨i, h⟩) (i + 1) else init) =
    List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
Theorem: Fin.foldl_eq_foldl_ofFn
Proof state before:
case succ
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
ih :
  ∀ (init : α) (i : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
init : α
i : ℕ
h : i + (j + 1) = n
this : i < n
⊢ (if h : i < n then foldl.loop n f (f init ⟨i, h⟩) (i + 1) else init) =
    List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
Tactic:
simp [this, cast]
Proof state after:
case succ
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
ih :
  ∀ (init : α) (i : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
init : α
i : ℕ
h : i + (j + 1) = n
this : i < n
⊢ foldl.loop n f (f init ⟨i, ⋯⟩) (i + 1) = List.foldl f (f init ⟨i, ⋯⟩) (List.ofFn fun i_1 => ⟨i + (↑i_1 + 1), ⋯⟩)
Theorem: Fin.foldl_eq_foldl_ofFn
Proof state before:
case succ
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
ih :
  ∀ (init : α) (i : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
init : α
i : ℕ
h : i + (j + 1) = n
this : i < n
⊢ foldl.loop n f (f init ⟨i, ⋯⟩) (i + 1) = List.foldl f (f init ⟨i, ⋯⟩) (List.ofFn fun i_1 => ⟨i + (↑i_1 + 1), ⋯⟩)
Tactic:
generalize f init _ = init'
Proof state after:
case succ
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
ih :
  ∀ (init : α) (i : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
init : α
i : ℕ
h : i + (j + 1) = n
this : i < n
init' : α
⊢ foldl.loop n f init' (i + 1) = List.foldl f init' (List.ofFn fun i_1 => ⟨i + (↑i_1 + 1), ⋯⟩)