a rational number is positive iff its numerator is positive

Stream: general

[Kenny Lau]

do we have that?

[Johan Commelin]

So $\frac{-1}{-1}$ is not a positive rational number?

[Kenny Lau]

in rat the denominator is always positive

[Johan Commelin]

So $\frac{1}{-2}$ is not a rational number...

[Kenny Lau]

denominator

[Johan Commelin]

I find this disturbing...

[Kenny Lau]

theorem rat.num_pos_of_pos (r : rat) (H : r > 0) : (r.num : ℚ) > 0 :=
calc  (r.num : ℚ)
    = r.num / (r.denom:ℤ) * r.denom : eq.symm $ div_mul_cancel _ $ ne_of_gt $ nat.cast_pos.2 r.pos
... = r * r.denom : by rw [← rat.mk_eq_div, ← rat.num_denom r]
... > 0 : mul_pos H $ nat.cast_pos.2 r.pos

[Kenny Lau]

it's hard to prove anything about the rational numbers when I don't have enough lemmas...

[Johan Commelin]

Are you building an interface for \Q ?

[Kenny Lau]

I'm using Q

[Kenny Lau]

and I'm finding everything hard to prove

[Johan Commelin]

Ok, then we need an interface... because end-users shouldn't use r.num and r.denom, in my opinion.

[Kenny Lau]

well don't rationals have denominators...

[Johan Commelin]

Not really well-defined... I think

[Kenny Lau]

they are

[Johan Commelin]

Of course you can make choices

[Kenny Lau]

no choices required

[Johan Commelin]

Well, not morally well-defined

[Kenny Lau]

in Lean a rational number consists of a numerator in Z, denominator in N, proof that the denominator is positive, and proof that they are coprime

[Kenny Lau]

and I find that to be morally well-defined also

[Kenny Lau]

every rational number has a simplified form

[Johan Commelin]

Yes, but that should be hidden away as much as possible

[Johan Commelin]

I think

[Kenny Lau]

I need its denominator to prove that every rational number is smaller than some power of 2

[Kenny Lau]

in particular, 1/2^r.denom < r

[Johan Commelin]

Well, part of the interface could say that for every rational number r there exists an integer n with r < n

[Johan Commelin]

Or something like that.

[Kenny Lau]

aha that's existing

[Kenny Lau]

but I don't like it :P

[Reid Barton]

there's even a class for that

[Kenny Lau]

theorem lt_two_pow (n : nat) : n < 2 ^ n :=
nat.rec_on n dec_trivial $ λ n ih,
calc  n + 1
    < 2^n + 1   : nat.add_lt_add_right ih 1
... ≤ 2^n + 2^n : nat.add_le_add_left (nat.pow_le_pow_of_le_right dec_trivial $ nat.zero_le n) (2^n)
... = 2^n * 2   : eq.symm $ mul_two (2^n)
... = 2^(n+1)   : eq.symm $ nat.pow_succ 2 n

