def BitVec.iunfoldr {w : Nat} {α : Type u_1} (f : Fin w → α → α × Bool) (s : α) : α × BitVec w

iunfoldr is an iterative operation that applies a function f repeatedly.

It produces a sequence of state values [s_0, s_1 .. s_w] and a bitvector v where f i s_i = (s_{i+1}, b_i) and b_i is bit ith least-significant bit in v (e.g., getLsb v i = b_i).

Theorems involving iunfoldr can be eliminated using iunfoldr_replace below.

Equations

• BitVec.iunfoldr f s = Fin.hIterate (fun (i : Nat) => α × BitVec i) (s, BitVec.nil) fun (i : Fin w) (q : α × BitVec ↑i) => (fun (p : α × Bool) => (p.fst, BitVec.cons p.snd q.snd)) (f i q.fst)

theorem BitVec.iunfoldr.fst_eq {w : Nat} {α : Type u_1} {f : Fin w → α → α × Bool} (state : Nat → α) (s : α) (init : s = state 0) (ind : ∀ (i : Fin w), (f i (state ↑i)).fst = state (↑i + 1)) : (iunfoldr f s).fst = state w

theorem BitVec.iunfoldr_getLsbD' {w : Nat} {α : Type u_1} {f : Fin w → α → α × Bool} (state : Nat → α) (ind : ∀ (i : Fin w), (f i (state ↑i)).fst = state (↑i + 1)) : (∀ (i : Fin w), (iunfoldr f (state 0)).snd.getLsbD ↑i = (f i (state ↑i)).snd) ∧ (iunfoldr f (state 0)).fst = state w

theorem BitVec.iunfoldr_getLsbD {w : Nat} {α : Type u_1} {f : Fin w → α → α × Bool} (state : Nat → α) (i : Fin w) (ind : ∀ (i : Fin w), (f i (state ↑i)).fst = state (↑i + 1)) : (iunfoldr f (state 0)).snd.getLsbD ↑i = (f i (state ↑i)).snd

theorem BitVec.iunfoldr_replace {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[↑i])) : iunfoldr f a = (state w, value)

Correctness theorem for iunfoldr.

theorem BitVec.iunfoldr_replace_snd {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[↑i])) : (iunfoldr f a).snd = value