Mathematics in Lean - (-0) vs 0

Stream: new members

[VayusElytra]

Hi, I just had a quick question about this excerpt from chapter 2 of Mathematics in Lean (page 12):
image.png
the comment about this theorem is "we had to use the annotation (-0 : R) instead of 0 because without specifying R it is impossible for Lean to infer which 0 we have in mind, and by default it would be interpreted as a natural number."

I am not sure I quite understand what this means. We use 0 everywhere in other theorems without specifying which 0 we are talking about; for instance in a theorem right above:
image.png

My hunch is that in this other theorem, for instance, the type of 0 can be inferred from that of a and b; they're elements of some ring R, so Lean can identify on its own that this 0 must be the 0 from the ring, while in the first theorem, there's no way for it to make that inferrence. Is this correct?

[Julian Berman]

That's right, in the other example it's because Lean knows the type of the left side of the = sign so it therefore knows 0 on the right side also must be 0 : R.

[Julian Berman]

Whereas if you just have 0 = 0 or -0 = 0 then Lean has no information and therefore will conservatively assume that's an equality of natural numbers.

[VayusElytra]

Thank you! That makes complete sense.

[VayusElytra]

I'll write this here again since I am not sure what the etiquette is regarding opening new topics. I am slightly confused by this excerpt from Mathematics in Lean, page 12 again:

image.png

Q1) It seems to suggest that a - b = a + (-b) is not a definition in Lean's implementation of rings. This is very strange to me; I have only ever seen the symbol "-" in rings be defined by that equality. So how is it defined in Lean then?

Q2) The code below "On the real numbers, it is defined that way" is surely meant to bring attention to the fact that the "by" is not necessary here, but I'm unsure why. What does by actually do, and when is it necessary?

[Kevin Buzzard]

Is a group a set with a multiplication? Or is it a set with a multiplication and an inverse and an identity? There are lots of different ways to set up mathematical objects. In Lean, for reasons which are essentially not mathematical, a ring (and indeed also an additive group) by definition has a subtraction and a negation, and an axiom saying they're related in the usual way. It's "to avoid diamonds".

[Kevin Buzzard]

I think one message here is that mathematicians might want to optimise for as few definitions as possible, and then make the rest from what you have, and in general in Lean something like the exact opposite is true, because you get better definitional equalities that way.

[Kevin Buzzard]

Another message is that sub_eq_add_neg is a theorem, and as a user this should be all you care about -- whether it not is true by definition is a question for the people who are implementing rings, not something which the users need to worry about.

[Kevin Buzzard]

To give an example of why "is this true by definition" is not a good mathematical question: if n is a natural number then n+0=n is true by definition but 0+n=n is not.

[VayusElytra]

I know you are asking this rhetorically, but my answer would be that a group is a set with multiplication, inverse and identity, and stripping away inverse yields a monoid. Though of course, I understand the exact details of these definitions is not particularly relevant.

I think I understand what you are saying, though; there is a difference in approach between the mathematics in a textbook and their realisation in a formal proof language, since our priorities are not the same in either setting.

I also understand your point about

sub_eq_add_neg

but I do have to admit that I find not worrying about these kinds of details to be difficult to get used to...

[Kevin Buzzard]

My point is that with just the multiplication you can add axioms (rather than data) saying "there exists an inverse map" as opposed to making the inverse map part of the data: the inverse map is uniquely determined by the multiplication in a group so can be thought of as a fact about the multiplication. Whether you want axioms or data is a design decision, and in some sense not a mathematical question. Yes, writing a textbook and writing a mathematics library turn out to be different things. See Heather Macbeth's recent paper https://arxiv.org/abs/2405.04699 .

[VayusElytra]

Thank you, this was an enlightening read!

[Patrick Massot]

VayusElytra said:

I also understand your point about

sub_eq_add_neg

but I do have to admit that I find not worrying about these kinds of details to be difficult to get used to...

Maybe MIL is not clear, but you don’t have to worry about these kind of details.

[Daniel Weber]

Regarding your second question, the rfl in the first example is docs#rfl. It only applies for equality. In the second example rfl is a tactic, docs#Lean.Parser.Tactic.tacticRfl, which tries multiple reflexive tactics. For example, it also tries docs#Iff.rfl

[VayusElytra]

Thank you! That makes sense.

[VayusElytra]

