Why can't `ring` prove $$x^2 - y^2 = (x+y) (x-y)$$?

Stream: new members

[Divya Ranjan]

The following code:

import Mathlib

example (x y : ℕ): x^2 - y^2 = (x+y) * (x-y) := by
  ring
  sorry

only goes so far as to expand the RHS into x * (x - y) + y * (x - y)

[Divya Ranjan]

Obviously Nat.sq_sub_sq does it, but I just wanna know what stops ring from doing it.

[Ben Eltschig]

The subtraction you are doing takes place in the natural numbers, not a ring, and subtraction in $\mathbb N$ is not well-behaved. In usual mathematics, it only is a partial operation, defined on $\{n,m\in\mathbb N\mid m\le n\}$; in lean, it is defined on all pairs of natural numbers by setting $n - m$ to be $0$ when $n<m$. This is convenient because it allows you to take the difference of two numbers without proving that one is greater than the other, but also means that many of the usual properties of subtraction don't apply.

[Ben Eltschig]

If you annotate the type as $\mathbb Z$ or $\mathbb R$ anywhere in your theorem though, lean will understand that the operations should take place in that ring. For example, this works:

import Mathlib

example (x y : ℕ): (x^2 - y^2 : ℤ) = (x+y) * (x-y) := by ring

[Divya Ranjan]

Ben Eltschig said:

The subtraction you are doing takes place in the natural numbers, not a ring, and subtraction in $\mathbb N$ is not well-behaved. In usual mathematics, it only is a partial operation, defined on $\{n,m\in\mathbb N\mid m\le n\}$; in lean, it is defined on all pairs of natural numbers by setting $n - m$ to be $0$ when $n<m$. This is convenient because it allows you to take the difference of two numbers without proving that one is greater than the other, but also means that many of the usual properties of subtraction don't apply.

Wouldn't the other way be easier? To have subtraction strictly defined on $m \leq n$ and its responsibility of the proof reader/writer to ensure that the numbers being operated remain within Naturals. The reason I say this is that, this makes some simplification processes unnecessarily complicated. Like the below:

have h1: (10 * a + b + (10 * b + a)) * (10 * a + b - (10 * b + a)) = 11*(a+b) - 9*(a-b) := by
  rw [show 10 * a + b + (10 * b + a) = 10*a + b + 10*b + a by ring_nf]
  rw [show 10 * a + b + 10 * b + a = 11*(a+b) by ring_nf]
  sorry

[Ben Eltschig]

Multiplication being only defined on $\{(n,m)\mid m\le n\}$ would mean that you can't even write n - m; the subtraction operator would have to take three inputs, n, m and a proof of m\le n. Writing down x^2 - y^2 = (x+y) * (x-y) alone would already require supplying two such proofs (via some corresponding notation instead of plain old -), before even trying to prove anything.

[Ben Eltschig]

The way it is implemented now, you still need to supply those proofs, but only when trying to prove something about the result of the subtraction, not to write it down in the first place. Sometimes you even get lucky and don't need to supply a proof at all; docs#Nat.sq_sub_sq is one such example, where the identity also holds for this extended subtraction.

[Divya Ranjan]

Ben Eltschig said:

Multiplication being only defined on $\{(n,m)\mid m\le n\}$ would mean that you can't even write n - m; the subtraction operator would have to take three inputs, n, m and a proof of m\le n. Writing down x^2 - y^2 = (x+y) * (x-y) alone would already require supplying two such proofs (via some corresponding notation instead of plain old -), before even trying to prove anything.

One would provide a corresponding assumption/hypothesis that indeed $m \leq n$ as natural numbers. We don't usually prove this in mathematics unless required, yet it is well-defined when used in a proof.

[Divya Ranjan]

And, I believe we'd have proofs also that if $m \leq n$ then it follows that $n^2 \geq m^2$ as well.

[Divya Ranjan]

Divya Ranjan said:

Ben Eltschig said:

The subtraction you are doing takes place in the natural numbers, not a ring, and subtraction in $\mathbb N$ is not well-behaved. In usual mathematics, it only is a partial operation, defined on $\{n,m\in\mathbb N\mid m\le n\}$; in lean, it is defined on all pairs of natural numbers by setting $n - m$ to be $0$ when $n<m$. This is convenient because it allows you to take the difference of two numbers without proving that one is greater than the other, but also means that many of the usual properties of subtraction don't apply.

Wouldn't the other way be easier? To have subtraction strictly defined on $m \leq n$ and its responsibility of the proof reader/writer to ensure that the numbers being operated remain within Naturals. The reason I say this is that, this makes some simplification processes unnecessarily complicated. Like the below:

