not understanding deliberate error with `ring` over ℕ

Stream: new members

[rzeta0]

The following is a short proof to show $(a+b)(a-b)=a^2-b^2$ where $a,b \in ℤ$.

import Mathlib.Tactic

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

If I intentionally change the variable types to be $a, b \in ℕ$ I hope to get an error, because the algebraic identity isn't always valid, that is, when $b>a$.

import Mathlib.Tactic

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

Question: I'm struggling to understand the meaning of Lean's error message. How do I interpret them?

I was hoping they would tell me that the algebraic identity is not valid for $a, b \in ℕ$ , but I can't seem to divine that from the errors.

04_algebra.lean:5:16
Expected type
⊢ Type
All Messages (2)
04_algebra.lean:7:40
Try this: ring_nf
04_algebra.lean:7:37
unsolved goals
a b : ℕ
⊢ (a - b) * a + (a - b) * b = a ^ 2 - b ^ 2

[Julian Berman]

It's a bit obtuse, but the explanation I think is -- when you say "not valid", you're saying not true right? Mathlib doesn't know many things about things which are not true, so it doesn't tell you something nice there that you can interpret as "no that's wrong".

[Julian Berman]

Instead what you're seeing is that the ring tactic which is what can be used to prove these kinds of identities is making some progress. It's managing to simplify the expressions somehow a bit.

[Julian Berman]

And then the error message you're seeing is the ring tactic saying "I'm a finishing tactic, you're supposed to use me at the end of a proof, but you're not done. So you should use ring_nf, which is the same tactic but can be used in the middle of the proof".

[Julian Berman]

And then that's all, Lean is then telling you "you have more to do", without also knowing that you are hopeless to ever finish.

[Julian Berman]

If you change ring to ring_nf and then again try ring afterwards, you should see an error message now telling you that ring makes no progress on your goal. Does the above help at all?

[Philippe Duchon]

My understanding is that the theorem is valid, though the "expand and collect" method with commutativity will probably not work; but the statement is true in the naturals, since the minus sign denotes truncated subtraction.

[rzeta0]

Julian - thanks for explaining what is happening, I'll need to re-read it several times to understand it.

Phillippe - thanks, I think the truncated subtraction and division will cause many errors for me! Do others think it is counter-intuitive, or is it just me?

[Julian Berman]

