Lean does not panic when division by zero

Stream: lean4

[Asei Inoue]

In programming languages, it is common to “abort execution and return an error.”
In many languages, including Haskell, dividing by zero causes a runtime error.
However, in Lean, division by zero does not cause an error (at least when using Nat.div).

I’ve read Kevin’s excellent article on why this happens.
It was very clear. As I understand it, the article argues that since functions in Lean are used both as programs and as proofs, it’s better to avoid partial functions.
I’ve been trying to come up with my own way to explain this idea.

I thought of the following explanation:
A function that “crashes midway without returning a value” is, in the sense that it doesn’t return a value, equivalent to a function that loops forever.
Therefore, such a function should be disallowed from the perspective of soundness.
Is this explanation correct?
If it is, would it be possible to actually demonstrate a contradiction by allowing “functions that crash midway without returning a value” using something like the unsafe modifier—just as we can with functions that loop forever when unsafe is allowed?

[Kenny Lau]

not sure if I understand you correctly, but I don't think there's any soundness bug here, since docs#panic requires the type to be inhabited

and also I'm not sure if we have a common understanding of how panic works, and how proofs work, because in the alternative universe where division by zero is panic (which is bad for other reasons), it doesn't actually do anything when you're proving theorems, because when you prove theorems you don't usually evaluate the functions inside. For example, notice how the following code does not panic:

def f : Nat := panic "asdf"

example : f = f := rfl

it doesn't even panic when you unfold f! in fact it just unfolds to panic, saying the action is different from doing the action

so actually the only to make it panic is by eval-ing it, and the only way to do that is to do native_decide, i.e.

def f : Nat := panic! "asdf"

example : f = 0 := by
  decide +native

[Asei Inoue]

@Kenny Lau

I don't think there's any soundness bug here, since docs#panic requires the type to be inhabited

Indeed, if we use Lean’s panic function, then it’s safe.
Even if we don’t use panic, since Nat itself is Inhabited, a function of type Nat → Nat → Nat that crashes midway would still not lead to a contradiction.

I see, that makes sense to me now. Thank you.

[Riccardo Brasca]

Lean is very close to mathematical language, and in my opinion this makes things much more clear (the following is surely not 100% accurate): in mathematics there is no such a thing as "crashing" or "being undefined", and in Lean it is the same, a function must have a value. You can use tricks to simulate crashing, like using a default value, but there must is a value. You can of course also change the domain, and this is in theory perfectly doable, but annoying in practice.

[Kenny Lau]

@Asei Inoue note that the standard way to represent "crashing" is to add Option to the return type,

def Nat.div? : Nat → Nat → Option Nat :=
  fun p q ↦ if q = 0 ∨ p % q ≠ 0 then none else some (p / q)

#eval (List.range 11).map (Nat.div? 10 ·)

[Kenny Lau]

but please don't do it in mathlib

[Yury G. Kudryashov]

BTW, I think that writing a library on top of Mathlib that use Option or Part/PFun to provide semantics that's closer to the pen&paper math would be a nice project, but I don't have time for it. E.g., this will allow us to express the semantic of "if the RHS is defined, then the LHS is defined and is equal to RHS" or "both sides of an equation are defined and they're equal" (common understanding of equations with square roots etc in high school).

[Kenny Lau]

we'll need to bind everything in statements then? we'll end up with monads everywhere

[Kenny Lau]

import Mathlib

noncomputable def sqrt? : ℝ → Option ℝ :=
  fun x ↦ if 0 ≤ x then √x else none

notation "√?" x => sqrt? x

example : pure 0 < (do √?(1 + (← √? 2))) :=
  sorry

[Kenny Lau]

the < instance also needs to be changed

[Yury G. Kudryashov]

I don't know what's the best way to make it useful/readable. I think that we should convert inputs to Part _ and stay there, but I don't want to spend my time on this. Also, this library should come with a tactic that converts the goal to a Part-free version that can be proved using Mathlib.

[Yury G. Kudryashov]

While I think that this would be a nice project for someone relatively new to Lean (probably, under a supervision of someone more experienced), I think that almost any project aiming to formalize a nice theorem is more important.

[Trebor Huang]

In particular, is Lean able to non-tautologically state the theorem "The square root of x/(x-1) is defined on the subset (-inf, 0] union (1, +inf)"? What would be a nice way to formalize this kind of statements?

[Kenny Lau]

if you follow the above suggestion to use Option, then the statement would say that this expression is Option.IsSome

[Kenny Lau]

@Trebor Huang

import Mathlib

#print Part

-- TODO: the two functions below could be made computable

@[simps!] noncomputable def Real.sqrt? : ℝ → Part ℝ :=
  fun x ↦ ⟨0 ≤ x, fun _ ↦ √x⟩

@[simps!] noncomputable def Real.div? : ℝ → ℝ → Part ℝ :=
  fun x y ↦ ⟨y ≠ 0, fun _ ↦ x / y⟩

notation "√?" x => Real.sqrt? x
notation a " /? " b => Real.div? a b

theorem foo (x : ℝ) : (do √?(← x /? (x - 1))).Dom ↔ x ≤ 0 ∨ 1 < x := by
  simp; grind [div_nonneg_iff, sub_eq_zero]

[Kenny Lau]

I love grind

[James E Hanson]

Riccardo Brasca said:

in mathematics there is no such a thing as "crashing" or "being undefined",

Where are you getting the idea that in mathematics there is no such thing as "being undefined"? Mathematicians use the concept of an undefined quantity literally all the time (such as when discussing division by zero or limits that don't converge).

[Riccardo Brasca]

I just mean that f x is defined for every x in the domain of f.

[James E Hanson]

I just find it strange to be justifying the fact that Lean can't handle 1/0 in a way that resembles standard mathematical practice on the basis of claiming that in mathematics there is no such thing as something "being undefined".

It feels like equating "mathematics" with "mathematics that is easily formalized in type theory".

[Niels Voss]

At least, standard mathematics does not have a quantity called undefined; when something is undefined it is actually undefined. If 1 / 0 were to crash but we could still manipulate it in proofs, then it would essentially be an explicit undefined ∈ ℕ which represents a crash or diverging computation, and in standard math you can't write "Let $x \in \mathbb{N}$ be the diverging computation".

[Niels Voss]

That's not really a justification for why 1 / 0 = 0 though. In my opinion the real justification is that theorem proving is not technologically advanced enough to deal with partial functions in an ergonomic way, and 1 / 0 = 0 is an acceptable trade-off.

[James E Hanson]

I agree with most of what you're saying. I just don't think that it's reasonable to summarize it as 'in mathematics there is no such thing as being undefined'. If you ask an average mathematician whether there's no such thing as being undefined in mathematics, they will not agree that this is an accurate statement.

[James E Hanson]

It simply isn't an accurate representation of the standard terminological conventions used in mainstream mathematics.