-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Folds.lean
theorem iunfoldr.eq_test
    {f : Fin w → α → α × Bool} (state : Nat → α) (value : BitVec w) (a : α)
    (init : state 0 = a)
    (step : ∀(i : Fin w), f i (state i.val) = (state (i.val+1), value.getLsbD i.val)) :
    iunfoldr f a = (state w, BitVec.truncate w value)

Proof state:
w : Nat
α : Type u_1
f : Fin w → α → α × Bool
state : Nat → α
value : BitVec w
a : α
init : state 0 = a
step : ∀ (i : Fin w), f i (state ↑i) = (state (↑i + 1), value.getLsbD ↑i)
⊢ (a, nil) = (state 0, truncate 0 value)

Tactic:
simp only [init, eq_nil]

Result:
no goals

Proof state:
case step
w : Nat
α : Type u_1
f : Fin w → α → α × Bool
state : Nat → α
value : BitVec w
a : α
init : state 0 = a
step : ∀ (i : Fin w), f i (state ↑i) = (state (↑i + 1), value.getLsbD ↑i)
⊢ ∀ (i : Fin w),
    (fun p => (p.fst, cons p.snd (state ↑i, truncate (↑i) value).snd)) (f i (state ↑i, truncate (↑i) value).fst) =
      (state (↑i + 1), truncate (↑i + 1) value)

Tactic:
case step =>
  intro i
  simp_all [setWidth_succ]

Result:
no goals

Proof state:
w : Nat
α : Type u_1
f : Fin w → α → α × Bool
state : Nat → α
value : BitVec w
a : α
init : state 0 = a
step : ∀ (i : Fin w), f i (state ↑i) = (state (↑i + 1), value.getLsbD ↑i)
⊢ iunfoldr f a = (state w, truncate w value)

Tactic:
apply Fin.hIterate_eq (fun i => ((state i, BitVec.truncate i value) : α × BitVec i))

Result:
case init
w : Nat
α : Type u_1
f : Fin w → α → α × Bool
state : Nat → α
value : BitVec w
a : α
init : state 0 = a
step : ∀ (i : Fin w), f i (state ↑i) = (state (↑i + 1), value.getLsbD ↑i)
⊢ (a, nil) = (state 0, truncate 0 value)

case step
w : Nat
α : Type u_1
f : Fin w → α → α × Bool
state : Nat → α
value : BitVec w
a : α
init : state 0 = a
step : ∀ (i : Fin w), f i (state ↑i) = (state (↑i + 1), value.getLsbD ↑i)
⊢ ∀ (i : Fin w),
    (fun p => (p.fst, cons p.snd (state ↑i, truncate (↑i) value).snd)) (f i (state ↑i, truncate (↑i) value).fst) =
      (state (↑i + 1), truncate (↑i + 1) value)

Proof state:
case init
w : Nat
α : Type u_1
f : Fin w → α → α × Bool
state : Nat → α
value : BitVec w
a : α
init : state 0 = a
step : ∀ (i : Fin w), f i (state ↑i) = (state (↑i + 1), value.getLsbD ↑i)
⊢ (a, nil) = (state 0, truncate 0 value)

case step
w : Nat
α : Type u_1
f : Fin w → α → α × Bool
state : Nat → α
value : BitVec w
a : α
init : state 0 = a
step : ∀ (i : Fin w), f i (state ↑i) = (state (↑i + 1), value.getLsbD ↑i)
⊢ ∀ (i : Fin w),
    (fun p => (p.fst, cons p.snd (state ↑i, truncate (↑i) value).snd)) (f i (state ↑i, truncate (↑i) value).fst) =
      (state (↑i + 1), truncate (↑i + 1) value)

Tactic:
case init =>
  simp only [init, eq_nil]

Result:
case step
w : Nat
α : Type u_1
f : Fin w → α → α × Bool
state : Nat → α
value : BitVec w
a : α
init : state 0 = a
step : ∀ (i : Fin w), f i (state ↑i) = (state (↑i + 1), value.getLsbD ↑i)
⊢ ∀ (i : Fin w),
    (fun p => (p.fst, cons p.snd (state ↑i, truncate (↑i) value).snd)) (f i (state ↑i, truncate (↑i) value).fst) =
      (state (↑i + 1), truncate (↑i + 1) value)

Proof state:
w : Nat
α : Type u_1
f : Fin w → α → α × Bool
state : Nat → α
value : BitVec w
a : α
init : state 0 = a
step : ∀ (i : Fin w), f i (state ↑i) = (state (↑i + 1), value.getLsbD ↑i)
⊢ ∀ (i : Fin w),
    (fun p => (p.fst, cons p.snd (state ↑i, truncate (↑i) value).snd)) (f i (state ↑i, truncate (↑i) value).fst) =
      (state (↑i + 1), truncate (↑i + 1) value)

Tactic:
intro i

Result:
w : Nat
α : Type u_1
f : Fin w → α → α × Bool
state : Nat → α
value : BitVec w
a : α
init : state 0 = a
step : ∀ (i : Fin w), f i (state ↑i) = (state (↑i + 1), value.getLsbD ↑i)
i : Fin w
⊢ (fun p => (p.fst, cons p.snd (state ↑i, truncate (↑i) value).snd)) (f i (state ↑i, truncate (↑i) value).fst) =
    (state (↑i + 1), truncate (↑i + 1) value)

Proof state:
w : Nat
α : Type u_1
f : Fin w → α → α × Bool
state : Nat → α
value : BitVec w
a : α
init : state 0 = a
step : ∀ (i : Fin w), f i (state ↑i) = (state (↑i + 1), value.getLsbD ↑i)
i : Fin w
⊢ (fun p => (p.fst, cons p.snd (state ↑i, truncate (↑i) value).snd)) (f i (state ↑i, truncate (↑i) value).fst) =
    (state (↑i + 1), truncate (↑i + 1) value)

Tactic:
simp_all [setWidth_succ]

Result:
no goals