integer subtraction / rational division

Stream: new members

[Miroslav Olšák]

Can I allocate some special symbols for the "non-standard" subtraction in natural numbers, or integer division, and interpret the symbols / and - in "the standard way", even though it may cause requiring a richer structure? A similar behavioral change was done from Python 2 to Python 3. Now, I am trying to prove something like a / b = 2^(c-d) where a, b, c, d originate from natural numbers (cardinalities of finite sets), and it is challenging to even understand how Lean understands it.
For broader context, the relevant lemma I wanted to prove is:

example (M N D n k : ℕ) (h1 : N * 2^k = D) (h2 : M * 2^k = D)
  (non_triv : M > 0) (nk_le n ≤ k)
  : (N : ℚ) / M = 2^(k-n)
:=

It is related to problem C4 from http://imo-official.org/problems/IMO2008SL.pdf

[Kenny Lau]

write a * 2^d = b * 2^c

[Miroslav Olšák]

well, yes, but that is not the statement of the original problem

[Miroslav Olšák]

the original IMO problem is about determining the ratio a / b

[Miroslav Olšák]

So I am basically asking, how to translate the solution a * 2^d = b * 2^c, to the "required" form.

[Miroslav Olšák]

And I believe that standard behavior of - and / would help.

[Kenny Lau]

import data.rat tactic.norm_cast

example (M N D n k : ℕ) (h1 : N * 2^n = D) (h2 : M * 2^k = D)
  (non_triv : M > 0) (nk_le : n ≤ k) :
  (N / M : ℚ) = 2^(k-n) :=
begin
  rw div_eq_iff_mul_eq,
  rw ← domain.mul_left_inj (ne_of_gt $ pow_pos two_pos n : (2^n : ℚ) ≠ 0),
  rw [← mul_assoc, ← pow_add, nat.add_sub_cancel' nk_le],
  rw mul_comm at h1 h2,
  exact_mod_cast h2.trans h1.symm,
  exact_mod_cast ne_of_gt non_triv
end

[Miroslav Olšák]

Thank you for the proof.

[Kevin Buzzard]

You can't change the horrible uses of these symbols because they're already standard. We just have to live with them as mathematicians

[Miroslav Olšák]

Hm... Python did it.

[Kevin Buzzard]

Remember you can always cast. If you really want to work with subtraction you can use integers and if you really want to worth with division you can use rationale

[Miroslav Olšák]

Maybe some future version of Lean will manage it as well.

[Kevin Buzzard]

Python is just one programming language. This subtraction nonsense has permeated loads of the theorem prover languages

[Miroslav Olšák]

I have meant the division.

[Kevin Buzzard]

I would happily vote for a change but the CS people like trolling us. Why not have this conversation in #general? I will be right behind you

[Miroslav Olšák]

OK :-)

[Miroslav Olšák]

By the way, another question: Why

import data.rat.basic
#eval (2/3 : ℚ) ^ (-1 : ℤ)

fails, and

import data.real.basic
#eval (2/3 : ℚ) ^ (-1 : ℤ)

succeeds?

[Kevin Buzzard]

One of them probably imports algebra.group_power

[Kevin Buzzard]

And the other doesn't

[Kevin Buzzard]

Powers are only defined for naturals in core

[Miroslav Olšák]

import data.rat.basic
import algebra.group_power
#eval (2/3 : ℚ) ^ (-1 : ℤ)

still does not work.

[Kevin Buzzard]

Well I'm not at a computer but I can tell you how to debug this yourself

[Kevin Buzzard]

def X := $(2/3)^(-1)$ in a situation where it works

[Kevin Buzzard]

And then #print X and we can try and figure out what function lean is using to do the power

[Miroslav Olšák]

It says

4:1: def X : ℚ :=
(2 / 3) ^ -1

[Miroslav Olšák]

Not much helpful...

[Miroslav Olšák]

I have got it, import algebra.field_power, by following the source code.

[Kevin Buzzard]

OK great. Here's how to solve it my way: set_option pp.all true and then #print X again

[Mario Carneiro]

Miroslav Olšák said:

Hm... Python did it.

Python is also a dynamically typed language

[Kevin Buzzard]

and then we see that the exact term for ^ is @has_pow.pow.{0 0} rat int (@int.has_pow.{0} rat rat.division_ring)

[Miroslav Olšák]

I know. On the other hand, Lean has a strong inference system that also often disquise the types from the user.