have h1: (10 * a + b + (10 * b + a)) * (10 * a + b - (10 * b + a)) = 11*(a+b) - 9*(a-b) := by
  rw [show 10 * a + b + (10 * b + a) = 10*a + b + 10*b + a by ring_nf]
  rw [show 10 * a + b + 10 * b + a = 11*(a+b) by ring_nf]
  sorry

Either way, it is this that has been frustrating me. Doing calculating proofs is a mess, and unless we're in the realm of abstract mathematical subjects (group theory, topology etc.), up until 3-dimensional calculus, it is such calculational algebra that makes up most of proofs. So I believe something can be made easier.

[Ben Eltschig]

Divya Ranjan said:

Ben Eltschig said:

Multiplication being only defined on $\{(n,m)\mid m\le n\}$ would mean that you can't even write n - m; the subtraction operator would have to take three inputs, n, m and a proof of m\le n. Writing down x^2 - y^2 = (x+y) * (x-y) alone would already require supplying two such proofs (via some corresponding notation instead of plain old -), before even trying to prove anything.

One would provide a corresponding assumption/hypothesis that indeed $m \leq n$ as natural numbers. We don't usually prove this in mathematics unless required, yet it is well-defined when used in a proof.

The thing is, lean can't work with this $m\le n$ assumption implicitly in the background like a mathematician can. When subtraction is only defined for some pairs of natural numbers, say as Nat.sub (n m : ℕ) (h : m ≤ n) : ℕ, then you would have to explicitly write Nat.sub n m h each time - or Nat.sub n m (by ...) if the proof is something more complicated you don't already have on hand. You couldn't even use - notation, because that takes two arguments and here you'd need 3.

[Ben Eltschig]

Really, the main thing that can make your proofs easier is to avoid subtraction of naturals where you can. I don't know what exactly you are working on, but I would hope there is some way to avoid this, for example by passing to integers and doing your computations there.

[Divya Ranjan]

Ben Eltschig said:

Divya Ranjan said:

Ben Eltschig said:

Multiplication being only defined on $\{(n,m)\mid m\le n\}$ would mean that you can't even write n - m; the subtraction operator would have to take three inputs, n, m and a proof of m\le n. Writing down x^2 - y^2 = (x+y) * (x-y) alone would already require supplying two such proofs (via some corresponding notation instead of plain old -), before even trying to prove anything.

One would provide a corresponding assumption/hypothesis that indeed $m \leq n$ as natural numbers. We don't usually prove this in mathematics unless required, yet it is well-defined when used in a proof.

The thing is, lean can't work with this $m\le n$ assumption implicitly in the background like a mathematician can. When subtraction is only defined for some pairs of natural numbers, say as Nat.sub (n m : ℕ) (h : m ≤ n) : ℕ, then you would have to explicitly write Nat.sub n m h each time - or Nat.sub n m (by ...) if the proof is something more complicated you don't already have on hand. You couldn't even use - notation, because that takes two arguments and here you'd need 3.

I see. Can Lean do partial application of functions like Haskell can?

[Divya Ranjan]

Ben Eltschig said:

Really, the main thing that can make your proofs easier is to avoid subtraction of naturals where you can. I don't know what exactly you are working on, but I would hope there is some way to avoid this, for example by passing to integers and doing your computations there.

Well. A big chunk of elementary algebra/number theory happens within $\N$. I was trying to prove a simple math competition problem, but gut stuck in figuring out these subtraction issues.

[Ben Eltschig]

Divya Ranjan said:

I see. Can Lean do partial application of functions like Haskell can?

You mean supplying only some of the inputs at a time? Yup. Nat.sub n m would then be of type m ≤ n → ℕ in that scenario, which would still make it rather annoying to work with.

[Eric Paul]

Also, it seems like what you were trying to show is not true:

import Mathlib

example : ¬∀a b : ℕ, (10 * a + b + (10 * b + a)) * (10 * a + b - (10 * b + a)) = 11*(a+b) - 9*(a-b) := by
  intro h
  specialize h 0 1
  simp at h

And not just because it is using natural number subtraction as we see here

import Mathlib

example : ¬∀a b : ℤ, (10 * a + b + (10 * b + a)) * (10 * a + b - (10 * b + a)) = 11*(a+b) - 9*(a-b) := by
  intro h
  specialize h 0 1
  simp at h

[Divya Ranjan]

Eric Paul said:

Also, it seems like what you were trying to show is not true:

import Mathlib

example : ¬∀a b : ℕ, (10 * a + b + (10 * b + a)) * (10 * a + b - (10 * b + a)) = 11*(a+b) - 9*(a-b) := by
  intro h
  specialize h 0 1
  simp at h

And not just because it is using natural number subtraction as we see here

