0 - 1 is a natural number

Stream: new members

[Maarten Derickx]

I recently started playing around in lean a bit. And I was a bit surprised that lean was not complaining about the following:

import Mathlib

#check ((0 - 1) : ℕ)

I do not really know too much of lean so I'm still feeling a but fuzzy on what kind of semantics to attach to this. However my gut feeling is that I just proved that -1 is a natural number which is very problematic to say the least.

[Riccardo Brasca]

Subtraction for ℕ is truncated subtraction, meaning that (0 : ℕ) - (1 : ℕ) = 0. You can read more about this here

[Riccardo Brasca]

If you want to use "standard" subtraction just use ℤ, so that (0 : ℤ) - (1 : ℤ) = -1 as expected.

[Kyle Miller]

It's worth a mention that there's no universal - operation, and instead each type can have its own implementation of - without any need for these operations to be related to one another. There's a theorem though that if a b : Nat and b <= a then ((a - b : Nat) : Int) is (a : Int) - (b : Int), where Lean inserts a coercion function Nat -> Int where the types don't match up. This coercion function is defined in the library and it's the sensible one.

[Maarten Derickx]

Thanks for the quick answers. Ok, so at least I managed as an exercise to actually proof that lean indeed uses truncated subtraction, where I am assuming nothing unexpected is happening with the + and the ≥ symbols.

theorem truncated_subtraction (n : ℕ) (m : ℕ) (h: m ≥ n): n - m = 0 := by
  simp
  exact h

theorem normal_subtraction (n : ℕ) (m : ℕ) (b : ℕ) (h: n = m + b): n - m = b := by
  rw [h]
  simp

[Riccardo Brasca]

My general suggestion, at least at the beginning, is simply to avoid subtraction of natural numbers (and similarly don't use division for integers) to avoid getting confused. An exception is division by 0, that is unavoidable, and it is defined in mathlib (you can prove by simp that (1 : ℚ) / 0 = 0 ).

At the beginning this can look crazy, but the reason behind this (that should be seen just as an implementation detail, it is mathematically irrelevant) is explained in the blogpost I linked above.

[Notification Bot]

This topic was moved here from #mathlib4 > 0 - 1 is a natural number by Riccardo Brasca.