[Mario Carneiro]

If you want to have subtraction in a "richer structure", then write (x - y : int) where x,y : nat

[Kevin Buzzard]

Yes, as a mathematician, you simply shouldn't be using these functions, not complaining that their notation is confusing.

[Kevin Buzzard]

I figure I'll just let the CS people do what they like

[Mario Carneiro]

But if you have to pass a subtraction to a function, as a nat, then nat subtraction is much better than any other option

[Kevin Buzzard]

and now #check int.has_pow which is the underlying function it's using

[Kevin Buzzard]

and peeking the definition does indeed indicate that it's defined in algebra.field_power

[Mario Carneiro]

If subtraction had type nat -> nat -> int then this wouldn't solve the problem of when the subtraction is actually a nat in the case of interest, and for typing reasons you need it to have type nat, so you have to cast it back with some ugly thing like to_nat... and now you've reinvented nat subtraction

[Kevin Buzzard]

The other part of @has_pow.pow.{0 0} rat int (@int.has_pow.{0} rat rat.division_ring) is the proof that the rationals are a division ring.

[Patrick Massot]

Miroslav, Mario's (x-y : int) trick is very important to understand because it relies on a very counter-intuitive Lean behavior which sometimes throws me off, even after more than two years of Lean. When you write (x - y : int) Lean does not "compute" x - y and then convert to int (which wouldn't solve your problem). It sees int and then infers that - should be an operation returning an int, which forces x and y to have type int, hence Lean inserts the coercion.

[Mario Carneiro]

I write C code sometimes and the coercion behavior is the other way around, it throws me off going back and forth

[Patrick Massot]

You can play with #eval (2 - 3 : int) (inserting coercions in various places).

[Mario Carneiro]

If in doubt, write (\u x - \u y : int)

[Mario Carneiro]

or (\u(x-y) : int)

[Miroslav Olšák]

Kevin Buzzard said:

Yes, as a mathematician, you simply shouldn't be using these functions, not complaining that their notation is confusing.

I don't understand. What do you mean by it? What functions should I not use?

[Mario Carneiro]

nat subtraction, that is, x - y : nat where x,y:nat

[Mario Carneiro]

when you write (x - y : int), the subtraction there has type int -> int -> int. It's a completely different function and a much more well behaved one

[Mario Carneiro]

However I disagree that you should avoid it completely. nat subtraction should be understood as a "totalized partial function", like division on reals or the sum of an infinite series or any number of other things. It returns garbage sometimes so you need to always be able to prove that you are not in the bad case when using it. This is somewhat of a pain, so if there are alternative formulations that avoid it they are probably preferable, but it's not the end of the world either

[Miroslav Olšák]

That is all nice, but how am I supposed to see what function is used in 2^(k-n), or even 2^(k-n) : ℚ -- that it is probably the wrong subtraction function?

[Miroslav Olšák]

And Mario, how do you perceive a / b : int? As rounded division, or as totalized partial function that returns garbage if the two integers are not divisible?

[Mario Carneiro]

The subtraction function always has the same output type as input type, A -> A -> A. Lean will never insert coercions unless it has to to avoid a type mismatch. In this case, k and n are nat and ^ is generic so it provides no hint about the type it is expecting in the input, so lean lets it be k - n : nat, finds the instance ^ : A -> nat -> A, and goes with that

[Mario Carneiro]

Actually the "totalized partial function" is not an all or nothing business. We have tried to make the "garbage" values as useful as possible given the constraints, so they may be less garbage-like depending on the application. Nat subtraction, for instance, returns 0 when the subtraction is out of bounds. One nice consequence of this is that it puts nat subtraction in an adjunction with addition, a - b <= c <-> a <= b + c, while some other garbage value like 37 wouldn't satisfy that.

[Kevin Buzzard]

Miroslav there is an algorithm for working out the type of everything and if you use set_option pp.all true you can figure it out

[Kevin Buzzard]

So the justification of natural subtraction is that it is an adjoint functor

[Kevin Buzzard]

Or you can just look at where the coercions are happening

[Mario Carneiro]

There is a similar adjunction for int division

[Patrick Massot]

All this is very nice, but it doesn't hide the fact that we currently don't have a good solution to handle numbers in a proof assistant. Things are simply broken, and the only thing we can explain is why it's difficult to fix them while keeping other things that we do like.

[Patrick Massot]

I know Mario knows this, I'm being explicit for Miroslav.

[Miroslav Olšák]

