a - b = a + -b for ℂ, ℝ, ℚ and ℤ

Stream: new members

[Isak Colboubrani]

Given $a-b := a+(-b)$ I naïvely expected the following examples to be true by definition (i.e. definitionally equal) for $\mathbb{C}$, $\mathbb{R}$, $\mathbb{Q}$ and $\mathbb{Z}$.

Is my expectation unfounded? What detail might I be overlooking?

#mwe

import Mathlib

example (a b : ℂ) : a - b = a + -b := by rfl
example (a b : ℝ) : a - b = a + -b := by rfl
example (a b : ℚ) : a - b = a + -b := by rfl
example (a b : ℤ) : a - b = a + -b := by rfl

[Etienne Marion]

It is docs#sub_eq_add_neg

[Etienne Marion]

Sorry I did not read the question :sweat_smile:

[Riccardo Brasca]

For rational numbers, for example, you can have a look at Rat.neg, that is the definition of negation.

[Riccardo Brasca]

And Rat.sub for the definition of subtraction.

[Isak Colboubrani]

I should add that the $\mathbb{C}$, $\mathbb{R}$, and $\mathbb{Z}$ examples work, but not the $\mathbb{Q}$ one.

I naïvely assumed—without looking at the implementation details—that it would either work for all of these examples or for none of them.

[Riccardo Brasca]

In general you should not worry too much about definitional equality. Sometimes it holds and sometimes it doesn't, for subtle reasons.

[Eric Wieser]

I think the reason these don't hold is because we mark things as irreducible, which explicitly asks for them not to hold

[Eric Wieser]

(as a performance optimization)

[Robin Arnez]

If you want to know exactly why: it uses something like a * d - c * b for subtraction and a * d + (-c) * b for addition of a negated value. (-c) * b turns out not to be definitionally equivalent to -(c * b) and thus the wholes are not definitionally equivalent. Because of these small things you should generally not rely on such definitional equalities and rather just use stuff like sub_eq_add_neg.

[Isak Colboubrani]

My question essentially is: why does the following work for $\mathbb{C}$, $\mathbb{R}$ and $\mathbb{Z}$, but not for $\mathbb{Q}$? What is unique about the $\mathbb{Q}$ case?

import Mathlib
example (a b : ℂ) : a - b = a + -b := by rfl -- Works
example (a b : ℝ) : a - b = a + -b := by rfl -- Works
example (a b : ℚ) : a - b = a + -b := by rfl -- Does not work
example (a b : ℤ) : a - b = a + -b := by rfl -- Works

Before testing these examples, I assumed that the solution would either work uniformly for all of them or fail uniformly. I also expected that, if a partial failure occurred, it would happen at a clear point in the inclusion hierarchy—impacting everything above or below that level—instead of affecting just one particular type in the middle.

Were those assumptions unfounded, or were they reasonable—with this scenario simply being an example of what software developers refer to as a "leaky abstraction"?

Out of curiosity, what would it take to make rfl work for the $\mathbb{Q}$ example as well (under the assumption that it was desirable)?

[spamegg]

Yes this could be viewed as a leaky abstraction.
If we look at the error it says that a - b and a + -b are not definitionally equivalent.

My guess is that this is a peculiarity of rationals, because there are too many ways to write the same rational: x/y and -x/-y, and also canceling common factors or not...

To make the representation unique, I believe a rational is usually defined as a pair of integers m/n where m,n are relatively prime, and n is positive. This is the crucial aspect, the denominator is required to be positive. So, negative rationals are: (negative integer) / (positive integer)

This way I can understand why a - b would not be definitionally equivalent to a + -b, because -b is going to have a different representation.

My understanding is that there are many non-uniform "oddities" in Mathlib that require "workarounds" like this.

[Kevin Buzzard]

@Isak Colboubrani as Riccardo pointed out, you can just answer the question of why it works in some cases and not others by chasing back to their definitions and observing that sometimes the equalities are definitional and sometimes they're not, and as you have already seen, it's pretty clear that the designers did not care about whether things happened to be definitionally equal or not. As a mathematician I regard definitional equality in this sort of situation as some kind of coincidence in the wiring which has nothing to do with the main aims of mathlib. To give another example, one of n+0 and 0+n is definitionally equal to n, the other isn't, and it doesn't matter to me which one is.

[Edward van de Meent]

You could have both be defeq, but your definition would be weird :upside_down:

[Kevin Buzzard]

How?

[Vlad Tsyrklevich]

Presumably

import Mathlib

abbrev myRat : Type := Int × Nat

def half : myRat := ⟨1, 2⟩
def one_quarter : myRat := ⟨1, 4⟩

def myRatAdd (l r : myRat) : myRat := ⟨l.1 * r.2 + r.1 * l.2, l.2 * r.2⟩
instance : Add myRat where
  add := myRatAdd
def myRatNeg (r : myRat) : myRat := ⟨-r.1, r.2⟩
instance : Neg myRat where
  neg := myRatNeg
def myRatSub (l r : myRat) : myRat := l + (myRatNeg r)
instance : Sub myRat where
  sub := myRatSub

#eval half + one_quarter
#eval half - one_quarter

example (a b : myRat) : a - b = a + -b := by rfl

Though now equality requires reducing fractions.

[Kevin Buzzard]

Oh sorry, my question was about how 0+n and n+0 could both be rfl for naturals. I'm not sure that this is possible, however weird you make the definition

[Vlad Tsyrklevich]

Ah yes, that's obvious now that I re-read it.

[Philippe Duchon]

Kevin Buzzard said:

Oh sorry, my question was about how 0+n and n+0 could both be rfl for naturals. I'm not sure that this is possible, however weird you make the definition

