internlm/Lean-Github huggingface dataset:
Theorem: LeanColls.Range.get_mem
Proof state before:
case mk
r : Range
i : ℕ
hi : i < r.size
⊢ i < r.size
Tactic:
simp [nth, hi]
Proof state after:
no goals
Theorem: LeanColls.Range.mem_iff_exists_get
Proof state before:
x : ℕ
r : Range
⊢ x ∈ r ↔ ∃ i, x = r.get i
Tactic:
constructor
Proof state after:
case mp
x : ℕ
r : Range
⊢ x ∈ r → ∃ i, x = r.get i

case mpr
x : ℕ
r : Range
⊢ (∃ i, x = r.get i) → x ∈ r
Theorem: LeanColls.Range.mem_iff_exists_get
Proof state before:
case mp
x : ℕ
r : Range
⊢ x ∈ r → ∃ i, x = r.get i
Tactic:
intro h
Proof state after:
case mp
x : ℕ
r : Range
h : x ∈ r
⊢ ∃ i, x = r.get i
Theorem: LeanColls.Range.mem_iff_exists_get
Proof state before:
case mp
x : ℕ
r : Range
h : x ∈ r
⊢ ∃ i, x = r.get i
Tactic:
have := nth_ofNth h
Proof state after:
case mp
x : ℕ
r : Range
h : x ∈ r
this : r.nth (r.ofNth x) = x
⊢ ∃ i, x = r.get i
Theorem: LeanColls.Range.mem_iff_exists_get
Proof state before:
case mp
x : ℕ
r : Range
h : x ∈ r
this : r.nth (r.ofNth x) = x
⊢ ∃ i, x = r.get i
Tactic:
rw [← this] at h ⊢
Proof state after:
case mp
x : ℕ
r : Range
h : r.nth (r.ofNth x) ∈ r
this : r.nth (r.ofNth x) = x
⊢ ∃ i, r.nth (r.ofNth x) = r.get i
Theorem: LeanColls.Range.mem_iff_exists_get
Proof state before:
case mp
x : ℕ
r : Range
h : r.nth (r.ofNth x) ∈ r
this : r.nth (r.ofNth x) = x
⊢ ∃ i, r.nth (r.ofNth x) = r.get i
Tactic:
clear this
Proof state after:
case mp
x : ℕ
r : Range
h : r.nth (r.ofNth x) ∈ r
⊢ ∃ i, r.nth (r.ofNth x) = r.get i
Theorem: LeanColls.Range.mem_iff_exists_get
Proof state before:
case mp
x : ℕ
r : Range
h : r.nth (r.ofNth x) ∈ r
⊢ ∃ i, r.nth (r.ofNth x) = r.get i
Tactic:
simp at h
Proof state after:
case mp
x : ℕ
r : Range
h : r.ofNth x < r.size
⊢ ∃ i, r.nth (r.ofNth x) = r.get i
Theorem: LeanColls.Range.mem_iff_exists_get
Proof state before:
case mp
x : ℕ
r : Range
h : r.ofNth x < r.size
⊢ ∃ i, r.nth (r.ofNth x) = r.get i
Tactic:
use ⟨_,h⟩
Proof state after:
case h
x : ℕ
r : Range
h : r.ofNth x < r.size
⊢ r.nth (r.ofNth x) = r.get ⟨r.ofNth x, h⟩
Theorem: LeanColls.Range.mem_iff_exists_get
Proof state before:
case h
x : ℕ
r : Range
h : r.ofNth x < r.size
⊢ r.nth (r.ofNth x) = r.get ⟨r.ofNth x, h⟩
Tactic:
rfl
Proof state after:
no goals
Theorem: LeanColls.Range.mem_iff_exists_get
Proof state before:
case mpr
x : ℕ
r : Range
⊢ (∃ i, x = r.get i) → x ∈ r
Tactic:
rintro ⟨⟨i,hi⟩,rfl⟩
Proof state after:
case mpr.intro.mk
r : Range
i : ℕ
hi : i < r.size
⊢ r.get ⟨i, hi⟩ ∈ r
Theorem: LeanColls.Range.mem_iff_exists_get
Proof state before:
case mpr.intro.mk
r : Range
i : ℕ
hi : i < r.size
⊢ r.get ⟨i, hi⟩ ∈ r
Tactic:
simp [get, hi]
Proof state after:
no goals
Theorem: LeanColls.Range.fold_def
Proof state before:
β : Type u_1
init : β
r : Range
f : β → ℕ → β
⊢ fold r f init = Fin.foldl r.size (fun acc i => f acc (r.get i)) init
Tactic:
simp [fold, foldl, Fin.foldl]
Proof state after:
β : Type u_1
init : β
r : Range
f : β → ℕ → β
⊢ foldl.aux r f r.start ⋯ init = Fin.foldl.loop r.size (fun acc i => f acc (r.get i)) init 0
Theorem: LeanColls.Range.fold_def
Proof state before:
β : Type u_1
init : β
r : Range
f : β → ℕ → β
⊢ foldl.aux r f r.start ⋯ init = Fin.foldl.loop r.size (fun acc i => f acc (r.get i)) init 0
Tactic:
sorry
Proof state after:
no goals
Theorem: Fin.foldl_eq_foldl'
Proof 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']
Proof 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
Theorem: Fin.foldl_eq_foldl'
Proof 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
Proof 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
Theorem: Fin.foldl_eq_foldl'
Proof 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
Proof 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
Theorem: Fin.foldl_eq_foldl'
Proof 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 [*]
Proof state after:
no goals
Theorem: Fin.foldl_eq_foldl'
Proof 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
Proof state after:
no goals
Theorem: Fin.foldl_eq_foldl'
Proof 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
Proof 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
Theorem: Fin.foldl_eq_foldl'
Proof 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
Proof 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
Theorem: Fin.foldl_eq_foldl'
Proof 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
Proof 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
Theorem: Fin.foldl_eq_foldl'
Proof 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
Proof 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
Theorem: Fin.foldl_eq_foldl'
Proof 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
Proof 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'
Theorem: Fin.foldl_eq_foldl'
Proof 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
Proof state after:
no goals
Theorem: Fin.foldl_eq_foldl'
Proof 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
Proof 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
Theorem: Fin.foldl_eq_foldl'
Proof 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
Proof 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
Theorem: Fin.foldl_eq_foldl'
Proof 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
Proof 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
Theorem: Fin.foldl_eq_foldl'
Proof 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
Proof 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
Theorem: Fin.foldl_eq_foldl'
Proof 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⟩)
Proof 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
Theorem: Fin.foldl_eq_foldl'
Proof 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
Proof 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
Theorem: Fin.foldl_eq_foldl'
Proof 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
Proof 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
Theorem: Fin.foldl_eq_foldl'
Proof 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
Proof 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'
Theorem: Fin.foldl_eq_foldl'
Proof 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 [*]
Proof state after:
no goals
Theorem: Fin.foldl_eq_foldl'
Proof 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
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 β
⊢ foldlM n init f =
    foldl n
      (fun macc i => do
        let acc ← macc
        f i acc)
      (pure init)
