CoqEAL binint, ported to Lean — sign + magnitude refines ℤ

CoqEAL's binint refines MathComp integers to a signed representation. Here a Bool × List Bool — a sign bit (true = negative) with a little-endian magnitude — refines ℤ via toInt, reusing BinNat.toNat for the magnitude. The concrete sign flip binNeg refines ℤ negation (the CoqEAL Rneg square).

The relation is non-injective (+0 and -0 both denote 0), a map-level refinement — the same shape as the companion binnat, seqpoly, and seqmatrix data refinements.

@[reducible, inline]

abbrev Transfer.Examples.CoqEAL.BinInt.BinInt : Type

A sign bit (true = negative) with a little-endian magnitude, refining ℤ.

Equations

• Transfer.Examples.CoqEAL.BinInt.BinInt = (Bool × List Bool)

def Transfer.Examples.CoqEAL.BinInt.toInt : BinInt → ℤ

Decode a signed binary to the integer it denotes.

Equations

• Transfer.Examples.CoqEAL.BinInt.toInt (s, l) = if s = true then -↑(Transfer.Examples.CoqEAL.BinNat.toNat l) else ↑(Transfer.Examples.CoqEAL.BinNat.toNat l)

def Transfer.Examples.CoqEAL.BinInt.binNeg : BinInt → BinInt

Concrete negation: flip the sign bit.

Equations

• Transfer.Examples.CoqEAL.BinInt.binNeg (s, l) = (!s, l)

theorem Transfer.Examples.CoqEAL.BinInt.toInt_binNeg (x : BinInt) : toInt (binNeg x) = -toInt x

The CoqEAL Rneg refinement square. The concrete sign flip refines ℤ negation: toInt (binNeg x) = -(toInt x).