Zulip Chat Archive

Stream: general

Topic: a rational number is positive iff its numerator is positive


view this post on Zulip Kenny Lau (Apr 30 2018 at 18:22):

do we have that?

view this post on Zulip Johan Commelin (Apr 30 2018 at 18:29):

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

view this post on Zulip Kenny Lau (Apr 30 2018 at 18:29):

in rat the denominator is always positive

view this post on Zulip Johan Commelin (Apr 30 2018 at 18:30):

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

view this post on Zulip Kenny Lau (Apr 30 2018 at 18:30):

denominator

view this post on Zulip Johan Commelin (Apr 30 2018 at 18:31):

I find this disturbing...

view this post on Zulip Kenny Lau (Apr 30 2018 at 18:34):

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

view this post on Zulip Kenny Lau (Apr 30 2018 at 18:34):

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

view this post on Zulip Johan Commelin (Apr 30 2018 at 18:36):

Are you building an interface for \Q ?

view this post on Zulip Kenny Lau (Apr 30 2018 at 18:36):

I'm using Q

view this post on Zulip Kenny Lau (Apr 30 2018 at 18:36):

and I'm finding everything hard to prove

view this post on Zulip Johan Commelin (Apr 30 2018 at 18:37):

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

view this post on Zulip Kenny Lau (Apr 30 2018 at 18:37):

well don't rationals have denominators...

view this post on Zulip Johan Commelin (Apr 30 2018 at 18:38):

Not really well-defined... I think

view this post on Zulip Kenny Lau (Apr 30 2018 at 18:38):

they are

view this post on Zulip Johan Commelin (Apr 30 2018 at 18:38):

Of course you can make choices

view this post on Zulip Kenny Lau (Apr 30 2018 at 18:38):

no choices required

view this post on Zulip Johan Commelin (Apr 30 2018 at 18:38):

Well, not morally well-defined

view this post on Zulip Kenny Lau (Apr 30 2018 at 18:38):

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

view this post on Zulip Kenny Lau (Apr 30 2018 at 18:39):

and I find that to be morally well-defined also

view this post on Zulip Kenny Lau (Apr 30 2018 at 18:39):

every rational number has a simplified form

view this post on Zulip Johan Commelin (Apr 30 2018 at 18:40):

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

view this post on Zulip Johan Commelin (Apr 30 2018 at 18:40):

I think

view this post on Zulip Kenny Lau (Apr 30 2018 at 18:40):

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

view this post on Zulip Kenny Lau (Apr 30 2018 at 18:40):

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

view this post on Zulip Johan Commelin (Apr 30 2018 at 18:41):

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

view this post on Zulip Johan Commelin (Apr 30 2018 at 18:41):

Or something like that.

view this post on Zulip Kenny Lau (Apr 30 2018 at 18:42):

aha that's existing

view this post on Zulip Kenny Lau (Apr 30 2018 at 18:42):

but I don't like it :P

view this post on Zulip Reid Barton (Apr 30 2018 at 18:42):

there's even a class for that

view this post on Zulip Kenny Lau (Apr 30 2018 at 18:46):

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]

view this post on Zulip Kenny Lau (Apr 30 2018 at 18:46):

yay done

view this post on Zulip Johan Commelin (Apr 30 2018 at 18:47):

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.

view this post on Zulip Johan Commelin (Apr 30 2018 at 18:47):

That might be an immense computation

view this post on Zulip Johan Commelin (Apr 30 2018 at 18:47):

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

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 18:49):

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

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 18:49):

I found that file not too intimidating

view this post on Zulip Johan Commelin (Apr 30 2018 at 18:49):

Will do

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 18:50):

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

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 18:50):

(because it's Z localised away from 0)

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 18:50):

but in Lean working with equivalence classes is sometimes hard work

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 18:50):

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

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 18:52):

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!

view this post on Zulip Reid Barton (Apr 30 2018 at 18:52):

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

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 18:52):

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

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 18:52):

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

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 18:52):

and then they go on to make other constructors

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 18:53):

because they implemented Euclid already

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 18:54):

so you finally get a definition of mk

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 18:54):

on line 61

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 18:54):

and they define / to be mk

view this post on Zulip Johan Commelin (Apr 30 2018 at 18:54):

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

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 18:55):

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

view this post on Zulip Johan Commelin (Apr 30 2018 at 18:55):

It shouldn't actually start computing those primes.

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 18:55):

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

view this post on Zulip Johan Commelin (Apr 30 2018 at 18:55):

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

view this post on Zulip Reid Barton (Apr 30 2018 at 18:55):

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

view this post on Zulip Johan Commelin (Apr 30 2018 at 18:56):

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

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 18:56):

n/0=0.

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 18:56):

Mathematicians can often get upset about that.

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 18:57):

but the issue is just notation

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 18:57):

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

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 18:58):

and the asterisk indicates a footnote:

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 18:58):

"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."

view this post on Zulip Johan Commelin (Apr 30 2018 at 18:58):

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:

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 18:59):

because whenever a mathematician writes the symbol /

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 18:59):

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

view this post on Zulip Johan Commelin (Apr 30 2018 at 18:59):

Lol

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 18:59):

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

view this post on Zulip Johan Commelin (Apr 30 2018 at 18:59):

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

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 18:59):

but if you really make them keep their promises

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 18:59):

then that means that they have to supply a proof.

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 19:00):

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

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 19:00):

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

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 19:00):

with a guarantee that it's equal to /

view this post on Zulip Johan Commelin (Apr 30 2018 at 19:00):

Fair enough

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 19:00):

Mathematicans are full of promises.

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 19:01):

A is a hypergeometric schemeoid

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 19:01):

and B is a set that bijects with A

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 19:01):

therefore B is a hypergeometric schemeoid.

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 19:01):

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

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 19:02):

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"

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 19:02):

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

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 19:03):

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.

view this post on Zulip Johan Commelin (Apr 30 2018 at 19:04):

Yup...

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 19:04):

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

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 19:04):

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

view this post on Zulip Johan Commelin (Apr 30 2018 at 19:05):

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.

view this post on Zulip Johan Commelin (Apr 30 2018 at 19:05):

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"

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 19:05):

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.

view this post on Zulip Chris Hughes (Apr 30 2018 at 19:07):

pow_unbounded_of_gt_one in algebra.archimedean sounds like what you want.

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 19:07):

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?

view this post on Zulip Johan Commelin (Apr 30 2018 at 19:08):

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

view this post on Zulip Mario Carneiro (May 01 2018 at 00:18):

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 π(109)1π(109+1)1\frac{\pi(10^9)-1}{\pi(10^9+1)-1} where π(n)\pi(n) is the nn-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.

view this post on Zulip Johan Commelin (May 01 2018 at 04:59):

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 (-;

view this post on Zulip Reid Barton (May 01 2018 at 05:04):

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


Last updated: May 16 2021 at 21:11 UTC