0 - n = 0

Stream: new members

[Malvin Gattinger]

I think I just learned that 0 - n = 0 for any n : ℕ in Lean, is that correct?

lemma theLemma { m n : ℕ }: m = m - 1 - 1 - n + n + 2 :=
begin
  induction m,
  simp,
  -- why does Lean want me to prove  0 = n + 2  now?
  sorry,
  sorry,
end

-- oh, wait a minute!
#eval 0 - 1
-- | 0

[Riccardo Brasca]

Dont worry :)

[Riccardo Brasca]

You can read about it here

[Riccardo Brasca]

But the important part of the story is that subtraction on ℕ it's not exactly the operation you are familiar with (it is when its result is in ℕ). If you try the same in ℤ, everything will behave as expected.

[Riccardo Brasca]

If you are a beginner I would suggest just to avoid subtraction on ℕ (or division in ℤ).

[Mario Carneiro]

The short answer is that a - b in nat is actually the function max(a - b, 0)

[Malvin Gattinger]

Aha, okay, That blog post is excellent explanation and entertainment, thank you :sweat_smile: