The gap
Arithmetic/LeanModel.lean proves that Lean core's unpacked add, mul and div on finite operands with a finite result equal one nearest-even rounding of the exact real result. The addition theorem applies directly. The other two carry extra hypotheses:
toReal_ofModel_mul_finite_eq_roundAt assumes exponent₁ + exponent₂ ≤ (FloatFormat.toModel fmt).targetExponent (totalExponent (mantissa₁ * mantissa₂) (exponent₁ + exponent₂)).toReal_ofModel_div_finite_eq_roundAt assumes the same inequality for the outputs of divCore, and also (divCore (FloatFormat.toModel fmt) mantissa₁ exponent₁ mantissa₂ exponent₂).1 ≠ 0.
The multiplication hypothesis is needed for arbitrary unpacked operands: in binary64, two operands .finite .positive 1 0 have exact product 1, but core mul returns mantissa 1 at exponent 0, which packs to the least positive subnormal. It always holds, though, for operands produced by toModel. I could not find a lemma in FloatLib that proves either hypothesis, and neither theorem is used elsewhere in the library. The guide says the same in chapter 18: their conclusions "apply once those conditions and the stated finite conditions have been established". So someone reasoning about Float or Float32 products and quotients has to prove facts about targetExponent, totalExponent and divCore first.
The nonzero-quotient hypothesis is also false for some ordinary inputs. In binary64, dividing the least positive subnormal by 1.5 gives divCore the mantissas 1 and 3 * 2 ^ 51 and the exponents -1074 and -52. It selects exponent -1074, shifts the numerator to 2 ^ 52, and returns the quotient 2 ^ 52 / (3 * 2 ^ 51) = 0 with a nonzero remainder. The rounded result is the least positive subnormal, which is finite, but the theorem does not apply. (Lean's kernel confirms these values by decide and rfl.)
What I have
For operands unpacked from format words the exponent hypotheses always hold. The division theorem's exponent hypothesis holds for all nonzero mantissas, and its nonzero-quotient hypothesis is not needed. I have proofs of the following, for every descriptor with fmt.isIEEE = true, in the Model namespace. The first two ask only for what a caller must supply. A finite result already implies finite factors for multiplication, and a finite dividend and a nonzero divisor for division, because core mul and div return a NaN or an infinity otherwise. Division still needs a finite divisor, since a finite value over an infinity is a finite zero.
theorem toReal_ofModel_mul_toModel_eq_roundAt {fmt : FloatFormat} (hfmt : fmt.isIEEE = true)
(x y : Model fmt)
(hfinite :
isFinite
(ofModel fmt
(Float.Model.UnpackedFloat.mul (FloatFormat.toModel fmt)
(toModel x) (toModel y))) = true) :
toReal
(ofModel fmt
(Float.Model.UnpackedFloat.mul (FloatFormat.toModel fmt)
(toModel x) (toModel y))) =
roundAt fmt (toReal x * toReal y)
theorem toReal_ofModel_div_toModel_eq_roundAt {fmt : FloatFormat} (hfmt : fmt.isIEEE = true)
(x y : Model fmt) (hy : isFinite y = true)
(hfinite :
isFinite
(ofModel fmt
(Float.Model.UnpackedFloat.div (FloatFormat.toModel fmt)
(toModel x) (toModel y))) = true) :
toReal
(ofModel fmt
(Float.Model.UnpackedFloat.div (FloatFormat.toModel fmt)
(toModel x) (toModel y))) =
roundAt fmt (toReal x / toReal y)
/-- `toReal_ofModel_div_finite_eq_roundAt` without its two `divCore` hypotheses. -/
theorem toReal_ofModel_div_finite_eq_roundAt_of_isFinite
(fmt : FloatFormat) (hfmt : fmt.isIEEE = true)
(sign₁ sign₂ : Sign) (mantissa₁ mantissa₂ : Nat) (exponent₁ exponent₂ : Int)
(hmantissa₁ : 0 < mantissa₁) (hmantissa₂ : 0 < mantissa₂)
(hfinite :
isFinite
(ofModel fmt
(Float.Model.UnpackedFloat.div (FloatFormat.toModel fmt)
(.finite sign₁ mantissa₁ exponent₁ hmantissa₁)
(.finite sign₂ mantissa₂ exponent₂ hmantissa₂))) = true) :
toReal
(ofModel fmt
(Float.Model.UnpackedFloat.div (FloatFormat.toModel fmt)
(.finite sign₁ mantissa₁ exponent₁ hmantissa₁)
(.finite sign₂ mantissa₂ exponent₂ hmantissa₂))) =
roundAt fmt
(unpackedToReal (.finite sign₁ mantissa₁ exponent₁ hmantissa₁) /
unpackedToReal (.finite sign₂ mantissa₂ exponent₂ hmantissa₂))
/-- Lean core's finiteness test agrees with `isFinite`. -/
theorem isFinite_toModel {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (x : Model fmt) :
(toModel x).isFinite = isFinite xThe idea is one equivalence. The precondition of roundWithAccuracy holds exactly when the exponent is at or below the least exponent or the mantissa has at least as many bits as the format's precision. Unpacked subnormals satisfy the first condition and unpacked normals the second. A product keeps the property. divCore shifts the numerator far enough that the quotient has that many bits whenever its exponent is above the least exponent, so a zero quotient only occurs at or below the least exponent. There the selected exponent and the remainder's accuracy together locate the value, and roundWithAccuracy rounds it to a signed zero or a signed least subnormal.
Six short supporting lemmas state those steps and the NaN packing fact; they are on the branch with the theorems. Everything is in one new module beside Arithmetic/LeanModel/AddSub.lean. No existing statement changes; one existing lemma, accuracyRepresents_accuracyOfFraction, loses its private keyword so the new module can reuse it. The change is one commit on top of main: #3 (branch lean-core-mul-div-rounding on my fork).
Questions
- Would you like these in FloatLib?
- If so, where and in what form? Options I can see:
- a new module
Arithmetic/LeanModel/MulDiv.lean, as on the branch;
- the supporting lemmas moved beside the results they extend (
targetExponent_eq_normal in ModelRounding/Proof.lean, toReal_ofModel_roundWithAccuracy_eq_roundAt in Rounding/Accuracy/Proof.lean, toDyadic?_isSome_eq_isFinite in Dyadic/Classification.lean);
- or the two
divCore hypotheses removed from the existing division theorem, which is a small change to its proof once the divCore exponent lemma and the zero-mantissa rounding lemma exist. The multiplication theorem would keep its exponent hypothesis for arbitrary unpacked operands, with the new theorem added for operands obtained through toModel.
A note on hypotheses: the two theorems over format words carry none that the finite result already implies. If you prefer the shape of toReal_div_eq_roundAt, with explicit isFinite x and isZero y = false hypotheses, that is a one-line weakening of each.
The proofs were developed with AI assistance and are checked by Lean's kernel.
I am happy to reshape this any way you prefer, or to drop it if it does not fit your plans.
Not included
For conventional IEEE descriptors, Model.add_eq_ofModel_add_of_isFinite and Model.sub_eq_ofModel_sub_of_isFinite in IEEE754/Native/AddSub.lean already cover addition and subtraction of finite format words with either sign of zero on either side.
These would be natural follow-ups for multiplication and division, and I left them out to keep the change small:
- corollaries stated on
Float and Float32 values, like the addition and subtraction ones in IEEE754/Native/AddSub.lean;
- word-level agreement of
Model.mul and Model.div with Lean core's unpacked operations, including the sign of zero;
- a composed statement for a multiply-then-add step on Lean core's operations, as in Horner evaluation.
The gap
Arithmetic/LeanModel.leanproves that Lean core's unpackedadd,mulanddivon finite operands with a finite result equal one nearest-even rounding of the exact real result. The addition theorem applies directly. The other two carry extra hypotheses:toReal_ofModel_mul_finite_eq_roundAtassumesexponent₁ + exponent₂ ≤ (FloatFormat.toModel fmt).targetExponent (totalExponent (mantissa₁ * mantissa₂) (exponent₁ + exponent₂)).toReal_ofModel_div_finite_eq_roundAtassumes the same inequality for the outputs ofdivCore, and also(divCore (FloatFormat.toModel fmt) mantissa₁ exponent₁ mantissa₂ exponent₂).1 ≠ 0.The multiplication hypothesis is needed for arbitrary unpacked operands: in binary64, two operands
.finite .positive 1 0have exact product1, but coremulreturns mantissa1at exponent0, which packs to the least positive subnormal. It always holds, though, for operands produced bytoModel. I could not find a lemma in FloatLib that proves either hypothesis, and neither theorem is used elsewhere in the library. The guide says the same in chapter 18: their conclusions "apply once those conditions and the stated finite conditions have been established". So someone reasoning aboutFloatorFloat32products and quotients has to prove facts abouttargetExponent,totalExponentanddivCorefirst.The nonzero-quotient hypothesis is also false for some ordinary inputs. In binary64, dividing the least positive subnormal by
1.5givesdivCorethe mantissas1and3 * 2 ^ 51and the exponents-1074and-52. It selects exponent-1074, shifts the numerator to2 ^ 52, and returns the quotient2 ^ 52 / (3 * 2 ^ 51) = 0with a nonzero remainder. The rounded result is the least positive subnormal, which is finite, but the theorem does not apply. (Lean's kernel confirms these values bydecideandrfl.)What I have
For operands unpacked from format words the exponent hypotheses always hold. The division theorem's exponent hypothesis holds for all nonzero mantissas, and its nonzero-quotient hypothesis is not needed. I have proofs of the following, for every descriptor with
fmt.isIEEE = true, in theModelnamespace. The first two ask only for what a caller must supply. A finite result already implies finite factors for multiplication, and a finite dividend and a nonzero divisor for division, because coremulanddivreturn a NaN or an infinity otherwise. Division still needs a finite divisor, since a finite value over an infinity is a finite zero.The idea is one equivalence. The precondition of
roundWithAccuracyholds exactly when the exponent is at or below the least exponent or the mantissa has at least as many bits as the format's precision. Unpacked subnormals satisfy the first condition and unpacked normals the second. A product keeps the property.divCoreshifts the numerator far enough that the quotient has that many bits whenever its exponent is above the least exponent, so a zero quotient only occurs at or below the least exponent. There the selected exponent and the remainder's accuracy together locate the value, androundWithAccuracyrounds it to a signed zero or a signed least subnormal.Six short supporting lemmas state those steps and the NaN packing fact; they are on the branch with the theorems. Everything is in one new module beside
Arithmetic/LeanModel/AddSub.lean. No existing statement changes; one existing lemma,accuracyRepresents_accuracyOfFraction, loses itsprivatekeyword so the new module can reuse it. The change is one commit on top ofmain: #3 (branchlean-core-mul-div-roundingon my fork).Questions
Arithmetic/LeanModel/MulDiv.lean, as on the branch;targetExponent_eq_normalinModelRounding/Proof.lean,toReal_ofModel_roundWithAccuracy_eq_roundAtinRounding/Accuracy/Proof.lean,toDyadic?_isSome_eq_isFiniteinDyadic/Classification.lean);divCorehypotheses removed from the existing division theorem, which is a small change to its proof once thedivCoreexponent lemma and the zero-mantissa rounding lemma exist. The multiplication theorem would keep its exponent hypothesis for arbitrary unpacked operands, with the new theorem added for operands obtained throughtoModel.A note on hypotheses: the two theorems over format words carry none that the finite result already implies. If you prefer the shape of
toReal_div_eq_roundAt, with explicitisFinite xandisZero y = falsehypotheses, that is a one-line weakening of each.The proofs were developed with AI assistance and are checked by Lean's kernel.
I am happy to reshape this any way you prefer, or to drop it if it does not fit your plans.
Not included
For conventional IEEE descriptors,
Model.add_eq_ofModel_add_of_isFiniteandModel.sub_eq_ofModel_sub_of_isFiniteinIEEE754/Native/AddSub.leanalready cover addition and subtraction of finite format words with either sign of zero on either side.These would be natural follow-ups for multiplication and division, and I left them out to keep the change small:
FloatandFloat32values, like the addition and subtraction ones inIEEE754/Native/AddSub.lean;Model.mulandModel.divwith Lean core's unpacked operations, including the sign of zero;