Theorem: Fin.foldl_eq_foldl' (LeanColls/MathlibUpstream.lean)

State before:
α : Sort u_1
n : ℕ
f : α → Fin n → α
init : α
⊢ foldl n f init = foldl' n init fun i h acc => f acc ⟨i, h⟩
Tactic:
simp [foldl, foldl']
State after:
α : Sort u_1
n : ℕ
f : α → Fin n → α
init : α
⊢ foldl.loop n f init 0 = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) 0 ⋯ init

State before:
α : Sort u_1
n : ℕ
f : α → Fin n → α
init : α
⊢ foldl.loop n f init 0 = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) 0 ⋯ init
Tactic:
suffices ∀ i j (hj : i + j = n) acc,
  foldl.loop n f acc i =
    foldl'.aux (n := n) (β := fun _ _ => α)
      init (fun i h acc => f acc ⟨i, h⟩)
      i (hj ▸ Nat.le_add_right i j) acc
  from this 0 n (by simp) init
State after:
α : Sort u_1
n : ℕ
f : α → Fin n → α
init : α
⊢ ∀ (i j : ℕ) (hj : i + j = n) (acc : α), foldl.loop n f acc i = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc

State before:
α : Sort u_1
n : ℕ
f : α → Fin n → α
init : α
⊢ ∀ (i j : ℕ) (hj : i + j = n) (acc : α), foldl.loop n f acc i = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc
Tactic:
intro i j hj
State after:
α : Sort u_1
n : ℕ
f : α → Fin n → α
init : α
i j : ℕ
hj : i + j = n
⊢ ∀ (acc : α), foldl.loop n f acc i = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc

State before:
α : Sort u_1
n : ℕ
f : α → Fin n → α
init : α
i j : ℕ
hj : i + j = n
⊢ ∀ (acc : α), foldl.loop n f acc i = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc
Tactic:
induction j generalizing i with
| zero =>
  intro acc
  simp at hj; cases hj
  unfold foldl.loop; unfold foldl'.aux
  simp
| succ j' ih =>
  intro acc
  simp_all
  rw [Nat.add_succ, ← Nat.succ_add] at hj
  have hi : i < n := by calc
    _ ≤ Nat.succ i + j' := Nat.le_add_right _ _
    _ = n := hj
  have := ih (i+1) hj (f acc ⟨i,hi⟩)
  clear ih
  unfold foldl.loop; unfold foldl'.aux
  simp [*]
State after:
no goals

State before:
α : Sort u_1
n : ℕ
f : α → Fin n → α
init : α
this :
  ∀ (i j : ℕ) (hj : i + j = n) (acc : α), foldl.loop n f acc i = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc
⊢ 0 + n = n
Tactic:
simp
State after:
no goals

State before:
case zero
α : Sort u_1
n : ℕ
f : α → Fin n → α
init : α
i : ℕ
hj : i + 0 = n
⊢ ∀ (acc : α), foldl.loop n f acc i = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc
Tactic:
intro acc
State after:
case zero
α : Sort u_1
n : ℕ
f : α → Fin n → α
init : α
i : ℕ
hj : i + 0 = n
acc : α
⊢ foldl.loop n f acc i = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc

State before:
case zero
α : Sort u_1
n : ℕ
f : α → Fin n → α
init : α
i : ℕ
hj : i + 0 = n
acc : α
⊢ foldl.loop n f acc i = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc
Tactic:
simp at hj
State after:
case zero
α : Sort u_1
n : ℕ
f : α → Fin n → α
init : α
i : ℕ
hj✝ : i + 0 = n
acc : α
hj : i = n
⊢ foldl.loop n f acc i = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc

State before:
case zero
α : Sort u_1
n : ℕ
f : α → Fin n → α
init : α
i : ℕ
hj✝ : i + 0 = n
acc : α
hj : i = n
⊢ foldl.loop n f acc i = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc
Tactic:
cases hj
State after:
case zero.refl
α : Sort u_1
n : ℕ
f : α → Fin n → α
init acc : α
hj : n + 0 = n
⊢ foldl.loop n f acc n = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) n ⋯ acc