And couldn't just the rational division / integer subtraction be chosen as the default, with possible forcing of the rounded functions by the external typing? So that 1/2 = 2/3 would be false, whereas (1/2 : ℤ) = (2/3 : ℤ)would be true?

[Miroslav Olšák]

But of course, I don't see into the coersion / overloading rules. As far as I know, it is a mess even in C++.

[Kevin Buzzard]

Having integer subtraction as the default on naturals is literally impossible

[Kevin Buzzard]

Look at the type of has_sub.sub

[Kevin Buzzard]

It has to return an element of the same type as those it eats

[Kevin Buzzard]

This is a design decision that can't really be changed

[Kevin Buzzard]

It's also the right design for int, rat, real, complex, and any ring

[Kevin Buzzard]

If you don't like subtraction on semirings, don't use it

[Kevin Buzzard]

We very rarely need it

[Kevin Buzzard]

The only convincing example I've ever seen in mathematics is when we differentiate X^n and even in this case you can split into zero and successor cases if you want

[Sebastien Gouezel]

Do you know how many ways you have to decompose an integer n as a sum i_1 + ... + i_k of positive integers (where k is not fixed)? The answer is 2^(n-1). This is proved by thinking of a decomposition of {0, ..., n-1} into blocks, and taking the leftmost point of each of your blocks but the first one. This gives you a bijection between the set of decompositions and finite subsets of {1, ..., n-1}, which have cardinality 2^(n-1). Fun fact: all this also works for n = 0(where subtraction is nat subtraction).

[Sebastien Gouezel]

And the proof of this (which I needed to prove that the composition of analytic functions is analytic, upcoming PR once #2197 is merged) never distinguishes between n = 0 and n > 0!

[Patrick Massot]

I never got my answer about #2197, but I can merge anyway if it's blocking you.

[Sebastien Gouezel]

Your question was not about #2197 but about preexisting files, right? I don't have a good answer, I can only say it follows the same design as in the file for the operator norm.

[Patrick Massot]

You don't know whether those norms lemmas are used directly in later files? Even in the operator norm case?

[Sebastien Gouezel]

I don't think they are (and a quick grep agrees with me). In the operator norm case, we are talking about the four lemmas op_norm_zero_iff, op_norm_add_le, op_norm_neg and op_norm_smul, which prove that the operator norm satisfies the usual properties of a norm. Then, the normed space instance is derived from these lemmas, and they become unnecessary as they are covered by general normed space properties. Still, the proofs of these lemmas depend on the previous lemmas, so it would not be obvious to give a direct proof of the instance (and in any case we say that in general it is good practice to split a big proof in smaller lemmas). The question is whether we should mark them as private. I don't really have an opinion on this.

[Patrick Massot]

Yes, the question was about making them private. This is a very general question that I think should have a least a general guiding principle. But that's not a good reason to postpone merging.

[Miroslav Olšák]

And if let's say, naturals didn't have has_sub and has_div, Lean still could not realize that a - b should be an integer and a / b should be a rational?

[Kenny Lau]

- is has_sub.sub

[Miroslav Olšák]

I understand, and if I deleted it?

[Miroslav Olšák]

from naturals

[Kevin Buzzard]

Then everything would break because this is a design decision

[Kevin Buzzard]

Core would break

[Kevin Buzzard]

- notation is tied to has_sub.sub

[Kevin Buzzard]

And natural subtraction is used all over the place in parts of core that a mathematician has no interest in looking at but which make all the tactics work

[Kevin Buzzard]

I should say that this is just a conjecture

[Kevin Buzzard]

But if they didn't need natural subtraction it probably wouldn't be in core

[Kevin Buzzard]

I guess here is how to refactor

[Kevin Buzzard]

First change core so that the notation for has_sub.sub is some weird minus sign with a warning symbol above it

[Kevin Buzzard]

Then define a new notational typeclass for - and let it go from A x A to B. We can think of this as mathematician's subtraction

[Kevin Buzzard]

And now for rings you use this notation instead with B=A

[Kevin Buzzard]

And for nat you let it take values in int

[Kevin Buzzard]

But it wouldn't be long before you started regretting it

[Kevin Buzzard]

Because then you'll end up with goals where you think you've proved naturals a and b are equal but you've only proved that integers a and b are equal

[Kevin Buzzard]

And you'll have to apply the norm_cast tactic to fix things up which is a pain if you're writing a term mode proof

[Kevin Buzzard]

And will slow down your code immensely

[Kevin Buzzard]

I am sticking with my original assertion. If you do want to use negative numbers when why are you using nats in the first place? I have a student working on a dots and boxes project and she's using ints even though everything at the end is nonnegative and it hasn't caused any problems at all

[Kevin Buzzard]

And if you don't want to use them then just avoid subtraction by rephrasing in terms of addition

[Miroslav Olšák]

I understand that everything would break now :-). I was just curious whether the refactor would be hypotetically possible. I would imagine using other symbol for natural subtraction, and integer division (for example a \ b and a ÷ b). But I would need Lean to trigger the integer subtraction, whenever I write a - b for a, b naturals. The question is whether the typing system would allow such behavior.
I am not doing it, I am just asking, it could help me with understanding insides of Lean. We can discuss on whether it would be a good idea later, now I just want to understand whether it is a possibility.

