Correctness of signed-magnitude dyadic addition

The runtime aligns dyadic significands and combines their natural-number magnitudes by sign. Internal.addDyadic_eq identifies this implementation with exact dyadic addition, including cancellation and the signed-zero rule.

The @[csimp] theorem addDyadic_eq_internal supplies the equality used by the compiler substitution. The remaining public lemmas describe equal- and adjacent-exponent cases used by native arithmetic refinements.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.addDyadic_sameSign_sameExponent (sign : Bool) (left right : ℕ) (exponent : ℤ) (hleft : left ≠ 0) (hright : right ≠ 0) : addDyadic { negative := sign, significand := left, exponent := exponent } { negative := sign, significand := right, exponent := exponent } = { negative := sign, significand := left + right, exponent := exponent }

Adding two nonzero dyadics with the same sign and exponent adds their significands.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.addDyadic_oppositeSign_sameExponent_largeLeft (largeSign smallSign : Bool) (large small : ℕ) (exponent : ℤ) (hlarge : large ≠ 0) (hsmall : small ≠ 0) (hsign : largeSign ≠ smallSign) (hlt : small < large) : addDyadic { negative := largeSign, significand := large, exponent := exponent } { negative := smallSign, significand := small, exponent := exponent } = { negative := largeSign, significand := large - small, exponent := exponent }

Adding equal-exponent dyadics of opposite signs subtracts the smaller magnitude from the larger left one.

The result keeps the sign of the larger magnitude and needs no rounding or exponent adjustment.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.addDyadic_oppositeSign_sameExponent_largeRight (smallSign largeSign : Bool) (small large : ℕ) (exponent : ℤ) (hsmall : small ≠ 0) (hlarge : large ≠ 0) (hsign : smallSign ≠ largeSign) (hlt : small < large) : addDyadic { negative := smallSign, significand := small, exponent := exponent } { negative := largeSign, significand := large, exponent := exponent } = { negative := largeSign, significand := large - small, exponent := exponent }

Adding equal-exponent dyadics of opposite signs subtracts the smaller left magnitude from the larger right one.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.addDyadic_oppositeSign_sameExponent_eq_zero (leftSign rightSign : Bool) (magnitude : ℕ) (exponent : ℤ) (hmagnitude : magnitude ≠ 0) (hsign : leftSign ≠ rightSign) : addDyadic { negative := leftSign, significand := magnitude, exponent := exponent } { negative := rightSign, significand := magnitude, exponent := exponent } = { negative := false, significand := 0, exponent := 0 }

Equal nonzero magnitudes with opposite signs cancel to canonical positive zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.addDyadic_oppositeSign_adjacentExponent_largeLeft (largeSign smallSign : Bool) (large small : ℕ) (exponent : ℤ) (hlarge : large ≠ 0) (hsmall : small ≠ 0) (hsign : largeSign ≠ smallSign) (hlt : small < large.shiftLeft 1) : addDyadic { negative := largeSign, significand := large, exponent := exponent + 1 } { negative := smallSign, significand := small, exponent := exponent } = { negative := largeSign, significand := large.shiftLeft 1 - small, exponent := exponent }

Opposite signs with the larger left operand one exponent higher give 2 * large - small.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.addDyadic_oppositeSign_adjacentExponent_largeRight (smallSign largeSign : Bool) (small large : ℕ) (exponent : ℤ) (hsmall : small ≠ 0) (hlarge : large ≠ 0) (hsign : smallSign ≠ largeSign) (hlt : small < large.shiftLeft 1) : addDyadic { negative := smallSign, significand := small, exponent := exponent } { negative := largeSign, significand := large, exponent := exponent + 1 } = { negative := largeSign, significand := large.shiftLeft 1 - small, exponent := exponent }

Opposite signs with the larger right operand one exponent higher give 2 * large - small.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.addDyadic_alignRightOffset (offset : ℕ) (xSign ySign : Bool) (xMagnitude yMagnitude xScale yScale : ℕ) (hx : xMagnitude ≠ 0) (hy : yMagnitude ≠ 0) (hscale : xScale ≤ yScale) : addDyadic { negative := xSign, significand := xMagnitude, exponent := Int.ofNat xScale - Int.ofNat offset } { negative := ySign, significand := yMagnitude, exponent := Int.ofNat yScale - Int.ofNat offset } = addDyadic { negative := xSign, significand := xMagnitude, exponent := Int.ofNat xScale - Int.ofNat offset } { negative := ySign, significand := yMagnitude <<< (yScale - xScale), exponent := Int.ofNat xScale - Int.ofNat offset }

Align the right dyadic magnitude to the left exponent without changing the exact sum.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.addDyadic_alignLeftOffset (offset : ℕ) (xSign ySign : Bool) (xMagnitude yMagnitude xScale yScale : ℕ) (hx : xMagnitude ≠ 0) (hy : yMagnitude ≠ 0) (hscale : yScale < xScale) : addDyadic { negative := xSign, significand := xMagnitude, exponent := Int.ofNat xScale - Int.ofNat offset } { negative := ySign, significand := yMagnitude, exponent := Int.ofNat yScale - Int.ofNat offset } = addDyadic { negative := xSign, significand := xMagnitude <<< (xScale - yScale), exponent := Int.ofNat yScale - Int.ofNat offset } { negative := ySign, significand := yMagnitude, exponent := Int.ofNat yScale - Int.ofNat offset }

Align the left dyadic magnitude to the right exponent without changing the exact sum.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.addDyadic_eq (a b : Numerics.Dyadic) : addDyadic a b = Model.addDyadic a b

Signed-magnitude dyadic addition equals Model.addDyadic.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.addDyadic_comm (a b : Numerics.Dyadic) : addDyadic a b = addDyadic b a

Exact dyadic addition is commutative, including its signed-zero rule.

@[csimp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.addDyadic_eq_internal : addDyadic = Internal.addDyadic

Compiled code runs exact dyadic addition as the signed-magnitude Internal.addDyadic.