Documentation

Init.Data.BitVec.Folds

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
Instances For
    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)) :
    (BitVec.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), (BitVec.iunfoldr f (state 0)).snd.getLsbD i = (f i (state i)).snd) (BitVec.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)) :
    (BitVec.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.getLsbD i)) :
    BitVec.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.getLsbD i)) :
    (BitVec.iunfoldr f a).snd = value