(Ah indeed I didn't even read carefully enough to see whether the statement was true or not!)

[Julian Berman]

I think the truncated subtraction and division will cause many errors for me! Do others think it is counter-intuitive, or is it just me?

There's two pieces to this I think from what I've seen in the community -- one about Nat.sub specifically, where I think some Elder Experts say "avoid it" (but I'm just repeating what I recall seeing so hopefully someone will chime in with specifics about Nat.sub -- I believe it's simply because it doesn't have very many nice mathematical properties?).

But the broader question of "isn't it error-prone to have total functions everywhere and make lots of use of garbage values" I think the community believes to be resoundingly (if counterintuitively) beneficial, and simplifies lots of things in formalization. The TL;DR is that proofs which rely on not evaluating functions at the garbage value can include that as a hypothesis as needed, but often the garbage value can even make theorems true at even more of the domain if the garbage value is chosen well.

[Julian Berman]

And there's a post somewhere from Kevin which elaborates a bit more, let's see if I find it before someone else links it.

[Julian Berman]

https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/ I believe this one.

[Yaël Dillies]

I do wonder whether we could write linter.garbageValue, a linter that complains every time you use a total function with garbage values without an hypothesis in context that your input is not garbage

[Yaël Dillies]

Eg

example (a b : Nat) : a - b = 0 := sorry
example (a b : Nat) : a / b = 0 := sorry
example (a b : Int) : a / b = 0 := sorry
example (a b : Rat) : a / b = 0 := sorry
example (a b : Rat) : a / b = 0 := sorry
example (s : Real) : sSup s = 0 := sorry

would all complain, but

example (a b : Nat) (hba : b ≤ a) : a - b = 0 := sorry
example (a b : Nat) (hba : b ∣ a) (hb : b ≠ 0) : a / b = 0 := sorry
example (a b : Int) (hba : b ∣ a) (hb : b ≠ 0) : a / b = 0 := sorry
example (a b : Rat) (hb : b ≠ 0) : a / b = 0 := sorry
example (s : Real) (hs₀ : s.Nonempty) (hs₁ : BddAbove s) : sSup s = 0 := sorry
example (s : ENNReal) : sSup s = 0 := sorry

would not

[Damiano Testa]

That linter exists in branch format: branch#adomani/papercut_linter.

[Damiano Testa]

Right now, it would complain always (and not on everything that you mentioned). Adding more context awareness is of course possible but tricky.

[Damiano Testa]

On that branch, these are the messages:

import Batteries.Data.Rat.Basic
import Mathlib.Tactic.Linter.Papercut

set_option linter.papercut true

/-- an axiom just so `#guard_msgs` does not flag the `sorry` each time. -/
axiom paperSorry {α} : α

/--
warning: Subtraction in ℕ is actually truncated subtraction: e.g. `1 - 2 = 0`!
note: this linter can be disabled with `set_option linter.papercut false`
-/
#guard_msgs in
example (a b : Nat) : a - b = 0 := paperSorry

/--
warning: Division in ℕ is actually the floor of the division: e.g. `1 / 2 = 0`!
note: this linter can be disabled with `set_option linter.papercut false`
-/
#guard_msgs in
example (a b : Nat) : a / b = 0 := paperSorry

/--
warning: Division in ℤ is actually the floor of the division: e.g. `(1 : ℤ) / 2 = 0`!
note: this linter can be disabled with `set_option linter.papercut false`
-/
#guard_msgs in
example (a b : Int) : a / b = 0 := paperSorry

/--
warning: Division by `0` is usually defined to be zero: e.g. `3 / 0 = 0`!
note: this linter can be disabled with `set_option linter.papercut false`
-/
#guard_msgs in
example (a : Rat) : a / 0 = 0 := paperSorry

and in each case, the relevant operation is underlined

[Damiano Testa]

By the way, there is a tactic called slim_check that can help figure out whether some propositions have simple counterexamples:

import Mathlib.Tactic

example {a b : ℕ} : (a - b) * (a + b) = a^2 - b^2 := by
  slim_check  -- Success  (implying that it tried out a few cases and they all were true statements)

example {a b : ℕ} : (a - b) = (a + b) := by
  slim_check
-- Found problems ...

[Kyle Miller]

Fun fact, the theorem about Nat is true:

example {a b : ℕ} : (a - b) * (a + b) = a^2 - b^2 := by
  by_cases h : a ≥ b
  · simp [Nat.sub_mul, Nat.mul_add]
    rw [← Nat.add_sub_assoc]
    swap; apply Nat.mul_le_mul_right _ h
    rw [mul_comm b a, Nat.sub_add_cancel]
    swap; apply Nat.mul_le_mul_left _ h
    rw [pow_two, pow_two]
  · simp at h
    have : a - b = 0 := by omega
    rw [this]
    have : a^2 < b^2 := by gcongr
    have : a^2 - b^2 = 0 := by omega
    rw [this]
    simp

(I'm sure this could be more elegantly done!)

[Kyle Miller]

I think the truncated subtraction and division will cause many errors for me! Do others think it is counter-intuitive, or is it just me?

It's a bit counterintuitive, but what I've come to realize is that each theorem you prove with a given theorem is a test for that theorem. If you stated the theorem incorrectly, eventually you will discover the mistake. (Plus, you get used to avoiding Nat subtraction since it's so annoying to prove anything about. Though sometimes it's nice that it's monus since truncation is the "right" junk value, as this example above shows. Isn't it sort of nice that you don't need the hypothesis that a >= b to apply it?)

[Damiano Testa]

Yaël Dillies said:

I do wonder whether we could write linter.garbageValue, a linter that complains every time you use a total function with garbage values without an hypothesis in context that your input is not garbage

In case anyone in this thread is interested, #13999 is a PR with the linter.

[rzeta0]

Yaël Dillies said:

Eg

example (a b : Nat) : a - b = 0 := sorry
example (a b : Nat) : a / b = 0 := sorry
example (a b : Int) : a / b = 0 := sorry
example (a b : Rat) : a / b = 0 := sorry
example (a b : Rat) : a / b = 0 := sorry
example (s : Real) : sSup s = 0 := sorry

would all complain, but

example (a b : Nat) (hba : b ≤ a) : a - b = 0 := sorry
example (a b : Nat) (hba : b ∣ a) (hb : b ≠ 0) : a / b = 0 := sorry
example (a b : Int) (hba : b ∣ a) (hb : b ≠ 0) : a / b = 0 := sorry
example (a b : Rat) (hb : b ≠ 0) : a / b = 0 := sorry
example (s : Real) (hs₀ : s.Nonempty) (hs₁ : BddAbove s) : sSup s = 0 := sorry
example (s : ENNReal) : sSup s = 0 := sorry

would not

I feel this is the correct way.

[Eric Wieser]

Kyle Miller said:

(I'm sure this could be more elegantly done!)

docs#Nat.mul_self_sub_mul_self_eq

[Eric Wieser]

@Yaël Dillies, how does this generalization look to you?

import Mathlib.Algebra.Order.Ring.Canonical
import Mathlib.Algebra.Order.Ring.Nat

theorem mul_self_tsub_mul_self_eq' {α}
    [CanonicallyOrderedCommSemiring α] [Sub α] [OrderedSub α] [ExistsAddOfLE α]
    [CovariantClass α α (· + ·) (· ≤ ·)]
    [ContravariantClass α α (· + ·) (· ≤ ·)]
    [@IsTotal α (· ≤ ·)] (a b : α) :
    a * a - b * b = (a - b) * (a + b) := by
  obtain h | h := @IsTotal.total _ (· ≤ ·) _ b a
  · simp [tsub_mul, mul_add]
    rw [← add_tsub_assoc_of_le]
    swap; apply mul_le_mul_right' h
    rw [mul_comm b a, tsub_add_cancel_of_le]
    apply mul_le_mul_left' h
  · have : a - b = 0 := tsub_eq_zero_of_le h
    rw [this]
    have : a*a - b*b = 0 := tsub_eq_zero_of_le (mul_le_mul' h h)
    rw [this]
    simp

[Eric Wieser]

It works for Nat(and presumably NNRat and NNReal), but the typeclasses feel pretty stupid

[Yaël Dillies]

I think there is a much better proof (with probably fewer typeclasses, in particular no Canonical...) if you substitute a = b + c or b = a + c after the obtain h | h := total_of (· ≤ ·) b a

[Yaël Dillies]

That's the usual trick I play to prove things about canonical semirings and rings simultaneously

[Eric Wieser]

This is at least much shorter:

theorem mul_self_tsub_mul_self_eq {α}
    [CanonicallyOrderedCommSemiring α] [Sub α] [OrderedSub α]
    [ContravariantClass α α (· + ·) (· ≤ ·)]
    [@IsTotal α (· ≤ ·)] (a b : α) :
    a * a - b * b = (a + b) * (a - b) := by
  rw [mul_tsub, add_mul, add_mul, tsub_add_eq_tsub_tsub, mul_comm b a, add_tsub_cancel_right]

[Eric Wieser]

(and matches the generality of mul_tsub)

[Eric Wieser]

#15494

[Eric Wieser]

If anyone is looking for a small challenge, geom_sum₂_mul can likely be stated in this generality too