Next question in line is from page 18, when trying to prove the goal min (a + c) (b + c) ≤ min a b + c.
My approach to this would be to rewrite min (a + c) (b + c) as min (a + c) (b + c) - c + c using rw [\l sub_add_cancel], but in practice this fails with the following error message:
image.png

The solution works around this by using a lemma:

  have h : min (a + c) (b + c) = min (a + c) (b + c) - c + c := by rw [sub_add_cancel]

My question: is there a way to make my original idea work directly, without needing to establish a lemma like this? In general I have been having somewhat of a hard time with rewrites where one needs to replace an implicit +0 by + a - a; what is the correct way to go about them?

[Richard Osborn]

If I understand correctly, rw [← sub_add_cancel (min (a + c) (b + c)) c] should work.

[Ruben Van de Velde]

As you've noticed, lean is better at simplifying terms than making them more complicated. I don't know what's already been explained in mil at this point, but generally I might use calc or trans to write out the complicated middle expression, and then you have two subgoals where you can simplify

[Kevin Buzzard]

@VayusElytra do you understand the error message? rw [\l sub_add_cancel] means "change something to something-x+x for some x" so Lean's response "which something? There are about ten in the goal" (a, a+c, min a b, ...) is not an unreasonable response

[VayusElytra]

I do understand (I think!). I was surprised because I know that when given an expression in which multiple somethings match the pattern, the rw tactic rewrites the first one as well as all remaining somethings with the same value for a, which is why only the (0+0)s get rewritten in this example from the NNG:
image.png

So I would've expected the rw [\l sub_add_cancel] here to rewrite something (the first occurence of a real number in the expression, perhaps). Though now that I am writing this, I realise this situation might be slightly different, since rw [\l sub_add_cancel] would also need to know what x to use in its rewrite.

Thank you all for answering, and apologies for asking what I could've figured out on my own

[Kevin Buzzard]

You're right, there seems to be a subtlety here which I've only just realised. rw seems to be checking specifically whether you have given it zero clues (ie you're literally asking it to rewrite a pattern represented by a bare metavariable) and bails early if so. With add_zero even if it can match ten times, it's having to match ?a + 0 so this check isn't triggering.

[VayusElytra]

Today a question about proof terms.
This example is from page 27 of mathematics in Lean:
image.png

If I understand properly: on the right side, we start by applying the hypothesis rsubs : r ⊆ s to the hypothesis xr : x ∈ r which yields x \in s. Then, we apply ssubt : s ⊆ t to that to obtain the desired result x ∈ t.
So what is the lambda abstraction on the left actually doing? I remember reading elsewhere that a property P1 implying some other property P2 can be formalized by saying that there exists a function mapping (elements of type) P1 to (elements of type) P2. Is this what the function we are trying to construct is doing?

I understand this question probably requires a lot of extra reading to answer properly, so please feel free to just point me in the direction of a book or paper to look into!

[Patrick Massot]

The lambda abstraction is doing what the intro tactic does. Does it help?

[Luigi Massacci]

#tpil has an explanation of proposition as types (including the notion of implications as functions, which is indeed what is happening there) and also how the forall quantifier works

[VayusElytra]

Thank you so much, that is exactly what I was looking for!

[VayusElytra]

Was curious about this solution to the first example on page 34 today.

image.png

After intro hh we arrive at a spot where we have two hypothesesh : ∀ ε > 0, x < ε and hh : x > 0. From trying on my end, at this point, linarith and linarith [h hh] both fail to solve the goal, but linarith [h _ hh] does. My questions:

1) Why does linarith fail to solve the goal here? In my understanding, linarith already tries to apply all available hypotheses, so we shouldn't have to specify that it should use h and hh.

2) My understanding as to why linarith [h hh] fails is that lean tries to interpret hh as a real number, which causes a type mismatch error. Why is h looking for a parameter when it is true for all epsilon?

[Kevin Buzzard]

I find it a bit jarring that we're talking about all manner of things in a thread called -(-0) vs 0. Threads are cheap; feel free to start a new one with each question!

1) linarith doesn't solve the goal because this would be scope creep. The moment you start asking linarith to instantiate forall statements with clever choices, you're asking it to do something which isn't in its remit.
2) h hh doesn't make sense because h is a function which first wants to eat a number, and then a proof that it's positive, and hh isn't a number.

[Ruben Van de Velde]

Does linarith eat errors like that in its argument? If so, we should fix that

[VayusElytra]

Noted! If that is appropriate etiquette, I will make new threads for new questions in the future.
Thank you for your answers, this makes complete sense.