Generated by lean2il from the Lean project lean. Every word below comes from the Lean source: docstrings, theorem statements, and proved examples. Do not edit this file; edit the Lean and run lean2il again.
Every proof was re-checked by Tenet, an independent Lean kernel: 231 declarations in 4 modules, the project’s own modules, none rejected (Lean 4.33.1). Every example on this page was run against
Finance.Proven.dllwhen it was built and returned the proved value. 300 random calls to 3 functions, each run by Lean’s own compiler and by the IL, gave the same answer every time.
Finance.Rounding.NET’s Math.Round(decimal) rounds a midpoint to the nearest even digit unless you say otherwise, so
Math.Round(0.125m, 2) is 0.12, not the 0.13 an invoice expects. Math.Round(1.005, 2,
MidpointRounding.AwayFromZero) on a double is 1, because the double nearest to 1.005 sits just
below it; of the 10,000 prices from 0.005 to 99.995 that end in a half cent, 572 round the wrong way
as doubles on .NET 10. And the hand-rolled fix, Math.Floor(x * 100 + 0.5) / 100, rounds a refund of
-2.675 to -2.67 while the sale rounds to 2.68.
This file defines rounding on exact decimals, a mantissa and a scale like System.Decimal, and proves
what it does: the result is within half a unit of the last kept digit, a midpoint goes where the mode
says, a refund rounds to the negative of its sale, and a value already at the precision is left alone.
The functions marked @[export] are compiled to a .NET assembly by lean2il, which re-checks every
proof here with Tenet first.
Finance.SplitSplit a $100.00 bill three ways and the obvious code, total / 3 each, charges $99.99: a cent disappears.
Round each share instead and you can get $100.02. Every billing system has to decide who pays the extra cents,
and every one has at some point shipped a split that did not add up.
splitEven works in cents. It gives the first total % n people one cent more than the rest, and this file
proves what an auditor would ask: there are exactly n shares, they add up to exactly the total (refunds, which
are negative, included), and no share differs from another by more than a cent.
Reference the two assemblies (the second is lean2il’s small runtime):
<ItemGroup>
<Reference Include="Finance.Proven" HintPath="path/to/Finance.Proven.dll" />
<Reference Include="LeanToDotNet.Runtime" HintPath="path/to/LeanToDotNet.Runtime.dll" />
</ItemGroup>
Proven.Roundpublic static decimal Round(decimal x, int digits, RoundingMode mode)
public static Dec Round(Dec x, BigInteger digits, RoundingMode mode)
Round x to digits decimal places by mode, as Math.Round(x, digits, mode) does for a decimal.
A value with no more than digits places comes back unchanged.
Proved below: the result is within half a unit of its last digit for the two midpoint modes
(round_error_le_half), a midpoint goes where the mode says (round_tie_awayFromZero,
round_tie_toEven), round (-x) = -(round x) for the symmetric modes (round_neg), and rounding
twice to the same precision is rounding once (round_round).
Proved examples, each one a theorem in the Lean and a call that was run against the IL:
using Finance;
Proven.Round(0.125m, 2, RoundingMode.ToEven); // 0.12 (bankers_default_example)
Proven.Round(0.125m, 2, RoundingMode.AwayFromZero); // 0.13 (invoice_example)
Proven.Round(-2.675m, 2, RoundingMode.AwayFromZero); // -2.68 (refund_example)
Proven.Round(1.005m, 2, RoundingMode.AwayFromZero); // 1.01 (decimal_1_005_example)
Proven.Round(2.675m, 2, RoundingMode.AwayFromZero); // 2.68 (sale_example)
What is proved about it:
| Theorem | Says | Rests on |
|---|---|---|
round_of_scale_le (source) |
A value with no more than digits places is returned unchanged.∀ (x : Finance.Dec) (digits : ℕ) (mode : Finance.RoundingMode), x.scale ≤ digits → Finance.round x digits mode = x |
propext |
round_scale_le (source) |
The result has at most digits places.∀ (x : Finance.Dec) (digits : ℕ) (mode : Finance.RoundingMode), (Finance.round x digits mode).scale ≤ digits |
Quot.sound, propext |
round_error_le_half (source) |
Half a unit. For the two midpoint modes, rounding x to digits places moves it by at most half of 10 ^ (-digits). Both sides are written at x’s scale, s, so the claim is about integers: twice the change in the mantissa is at most 10 ^ (s - digits), one unit of the last kept digit.∀ (x : Finance.Dec) (digits : ℕ) (mode : Finance.RoundingMode), mode = Finance.RoundingMode.toEven ∨ mode = Finance.RoundingMode.awayFromZero → digits < x.scale → 2 * (x.mantissa - ↑(10 ^ (x.scale - digits)) * (Finance.round x digits mode).mantissa).natAbs ≤ 10 ^ (x.scale - digits) |
Classical.choice, Quot.sound, propext |
round_nearest (source) |
Nearest. For the two midpoint modes no other value with digits places is closer to x.∀ (x : Finance.Dec) (digits : ℕ) (mode : Finance.RoundingMode), mode = Finance.RoundingMode.toEven ∨ mode = Finance.RoundingMode.awayFromZero → digits < x.scale → ∀ (k : ℤ), (x.mantissa - ↑(10 ^ (x.scale - digits)) * (Finance.round x digits mode).mantissa).natAbs ≤ (x.mantissa - ↑(10 ^ (x.scale - digits)) * k).natAbs |
Classical.choice, Quot.sound, propext |
round_tie_awayFromZero (source) |
Midpoints, away from zero. When x is exactly halfway, the result is the neighbor further from zero: 0.125 goes to 0.13 and -0.125 to -0.13.∀ (x : Finance.Dec) (digits : ℕ), digits < x.scale → 2 * (x.mantissa % ↑(10 ^ (x.scale - digits))) = ↑(10 ^ (x.scale - digits)) → x.mantissa.natAbs < (↑(10 ^ (x.scale - digits)) * (Finance.round x digits Finance.RoundingMode.awayFromZero).mantissa).natAbs |
Quot.sound, propext |
round_tie_toEven (source) |
Midpoints, to even. When x is exactly halfway, the last kept digit is even: 0.125 goes to 0.12 and 0.135 to 0.14.∀ (x : Finance.Dec) (digits : ℕ), digits < x.scale → 2 * (x.mantissa % ↑(10 ^ (x.scale - digits))) = ↑(10 ^ (x.scale - digits)) → (Finance.round x digits Finance.RoundingMode.toEven).mantissa % 2 = 0 |
Quot.sound, propext |
round_neg (source) |
Refunds. Rounding a negated amount gives the negated rounding, for banker’s rounding, away-from-zero and truncation. Math.Floor(x * 100 + 0.5) / 100 fails this at every negative midpoint.∀ (x : Finance.Dec) (digits : ℕ) (mode : Finance.RoundingMode), mode = Finance.RoundingMode.toEven ∨ mode = Finance.RoundingMode.awayFromZero ∨ mode = Finance.RoundingMode.toZero → Finance.round (-x) digits mode = -Finance.round x digits mode |
Classical.choice, Quot.sound, propext |
round_round (source) |
Once is enough. Rounding a rounded value to the same precision changes nothing.∀ (x : Finance.Dec) (digits : ℕ) (mode : Finance.RoundingMode), Finance.round (Finance.round x digits mode) digits mode = Finance.round x digits mode |
Quot.sound, propext |
double_rounding_example (source) |
Double rounding is not rounding. Rounding 2.4449 to three places and then to two gives 2.45; rounding it to two directly gives 2.44. Round once, from the exact value, at the end.Finance.round (Finance.round { mantissa := 24449, scale := 4 } 3 Finance.RoundingMode.awayFromZero) 2 Finance.RoundingMode.awayFromZero ≠ Finance.round { mantissa := 24449, scale := 4 } 2 Finance.RoundingMode.awayFromZero |
no axioms |
Proven.RoundCentspublic static decimal RoundCents(decimal x)
public static Dec RoundCents(Dec x)
Round to cents with midpoints away from zero: the rule on an invoice.
Proved examples, each one a theorem in the Lean and a call that was run against the IL:
using Finance;
Proven.RoundCents(19.995m); // 20.00 (roundCents_example)
What is proved about it:
| Theorem | Says | Rests on |
|---|---|---|
roundCents_spec (source) |
Invoices. Cents are within half a cent of the amount, and a refund rounds to minus its sale.∀ (x : Finance.Dec), (2 < x.scale → 2 * (x.mantissa - ↑(10 ^ (x.scale - 2)) * (Finance.roundCents x).mantissa).natAbs ≤ 10 ^ (x.scale - 2)) ∧ Finance.roundCents (-x) = -Finance.roundCents x |
Classical.choice, Quot.sound, propext |
Proven.SplitEvenpublic static LeanList<BigInteger> SplitEven(BigInteger total, BigInteger n)
Split total cents into n shares that add up to exactly total and differ by at most one cent: the first
total % n shares get the extra cent. Negative totals, refunds, split the same way. Zero shares is the empty
list.
Proved examples, each one a theorem in the Lean and a call that was run against the IL:
using Finance;
Proven.SplitEven(-10000, 3); // [-3333, -3333, -3334] (splitEven_refund_example)
Proven.SplitEven(10000, 3); // [3334, 3333, 3333] (splitEven_example)
Proven.SplitEven(1, 4); // [1, 0, 0, 0] (splitEven_penny_example)
What is proved about it:
| Theorem | Says | Rests on |
|---|---|---|
splitEven_length (source) |
Everyone gets a share. There are exactly n of them.∀ (total : ℤ) (n : ℕ), (Finance.splitEven total n).length = n |
propext |
splitEven_sum (source) |
Not a cent lost or invented. For any number of people, the shares add up to exactly the total, refunds included.∀ (total : ℤ) (n : ℕ), 0 < n → (Finance.splitEven total n).sum = total |
Quot.sound, propext |
splitEven_fair (source) |
Fair to the cent. Every share is the total divided by n, rounded down, or one cent more.∀ (total : ℤ) (n : ℕ) (x : ℤ), x ∈ Finance.splitEven total n → x = total / ↑n ∨ x = total / ↑n + 1 |
Quot.sound, propext |
Finance.DecAn exact decimal number, mantissa × 10 ^ (-scale), the same shape as System.Decimal without its
96-bit limit. lean2il passes a .NET decimal in and out of any function over Dec.
BigInteger Mantissa: The digits, as an integer. 2.675 is mantissa 2675.BigInteger Scale: How many of those digits are after the decimal point. 2.675 is scale 3.A Dec has the shape of a System.Decimal, so every function over it also takes and returns decimal.
Finance.RoundingModeHow to settle a value that is not already at the requested precision. The five cases are .NET’s
MidpointRounding, in its order, with the same meaning: the first two only decide exact midpoints and
otherwise round to nearest; the last three are directed and ignore midpoints altogether.
ToEven: Nearest; a midpoint goes to the even neighbor. Banker’s rounding, and .NET’s default.AwayFromZero: Nearest; a midpoint goes away from zero. What invoices, tax forms and most people expect.ToZero: Toward zero: truncate.ToNegativeInfinity: Toward negative infinity: floor.ToPositiveInfinity: Toward positive infinity: ceiling.propext, Quot.sound and Classical.choice are Lean’s standard three; sorryAx would mean an unfinished proof and lean2il reports it.LeanToDotNet.Runtime: BigInteger arithmetic with Lean’s meaning for Nat and Int, Lean’s meaning for fixed-width integers where it differs from C#’s (division by zero, shift counts), and the exact decimal conversion.f.eq_def), which Tenet re-checks with everything else; each method is compiled from its equation’s right-hand side.