import Mathlib

example : ¬∀a b : ℤ, (10 * a + b + (10 * b + a)) * (10 * a + b - (10 * b + a)) = 11*(a+b) - 9*(a-b) := by
  intro h
  specialize h 0 1
  simp at h

I forgot to mention but that I had a hypothesis that demanded $a,b \neq 0$. And for all non-zero positive natural numbers, the equation does hold:
$(10a + b + 10b + a)(10a + b - 10b -a) = (11(a+b))(9(a-b))$

[Divya Ranjan]

Ah, I see the typo now.

[Divya Ranjan]

I had a minus in the R.H.S, apologies.

[Divya Ranjan]

But beyond that, I believe one does get into a mess of simplification:

import Mathlib

open Nat

theorem number_theory_21 {x y a b m : ℕ} (hx: x = 10*a + b) (hab: a ≠ 0 ∧ b ≠ 0) (hy: y = 10*b + a) (hxym: x^2 - y^2 = m^2) : x + y + m = 154 := by
intros
have hxy: x^2 - y^2 = 11 * (a+b) * 9 * (a - b) := by
  rw [sq_sub_sq]
  rw [hx, hy]
  rw [show 10 * a + b + (10 * b + a) = 10*a + b + 10*b + a by ring_nf]
  rw [show 10 * a + b + 10 * b + a = 11*(a+b) by ring_nf]
  nth_rw 1 [sub_add_eq]
  sorry
sorry

[Eric Paul]

If whenever you have subtraction you move into the integers, things become much easier.
Note that the variables you're using are still natural numbers, but you're moving to the integers for calculation.

import Mathlib

open Nat

theorem number_theory_21 {x y a b m : ℕ} (hx: x = 10*a + b) (hab: a ≠ 0 ∧ b ≠ 0) (hy: y = 10*b + a) (hxym: x^2 - (y^2 : ℤ) = m^2) : x + y + m = 154 := by
  have hxy: (x^2 : ℤ) - y^2 = 11 * (a+b) * 9 * (a - b) := by
    simp [hx, hy]
    ring
  sorry

[Divya Ranjan]

Eric Paul said:

If whenever you have subtraction you move into the integers, things become much easier.
Note that the variables you're using are still natural numbers, but you're moving to the integers for calculation.

import Mathlib

open Nat

theorem number_theory_21 {x y a b m : ℕ} (hx: x = 10*a + b) (hab: a ≠ 0 ∧ b ≠ 0) (hy: y = 10*b + a) (hxym: x^2 - (y^2 : ℤ) = m^2) : x + y + m = 154 := by
  have hxy: (x^2 : ℤ) - y^2 = 11 * (a+b) * 9 * (a - b) := by
    simp [hx, hy]
    ring
  sorry

Does the type annotation for "moving into integers" just remain for that step? I don't have to do work to port it back to Natural numbers?

[Eric Paul]

That is a fact about two expressions involving integers being equal to each other.
But if you show your goal for things as integers, it does imply it for them as natural numbers:

import Mathlib

open Nat

example (x y m : ℕ) (h : (x : ℤ) + y + m = 154) : x + y + m = 154 := by
  exact Int.ofNat_inj.mp h

[Ben Eltschig]

Note also that he added the : ℤ not just in hxy, but also in hxym - it's a bit hard to see because the line is so long. That simply means that your assumption is now "the difference of $x^2$ and $y^2$ as integers is equal to $m^2$" even though $x$, $y$ and $m$ are naturals, which is probably closer to the assumption you actually want.

[Divya Ranjan]

Ben Eltschig said:

Note also that he added the : ℤ not just in hxy, but also in hxym - it's a bit hard to see because the line is so long. That simply means that your assumption is now "the difference of $x^2$ and $y^2$ as integers is equal to $m^2$" even though $x$, $y$ and $m$ are naturals, which is probably closer to the assumption you actually want.

Indeed, I'll keep note of this method.

[Mario Carneiro]

By the way, the zify tactic is intended exactly for this use case: when your goal has natural subtractions in it and you want to work over integers, you call zify and pass proofs that everything relevant is ordered, like this

theorem number_theory_21 {x y a b m : ℕ} (hx: x = 10*a + b) (hab: a ≠ 0 ∧ b ≠ 0)
    (hy: y = 10*b + a) (hxym: x^2 - y^2 = m^2) : x + y + m = 154 := by
  have : y^2 ≤ x^2 := sorry
  zify [this] at *

[Mario Carneiro]

notice that without the have statement hxym is translated to hxym : ↑(x ^ 2 - y ^ 2) = ↑m ^ 2 instead of hxym : ↑x ^ 2 - ↑y ^ 2 = ↑m ^ 2