is lean really catching that $$n \in ℕ ≥ 0$$ ?

Stream: new members

[rzeta0]

The following is a simple proof that $(a-b)(a+b)=a^2-b^2$ for $a,b \in ℤ$:

-- 04 - Simple Algebra

import Mathlib.Tactic

example {a b : ℤ} : (a - b) * (a + b) = a^2 - b^2 :=
  calc
    (a - b) * (a + b) = a^2 - a*b + a*b - b^2 := by ring
    _ = a^2 - b^2 := by ring

If I deliberately change {a b : ℤ} to {a b : ℕ} lean throws errors:

04_algebra.lean:7:52
Try this: ring_nf
04_algebra.lean:7:49
unsolved goals
a b : ℕ
⊢ (a - b) * a + (a - b) * b = a * b + (a ^ 2 - a * b) - b ^ 2

Question: Is Lean really catching the fact that $(a-b)$ does not make sense if $b>a$, because natural numbers can't be negative integers?

The error messages don't make it clear what Lean actually found to be problematic. I am really hoping Lean caught the case that $b>a$ is not valid in ℕ.

[Josha Dekker]

rzeta0 said:

The following is a simple proof that $(a-b)(a+b)=a^2-b^2$ for $a,b \in ℤ$:

-- 04 - Simple Algebra

import Mathlib.Tactic

example {a b : ℤ} : (a - b) * (a + b) = a^2 - b^2 :=
  calc
    (a - b) * (a + b) = a^2 - a*b + a*b - b^2 := by ring
    _ = a^2 - b^2 := by ring

If I deliberately change {a b : ℤ} to {a b : ℕ} lean throws errors:

04_algebra.lean:7:52
Try this: ring_nf
04_algebra.lean:7:49
unsolved goals
a b : ℕ
⊢ (a - b) * a + (a - b) * b = a * b + (a ^ 2 - a * b) - b ^ 2

Question: Is Lean really catching the fact that $(a-b)$ does not make sense if $b>a$, because natural numbers can't be negative integers?

The error messages don't make it clear what Lean actually found to be problematic. I am really hoping Lean caught the case that $b>a$ is not valid in ℕ.

If I'm correct (but someone more experienced should verify this) subtraction of natural numbers is defined with junk values if $b > a$.

Judging by the error, what Lean is picking up is that ring can't close the goal in N, which I think is either because N is not a ring or because of these junk values.

[Damiano Testa]

I'm having a déjà vu... :smile:

[Giacomo Stevanato]

Substraction when b > a is defined to be 0 rather than some arbitrary junk value.

[Damiano Testa]

Giacomo Stevanato said:

Substraction when b > a is defined to be 0 rather than some arbitrary junk value.

While I agree with the sentiment, I still feel that 1 - 2 = 0 is a pretty junk value...

[Giacomo Stevanato]

Yeah, I'm not saying it is well defined, rather that it could be junkier (e.g. some seemingly random and implementation defined value)

[Giacomo Stevanato]

You can still reason about such subtraction operation, it just won't be the natural one.

[Riccardo Brasca]

@rzeta0 The short answer is just to avoid using subtraction on natural numbers. What you would obtain is probably not you think. If you want to know more there are a lot of threads on Zulip about this.

[rzeta0]

so just to refocus on the actual question - is Lean catching this because

(a) ℕ is not a ring
(b) something else (I don't understand junk values)

I'm hoping the answer is (a).

Why?

Because I would hope a theorem prover actually catches or cautions against the use of subtraction when the results might not be in the defined set of numbers.

[Yaël Dillies]

It is catching the issue because there is no Ring ℕ instance

[Riccardo Brasca]

The point is that the result is in ℕ, always.

[rzeta0]

Yaël, Riccardo - thanks for trying to help. You'll have to forgive me I am not mathematically trained (and my coding is not expert either). Can I check then:

Yaël - There is no Ring ℕ instance means that within mathlib there is no definition of ℕ as a ring. Which to me sounds like primarily "N is not a ring under addition/subtraction" and so secondarily nobody implemented it as a Ring in mathlib. Is this correct?

Riccardo - I'm not clear on what. you mean by "the result is in ℕ always". Are you saying the because the result of $a-b$ might not be in ℕ, that is the reason it fails. In which case you're saying the same thing as (a). Am I right?

Thanks for your patience :)

[Riccardo Brasca]

ℕ is what is called a semiring: in a ring every element needs to have an additive inverse, so ℕ is not a ring.

[Riccardo Brasca]

I mean that in Lean 3 - 5 = 0, and everything is in ℕ.

[Yaël Dillies]

rzeta0 said:

Yaël - There is no Ring ℕ instance means that within mathlib there is no definition of ℕ as a ring. Which to me sounds like primarily "N is not a ring under addition/subtraction" and so secondarily nobody implemented it as a Ring in mathlib. Is this correct?

Yes, that is correct. Note that no one is stopping you from writing an instance of Ring ℕ but, as you note, it would need to have a different addition/subtraction than what is currently provided.

[Riccardo Brasca]

This may look very strange, but as I said beginners should just ignore it, and not use subtraction of natural numbers (if you're curious just look at any of the various discussions about this).

[Bbbbbbbbba]

Damiano Testa said:

Giacomo Stevanato said:

Substraction when b > a is defined to be 0 rather than some arbitrary junk value.

While I agree with the sentiment, I still feel that 1 - 2 = 0 is a pretty junk value...

I do believe that truncated subtraction (https://en.wikipedia.org/wiki/Monus#Natural_numbers) is occasionally useful.

[rzeta0]

Hi Riccardo - "beginners should not use subtraction of natural numbers" feels like a huge request :)

In fact it feels counter-intuitive. I suspect I have lots to learn ... and when I reach nirvana, I will understand why I can't subtract two natural numbers! :)

[rzeta0]

hi @Bbbbbbbbba - should a different symbol be used for monus?

[Riccardo Brasca]

There are really a lot of threads about this. For example this one

[Bbbbbbbbba]

Introducing a monus symbol is actually an interesting proposal

[Bbbbbbbbba]

∸ is a Unicode symbol and I think its meaning is pretty established

[Riccardo Brasca]

This has already been discussed, the main problem is what to do with the - symbol.

[Riccardo Brasca]

Let's try to not replicate the other thread :)