That would require defining 0+0 twice, would it not? you should be able to define n+0 to be 0 and 0+ succ n to be succ n, but then 0+n = n would not be rfl - you'd have to do a case analysis on n, and both cases would be rfl.

Or is there a way to tell Lean something like "it looks like I'm defining this twice, but look, both definitions agree"?

[Ruben Van de Velde]

I think this is getting into somewhat obscure territory just to avoid the answer "it doesn't matter mathematically which one is the definition"

[Edward van de Meent]

you're right, lean doesn't like the double 0 + 0 definition

@[reducible]
def add' (m n : Nat) : Nat := match m, n with
  | 0, n' => n'
  | m', 0 => m'
  | m' + 1, n' + 1 => (add' m' n') + 2

example {m : Nat} : add' 0 m = m := by
  rw [add']

example {m : Nat} : add' m 0 = m := by
  rw [add'] -- huh, weird. rewriting gives an unsolvable goal, even tho it's true.

[Aaron Liu]

For this you probably need cases on m.

[Aaron Liu]

@[reducible]
def add' (m n : Nat) : Nat := match m, n with
  | 0, n' => n'
  | m', 0 => m'
  | m' + 1, n' + 1 => (add' m' n') + 2

example {m : Nat} : add' m 0 = m := by
  -- rfl fails here
  cases m with
  | zero => rfl
  | succ => rfl

[Edward van de Meent]

yea, i figured

[Isak Colboubrani]

Thank you for all your helpful comments—I’ve learned a great deal.

I now understand that certain implementation details cause things to behave less uniformly than I had naively expected for this particular inclusion chain. I feel confident enough in my understanding to explain to a fellow mathematics student why this "discrepancy" isn’t an issue (if they were to see it as one).

I have a follow-up question: if rfl isn’t the "weakest" tactic that solves all four examples, what is the "weakest" tactic that handles them all?

import Mathlib
example (a b : ℂ) : a - b = a + -b := by rfl -- Works
example (a b : ℝ) : a - b = a + -b := by rfl -- Works
example (a b : ℚ) : a - b = a + -b := by rfl -- Does not work
example (a b : ℤ) : a - b = a + -b := by rfl -- Works

[Robin Arnez]

ring works but the "weakest" tactic would be exact sub_eq_add_neg .. or rw [sub_eq_add_neg].

[Isak Colboubrani]

@Robin Arnez Oh, sorry—I meant the "weakest" tactic that needs no arguments. I should have clarified that.

[Robin Arnez]

oh, abel also works in this case and I'm pretty sure that's simpler

[Isak Colboubrani]

@Robin Arnez I performed a brute-force search and identified the following zero-argument tactics that work for all four cases ($\mathbb{C}$, $\mathbb{R}$, $\mathbb{Q}$, and $\mathbb{Z}$):

import Mathlib
example (a b : ℚ) : a - b = a + -b := by abel
example (a b : ℚ) : a - b = a + -b := by bound
example (a b : ℚ) : a - b = a + -b := by exact?
example (a b : ℚ) : a - b = a + -b := by group
example (a b : ℚ) : a - b = a + -b := by hint
example (a b : ℚ) : a - b = a + -b := by module
example (a b : ℚ) : a - b = a + -b := by noncomm_ring
example (a b : ℚ) : a - b = a + -b := by polyrith
example (a b : ℚ) : a - b = a + -b := by reduce_mod_char
example (a b : ℚ) : a - b = a + -b := by ring
example (a b : ℚ) : a - b = a + -b := by ring_nf
example (a b : ℚ) : a - b = a + -b := by rw?
example (a b : ℚ) : a - b = a + -b := by rw_search

[Isak Colboubrani]

I understand why most of these tactics solve this goal (as noted above rfl doesn't handle the $\mathbb{Q}$ case), but bound, module and reduce_mod_char surprised me somewhat. Since these three tactics are new to me, I'm not sure if this surprise is warranted or if it's simply a reflection of their underlying design.

When debugging a case like this, is there a more straightforward way to understand how a tactic is solving a particular goal rather than having to dig into its source code? Specifically, I'm curious whether these three tactics internally call any of the other tactics mentioned above, or if they use their own independent logic to close the goal.

For instance, even though bound is built on top of aesop, it seems that aesop by itself wouldn’t close this goal.

[Ruben Van de Velde]

bound actually uses linarith under the hood as well, and that's what solves this goal (though it is significantly overpowered for it)

[Ruben Van de Velde]

module seems to use ring

[Ruben Van de Velde]

reduce_mod_char explicitly marks sub_eq_add_neg as a lemma to use

[Ruben Van de Velde]

All of them seem to come down to "let's deal with basic arithmetic to maximize the number of goals we can solve"

[Isak Colboubrani]

Are you sure the bound success is solely thanks to linarith?

bound can solve the ℂ case, which linarith cannot handle:

import Mathlib
example (a b : ℂ) : a - b = a + -b := by bound -- Works
example (a b : ℂ) : a - b = a + -b := by linarith -- Does not work

[Ruben Van de Velde]

For \Q, yeah. In the case of \C, it uses rfl

[Isak Colboubrani]

Ah, I see! That makes perfect sense—thank you!

[Ruben Van de Velde]

Some sense, at least. Not sure about "perfect" :)

[Isak Colboubrani]

Out of curiosity, did you examine the source code for these findings, or is there a simpler way to debug the inner workings of a tactic in situations like this?

[Ruben Van de Velde]

If you write by? rather than by, lean shows the term mode proof that the tactic generated

[Isak Colboubrani]

TIL. Nice! Something like by? was exactly what I was looking for. It's nice to have a way to see which tactics that do the heavy lifting and those that primarily delegate to others.