Tactic:
simp [foldl, foldlM]
Proof state after:
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
⊢ foldlM.aux n f 0 init =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      (pure init) 0
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 β
⊢ foldlM.aux n f 0 init =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      (pure init) 0
Tactic:
suffices ∀ i j (hj : i + j = n) macc,
  (macc >>= fun acc => foldlM.aux n f i acc) =
    foldl.loop n _ macc i
  by
  have := this 0 n (by simp) (pure init)
  simp at this
  exact this
Proof state after:
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
⊢ ∀ (i j : ℕ),
    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
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 β
⊢ ∀ (i j : ℕ),
    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
Tactic:
intro i j hj
Proof state after:
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
i j : ℕ
hj : 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
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 β
i j : ℕ
hj : 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
Tactic:
induction j generalizing i with
| zero =>
  intro macc
  simp at hj; cases hj
  unfold foldl.loop; unfold foldlM.aux
  simp
| succ j' ih =>
  intro macc
  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 (macc >>= fun acc => f ⟨i,hi⟩ acc)
  clear ih
  unfold foldl.loop; unfold foldlM.aux
  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 β
this :
  ∀ (i j : ℕ) (hj : i + j = n) (macc : m β),
    (do
        let acc ← macc
        foldlM.aux n f i acc) =
      foldl.loop n (?m.30970 i j hj macc) macc i
⊢ foldlM.aux n f 0 init =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      (pure init) 0
Tactic:
have := this 0 n (by simp) (pure init)
Proof state after:
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
this✝ :
  ∀ (i j : ℕ) (hj : i + j = n) (macc : m β),
    (do
        let acc ← macc
        foldlM.aux n f i acc) =
      foldl.loop n (?m.30970 i j hj macc) macc i
this :
  (do
      let acc ← pure init
      foldlM.aux n f 0 acc) =
    foldl.loop n (?m.30970 0 n ⋯ (pure init)) (pure init) 0
⊢ foldlM.aux n f 0 init =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      (pure init) 0
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 β
this✝ :
  ∀ (i j : ℕ) (hj : i + j = n) (macc : m β),
    (do
        let acc ← macc
        foldlM.aux n f i acc) =
      foldl.loop n (?m.30970 i j hj macc) macc i
this :
  (do
      let acc ← pure init
      foldlM.aux n f 0 acc) =
    foldl.loop n (?m.30970 0 n ⋯ (pure init)) (pure init) 0
⊢ foldlM.aux n f 0 init =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      (pure init) 0
Tactic:
simp at this
Proof state after:
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
this✝ :
  ∀ (i j : ℕ) (hj : i + j = n) (macc : m β),
    (do
        let acc ← macc
        foldlM.aux n f i acc) =
      foldl.loop n (?m.30970 i j hj macc) macc i
this : foldlM.aux n f 0 init = foldl.loop n (?m.30970 0 n ⋯ (pure init)) (pure init) 0
⊢ foldlM.aux n f 0 init =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      (pure init) 0
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 β
this✝ :
  ∀ (i j : ℕ) (hj : i + j = n) (macc : m β),
    (do
        let acc ← macc
        foldlM.aux n f i acc) =
      foldl.loop n (?m.30970 i j hj macc) macc i
this : foldlM.aux n f 0 init = foldl.loop n (?m.30970 0 n ⋯ (pure init)) (pure init) 0
⊢ foldlM.aux n f 0 init =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      (pure init) 0
Tactic:
exact this
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 β
this :
  ∀ (i j : ℕ) (hj : i + j = n) (macc : m β),
    (do
        let acc ← macc
        foldlM.aux n f i acc) =
      foldl.loop n (?m.30970 i j hj macc) macc i
⊢ 0 + n = n
Tactic:
simp
Proof state after:
no goals
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 : ℕ
hj : i + 0 = 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 zero
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
i : ℕ
hj : i + 0 = 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 zero
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
i : ℕ
hj : i + 0 = 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:
simp at hj
Proof state after:
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