theorem rat.coe_pow (m n : nat) : (m : ℚ) ^ n = (m^n : ℕ) :=
nat.rec_on n rfl $ λ n ih, by simp [pow_succ', ih, nat.pow_succ]

theorem rat.num_pos_of_pos (r : rat) (H : r > 0) : r.num > 0 :=
int.cast_lt.1 $
calc  (r.num : ℚ)
    = r.num / (r.denom:ℤ) * r.denom : eq.symm $ div_mul_cancel _ $ ne_of_gt $ nat.cast_pos.2 r.pos
... = r * r.denom : by rw [← rat.mk_eq_div, ← rat.num_denom r]
... > 0 : mul_pos H $ nat.cast_pos.2 r.pos

theorem rat.one_le_num_of_pos (r : rat) (H : r > 0) : 1 ≤ (r.num : ℚ) :=
have H1 : ((0+1:ℤ):ℚ) = (1:ℚ), from rfl,
H1 ▸ int.cast_le.2 $ int.add_one_le_of_lt $ rat.num_pos_of_pos r H

theorem rat.lt (r : ℚ) (H : r > 0) : (1 / 2^r.denom : ℚ) < r :=
calc  (1 / 2^r.denom : ℚ)
    < 1 / r.denom : one_div_lt_one_div_of_lt (nat.cast_pos.2 r.pos)
  (trans_rel_left _ (nat.cast_lt.2 $ lt_two_pow _) (rat.coe_pow 2 _).symm)
... ≤ r.num / r.denom : div_le_div_of_le_of_pos (rat.one_le_num_of_pos r H) (nat.cast_pos.2 r.pos)
... = r.num / (r.denom:ℤ) : rfl
... = r : by rw [← rat.mk_eq_div, ← rat.num_denom r]

[Kenny Lau]

yay done

[Johan Commelin]

I just don't like the fact that if some computation spits out two integers, a and b, with b \ne 0, and I want to consider the rational number a/b, then Lean decides it also wants to put them in lowest terms.

[Johan Commelin]

That might be an immense computation

[Johan Commelin]

Or can it formally divide away the gcd, without actually calculating it?

[Kevin Buzzard]

Johan you should take a look at data/rat.lean in mathlib

[Kevin Buzzard]

I found that file not too intimidating

[Johan Commelin]

Will do

[Kevin Buzzard]

I would tell my students "of course a rational number is an equivalence class"

[Kevin Buzzard]

(because it's Z localised away from 0)

[Kevin Buzzard]

but in Lean working with equivalence classes is sometimes hard work

[Kevin Buzzard]

so if they can get away with it, they work with an inductive type

[Kevin Buzzard]

So they go with this structure of a numerator n in Z, a denominator d in N, a proof that d > 0 and a proof that n and d are coprime!

[Reid Barton]

If you don't reduce to lowest terms, then 1/2 + 1/2 + 1/2 + ... + 1/2 becomes an unwieldy computation

[Kevin Buzzard]

At this point you can't even make 6/8

[Kevin Buzzard]

but it's OK, they're only a few lines in

[Kevin Buzzard]

and then they go on to make other constructors

[Kevin Buzzard]

because they implemented Euclid already

[Kevin Buzzard]

so you finally get a definition of mk

[Kevin Buzzard]

on line 61

[Kevin Buzzard]

and they define / to be mk

[Johan Commelin]

Well, Lean can decide to reduce to lowest terms when I force it to actually compute something. But if I want to define $\frac{\pi(10^9)-1}{\pi(10^9+1)-1}$ where $\pi(n)$ is the $n$-th prime, that should be possible, right?

[Kevin Buzzard]

inductive structures with lots of things which are quite easy to carry around are very popular round here

[Johan Commelin]

It shouldn't actually start computing those primes.

[Kevin Buzzard]

If you want to actually work something complicated out then you should not be using Lean at this point

[Johan Commelin]

Also, I would want to have a proof that d = 0, all the time

[Reid Barton]

If you believe it won't start computing the primes, then why would it need to do the conversion to lowest terms?

[Johan Commelin]

But there they choose to just put n/0 = 0

[Kevin Buzzard]

n/0=0.

[Kevin Buzzard]

Mathematicians can often get upset about that.

[Kevin Buzzard]

but the issue is just notation

[Kevin Buzzard]

Just imagine you went through all the Lean source code replacing the notation / with something that looked more like $/^*$

[Kevin Buzzard]

and the asterisk indicates a footnote:

[Kevin Buzzard]

"Note to mathematicians: this is not your divide. This is just notation for a different function which we invented because we find it more useful."

[Johan Commelin]

If you want to actually work something complicated out then you should not be using Lean at this point

Says the person who is formalising schemes... :rolling_on_the_floor_laughing:

[Kevin Buzzard]

because whenever a mathematician writes the symbol /

[Kevin Buzzard]

they are doing that thing that mathematicians love to do -- they are making a promise.

[Johan Commelin]

Lol

[Kevin Buzzard]

They are saying "I promise that the denominator is not zero."

[Johan Commelin]

Yeah, ok... I'll try to forget some of my home culture.

[Kevin Buzzard]

but if you really make them keep their promises

[Kevin Buzzard]

then that means that they have to supply a proof.

[Kevin Buzzard]

And that is your input which you as a mathematician enter into /

[Kevin Buzzard]

and that's exactly the data needed to work out /*

[Kevin Buzzard]

with a guarantee that it's equal to /

[Johan Commelin]

Fair enough

[Kevin Buzzard]

Mathematicans are full of promises.

[Kevin Buzzard]

A is a hypergeometric schemeoid

[Kevin Buzzard]

and B is a set that bijects with A

[Kevin Buzzard]

therefore B is a hypergeometric schemeoid.

[Kevin Buzzard]

That statement comes with a promise. I had not realised this until very recently.

[Kevin Buzzard]

The promise is: "I promise that the definition of a hypergeometric schemeoid structure on a set A does not involve actually looking at any of A's elements"

[Kevin Buzzard]

"it just involves things like structures of multiplication and addition on A

[Kevin Buzzard]

You don't have to rely on A having an element containing an element containing the empty set in the definition -- but such a condition is a completely valid thing to say in ZFC.

[Johan Commelin]

Yup...

[Kevin Buzzard]

So when you make that transport of structure you are making a promise

[Kevin Buzzard]

and mathematicians have kind of forgotten this, because it's just part of the culture.

[Johan Commelin]

And lately we have more or less been working under that promise all the time... to never actually look at the elements of our sets.

[Johan Commelin]

Our objects may have an element "3", but we don't actually care what that element "3" looks like. As long as it behaves like a "3"

[Kevin Buzzard]

There are certain things we _can_ do to sets, but we choose not to do. If G is a group, I don't care about the underlying set, I just care about one special element of G with the _name_ "identity" -- I don't care which set it is -- and the inversion and multiplication.

[Chris Hughes]

pow_unbounded_of_gt_one in algebra.archimedean sounds like what you want.

[Kevin Buzzard]

And I would be really interested in formalising the notion of what we as mathematicians consider decent things to do to types. Exactly what can mathematicians do to mathematical objects?

[Johan Commelin]

Agreed. (But we are stealing Kenny's thread...) Chris subtly reminded me of that (-;

[Mario Carneiro]

I just don't like the fact that if some computation spits out two integers, a and b, with b \ne 0, and I want to consider the rational number a/b, then Lean decides it also wants to put them in lowest terms. That might be an immense computation

The runtime for doing this is not much more than multiplication of rationals to begin with, so I think it's a reasonable cost given you are doing a division. As Reid says, the alternative is much worse, unnormalized rationals have exponentially worse runtime in some situations.

Well, Lean can decide to reduce to lowest terms when I force it to actually compute something. But if I want to define $\frac{\pi(10^9)-1}{\pi(10^9+1)-1}$ where $\pi(n)$ is the $n$-th prime, that should be possible, right?

If you say def x : rat := pi bla bla... then nothing is computed up front, but x is computed when you use it in a program which is #eval'd. In particular, Lean uses an eager evaluation semantics, so in fact pi(10^9) will be calculated regardless of whether rationals are defined as a quotient or as reduced fractions. (This isn't Haskell!) The only way to avoid the calculation at this stage is to have / be some sort of thunk-taking operation so as to defer evaluation of its arguments, but it is not at all obvious that these "lazy rats" are the intended usual use of rational numbers.

[Johan Commelin]

Ok, understood. Somehow laziness feels natural to me. But I don't have that much experience actually. If at some point I need it, then I'll bring it up again (-;

[Reid Barton]

The point I was (too obliquely) trying to make before is that if Lean were lazy, then it would presumably have no reason to do the GCD computation, either