Reference · Data types

rainbow.data.binary

Data types src/rainbow/data/binary.clj25 definitions, 0 theorems

Binary (positional) numerals -- foundation stone for magnitude-INDEPENDENT arithmetic. Motivation: `data/Nat` is unary (a succ-chain), so kernel reduction of nat/nnrat arithmetic costs O(magnitude). That is the recurring 'LP ceiling is magnitude' wall and the reason the verified-scaling bridge is impractical past one dimension (see the design notes and memory rainbow-scaling-bridge-magnitude-wall). A positional numeral whose arithmetic recurses on O(log magnitude) constructors reduces in O(log) steps; a certified `Bin <-> Nat` bridge then lets the numeric layer pay log cost while keeping the Nat-based theorems. This module is the first brick: the `data/Bin` inductive and its recursor. data/Bin ::= bin-zero -- 0 | bin-even half -- 2 * half | bin-odd half -- 2 * half + 1 (Non-canonical: bin-even bin-zero also denotes 0; canonicalisation and the Bin<->Nat interpretation/arithmetic are the next bricks.) The block installs cleanly and its recursor `data/Bin.rec` reduces (verified in binary_test by a fold into Nat). Additive and opt-in: it adds a block to a checked environment via `extend-environment`, mirroring rainbow.data.list; it does not touch the trusted base.

bin/double

DefinitionSource, line 67

bin/double :
  (x₁ : ℕ)
  → ℕ

ℕ = data/Nat

bin/to-nat

DefinitionSource, line 76

bin/to-nat :
  (x₁ : data/Bin)
  → ℕ

ℕ = data/Nat

bin/bin-succ

DefinitionSource, line 92

bin/bin-succ :
  (x₁ : data/Bin)
  → data/Bin

bin/from-nat

DefinitionSource, line 107

bin/from-nat :
  (x₁ : ℕ)
  → data/Bin

ℕ = data/Nat

bin/bin-add

DefinitionSource, line 147

bin/bin-add :
  (x₁ x₂ : data/Bin)
  → data/Bin

bin/bit-length

DefinitionSource, line 122

bin/bit-length :
  (x₁ : data/Bin)
  → ℕ

ℕ = data/Nat

bin/to-nat-of-bin-succ

DefinitionSource, line 191

bin/to-nat-of-bin-succ :
  (b : data/Bin)
  → bin/to-nat (bin/bin-succ b) = data/succ (bin/to-nat b)

= = equality/Eq

bin/to-nat-from-nat

DefinitionSource, line 211

bin/to-nat-from-nat :
  (n : ℕ)
  → bin/to-nat (bin/from-nat n) = n

= = equality/Eqℕ = data/Nat

bin/double-distributes-add

DefinitionSource, line 239

bin/double-distributes-add :
  (x y : ℕ)
  → bin/double (algebra/nat-add x y) = algebra/nat-add (bin/double x) (bin/double y)

= = equality/Eqℕ = data/Nat

bin/to-nat-bin-add

DefinitionSource, line 260

bin/to-nat-bin-add :
  (a b : data/Bin)
  → bin/to-nat (bin/bin-add a b) = algebra/nat-add (bin/to-nat a) (bin/to-nat b)

= = equality/Eq

bin/double-self

DefinitionSource, line 317

bin/double-self :
  (y : ℕ)
  → bin/double y = algebra/nat-add y y

= = equality/Eqℕ = data/Nat

bin/double-multiply-left

DefinitionSource, line 335

bin/double-multiply-left :
  (x y : ℕ)
  → bin/double (nat/multiply x y) = nat/multiply (bin/double x) y

= = equality/Eqℕ = data/Nat

bin/bin-multiply

DefinitionSource, line 352

bin/bin-multiply :
  (x₁ x₂ : data/Bin)
  → data/Bin

bin/to-nat-bin-multiply

DefinitionSource, line 374

bin/to-nat-bin-multiply :
  (a b : data/Bin)
  → bin/to-nat (bin/bin-multiply a b) = nat/multiply (bin/to-nat a) (bin/to-nat b)

= = equality/Eq

bin/nonzero

DefinitionSource, line 426

bin/nonzero :
  (x₁ : data/Bin)
  → data/Bool

bin/compare

DefinitionSource, line 439

bin/compare :
  (x₁ x₂ : data/Bin)
  → data/Product data/Bool data/Bool

bin/at-most

DefinitionSource, line 470

bin/at-most :
  (x₁ x₂ : data/Bin)
  → data/Bool

bin/decide-double-double

DefinitionSource, line 496

bin/decide-double-double :
  (A B : ℕ)
  → nat/decide-at-most (bin/double A) (bin/double B) = nat/decide-at-most A B

= = equality/Eqℕ = data/Nat

bin/decide-double-succ-double

DefinitionSource, line 517

bin/decide-double-succ-double :
  (A B : ℕ)
  → nat/decide-at-most (bin/double A) (data/succ (bin/double B)) = nat/decide-at-most A B

= = equality/Eqℕ = data/Nat

bin/decide-one-double

DefinitionSource, line 538

bin/decide-one-double :
  (m : ℕ)
  → nat/decide-at-most 1 (bin/double m) = nat/decide-at-most 1 m

= = equality/Eqℕ = data/Nat

bin/decide-succ-double-double

DefinitionSource, line 553

bin/decide-succ-double-double :
  (A B : ℕ)
  → nat/decide-at-most (data/succ (bin/double A)) (bin/double B) = nat/decide-at-most (data/succ A) B

= = equality/Eqℕ = data/Nat

bin/decide-double-zero

DefinitionSource, line 574

bin/decide-double-zero :
  (A : ℕ)
  → nat/decide-at-most (bin/double A) 0 = nat/decide-at-most A 0

= = equality/Eqℕ = data/Nat

bin/nonzero-reflects

DefinitionSource, line 589

bin/nonzero-reflects :
  (b : data/Bin)
  → bin/nonzero b = nat/decide-at-most 1 (bin/to-nat b)

= = equality/Eq

bin/compare-reflects

DefinitionSource, line 668

bin/compare-reflects :
  (a b : data/Bin)
  → data/Product (first = most₃) (second = most)
  where first := product/first data/Bool data/Bool (bin/compare a b)
  where most := nat/decide-at-most (data/succ (bin/to-nat a)) (bin/to-nat b)
  where most₃ := nat/decide-at-most (bin/to-nat a) (bin/to-nat b)
  where second := product/second data/Bool data/Bool (bin/compare a b)

= = equality/Eq

bin/at-most-reflects

DefinitionSource, line 676

bin/at-most-reflects :
  (a b : data/Bin)
  → bin/at-most a b = nat/decide-at-most (bin/to-nat a) (bin/to-nat b)

= = equality/Eq