[Kevin Buzzard]

What Lean does when it sees a-b depends simply on the definition of the notation -

[Kevin Buzzard]

Currently that notation is used in 1000 places in mathlib and is hard wired to mean something of type X to X to X

[Kevin Buzzard]

You can redefine it to go from X to X to Y and then fix 1000 errors

[Kevin Buzzard]

And then it'll work fine except that you'll find that it's really annoying

[Kevin Buzzard]

Because you don't want the types of your objects changing when you apply fundamental operations to them

[Kevin Buzzard]

I think that your idea of a subtraction operation from nat x nat to int is just as unnatural as leans design decision

[Kevin Buzzard]

If you want to subtract naturals you should be using integers from the beginning

[Miroslav Olšák]

Whether some idea is "natural" / "unnatural" is a subjective opinion, we apparently cannot resolve it here :-).
But my question was somewhat different, let's phrase it without naturals.
Let's say, I have a type α, and I would like to have a subtraction such that (x-y : β) for any x y : α. Would it be possible?

[Kevin Buzzard]

If you edit core lean, yes

[Kevin Buzzard]

Do you understand typeclass notation?

[Reid Barton]

It's not possible with the current definition of has_sub.sub and with - being notation for has_sub.sub. If you want to change everything, then anything is possible.

[Kevin Buzzard]

Look at the definition of - and then look at the definition of has_sub and then there you are at one of the first lean files lean ever reads when starting up and that's the line you have to change and it will break everything that comes later

[Miroslav Olšák]

I understand typeclasses just roughly. If I wrote (sub : α → α → β) in the core instead, and kept all the instances of has_sub as they are now, what would break?

[Mario Carneiro]

nothing. except all of core and mathlib

[Miroslav Olšák]

:D

[Mario Carneiro]

One issue with a subtraction function like that is that the type is not determined by the input

[Mario Carneiro]

if you write let z := x - y, lean has no idea what type z has, so it can't even find out if the subtraction typeclass exists

[Mario Carneiro]

so you would probably want beta to be an out_param, essentially saying that subtraction maps each type with a subtraction operation to a unique other type

[Miroslav Olšák]

I see, out_param like in is_mem.

[Mario Carneiro]

But this causes problems elsewhere. For example, assuming that this isn't just a hack to support nat specifically, we might want a generalized version of the construction, for example mapping any semiring R to a new type integral_closure R formed by taking formal subtractions of elements of R. But then we have a conflict because a ring is a semiring, so the subtraction on R would land in both R and integral_closure R (which is isomorphic to R)

[Kevin Buzzard]

Mario we have monoid localisation thanks to @Amelia Livingston :-)

[Miroslav Olšák]

Ring is a semiring? I thought there is just coercion to semiring.

[Mario Carneiro]

The type is the same, there is no coercion, but the typeclasses are in a parent relationship

[Miroslav Olšák]

OK, I think I understand why it is so problematic.

[Kevin Buzzard]

In 99% of use cases, if a and b have type R then you really want a-b to have type R. So you can see why they went for this design decision.

[Kevin Buzzard]

However there is clearly a dichotomy because there are loads of lemmas called things like sub_add_cancel or whatever, that have versions nat.sub_add_cancel, so the contentious design decision of using this notation for natural subtraction has caused problems down the line. However without editing any Lean you could define a new kind of subtraction sub' with a different notation which mapped nat x nat to int. But then you'd realise that it didn't really fix any of the problems because now you'll need nat.sub'_add_cancel as well, which will say that some integer equals a coercion to integer of some natural.