Division by zero; integrating non-integrable functions

Stream: general

[Axel Boldt]

I just finished the excellent book #mil and twice I experienced intense pain in my heart. Division by zero is defined to be zero, as is the integral of non-integrable functions. To me, this does violence to cherished defenseless notions.

Not knowing anything: isn't there a danger that somewhere in the bowels of a complicated proof, someone might inadvertently divide by zero or integrate a non-integrable function, and Lean will accept it? It seems that lots of proofs of "1=0" depend on a hidden division by zero. Even if it won't result in wrong proofs, it could very well result in wrong interpretations of Lean theorems or wrong formalizations of known math. Normally, when I see "a / b = 0", I will conclude "a = 0", or possibly "b= ∞" if that makes sense in the context, but the option "b=0" does not enter my mind. Similarly, when I see a formula for some integral, I will assume that the integrand is integrable in all (or almost all) cases, big mistake.

Do the advantages of those non-standard conventions really outweigh these downsides?

[Jireh Loreaux]

In short, yes, we're pretty convinced that the use of junk values like this is worth the downside of possible misinterpretation. It won't result in invalid proofs though.

To get a basic idea of why this is an issue: I encourage you to write the expression 1 / ((2 / 3) + (4 / 5)) : ℚ using docs#divp

import Mathlib.Tactic.NormNum

example : ℚ :=
  1 /ₚ .mk0 (2 /ₚ .mk0 3 (by norm_num) + 4 /ₚ .mk0 5 (by norm_num) : ℚ) (by norm_num)

[Etienne Marion]

Also mentioning this blog post https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/ on this topic (by Kevin Buzzard I think?).

[Jireh Loreaux]

This trick makes it slightly less painful, but I'm not even sure we should have this in Mathlib:

import Mathlib.Tactic.NormNum
import Mathlib.Tactic.OfNat

instance {R : Type*} [DivisionSemiring R] [CharZero R] (n : ℕ) [hn : NeZero n] : OfNat Rˣ n where
  ofNat := .mk0 (OfNat.ofNat n) (by rw [Lean.Grind.Semiring.ofNat_eq_natCast]; simp [hn.out])

@[simp]
lemma Units.val_ofNat {R : Type*} [DivisionSemiring R] [CharZero R] (n : ℕ) [hn : NeZero n] :
    ((ofNat(n) : Rˣ) : R) = (ofNat(n) : R) :=
  rfl

example : ℚ :=
  1 /ₚ .mk0 (2 /ₚ 3 + 4 /ₚ 5) (by simp [divp_eq_div]; norm_num)

[James E Hanson]

Axel Boldt said:

isn't there a danger that somewhere in the bowels of a complicated proof, someone might inadvertently divide by zero or integrate a non-integrable function, and Lean will accept it?

This is an issue in principle, yes. The value of the Riemann zeta function at $1$ in Lean is $\frac{1}{2}(\gamma - \log 4\pi)$, which results from the $\frac{1}{0} = 0$ convention and the way $\zeta(s)$ is defined. Because of this, there is a mathematically non-trivial junk theorem in Mathlib, riemannZeta_one, which was necessary to prove in order to establish that $\zeta(1) \neq 0$. If it had happened to be the case that $\zeta(1) = 0$, this would make certain innocuous statements of the Riemann hypothesis trivially false. This is discussed in section 5 of this paper by Loeffler and Stoll.

[Etienne Marion]

Well I mean if you are not confident with this you can always add the hypotheses you'd expect irl to be sure. For instance in the formalization of the Riemann hypothesis they could have add a ≠ 1 hypothesis to be safe.

[Kevin Buzzard]

docs#RiemannHypothesis does have an s ≠ 1 hypothesis (even though as James points out it's not strictly necessary)

[Etienne Marion]

Oh that's funny I seemed to recall there wasn't

[Kevin Buzzard]

That is also true :-)

[Etienne Marion]

Ok I didn't have an hallucination then :sweat_smile:

[Niels Voss]

See also: https://leanprover-community.github.io/extras/pitfalls.html#division-by-0

[Riccardo Brasca]

This has been discussed a lot in zulip, my suggestion is to read some of these conversations (I don't have links sadly).

The TLDR is what has been already said above: experience told us this is the best solution. We agree it's not perfect, but any other solution that may look better at the beginning is actually worst.

[Bhavik Mehta]

I think it's worth saying though that, as James points out, this can lead to reasonable looking statements not meaning what they should mean. But this can't lead to incorrect proofs being accepted by Lean only for Lean to accept a correct proof of a dubious statement. For instance, the usual "proofs" of 1 = 0 will at some point not get accepted by Lean, precisely because of a theorem about a division not being applicable.

[Axel Boldt]

Bhavik Mehta said:

this can lead to reasonable looking statements not meaning what they should mean.

Or even: the real meaning of statements being entirely unclear. Take for instance the very last example in #mil, the general substitution rule:

example {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]

    [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] {F : Type*}

    [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {s : Set E} {f : E → E}

    {f' : E → E →L[ℝ] E} (hs : MeasurableSet s)

    (hf : ∀ x : E, x ∈ s → HasFDerivWithinAt f (f' x) s x) (h_inj : InjOn f s) (g : E → F) :

    ∫ x in f '' s, g x ∂μ = ∫ x in s, |(f' x).det| • g (f x) ∂μ :=

    sorry

Note that there's no assumption on g. I couldn't translate this statement into math; I have this weird fear that one integral might be zero because it doesn't exist, while the other integral just happens to be zero.

[Sébastien Gouëzel]

You're absolutely right. If the library is written in a sane way, this theorem should have a very nearby friend saying that g is integrable on f '' s iff |(f' x).det| • g (f x) is integrable on s. And indeed we have it, it's docs#MeasureTheory.integrableOn_image_iff_integrableOn_abs_det_fderiv_smul (the theorem just before the one you mention)