Bitvectors and Boolean lists

DefinitionLittle-endian bits of a bitvector#✓fully proved

The bits of a bitvector in little-endian order, least significant bit first.

def toBoolListLE {n : Nat} (x : BitVec n) : List Bool :=
  List.ofFn fun i : Fin n => x.getLsbD i

Used by 9

Used byFixed-width binary words as residues modulo a monic polynomial · Remainder coefficients of an encoded binary word are its bits · Coefficients of the binary polynomial of a bitvector · Evaluation of modular Horner multiplication · The binary modulus is monic · Degree of the binary modulus · Modular multiplication of binary polynomial residues · Binary polynomial of a bitvector · Little-endian Boolean lists are equivalent to bitvectors

DefinitionLittle-endian Boolean lists are equivalent to bitvectors#✓fully proved

Fixed-width little-endian Boolean lists are equivalent to bitvectors of the same width.

BitVec.equivBoolListLE · 17 lines

def equivBoolListLE (n : Nat) : BitVec n ≃ {w : List Bool // w.length = n} where
  toFun x := ⟨x.toBoolListLE, x.length_toBoolListLE⟩
  invFun w := (BitVec.ofBoolListLE w).cast w.property
  left_inv x := by
    apply BitVec.eq_of_getLsbD_eq
    intro i hi
    rw [BitVec.getLsbD_cast, BitVec.getLsbD_ofBoolListLE, getD_toBoolListLE]
  right_inv w := by
    rcases w with ⟨w, rfl⟩
    apply Subtype.ext
    change List.ofFn (fun i : Fin w.length => (BitVec.ofBoolListLE w).getLsbD i) = w
    conv_rhs => rw [← List.ofFn_getElem (xs := w)]
    apply congrArg List.ofFn
    funext i
    rw [BitVec.getLsbD_ofBoolListLE, List.getD_eq_getElem?_getD,
      List.getElem?_eq_getElem i.isLt]
    rfl

Uses 1

Statement usesLittle-endian bits of a bitvector

TheoremSum of a Boolean list counts its true entries#✓fully proved

The sum of the natural values of a Boolean list is its number of true entries.

theorem sum_map_toNat_eq_count_true (bits : List Bool) :
    (bits.map Bool.toNat).sum = bits.count true

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.