State before:
case zero.refl
α : Sort u_1
n : ℕ
f : α → Fin n → α
init acc : α
hj : n + 0 = n
⊢ foldl.loop n f acc n = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) n ⋯ acc
Tactic:
unfold foldl.loop
State after:
case zero.refl
α : Sort u_1
n : ℕ
f : α → Fin n → α
init acc : α
hj : n + 0 = n
⊢ (if h : n < n then foldl.loop n f (f acc ⟨n, h⟩) (n + 1) else acc) =
    foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) n ⋯ acc

State before:
case zero.refl
α : Sort u_1
n : ℕ
f : α → Fin n → α
init acc : α
hj : n + 0 = n
⊢ (if h : n < n then foldl.loop n f (f acc ⟨n, h⟩) (n + 1) else acc) =
    foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) n ⋯ acc
Tactic:
unfold foldl'.aux
State after:
case zero.refl
α : Sort u_1
n : ℕ
f : α → Fin n → α
init acc : α
hj : n + 0 = n
⊢ (if h : n < n then foldl.loop n f (f acc ⟨n, h⟩) (n + 1) else acc) =
    if h' : n < n then foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) (n + 1) h' (f acc ⟨n, h'⟩)
    else
      let_fun this := ⋯;
      Eq.ndrec (motive := fun n_1 =>
        {β : (i : ℕ) → i ≤ n_1 → Sort u_1} →
          β 0 ⋯ → ((i : ℕ) → (h : i < n_1) → β i ⋯ → β (i + 1) h) → (h : n ≤ n_1) → β n h → ¬n < n_1 → β n_1 ⋯)
        (fun {β} init f h acc h' => acc) this init (fun i h acc => f acc ⟨i, h⟩) ⋯ acc h'

State before:
case zero.refl
α : Sort u_1
n : ℕ
f : α → Fin n → α
init acc : α
hj : n + 0 = n
⊢ (if h : n < n then foldl.loop n f (f acc ⟨n, h⟩) (n + 1) else acc) =
    if h' : n < n then foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) (n + 1) h' (f acc ⟨n, h'⟩)
    else
      let_fun this := ⋯;
      Eq.ndrec (motive := fun n_1 =>
        {β : (i : ℕ) → i ≤ n_1 → Sort u_1} →
          β 0 ⋯ → ((i : ℕ) → (h : i < n_1) → β i ⋯ → β (i + 1) h) → (h : n ≤ n_1) → β n h → ¬n < n_1 → β n_1 ⋯)
        (fun {β} init f h acc h' => acc) this init (fun i h acc => f acc ⟨i, h⟩) ⋯ acc h'
Tactic:
simp
State after:
no goals

State before:
case succ
α : Sort u_1
n : ℕ
f : α → Fin n → α
init : α
j' : ℕ
ih :
  ∀ (i : ℕ) (hj : i + j' = n) (acc : α), foldl.loop n f acc i = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc
i : ℕ
hj : i + (j' + 1) = n
⊢ ∀ (acc : α), foldl.loop n f acc i = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc
Tactic:
intro acc
State after:
case succ
α : Sort u_1
n : ℕ
f : α → Fin n → α
init : α
j' : ℕ
ih :
  ∀ (i : ℕ) (hj : i + j' = n) (acc : α), foldl.loop n f acc i = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc
i : ℕ
hj : i + (j' + 1) = n
acc : α
⊢ foldl.loop n f acc i = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc

State before:
case succ
α : Sort u_1
n : ℕ
f : α → Fin n → α
init : α
j' : ℕ
ih :
  ∀ (i : ℕ) (hj : i + j' = n) (acc : α), foldl.loop n f acc i = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc
i : ℕ
hj : i + (j' + 1) = n
acc : α
⊢ foldl.loop n f acc i = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc
Tactic:
simp_all
State after:
case succ
α : Sort u_1
n : ℕ
f : α → Fin n → α
init : α
j' i : ℕ
hj : i + (j' + 1) = n
acc : α
ih :
  ∀ (i : ℕ) (hj : i + j' = n) (acc : α), foldl.loop n f acc i = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc
⊢ foldl.loop n f acc i = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc

State before:
case succ
α : Sort u_1
n : ℕ
f : α → Fin n → α
init : α
j' i : ℕ
hj : i + (j' + 1) = n
acc : α
ih :
  ∀ (i : ℕ) (hj : i + j' = n) (acc : α), foldl.loop n f acc i = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc
⊢ foldl.loop n f acc i = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc
Tactic:
rw [Nat.add_succ, ← Nat.succ_add] at hj
State after:
case succ
α : Sort u_1
n : ℕ
f : α → Fin n → α
init : α
j' i : ℕ
hj✝ : i + (j' + 1) = n
hj : i.succ + j' = n
acc : α
ih :
  ∀ (i : ℕ) (hj : i + j' = n) (acc : α), foldl.loop n f acc i = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc
⊢ foldl.loop n f acc i = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc

State before:
case succ
α : Sort u_1
n : ℕ
f : α → Fin n → α
init : α
j' i : ℕ
hj✝ : i + (j' + 1) = n
hj : i.succ + j' = n
acc : α
ih :
  ∀ (i : ℕ) (hj : i + j' = n) (acc : α), foldl.loop n f acc i = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc
⊢ foldl.loop n f acc i = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc
Tactic:
have hi : i < n := by calc
  _ ≤ Nat.succ i + j' := Nat.le_add_right _ _
  _ = n := hj
State after:
case succ
α : Sort u_1
n : ℕ
f : α → Fin n → α
init : α
j' i : ℕ
hj✝ : i + (j' + 1) = n
hj : i.succ + j' = n
acc : α
ih :
  ∀ (i : ℕ) (hj : i + j' = n) (acc : α), foldl.loop n f acc i = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc
hi : i < n
⊢ foldl.loop n f acc i = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc

State before:
case succ
α : Sort u_1
n : ℕ
f : α → Fin n → α
init : α
j' i : ℕ
hj✝ : i + (j' + 1) = n
hj : i.succ + j' = n
acc : α
ih :
  ∀ (i : ℕ) (hj : i + j' = n) (acc : α), foldl.loop n f acc i = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc
hi : i < n
⊢ foldl.loop n f acc i = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc
Tactic:
have := ih (i+1) hj (f acc ⟨i,hi⟩)
State after:
case succ
α : Sort u_1
n : ℕ
f : α → Fin n → α
init : α
j' i : ℕ
hj✝ : i + (j' + 1) = n
hj : i.succ + j' = n
acc : α
ih :
  ∀ (i : ℕ) (hj : i + j' = n) (acc : α), foldl.loop n f acc i = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc
hi : i < n
this :
  foldl.loop n f (f acc ⟨i, hi⟩) (i + 1) = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) (i + 1) ⋯ (f acc ⟨i, hi⟩)
⊢ foldl.loop n f acc i = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc

State before:
case succ
α : Sort u_1
n : ℕ
f : α → Fin n → α
init : α
j' i : ℕ
hj✝ : i + (j' + 1) = n
hj : i.succ + j' = n
acc : α
ih :
  ∀ (i : ℕ) (hj : i + j' = n) (acc : α), foldl.loop n f acc i = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc
hi : i < n
this :
  foldl.loop n f (f acc ⟨i, hi⟩) (i + 1) = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) (i + 1) ⋯ (f acc ⟨i, hi⟩)
⊢ foldl.loop n f acc i = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc
Tactic:
clear ih
State after:
case succ
α : Sort u_1
n : ℕ
f : α → Fin n → α
init : α
j' i : ℕ
hj✝ : i + (j' + 1) = n
hj : i.succ + j' = n
acc : α
hi : i < n
this :
  foldl.loop n f (f acc ⟨i, hi⟩) (i + 1) = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) (i + 1) ⋯ (f acc ⟨i, hi⟩)
⊢ foldl.loop n f acc i = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc

State before:
case succ
α : Sort u_1
n : ℕ
f : α → Fin n → α
init : α
j' i : ℕ
hj✝ : i + (j' + 1) = n
hj : i.succ + j' = n
acc : α
hi : i < n
this :
  foldl.loop n f (f acc ⟨i, hi⟩) (i + 1) = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) (i + 1) ⋯ (f acc ⟨i, hi⟩)
⊢ foldl.loop n f acc i = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc
Tactic:
unfold foldl.loop
State after:
case succ
α : Sort u_1
n : ℕ
f : α → Fin n → α
init : α
j' i : ℕ
hj✝ : i + (j' + 1) = n
hj : i.succ + j' = n
acc : α
hi : i < n
this :
  foldl.loop n f (f acc ⟨i, hi⟩) (i + 1) = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) (i + 1) ⋯ (f acc ⟨i, hi⟩)
⊢ (if h : i < n then foldl.loop n f (f acc ⟨i, h⟩) (i + 1) else acc) =
    foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc

State before:
case succ
α : Sort u_1
n : ℕ
f : α → Fin n → α
init : α
j' i : ℕ
hj✝ : i + (j' + 1) = n
hj : i.succ + j' = n
acc : α
hi : i < n
this :
  foldl.loop n f (f acc ⟨i, hi⟩) (i + 1) = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) (i + 1) ⋯ (f acc ⟨i, hi⟩)
⊢ (if h : i < n then foldl.loop n f (f acc ⟨i, h⟩) (i + 1) else acc) =
    foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc
Tactic:
unfold foldl'.aux
State after:
case succ
α : Sort u_1
n : ℕ
f : α → Fin n → α
init : α
j' i : ℕ
hj✝ : i + (j' + 1) = n
hj : i.succ + j' = n
acc : α
hi : i < n
this :
  foldl.loop n f (f acc ⟨i, hi⟩) (i + 1) = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) (i + 1) ⋯ (f acc ⟨i, hi⟩)
⊢ (if h : i < n then foldl.loop n f (f acc ⟨i, h⟩) (i + 1) else acc) =
    if h' : i < n then foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) (i + 1) h' (f acc ⟨i, h'⟩)
    else
      let_fun this := ⋯;
      Eq.ndrec (motive := fun n =>
        {β : (i : ℕ) → i ≤ n → Sort u_1} →
          β 0 ⋯ → ((i : ℕ) → (h : i < n) → β i ⋯ → β (i + 1) h) → (h : i ≤ n) → β i h → ¬i < n → β n ⋯)
        (fun {β} init f h acc h' => acc) this init (fun i h acc => f acc ⟨i, h⟩) ⋯ acc h'

State before:
case succ
α : Sort u_1
n : ℕ
f : α → Fin n → α
init : α
j' i : ℕ
hj✝ : i + (j' + 1) = n
hj : i.succ + j' = n
acc : α
hi : i < n
this :
  foldl.loop n f (f acc ⟨i, hi⟩) (i + 1) = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) (i + 1) ⋯ (f acc ⟨i, hi⟩)
⊢ (if h : i < n then foldl.loop n f (f acc ⟨i, h⟩) (i + 1) else acc) =
    if h' : i < n then foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) (i + 1) h' (f acc ⟨i, h'⟩)
    else
      let_fun this := ⋯;
      Eq.ndrec (motive := fun n =>
        {β : (i : ℕ) → i ≤ n → Sort u_1} →
          β 0 ⋯ → ((i : ℕ) → (h : i < n) → β i ⋯ → β (i + 1) h) → (h : i ≤ n) → β i h → ¬i < n → β n ⋯)
        (fun {β} init f h acc h' => acc) this init (fun i h acc => f acc ⟨i, h⟩) ⋯ acc h'
Tactic:
simp [*]
State after:
no goals

State before:
α : Sort u_1
n : ℕ
f : α → Fin n → α
init : α
j' i : ℕ
hj✝ : i + (j' + 1) = n
hj : i.succ + j' = n
acc : α
ih :
  ∀ (i : ℕ) (hj : i + j' = n) (acc : α), foldl.loop n f acc i = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc
⊢ i < n
Tactic:
calc
_ ≤ Nat.succ i + j' := Nat.le_add_right _ _
_ = n := hj
State after:
no goals