CoqEAL binnat, ported to Lean — List Bool refines the natural numbers #
CoqEAL's binnat refines MathComp nat to a binary representation N. Here we
port the data-refinement core of that example: a little-endian (lsb-first)
bit list List Bool refines the abstract ℕ via toNat, and the concrete
binary increment binSucc refines the abstract Nat.succ — the CoqEAL
Rsucc_N (carry-ripple) refinement square.
This mirrors the companion SeqPoly.lean (seqpoly add) and SeqMatrix.lean
(seqmatrix add): the refinement mechanism — a relation between an abstract
and a concrete representation, plus transfer of operations — is the same
ReprTransfer layer, and this file is one worked instance over the binnat
representation. The carry ripple of binSucc (flip trailing trues to false,
then set the first false/append) is exactly the structural recursion whose
refinement square toNat_binSucc discharges.
Scope (the rest of CoqEAL) #
The first-order data refinements — binnat (here), binint, binrat, seqpoly,
seqmatrix — and the fast algorithms — Karatsuba and Strassen multiplication,
Gaussian elimination — are ported alongside this file in the suite. The remaining
tail — Toom-Cook multiplication, the Bareiss fraction-free determinant, matrix
rank, multivariate polynomials, and the normal-form theory (Smith, Jordan,
Frobenius) — is CoqEAL's research contribution, a much larger development,
documented as the suite's frontier rather than ported.
The CoqEAL binnat refinement relation: a little-endian (lsb-first) bit list
denotes the natural number it encodes (true/false are bits 1/0).
Equations
Instances For
The concrete (computational) binary increment, with explicit carry ripple:
[] becomes [1]; a low 0 becomes 1; a low 1 becomes 0 and the
carry propagates into the higher bits.