Zulip Chat Archive

Stream: maths

Topic: The real numbers


view this post on Zulip Kevin Buzzard (May 30 2018 at 22:07):

How are our real numbers getting along? Do we have the definition of a differentiable function yet, and of its derivative?

view this post on Zulip Kenny Lau (May 30 2018 at 22:08):

one thing about analysis is that there are a lot of promises made

view this post on Zulip Kenny Lau (May 30 2018 at 22:08):

when we say the derivative of a function, we don't just mean the derivative of a function

view this post on Zulip Kenny Lau (May 30 2018 at 22:08):

we mean that it exists

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:11):

Do we have that the reals are the unique Dedekind-complete ordered field up to unique isomorphism?

view this post on Zulip Kenny Lau (May 30 2018 at 22:12):

is R[ε] Dedekind-complete?

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:12):

I was writing a chapter in my book on reals and I was trying to figure out the interface that a mathematician needed.

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:13):

I figure we need the uniqueness statement above, and the intermediate value theorem and the mean value theorem

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:13):

and I reckon we have then got a huge chunk of 1st year Imperial analysis

view this post on Zulip Andrew Ashworth (May 30 2018 at 22:13):

analysis is tricky, I took a long look at awhile back since I was interested in probability

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:13):

I could get students working on this over the summer but I don't have a clue about the current state of things and just thought it was easiest to ask

view this post on Zulip Kenny Lau (May 30 2018 at 22:13):

I already proved the IVT ^^

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:14):

Where Kenny?

view this post on Zulip Kenny Lau (May 30 2018 at 22:14):

in my own construction of the real numbers

view this post on Zulip Kenny Lau (May 30 2018 at 22:14):

https://github.com/kckennylau/Lean/blob/master/cauchy_real.lean#L1508

view this post on Zulip Andrew Ashworth (May 30 2018 at 22:15):

my plan for attacking it (which I eventually gave up on when I realized is was quite some work) was to follow the isabelle analysis theorems (many of them were written by johannes and jeremy avigad!)

view this post on Zulip Andrew Ashworth (May 30 2018 at 22:17):

well, you could just ask @Johannes Hölzl for his advice on what analysis developments to work on :)

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:18):

Kenny did you prove that your real numbers were the unique complete ordered field up to unique isomorphism?

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

no

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:18):

Is it in mathlib?

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

no idea

view this post on Zulip Andrew Ashworth (May 30 2018 at 22:21):

out of curiosity is there a good reference on filters around? I only know about the Cauchy sequence construction, but it seems I must know more to use the reals in mathlib...

view this post on Zulip Johannes Hölzl (May 30 2018 at 22:21):

@Andrew Ashworth most of Isabelle's analysis developed over some time. Starting from Fleuriot, over porting stuff from HOL Light by Amine Chaieb, and then generalizing it to type classes by Brian Huffman, Fabian Immler and me.

view this post on Zulip Johannes Hölzl (May 30 2018 at 22:22):

and a lot of other people

view this post on Zulip Johannes Hölzl (May 30 2018 at 22:22):

@Kevin Buzzard I don't think there is a uniqueness proof in mathlib

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:24):

@Andrew Ashworth Given a point in a space, you get a "filter" of sets on the space, namely the sets containing the point.

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:24):

So a filter is kind-of a generalization of a point

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:24):

it's a really cool way of saying "tends to +infinity" for example

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:24):

because even though infinity isn't a real number

view this post on Zulip Johannes Hölzl (May 30 2018 at 22:24):

@Andrew Ashworth do you know our filter paper http://home.in.tum.de/~hoelzl/documents/hoelzl2013typeclasses.pdf ? at least it explains how filters are used in Isabelle.

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:24):

the sets of reals that contain an open interval (r,infinity) is a filter

view this post on Zulip Johannes Hölzl (May 30 2018 at 22:25):

  • the sets of sets (r, infinite) over all r

view this post on Zulip Johannes Hölzl (May 30 2018 at 22:26):

the sets of all neighbourhoods around x forms a filter, all left neighbourhoods (and right neibourhoods) etc

view this post on Zulip Johannes Hölzl (May 30 2018 at 22:29):

but currently you need to do a lot of operations directly with filters, there is a lot of porcelian missing. Porcelain the sense that a lot the nice lemmas to show continuity of a function and using it are just not there yet. Many should be proved in a couple of lines but need to be written down.

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:30):

Am I right in thinking that @Mario Carneiro @Johannes Hölzl and @Kenny Lau -- that all of you wrote distinct definitions of real numbers recently?

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:30):

Each one of you should prove the fundamental theorem of real numbers

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:30):

that you are a Dedekind complete ordered field

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:31):

and the moment you do that you can access all the theorems proved about the other real numbers

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:31):

Did you all do that?

view this post on Zulip Mario Carneiro (May 30 2018 at 22:32):

Uniqueness is overrated

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:32):

rofl

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:32):

you people

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:32):

you don't understand equality

view this post on Zulip Mario Carneiro (May 30 2018 at 22:32):

It's really not needed for anything practical though

view this post on Zulip Mario Carneiro (May 30 2018 at 22:32):

in a sense it tells you you "got it right" but that's it

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:32):

it's needed for clear thinking

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:33):

and so we have to teach it to computers

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:33):

it makes the world a simpler place

view this post on Zulip Mario Carneiro (May 30 2018 at 22:33):

when you want to apply theorems about reals, you need to have theorems on (your) reals

view this post on Zulip Mario Carneiro (May 30 2018 at 22:33):

a uniqueness statement doesn't help here

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:34):

I just mean you can port theorems with the uniqueness statement

view this post on Zulip Mario Carneiro (May 30 2018 at 22:35):

yeah, that's a bad idea, avoid if you can help it

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:35):

I want to do more than port theorems

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:35):

I want to identify them as one

view this post on Zulip Mario Carneiro (May 30 2018 at 22:36):

Better to have a single definition and prove equivalent "views" of it

view this post on Zulip Kenny Lau (May 30 2018 at 22:36):

uniqueness theorem is a part of interface, because sometimes you would have more than one instance, because it's describing a class of objects (e.g. algebra homomorphism)

view this post on Zulip Kenny Lau (May 30 2018 at 22:36):

but in this case there is only one object that we call the real numbers

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:36):

I have so much to learn about the way you guys think about things.

view this post on Zulip Kenny Lau (May 30 2018 at 22:36):

we won't be constructing other real numbers

view this post on Zulip Kenny Lau (May 30 2018 at 22:36):

so I don't see why uniqueness is important

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:37):

What is the point of having three copies of the real numbers?

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:37):

Is one of them "the best one" or do they all have their merits or what?

view this post on Zulip Kenny Lau (May 30 2018 at 22:37):

i just did it for myself

view this post on Zulip Mario Carneiro (May 30 2018 at 22:37):

There's only one I'm aware of, unless Kenny did something

view this post on Zulip Kenny Lau (May 30 2018 at 22:37):

i did it privately

view this post on Zulip Mario Carneiro (May 30 2018 at 22:38):

There was an old construction by Johannes and I replaced it with my own

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:38):

I thought we had a filter one and a cauchy sequence one in mathlib at different times

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:38):

right

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:38):

and then Kenny's

view this post on Zulip Mario Carneiro (May 30 2018 at 22:38):

The filter construction is gone, although the theorems aren't

view this post on Zulip Kenny Lau (May 30 2018 at 22:38):

rip filter construction 2017-2018

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:39):

OK so Mario, let's say that in Johannes' construction of real numbers with filters, he proved that the real numbers were a Dedekind complete totally ordered field (he almost certainly did prove this, I believe I remember checking once).

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:39):

Then isn't that all you will ever need from the real numbers?

view this post on Zulip Mario Carneiro (May 30 2018 at 22:40):

Yes, and that theorem is still there

view this post on Zulip Kenny Lau (May 30 2018 at 22:40):

no, you need a way to construct real numbers

view this post on Zulip Kenny Lau (May 30 2018 at 22:40):

like sqrt(2)

view this post on Zulip Kenny Lau (May 30 2018 at 22:40):

and filters are hard to work with

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:40):

but if Johannes had made it to that pinnacle

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:40):

you would never need to think about filters any more

view this post on Zulip Kenny Lau (May 30 2018 at 22:40):

how would you make sqrt(2)?

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:40):

take the sup of the set of real whose square was less than 2

view this post on Zulip Mario Carneiro (May 30 2018 at 22:41):

My construction just slots in where the old one was, all the theorems still work after porting (with filters and everything)

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:41):

and then say that you're a complete field

view this post on Zulip Mario Carneiro (May 30 2018 at 22:41):

The abstract theorems like that exist, but that's still a far cry from the "algebraic" theory with say transcendental functions

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:42):

Chris did exp and sin and cos

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:42):

did that ever make it into mathlib?

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:42):

I need that for October!

view this post on Zulip Kenny Lau (May 30 2018 at 22:42):

it's still in PR i think

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:42):

If it needs work, let me know, that would be a great thing for students to work on

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:43):

I need e^(i theta) = cos(theta) + i sin(theta)

view this post on Zulip Kenny Lau (May 30 2018 at 22:43):

you're on the wrong thread then

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:43):

you mentioned R[e] earlier, this is R[i]

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:51):

https://math.stackexchange.com/questions/269353/isomorphism-of-dedekind-complete-ordered-fields

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:51):

The quote from Spivak

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:51):

[not the question itself]

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:51):

Is that proof, that any two complete ordered fields are isomorphic, in mathlib?

view this post on Zulip Kenny Lau (May 30 2018 at 22:52):

(removed)

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:52):

up to unique isomorphism

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:52):

they are _the same_

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:52):

they are equal

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:53):

they are maths-equivalent

view this post on Zulip Mario Carneiro (May 30 2018 at 22:56):

Having that theorem will just make you more frustrated when it isn't as powerful as you want

view this post on Zulip Reid Barton (May 30 2018 at 22:58):

Incidentally, in my limited experience, it's better not to work with any particular model of the reals directly, but just axiomatize the features that you need using type classes

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:59):

Don't prove a single theorem about the reals

view this post on Zulip Kevin Buzzard (May 30 2018 at 22:59):

just prove a theorem about complete totally ordered fields?

view this post on Zulip Reid Barton (May 30 2018 at 22:59):

I got frustrated when Lean would keep running out of memory when trying to check stuff like rfl : 2 * 1 = 1 + 1

view this post on Zulip Reid Barton (May 30 2018 at 23:00):

but then when I switched to working over a general totally ordered discrete topological whatever field, my compile times went way down

view this post on Zulip Kenny Lau (May 30 2018 at 23:00):

that one is mul_one :P

view this post on Zulip Kevin Buzzard (May 30 2018 at 23:00):

norm_num ftw

view this post on Zulip Reid Barton (May 30 2018 at 23:00):

I know, but it's hard to stop Lean from trying to reduce

view this post on Zulip Kenny Lau (May 30 2018 at 23:00):

2 is defined to be bit0 1, which is defined to be 1+1

view this post on Zulip Reid Barton (May 30 2018 at 23:00):

It means every time you use simp or something, you might fall into a memory leak

view this post on Zulip Mario Carneiro (May 30 2018 at 23:00):

but you still have to reduce (1+1)*1 = 1+1 there

view this post on Zulip Reid Barton (May 30 2018 at 23:00):

and then you have to back up and carefully walk around it

view this post on Zulip Reid Barton (May 30 2018 at 23:01):

Sure, and then norm_num can do that for you

view this post on Zulip Kenny Lau (May 30 2018 at 23:01):

so I said it's mul_one

view this post on Zulip Andrew Ashworth (May 30 2018 at 23:01):

I have wondered whether the reals should be a typeclass too, in case somebody wants to have a really efficient computable version at some point in the future

view this post on Zulip Kevin Buzzard (May 30 2018 at 23:01):

but Kenny what about 2/3*4/5=8/30*2

view this post on Zulip Kenny Lau (May 30 2018 at 23:01):

but there is no computable version

view this post on Zulip Mario Carneiro (May 30 2018 at 23:02):

well, the current version is as computable as it gets

view this post on Zulip Kevin Buzzard (May 30 2018 at 23:02):

I see, so the issue is of course not about proving theorems, it is about doing calculations

view this post on Zulip Kevin Buzzard (May 30 2018 at 23:02):

computations

view this post on Zulip Mario Carneiro (May 30 2018 at 23:02):

i.e. stuff like 2 * 3 = 6 computes

view this post on Zulip Kenny Lau (May 30 2018 at 23:02):

everything is about computation

view this post on Zulip Kevin Buzzard (May 30 2018 at 23:02):

which are of course important when you want to prove theorems

view this post on Zulip Kevin Buzzard (May 30 2018 at 23:03):

you want your reals to be "as computable as possible"?

view this post on Zulip Mario Carneiro (May 30 2018 at 23:03):

well yes

view this post on Zulip Kevin Buzzard (May 30 2018 at 23:03):

Don't you take one look at a question involving rationals and instantly descend to the rationals?

view this post on Zulip Kenny Lau (May 30 2018 at 23:03):

then make inv into a function that takes a proof that it is not zero

view this post on Zulip Mario Carneiro (May 30 2018 at 23:03):

I did

view this post on Zulip Andrew Ashworth (May 30 2018 at 23:03):

Kenny, there is such a thing as constructive, computable reals. You can treat it as arbitrary-precision floating point

view this post on Zulip Mario Carneiro (May 30 2018 at 23:04):

It's called divp

view this post on Zulip Kevin Buzzard (May 30 2018 at 23:04):

and does it work on an arbitrary complete totally ordered field?

view this post on Zulip Mario Carneiro (May 30 2018 at 23:04):

It works on any ring

view this post on Zulip Kenny Lau (May 30 2018 at 23:04):

you won't want to formalize computable reals

view this post on Zulip Andrew Ashworth (May 30 2018 at 23:05):

you won't want to, but yet it'll be super useful

view this post on Zulip Kenny Lau (May 30 2018 at 23:06):

are you going to set up turing machines now

view this post on Zulip Mario Carneiro (May 30 2018 at 23:07):

lol I'm actually typing out turing machines right now

view this post on Zulip Mario Carneiro (May 30 2018 at 23:07):

Actually I'm going via Wang B-machines

view this post on Zulip Kevin Buzzard (May 31 2018 at 00:04):

Lean challenge : (2+3)2=5+26(\surd2+\surd3)^2=5+2\surd6

view this post on Zulip Kenny Lau (May 31 2018 at 00:10):

import data.real.basic tactic.norm_num

prefix ``:90 := real.sqrt

example : (2 + 3)^2 = 5 + 2*6 :=
by rw [pow_two, add_mul_self_eq, mul_assoc,
   real.sqrt_mul,  real.sqrt_mul,  real.sqrt_mul,
  real.sqrt_mul_self, real.sqrt_mul_self]; norm_num;
  rw [ add_assoc]; refl

view this post on Zulip Kenny Lau (May 31 2018 at 00:14):

import data.real.basic tactic.norm_num

prefix ``:90 := real.sqrt

example : (2 + 3)^2 = 5 + 2*6 :=
by rw [pow_two, add_mul_self_eq, mul_assoc,
   real.sqrt_mul,  real.sqrt_mul,  real.sqrt_mul,
  real.sqrt_mul_self, real.sqrt_mul_self, add_right_comm];
  norm_num

view this post on Zulip Kevin Buzzard (May 31 2018 at 02:28):

Thanks Kenny.

view this post on Zulip Kevin Buzzard (May 31 2018 at 02:29):

In data/real/basic.lean there is an import of algebra.big_operators which doesn't seem to me to be used. Is this sort of PR welcome?

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:02):

https://github.com/leanprover/mathlib/blob/bdd54acda358f535b42951b784757135213dcf52/data/real/basic.lean#L16

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:03):

At that line, #check mk gives that mk is rat.mk. And then on the next line it feels like it was redefined. Why is mk not overloaded now?

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:03):

Is there some priority trick?

view this post on Zulip Mario Carneiro (May 31 2018 at 03:08):

mk is overloaded at that point. But when one of the theorems with that name is in the current namespace (i.e. inside a namespace block), it takes precedence over other open namespaces.

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:09):

I see. Thanks.

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:09):

instance : has_add  :=
⟨λ x y, quotient.lift_on₂ x y (λ f g, mk (f + g)) $
  λ f₁ g₁ f₂ g₂ hf hg, quotient.sound $
  by simpa [(), setoid.r] using add_lim_zero hf hg

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:09):

and then

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:09):

instance : has_neg  :=
⟨λ x, quotient.lift_on x (λ f, mk (-f)) $
  λ f₁ f₂ hf, quotient.sound $
  by simpa [(), setoid.r] using neg_lim_zero hf

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:09):

That's the same code again!

view this post on Zulip Mario Carneiro (May 31 2018 at 03:10):

sure is, less than 30 seconds copy paste work

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:10):

That should be by math_trivial [add_lim_zero]

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:10):

and then by math_trivial [neg_lim_zero]

view this post on Zulip Mario Carneiro (May 31 2018 at 03:10):

like I said, ~20 times repetition before I even consider making a tactic

view this post on Zulip Mario Carneiro (May 31 2018 at 03:11):

6 or 7 times is not enough

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:11):

but if someone just came along and made that tactic and offered it to mathlib, do you think it would be useful?

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:11):

I am seeing this ... idiom or whatever you call it over and over again

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:11):

"we laboriously transport structure"

view this post on Zulip Mario Carneiro (May 31 2018 at 03:11):

in particular, it is often the case that all the axioms of concrete structure X are similar to each other, but not similar to structure Y

view this post on Zulip Mario Carneiro (May 31 2018 at 03:12):

having a tactic that proves axioms of X is not that helpful since there are only O(1) of them, and the tactic won't help with Y

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:13):

Transport of structure is a central idea of mathematics as we see in the work of Grothendieck and Deligne

view this post on Zulip Mario Carneiro (May 31 2018 at 03:13):

Would this math_trivial tactic apply equally to real and pnat?

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:13):

This is just the sort of thing I want to find out

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:13):

I found myself when doing schemes

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:13):

wanting a tactic like this

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:13):

and I know that when I start perfectoids

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:13):

I'll find it again

view this post on Zulip Mario Carneiro (May 31 2018 at 03:14):

My point is that there are not that many similarities between the proof that pnat has an add and real does

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:14):

yeah isn't that interesting

view this post on Zulip Kenny Lau (May 31 2018 at 03:14):

lol

view this post on Zulip Kenny Lau (May 31 2018 at 03:14):

Kevin

view this post on Zulip Kenny Lau (May 31 2018 at 03:14):

the sky is blue

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:15):

These guys need to make a proper mathematician

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:15):

with the right kind of equals

view this post on Zulip Kenny Lau (May 31 2018 at 03:16):

it's foggy

view this post on Zulip Kenny Lau (May 31 2018 at 03:16):

relative humidity 98%

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:19):

/- Extra instances to short-circuit type class resolution -/
instance : semigroup       := by apply_instance
instance : monoid          := by apply_instance
instance : comm_semigroup  := by apply_instance
instance : comm_monoid     := by apply_instance
instance : add_monoid      := by apply_instance
instance : add_group       := by apply_instance
instance : add_comm_group  := by apply_instance
instance : ring            := by apply_instance

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:19):

Why do they make life better?

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:19):

This is all in data/real/basic.lean

view this post on Zulip Kenny Lau (May 31 2018 at 03:19):

because beneath you is an uncomputable instance

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:19):

those are the best kind IMO

view this post on Zulip Kenny Lau (May 31 2018 at 03:19):

if you don't do this, the uncomputable instance will be used

view this post on Zulip Kenny Lau (May 31 2018 at 03:20):

so your definitions would have to be noncomputable

view this post on Zulip Kenny Lau (May 31 2018 at 03:20):

and it is used because it is declared the latest

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:20):

none of this makes any sense to me

view this post on Zulip Mario Carneiro (May 31 2018 at 03:20):

no, that's not related

view this post on Zulip Mario Carneiro (May 31 2018 at 03:20):

those instances

short-circuit type class resolution

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:20):

so they are creating new paths in the system

view this post on Zulip Kenny Lau (May 31 2018 at 03:20):

well in my construction, if I don't do that, my things become uncomputable

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:20):

which are defeq to longer paths

view this post on Zulip Mario Carneiro (May 31 2018 at 03:20):

yes

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:21):

and this is perhaps making the system better for some reason

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:21):

why doesn't the system run all those commands every time anyone makes anything a comm_ring?

view this post on Zulip Mario Carneiro (May 31 2018 at 03:21):

it means less time traversing the instance graph

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:21):

then it would be much less time

view this post on Zulip Mario Carneiro (May 31 2018 at 03:22):

because that wouldn't save any time, it would just create lots of space

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:22):

instance : has_lt  :=
⟨λ x y, quotient.lift_on₂ x y (<) $
  λ f₁ g₁ f₂ g₂ hf hg, propext $
  ⟨λ h, lt_of_eq_of_lt (setoid.symm hf) (lt_of_lt_of_eq h hg),
   λ h, lt_of_eq_of_lt hf (lt_of_lt_of_eq h (setoid.symm hg))⟩⟩

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:22):

They're getting quite tricky for my tactic now

view this post on Zulip Mario Carneiro (May 31 2018 at 03:22):

If you do it in every case, there is no advantage over just searching the graph, since you have just precalculated all paths

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:23):

ha ha

view this post on Zulip Mario Carneiro (May 31 2018 at 03:23):

the point is that I know that real is important and people want to use it lots

view this post on Zulip Mario Carneiro (May 31 2018 at 03:23):

so I set up the system to make that easier

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:24):

What else can you control within the type class inference system?

view this post on Zulip Mario Carneiro (May 31 2018 at 03:24):

so that when weirdos state ring theorems over the reals for some reason, it's not horribly slow

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:24):

I liked @Reid Barton 's comment about typeclasses.

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:25):

--def real := quotient (@cau_seq.equiv ℚ _ _ _ abs _) -- orig
def real := quotient (cau_seq.equiv : setoid (cau_seq  abs)) -- clearer for me

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:25):

You prefer yours?

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:26):

@ and _ are a bit ugly maybe

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:26):

but yours is shorter

view this post on Zulip Mario Carneiro (May 31 2018 at 03:28):

def real := @quotient (cau_seq ℚ abs) cau_seq.equiv

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:45):

What is your preference? The mathlib one?

view this post on Zulip Mario Carneiro (May 31 2018 at 03:45):

I don't have a strong preference

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:45):

In terms of Lean they're all presumably defeq

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:46):

but in terms of readability some have more worth than others

view this post on Zulip Mario Carneiro (May 31 2018 at 03:46):

they are all syntactically equal

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:47):

My favourite is the last one @quotient (cau_seq ℚ abs) cau_seq.equiv because it's the most readable to mathematicians

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:48):

instance : has_le ℝ := ⟨λ x y, x < y ∨ x = y⟩

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:48):

You've gone the wrong way

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:48):

you can do has_le first and get has_lt for free!

view this post on Zulip Mario Carneiro (May 31 2018 at 03:48):

I know

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:49):

You did it this way for a reason, presumably?

view this post on Zulip Mario Carneiro (May 31 2018 at 03:49):

the constructively natural one is lt

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:49):

I see

view this post on Zulip Kevin Buzzard (May 31 2018 at 03:49):

it's all about computing

view this post on Zulip Mario Carneiro (May 31 2018 at 03:49):

it states that there is some epsilon separating them

view this post on Zulip Mario Carneiro (May 31 2018 at 03:50):

for le, it's either the negation of that or the disjunction with equals

view this post on Zulip Patrick Massot (May 31 2018 at 07:06):

that you are a Dedekind complete ordered field

Note: as a mathematician, I use real numbers every day, and I have no idea what is a "Dedekind complete ordered field"

view this post on Zulip Patrick Massot (May 31 2018 at 07:08):

How are our real numbers getting along? Do we have the definition of a differentiable function yet, and of its derivative?

I have a definition of a function from a real normed vector space to another one which is differentiable at a point. But I don't have a normed space structure on ℝ^n because I'm swamped in type class resolution issues (https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/tc.20loop.20again). Life is really hard here.

view this post on Zulip Kevin Buzzard (May 31 2018 at 23:09):

boggle I am typing up my exam into Lean and I need the fact that the decimal expansion of the real number 0.71 contains no 8's :-)

view this post on Zulip Kevin Buzzard (May 31 2018 at 23:09):

does Lean have decimal expansions??

view this post on Zulip Kevin Buzzard (May 31 2018 at 23:10):

maybe a function from the non-negative reals to (functions from nat to nat)

view this post on Zulip Kevin Buzzard (May 31 2018 at 23:10):

with f(succ n)<=9

view this post on Zulip Kenny Lau (May 31 2018 at 23:11):

you can write that yourself

view this post on Zulip Kenny Lau (May 31 2018 at 23:11):

it's quite explicit using floor

view this post on Zulip Kevin Buzzard (May 31 2018 at 23:11):

you are right!

view this post on Zulip Kenny Lau (May 31 2018 at 23:11):

given a real number r

view this post on Zulip Kevin Buzzard (May 31 2018 at 23:11):

But I was just asking if someone had already written it

view this post on Zulip Kevin Buzzard (May 31 2018 at 23:11):

Kenny I can do it :-)

view this post on Zulip Kevin Buzzard (May 31 2018 at 23:11):

I even lecture it in M1F some years

view this post on Zulip Kevin Buzzard (May 31 2018 at 23:11):

Darn it

view this post on Zulip Kevin Buzzard (May 31 2018 at 23:11):

if I'd lectured it this year then @Chris Hughes would have done it :-)

view this post on Zulip Kevin Buzzard (May 31 2018 at 23:48):

import analysis.real -- should come with a warning

noncomputable definition real.floor (x : ) :  :=
  classical.some (real.exists_floor x)

noncomputable definition expansion (r : ) (H : r  0) :   
| 0 := real.floor r
| (n + 1) := 7

view this post on Zulip Kevin Buzzard (May 31 2018 at 23:48):

I made a slip: real.floor r on the last but one line is an int not a nat

view this post on Zulip Kenny Lau (May 31 2018 at 23:48):

Kevin

view this post on Zulip Kenny Lau (May 31 2018 at 23:48):

the fllor is there already

view this post on Zulip Kevin Buzzard (May 31 2018 at 23:48):

but when using reals, sllips like this bring the system to its knees. 100% CPU usage, orange bars

view this post on Zulip Kenny Lau (May 31 2018 at 23:48):

it's in archimedean

view this post on Zulip Kevin Buzzard (May 31 2018 at 23:49):

Thanks

view this post on Zulip Kevin Buzzard (May 31 2018 at 23:49):

but why does my code make Lean have a deterministic timeout?

view this post on Zulip Kevin Buzzard (May 31 2018 at 23:49):

Mario has answered this before

view this post on Zulip Kevin Buzzard (May 31 2018 at 23:50):

but this behaviour ("use the imported definitions wisely or there will be timeouts") is not the norm

view this post on Zulip Kenny Lau (May 31 2018 at 23:50):

it's just a typeclass fallout

view this post on Zulip Kevin Buzzard (May 31 2018 at 23:50):

right

view this post on Zulip Kevin Buzzard (May 31 2018 at 23:50):

but is this a design problem with Lean or something which can be fixed in mathlib or what?

view this post on Zulip Kenny Lau (May 31 2018 at 23:51):

no idea

view this post on Zulip Kevin Buzzard (May 31 2018 at 23:52):

hey that floor_ring stuff is a really cool way of doing it :-)

view this post on Zulip Kevin Buzzard (May 31 2018 at 23:56):

⌊10 / 3⌋ : ℤ

view this post on Zulip Kevin Buzzard (May 31 2018 at 23:57):

#reduce ⌊(real.sqrt 2 : ℝ)⌋

view this post on Zulip Kevin Buzzard (May 31 2018 at 23:57):

100% CPU usage!

view this post on Zulip Mario Carneiro (May 31 2018 at 23:57):

For some reason, coercing an int to a nat causes a typeclass overflow

view this post on Zulip Kevin Buzzard (May 31 2018 at 23:58):

segv :-)

view this post on Zulip Mario Carneiro (May 31 2018 at 23:58):

I've seen this many times before

view this post on Zulip Kevin Buzzard (May 31 2018 at 23:58):

but it's only with reals

view this post on Zulip Kevin Buzzard (May 31 2018 at 23:58):

Lean is really good with most structures

view this post on Zulip Kevin Buzzard (May 31 2018 at 23:58):

Oh indpt of reals?

view this post on Zulip Mario Carneiro (May 31 2018 at 23:59):

you defined an int function and applied it to get a nat

view this post on Zulip Kevin Buzzard (May 31 2018 at 23:59):

I know

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:00):

I assumed the problem was because reals always time out

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:00):

but maybe you fixed that

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:00):

and this is an independent timeout

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

The major source of that was fixed a while ago

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

this is just Z -> N timeout

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:00):

What do you get with

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:00):

#reduce ⌊(real.sqrt 2 : ℝ)⌋ ?

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

something horrible, don't do that

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

What part of noncomputable don't you understand?

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:01):

:-)

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:01):

I thought there was no harm trying

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

it will be some huge stuck term depending on classical.choice

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:02):

after all, schoolkid can do it

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:02):

it's 1 Mario

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:02):

You can do it, but not like this

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:02):

In order for reduce to work it has to be true generally

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:02):

this is going to be tough to explain to the mathematicians

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:02):

I'm just being daft, I know about eval

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:02):

and there are messy terms you can give where it's impossible to decide

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:03):

#eval won't do any better

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:03):

no but it could

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:03):

actually it will just complain up front

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:03):

no it can't, real.floor is necessarily noncomputable

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:03):

the reduce gives me a segv (twice now)

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:04):

What can do better is norm_num style tactics that prove specific instances of this in some subset of the full language of lean

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:04):

but the floor of the square root of 2 isn't noncomputable

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:04):

That statement doesn't make sense

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:05):

noncomputability is a property of a term, not its denotation

view this post on Zulip Kenny Lau (Jun 01 2018 at 00:05):

@Kevin Buzzard local computability does not patch to give global computability

view this post on Zulip Kenny Lau (Jun 01 2018 at 00:05):

it ain't no sheaf

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:05):

is the obstruction finite?

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:05):

?

view this post on Zulip Kenny Lau (Jun 01 2018 at 00:05):

floor is computable iff halting problem can be solved

view this post on Zulip Kenny Lau (Jun 01 2018 at 00:05):

you have an obstructio in each integer, so no it ain't finite

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:05):

I know but you can do it on sqrt(2)

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:05):

I can prove that 1 is floor of sqrt(2)

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:06):

So do that

view this post on Zulip Kenny Lau (Jun 01 2018 at 00:06):

that doesn't mean you can compute floor(sqrt(2))

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:06):

so it can be computed in this case

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:06):

Kenny -- doesn't it?

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:06):

floor (sqrt 2) is a computable number, yes

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:06):

but floor is not a computable function

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:07):

so you can't just plug sqrt 2 into floor and expect an answer

view this post on Zulip Kenny Lau (Jun 01 2018 at 00:07):

you need uniform computability without creativeness

view this post on Zulip Kenny Lau (Jun 01 2018 at 00:07):

informally

view this post on Zulip Kenny Lau (Jun 01 2018 at 00:07):

you need a canonical function

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:07):

We could get transcendental numbers into Lean if we could get Chris' sin and cos stuff

view this post on Zulip Kenny Lau (Jun 01 2018 at 00:07):

that works across everything

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:08):

floor is daft. Give me exp any day

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:08):

Is that computable?

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:08):

By the way, floor is computable on algebraic numbers

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:08):

I reckon I can prove the sequence is Cauchy

view this post on Zulip Kenny Lau (Jun 01 2018 at 00:09):

everything is computable on algebraic numbers

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:09):

so you can write floor (sqrt 2) and compute to 1

view this post on Zulip Kenny Lau (Jun 01 2018 at 00:09):

surprise

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:09):

exp is computable

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:09):

Kenny I'm sure there are non-recursive or whatever subsets of the natural numbers

view this post on Zulip Kenny Lau (Jun 01 2018 at 00:10):

I was uttering hyperbole

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:10):

and so of the algebraic numbers

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:10):

I think real numbers are overrated in math

view this post on Zulip Kenny Lau (Jun 01 2018 at 00:10):

agree

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:10):

They're just some random completion

view this post on Zulip Kenny Lau (Jun 01 2018 at 00:10):

I was about to say, let's study other local fields

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:10):

that sometimes helps in physics

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:10):

exactly

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:10):

you don't need full completion in 99.9% of cases

view this post on Zulip Kenny Lau (Jun 01 2018 at 00:11):

but there's a problem @Mario Carneiro

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:11):

in number theory we need the product of all the completions :-)

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:11):

something like complete under computable sequences is more than enough

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:12):

Mario do you think Langlands' work on cyclic base change would work with this smaller subset of the reals?

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:12):

or maybe "complete under all the operations I'm talking about today"

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:12):

I'm sure it uses AC everywhere

view this post on Zulip Kenny Lau (Jun 01 2018 at 00:12):

I can't recall the name of the theroem

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:12):

it's not so different to doing categories in ZFC

view this post on Zulip Kenny Lau (Jun 01 2018 at 00:12):

but essentially, if you include exp, then your field is noncomputable

view this post on Zulip Kenny Lau (Jun 01 2018 at 00:12):

algebraic numbers and exp

view this post on Zulip Kenny Lau (Jun 01 2018 at 00:12):

maybe some other things

view this post on Zulip Kenny Lau (Jun 01 2018 at 00:12):

maybe you'll know the name

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:12):

you just want enough stuff for your theorem, but you assume too much for simplicity

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:15):

@Kenny Lau I guess it would be too easy to just compute to find out if e + pi is irrational

view this post on Zulip Kenny Lau (Jun 01 2018 at 00:15):

that's irrelevant

view this post on Zulip Kenny Lau (Jun 01 2018 at 00:16):

for every rational r, if you spent enough time, you can prove that e+pi is not r

view this post on Zulip Kenny Lau (Jun 01 2018 at 00:16):

you just can't prove that, for every rational r, e+pi is not r

view this post on Zulip Kenny Lau (Jun 01 2018 at 00:16):

decidable equality doesn't mean decidable pi equality

view this post on Zulip Kenny Lau (Jun 01 2018 at 00:16):

pi equality meaning forall equality

view this post on Zulip Kenny Lau (Jun 01 2018 at 00:16):

not 3.14159

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:16):

I know, but rationality is decidable on algebraic numbers

view this post on Zulip Kenny Lau (Jun 01 2018 at 00:16):

oh is it

view this post on Zulip Kenny Lau (Jun 01 2018 at 00:16):

how do you define algebraic numbers?

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:17):

yes, just compute the minimal polynomial and see if it has degree 1

view this post on Zulip Kenny Lau (Jun 01 2018 at 00:17):

do you store the minimal polynomial?

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:17):

yes

view this post on Zulip Kenny Lau (Jun 01 2018 at 00:17):

I see

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

I think the most impressive thing about the algebraic numbers is that irreducibility and factoring of Q[x] polynomials is decidable

view this post on Zulip Kenny Lau (Jun 01 2018 at 00:19):

agree

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:33):

come on norm-num

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:33):

↑⌊0⌋ * 10 = 0

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:33):

you can do it

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:33):

gaargh

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:34):

stupid floor function

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:34):

oh there is a lemma

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:34):

I remember now

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:34):

floor_coe

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:35):

I guess floor_zero and floor_one should be simp lemmas

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:35):

and theorems

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:37):

oh you're right, that's not (0 : Z)

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:37):

that one of your other zeros

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:38):

it's defeq though, you can just apply floor_coe

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:48):

not in a rewrite :-/

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:49):

here, use as you like:

@[simp] theorem floor_zero : ⌊(0:α)⌋ = 0 := floor_coe 0

@[simp] theorem floor_one : ⌊(1:α)⌋ = 1 :=
by rw [← int.cast_one, floor_coe]

view this post on Zulip Kenny Lau (Jun 01 2018 at 00:49):

that one of your other zeros

lol

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:50):

unfortunately this doesn't help with say ⌊2⌋ = 2, that gets tricky in general

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:50):

because the two 2's are represented differently

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:51):

I've got interested in what needs names

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:51):

I would vote for floor_zero

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:52):

rofl I just tried it in my code and it didn't work

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:52):

and then I remembered that someone writing some code on the internet doesn't mean my computer runs it

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:52):

and you have to copy paste

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:53):

Those lines were written in archimedean.lean, they might not work out of context

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:55):

I know archimedean.lean so I could fix it up

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:55):

I've been reading some of the real code recently

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:55):

and I'd missed archimedean so I read it the moment Kenny pointed it out to me

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:56):

I already have added those lines to my local copy, they will be out with the next batch

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:56):

I was just thinking I should do the same

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:56):

but for me it's much harder

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:56):

I'm doing undergrad stuff in my xena project at the minute (e.g. decimal expansions) but the library imports your mathlib

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:57):

so I can't edit my fork of your mathlib and then run it easily in my project, unless I actually start importing my mathlib

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 01:22):

ha ha, to finish Q2 of my exam all I now need to do is to prove that if s : ℝ := 71/100 then ⌊s⌋ = 7

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 01:22):

the students didn't spend too much time on this bit

view this post on Zulip Kenny Lau (Jun 01 2018 at 01:23):

does that mean you finished Q1?

view this post on Zulip Mario Carneiro (Jun 01 2018 at 01:24):

I guess this isn't stated as a theorem explicitly, but the way to prove ⌊x⌋ = n is to prove n <= x < n+1, and norm_num will usually take care of that

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 01:24):

no

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 01:24):

I liked Q2 better

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 01:24):

right

view this post on Zulip Mario Carneiro (Jun 01 2018 at 01:25):

also, the theorem you stated is false

view this post on Zulip Mario Carneiro (Jun 01 2018 at 01:25):

the floor of s is zero

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 01:25):

:-)

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 01:25):

oh too many 10s

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 01:25):

sorry

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 01:25):

I have to work out the full decimal expansion

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 01:26):

so i need a fair few floors

view this post on Zulip Mario Carneiro (Jun 01 2018 at 01:26):

You really want to do this on rat

view this post on Zulip Mario Carneiro (Jun 01 2018 at 01:26):

then you can just compute

view this post on Zulip Mario Carneiro (Jun 01 2018 at 01:26):

just take your real number and map it to rat

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 01:28):

I didn't know to what extent that mattered

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 01:28):

now I need some theorem that says that the floors agree

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 01:29):

noncomputable definition s : ℝ := 71/100 lemma bound1 : 0 ≤ s := by norm_num -- fails :-(

view this post on Zulip Mario Carneiro (Jun 01 2018 at 01:29):

I am already on it

view this post on Zulip Kenny Lau (Jun 01 2018 at 01:29):

by unfold s; norm_num

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 01:29):

thanks

view this post on Zulip Mario Carneiro (Jun 01 2018 at 01:53):

this should work for you:

@[simp] theorem rat.cast_floor
  {α} [linear_ordered_field α] [archimedean α] (x : ℚ) :
  by haveI := archimedean.floor_ring α; exact ⌊(x:α)⌋ = ⌊x⌋ :=
begin
  haveI := archimedean.floor_ring α,
  apply le_antisymm,
  { rw [le_floor, ← @rat.cast_le α, rat.cast_coe_int],
    apply floor_le },
  { rw [le_floor, ← rat.cast_coe_int, rat.cast_le],
    apply floor_le }
end

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 01:57):

you have to use haveI in the statement to make it typecheck

view this post on Zulip Mario Carneiro (Jun 01 2018 at 01:57):

I did...

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 01:57):

and then again in the proof

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 01:57):

The devs don't come here, this is the maths chat

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 01:57):

what do you think about all this haveI stuff?

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 01:58):

Aren't things worse than they used to be?

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 01:58):

Or did other stuff get fixed when that change was made?

view this post on Zulip Mario Carneiro (Jun 01 2018 at 01:58):

I think I got Leo angry about it, so I'm not going to try again

view this post on Zulip Mario Carneiro (Jun 01 2018 at 01:58):

haveI is the compromise position

view this post on Zulip Mario Carneiro (Jun 01 2018 at 01:58):

...but it's not unreasonable here

view this post on Zulip Mario Carneiro (Jun 01 2018 at 01:59):

I'm injecting an instance which is not an instance normally

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:01):

Thanks.

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:11):

I feel like I want to apply int.succ_le_of_lt out of decency

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:11):

lemma int.succ_le_of_lt (a b : ℤ) : a < b → int.succ a ≤ b :=

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:11):

but proof is id

view this post on Zulip Mario Carneiro (Jun 01 2018 at 02:11):

It's up to you

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:12):

it looks like bad style to just know it's id

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:12):

who the .... cares

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:12):

it's the interface Kenny

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:12):

proofs are irrelevant

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:12):

id sometimes deserves a name :-)

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:12):

proofs are irrelevant but names are important

view this post on Zulip Mario Carneiro (Jun 01 2018 at 02:13):

You are absolutely right, using defeq like this breaks the interface

view this post on Zulip Mario Carneiro (Jun 01 2018 at 02:13):

but it's not a hill I want to die on

view this post on Zulip Mario Carneiro (Jun 01 2018 at 02:13):

I would say "use in moderation"

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:27):

lemma floor_of_bounds (r : α) (z : ) :
  z  r  r < (z + 1)   r  = z :=
begin
  split,swap, -- easy one
  { intro H,rw H,
    split,exact floor_le r,
    suffices : r < ↑⌊r + (1 : ),
      simpa using this,
    have H' := lt_succ_floor r,
    rw int.cast_add,
    exact H',
  },
  have H := λ d, @le_floor α _ d r,

  intro J,cases J with floor_le' lt_succ_floor',
  cases (le_or_gt r z) with HT HF,
  swap, exfalso, -- false one
  { have XXX := (H (z+1)).1 (int.succ_le_of_lt _ _ HF),
    rw int.cast_add at XXX,
    clear HF,
    have H2 := lt_of_le_of_lt XXX lt_succ_floor',
    revert H2,simp,
  },
  cases lt_or_eq_of_le HT with HF HT',swap,exact HT',
  exfalso,
  have XXX := (H z).2 floor_le',
  apply lt_irrefl z,
  exact lt_of_le_of_lt XXX HF,
end

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:27):

Rubbish lean code but it's a proof

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:27):

What tricks am I missing?

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:30):

le_floor?

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:30):

given z <= r, use le_floor to deduce z <= floor(r)

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:31):

here's the reals back to their old tricks

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:32):

given r < z+1, floor_lt tells you floor(r) < z + 1

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:32):

then deduce floor(r) <= z (everything is an integer now)

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:32):

and then le_antisymm

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:33):

noncomputable definition s :  := 71/100

example : floor s = 0 :=
begin
show floor ((71/100:):) = 0,
admit
end

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:33):

deterministic timeout

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:33):

because 71:R / 100:R is not defeq to 71:Q / 100:Q

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:34):

I did it by contradiction :-)

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:34):

you always want to do things constructively

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:34):

?

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:34):

I see

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:34):

to each their own

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:34):

I have no time

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:34):

I need to learn what the Weil group is

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:34):

oh the coercion to R is done before the division

view this post on Zulip Mario Carneiro (Jun 01 2018 at 02:35):

The magic of biconditional theorems...

lemma floor_of_bounds (r : α) (z : ℤ) :
  ↑z ≤ r ∧ r < (z + 1) ↔ ⌊ r ⌋ = z :=
by rw [← le_floor, ← int.cast_one, ← int.cast_add, ← floor_lt,
  int.lt_add_one_iff, le_antisymm_iff, and.comm]

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:35):

lol

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:35):

two lines vs 100 lines

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:35):

very nice

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:35):

but I never got stuck

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:35):

I just proved it and enjoyed it

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:36):

walking around the gardens of mathematics

view this post on Zulip Mario Carneiro (Jun 01 2018 at 02:37):

oh you proved by contradiction

view this post on Zulip Mario Carneiro (Jun 01 2018 at 02:37):

that's a bit roundabout

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:38):

it's inbuilt

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:38):

I asked 250 students to prove sup(S) + sup(T) = sup(S+T)

view this post on Zulip Mario Carneiro (Jun 01 2018 at 02:38):

you have so many cases in this proof...

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:38):

and about 80 did it

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:38):

really

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:38):

and 79 did it by contradiction

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:39):

such a simple theorem

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:39):

only 80 out of 250

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:39):

it's about that

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:39):

I didn't count carefully and it's all gone back to the exams office now

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:39):

@Mario Carneiro and the 1 is me lol

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:39):

maybe more

view this post on Zulip Mario Carneiro (Jun 01 2018 at 02:39):

I recall this story

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:39):

like seriously

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:39):

the UMPs of sup is all you need

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:39):

contradiction is the most powerful method of proof

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:39):

you get to assume the most stuff

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:40):

but 0% of the people know about UMP and UMP of sup

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:40):

rounded down to the nearest percent

view this post on Zulip Mario Carneiro (Jun 01 2018 at 02:40):

I'm not even against it on intuitionistic grounds

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:40):

if you've never had your brain polluted by constructivism it's a very natural first step

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:40):

cleansed

view this post on Zulip Mario Carneiro (Jun 01 2018 at 02:40):

it has a way of making thinking easier and proof more complicated

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:40):

right

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:41):

I even saw, on several occasions, and this is certainly not the first time,

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:41):

people writing

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:41):

it's not even about constructivism anymore, I'm just chaining UMPs all around

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:41):

it's not about constructivism when people use UMP in category theory

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:41):

because it's what it is

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:41):

it's the UMP

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:41):

"We want to prove X. Let's prove it by contradiction. So assume X is false. Now consider the following perfectly good proof of X. But X is false! Contradiction!

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:41):

"

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:42):

if you are a lazy person who only knows proof by contradiction it's a very natural first step

view this post on Zulip Mario Carneiro (Jun 01 2018 at 02:42):

For things like timed tests it's a good strategy

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:42):

I find UMPs easier

view this post on Zulip Mario Carneiro (Jun 01 2018 at 02:43):

where you just write and write until you get the answer

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:43):

I just use 100 UMPs until I get the answer

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:43):

and I always get it

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:43):

because it's universal

view this post on Zulip Mario Carneiro (Jun 01 2018 at 02:43):

Also resolution theorem proving is based on this idea

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:43):

solve_by_elim ain't

view this post on Zulip Mario Carneiro (Jun 01 2018 at 02:44):

where you whittle down a counterexample until it is impossible

view this post on Zulip Mario Carneiro (Jun 01 2018 at 02:44):

but the resulting proof looks ugly I think

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:45):

(whatever)

view this post on Zulip Mario Carneiro (Jun 01 2018 at 02:45):

when you want that "polished" look it's best to avoid proof by contradiction

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:51):

My goal is has_le.le (coe 0) (has_div.div 71 100)

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:51):

and if I try and unfold either has_le.le or coe I get a deterministic timeout

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:52):

so don't unfold them?

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:53):

norm_num times out too

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:54):

did you use div lemmas?

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:54):

div_nonneg

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:54):

oh I need to feed those in

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:54):

you just need that one

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:54):

the rest should be norm_num

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:54):

do I put it in the context?

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:55):

no, you apply it

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:56):

you want me to actually prove it by hand??

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:56):

what is this -- the 1980s?

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:57):

we have norm_num!

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:57):

my math teacher at high school would tell the story of people using calculators to verify that 5 x 0 = 0

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:58):

refine div_nonneg _ _, times out

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:58):

everything times out

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:58):

my goal is corrupted

view this post on Zulip Kenny Lau (Jun 01 2018 at 02:58):

code

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:59):

noncomputable definition s :  := 71/100

theorem sQ : s = ((71/100:):) := by unfold s;norm_num

--set_option pp.all true
example : floor s = 0 :=
begin
rw [sQ,rat.cast_floor],
apply (floor_of_bounds _ _).1,
split,
{ have H : (100 : )> 0 := by norm_num,
  refine div_nonneg _ _,
  --unfold has_le.le,
--show 0 ≤ 71 / 100,

    sorry},
{sorry}
end

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:59):

all this fuss about 0.71

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 02:59):

I should have been in bed hours ago

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 03:00):

I'm glad none of my students spent 2 hours on this bit

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 03:00):

it was only a 2 hour exam

view this post on Zulip Kenny Lau (Jun 01 2018 at 03:02):

example : floor s = 0 :=
begin
  rw  floor_of_bounds,
  split,
  { unfold s, apply div_nonneg; norm_num },
  { unfold s, rw div_lt_iff; norm_num }
end

view this post on Zulip Mario Carneiro (Jun 01 2018 at 03:06):

example : floor s = 0 := by rw [← floor_of_bounds, s, int.cast_zero]; norm_num

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 03:08):

So using rat.cast_floor was a bad idea

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 03:08):

Even though my instinct is to get out of R ASAP

view this post on Zulip Kenny Lau (Jun 01 2018 at 03:08):

there's a box

view this post on Zulip Mario Carneiro (Jun 01 2018 at 03:08):

I meant to use that if you were planning on kernel computation

view this post on Zulip Kenny Lau (Jun 01 2018 at 03:08):

think out of it

view this post on Zulip Kenny Lau (Jun 01 2018 at 03:08):

@Mario Carneiro i couldn't get the kernel to compute it

view this post on Zulip Mario Carneiro (Jun 01 2018 at 03:09):

Actually 71 might be too big for the kernel...

view this post on Zulip Kenny Lau (Jun 01 2018 at 03:09):

lol

view this post on Zulip Kenny Lau (Jun 01 2018 at 03:09):

71 is too big for the kernel

view this post on Zulip Kenny Lau (Jun 01 2018 at 03:09):

https://tio.run/##K6gsycjPM/7/v6AoM69Ew9xQS8vcUPP/fwA

view this post on Zulip Mario Carneiro (Jun 01 2018 at 03:09):

that's VM computation though

view this post on Zulip Mario Carneiro (Jun 01 2018 at 03:09):

or would be if it were lean

view this post on Zulip Mario Carneiro (Jun 01 2018 at 03:10):

python doesn't have to bother proving it is correct

view this post on Zulip Mario Carneiro (Jun 01 2018 at 03:10):

and it also doesn't use a braindead representation

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 03:45):

Kenny I did it:

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 03:45):

theorem no_eights (n : ℕ) : decimal.expansion s (by unfold s;norm_num) n ≠ 8 := ...

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 03:45):

0.71 has no 8's in its decimal expansion

view this post on Zulip Johan Commelin (Jun 01 2018 at 06:44):

Actually 71 might be too big for the kernel...

Would it help if we compute in base rr (with r=10r = 10 or 1616)? Then we could have a lookup-table of simp-lemmas. And we could implement stuff like https://en.wikipedia.org/wiki/Multiplication_algorithm#Karatsuba_multiplication

view this post on Zulip Johan Commelin (Jun 01 2018 at 06:45):

And for specific computations, of course a specific base could be used, with pre-computed lookup-tables.

view this post on Zulip Johan Commelin (Jun 01 2018 at 06:46):

Ok, to be clear: I am not suggesting that we change the implementation of nat. But I am suggesting that we have a parallel implementation specifically for computations in base r. And an isomorphism between the implementations.

view this post on Zulip Johan Commelin (Jun 01 2018 at 06:47):

But maybe this means that we also need a parallel implementation of int and rat. And then I'm not sure if I would want to go down that rabbit-hole

view this post on Zulip Mario Carneiro (Jun 01 2018 at 06:57):

Yes, it would help to work in base r. The really important part is that r should be greater than 1

view this post on Zulip Mario Carneiro (Jun 01 2018 at 06:57):

The num type is used to address these issues, by implementing binary natural numbers instead of the default nat which is unary

view this post on Zulip Mario Carneiro (Jun 01 2018 at 06:58):

znum is the parallel implementation of int; there is no qnum type (yet)

view this post on Zulip Johan Commelin (Jun 01 2018 at 07:01):

Hmm, ok. So then you would need a qnum and afterwards an rnum and a cnum...

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:02):

well, those last two don't matter anyway

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:02):

or at least, they would be significantly different from the real type you know and love

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:02):

because computable reals are not like regular reals

view this post on Zulip Johan Commelin (Jun 01 2018 at 07:02):

I am not suggesting that rnum be computable

view this post on Zulip Johan Commelin (Jun 01 2018 at 07:03):

But maybe then it isn't useful either (-;

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:03):

That's the whole point

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:03):

The idea is to have a "programming numbers" type which is proven isomorphic to the abstract version

view this post on Zulip Johan Commelin (Jun 01 2018 at 07:03):

Right

view this post on Zulip Johan Commelin (Jun 01 2018 at 07:04):

But for a speed-up of Kevin's question, you would like to convert to num at some point. Is that correct?

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:05):

Unfortunately, you currently have to make a decision between VM-optimized and kernel-optimized data types

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:05):

so there are valid reasons to keep both around

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:06):

nat is actually the faster one in the VM, because lean replaces it with GMP bignums or C ints if small enough

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:06):

while num is just a regular inductive type so it's implemented as a linked list of digits

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:08):

If you want to prove theorems by rfl or dec_trivial, you need to use kernel-efficient data types or else keep the numbers very small

view this post on Zulip Johan Commelin (Jun 01 2018 at 07:09):

Yes, I understand. So, are things like Karatsuba or Tom-Cook implemented for num?

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:09):

If you are using norm_num or simp, you want VM-efficient data types

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:09):

No, the numbers have not got that big (yet)

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:10):

That requires significant size before it pays off

view this post on Zulip Johan Commelin (Jun 01 2018 at 07:10):

I guess another problem is that for big numbers the conversion between nat and num will become the bottle-neck. Right?

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:11):

You can't do anything that even mentions nat in the kernel with big numbers

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:12):

you can't even accept nat input and convert to num because the parser produces some bit0 (bit0 ... 1) term to pass to your function, and the kernel evaluates it before getting to your function

view this post on Zulip Johan Commelin (Jun 01 2018 at 07:12):

O.o (-;

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:12):

So this means that any conversion from nat has to be done in the VM. The good news is that this can be done efficiently and still be verified

view this post on Zulip Johan Commelin (Jun 01 2018 at 07:13):

Ok, I don't follow this anymore... but I think it means that I can relax (-;

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:13):

You just have theorems saying bit0 \u x = \u bit0 x where \u : nat -> num

view this post on Zulip Johan Commelin (Jun 01 2018 at 07:13):

I thought that the VM cheated... and you would lose verification

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:14):

and you have a tactic (running in the VM) that selectively chooses to apply this theorem

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:14):

by looking at the term in the goal

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:14):

with regular lean functions you can only look at the value that is given, but tactics can decompose the expr that represents the value

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:15):

so something like bit0 (bit0 ... 1) has reasonable size as a term but not as a value

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:16):

and you can apply log(n) bit0 \u x = \u bit0 x theorems to get it down to a theorem just about num

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:16):

and then you prove by rfl or whatever

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:16):

and the kernel never has to evaluate big nats

view this post on Zulip Johan Commelin (Jun 01 2018 at 07:18):

Ok, I see the strategy.

view this post on Zulip Johan Commelin (Jun 01 2018 at 07:19):

I think Kevin is going to like that if at some point he wants to do some modular form stuff...

view this post on Zulip Johan Commelin (Jun 01 2018 at 07:19):

Because their coefficients explode

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:20):

So norm_num is also working in binary, I guess

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:20):

it produces a theorem that is longer for larger numbers though

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:21):

while a kernel proof is always just rfl

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:22):

For the most part, kernel computation is discouraged because it's not particularly optimized for that

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:23):

But I think it's amusing that in dependent type theory you can write down a very short proof of almost anything

view this post on Zulip Johan Commelin (Jun 01 2018 at 07:24):

What do you mean with that last statement?

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:24):

for example, I can write a program that enumerates proofs in ZFC or whatever, and then if there is a proof of RH with fewer than 2^2^2^2^2^2^2^2^2^2^2 symbols, then I can prove it by rfl

view this post on Zulip Johan Commelin (Jun 01 2018 at 07:25):

Right, but that proof will require a lot of prerequisite work

view this post on Zulip Johan Commelin (Jun 01 2018 at 07:25):

(Which I consider part of the proof.)

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:26):

The only work that needs to be done is the setup, stating the problem

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:26):

the "hard part" is completely absent from the accounting, except in the length bound

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:27):

but I can write functions that grow ridiculously fast in DTT so that's not saying much

view this post on Zulip Johan Commelin (Jun 01 2018 at 07:27):

Ok, so we can prove that RH doesn't have a short proof.

view this post on Zulip Johan Commelin (Jun 01 2018 at 07:27):

And neither has Fermat's Last Theorem

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:28):

Okay, fermat is a good example, since we know that one is true

view this post on Zulip Johan Commelin (Jun 01 2018 at 07:28):

For otherwise they would already have been in mathlib with a rfl proof.

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:28):

I can prove Fermat's last theorem by rfl

view this post on Zulip Johan Commelin (Jun 01 2018 at 07:28):

I would love to see that done.

view this post on Zulip Johan Commelin (Jun 01 2018 at 07:28):

The statement is already there

view this post on Zulip Johan Commelin (Jun 01 2018 at 07:28):

And that is all the setup you need.

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:29):

I just write a bool function that checks the first bazillion proofs and returns tt if one works, and assert by rfl that it is tt

view this post on Zulip Johan Commelin (Jun 01 2018 at 07:30):

Right. And of course Lean will never finish running.

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:30):

that proof checks if and only if there is a short enough proof of FLT, and since we know there is, that means I have a short proof

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:31):

Of course the problem with this kind of analysis is that lean will run (almost) forever on such a proof

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:31):

But it seems to be some kind of deficiency in DTT, that the length of a proof is no longer a suitable measure of the hardness of the proof

view this post on Zulip Johan Commelin (Jun 01 2018 at 07:32):

Yes, and that's why we still dont have FLT in mathlib (-;

view this post on Zulip Johan Commelin (Jun 01 2018 at 07:32):

No, but compile-time is still a good measure

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:33):

Yes. Or number of proof steps including definitional reductions

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:33):

This doesn't come up in ZFC since there's no definitional reduction, what you see is what you get

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:35):

anyway, this "feature" of DTT should be thought of as abuse of lean, so don't be surprised if it starts to sweat

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:35):

when you try to #reduce 71 / 100

view this post on Zulip Johan Commelin (Jun 01 2018 at 07:36):

Sure, and in fact, we don't even know what the value of "bazillion" is for your bool function. We only have a very clear suggestion that it is finite.

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:37):

I think there are some pretty reasonable upper bounds based on physical considerations

view this post on Zulip Mario Carneiro (Jun 01 2018 at 07:37):

i.e. the proof appears to fit in the universe, so it's shorter than Graham's number

view this post on Zulip Johan Commelin (Jun 01 2018 at 07:37):

ok, fair enough

view this post on Zulip Johan Commelin (Jun 01 2018 at 11:12):

It seems that real is not an instance of has_pow. Should I add it, or is there some computability reason for not doing that?

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 12:33):

I think the definition of has_pow is post-real so it might just be that nobody used them seriously enough since. As you can see, I've come back to the reals recently, and I am always interested in making them "undergraduate-friendly" so I would have run into this sooner or later.

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 12:33):

@Mario Carneiro -- where do these definitions go? Mathlib? My own Xena library? (I'm writing a library for stuff my UG mathematicians might want or need and which is not in mathlib -- can you envisage there being good reasons for such a library?)

definition is_upper_bound (x : ) (S : set ) :=  s  S, s  x
definition is_bounded_above (S : set ) :=  x, is_upper_bound x S
definition is_LUB (x : ) (S : set ) := is_upper_bound x S   y : , is_upper_bound y S  x  y

definition has_LUB (S : set ) :=  x, is_LUB x S

view this post on Zulip Johan Commelin (Jun 01 2018 at 12:39):

Hmm, I guess to do has_pow properly, we should define x^r for x r : real. And then all of a sudden you have to work.

view this post on Zulip Johan Commelin (Jun 01 2018 at 12:40):

Or can we have multiple instances, depending on whether r has type nat or int or rat or real.

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 12:42):

this is exactly the problem with pow

view this post on Zulip Johan Commelin (Jun 01 2018 at 12:43):

@Kevin Buzzard Isn't Sup already on line 316 of data.real.basic?

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 12:43):

Chris Hughes wrote exp : C -> C but it's still not in mathlib

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 12:49):

That's CS sup

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 12:49):

sup(S)+sup(T) = sup(S+T) is not true for that sup

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 12:49):

let S have one element and let T be empty

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 12:49):

(deleted)

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 12:49):

it returns 37 if the set has no sup

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 12:49):

This is philosophy not mathematics

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 12:50):

but if you're going to define sup globally

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 12:50):

then it should be taking values in -infty + R + infty

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 12:50):

not just spewing out 37s when it's stuck

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 12:51):

You see how my predicate solves this problem?

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 12:51):

I can say "if a is the sup of S and b is the sup of T then a + b is the sup of S + T

view this post on Zulip Johan Commelin (Jun 01 2018 at 12:51):

Ok, so I read too quickly (-;

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 12:51):

My question is how to formalize that statement in mathlib

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 12:51):

and my predicates make it look nice and easy

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 12:51):

whereas I can't quite do it with what we have

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 12:52):

however I am unclear about whether "what I want as someone who wants to formulate elementary lemmas about sup"

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 12:52):

has anything to do with "what should be in mathlib"

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 12:52):

I am very unclear about what the boundaries of mathlib are

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 12:52):

Look, watch this:

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 12:52):

@Mario Carneiro -- should I put schemes in mathlib? Let me know. I don't care either way but you never answer

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 12:52):

he never answers

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 12:53):

I think he reads the question, thinks "hmm, I don't know offhand, I should look at the repo, oh look it's 7000 lines of sometimes poorly-written code"

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 12:53):

"this will need some thought"

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 12:53):

I'll try another approach

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 12:55):

@Mario Carneiro I think definitions of high-level mathematical objects and statements of extremely technical theorems are extremely important things to have in Lean and I will be making quite a few of these in the future. Do you want them in mathlib or do you feel that they are beyond mathlib's remit? I hope I have conveyed in the past how I feel about this matter (namely that I think that there are many people whose interest would be sparked by a small database of complex objects built in Lean)

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 12:56):

I believe @Scott Morrison thinks they should be in mathlib

view this post on Zulip Johannes Hölzl (Jun 01 2018 at 13:32):

least upper bounds etc as predicates are already there: https://github.com/leanprover/mathlib/blob/master/order/bounds.lean

view this post on Zulip Sebastien Gouezel (Jun 01 2018 at 14:07):

You can also have a look at https://github.com/leanprover/mathlib/blob/master/order/conditionally_complete_lattice.lean

view this post on Zulip Mario Carneiro (Jun 01 2018 at 15:45):

-- should I put schemes in mathlib? Let me know. I don't care either way but you never answer

RIght now? No. As Patrick has mentioned before, the scheme code is huge and requires major refactoring to go into mathlib, much like some other planned additions, e.g. Scott's category theory stuff (and he's made some progress on this last I checked). As it currently exists, it is written as a "race to the finish" which gets the job done without worrying about looking good while doing it, whereas I need "polished" code to go into mathlib. It's like the difference between research notes and a journal article or textbook. This process of bringing schemes in will take a lot of both of our time and right now I think you have bigger plans, so I would hold off on attempting this for the present.

view this post on Zulip Mario Carneiro (Jun 01 2018 at 15:46):

I think definitions of high-level mathematical objects and statements of extremely technical theorems are extremely important things to have in Lean and I will be making quite a few of these in the future. Do you want them in mathlib or do you feel that they are beyond mathlib's remit?

The "level" of the definition is not a problem, it can be as advanced as you like. But it must also be good lean code, that's my main concern.

view this post on Zulip Mario Carneiro (Jun 01 2018 at 15:51):

@Johan Commelin There is a definition of has_pow on real, because it is a field. You can use a^n where n : nat and a : real

view this post on Zulip Mario Carneiro (Jun 01 2018 at 15:53):

Actually a^n where n : int is not quite there, since the instance that exists is for groups and real isn't a (multiplicative) group. Maybe there should be another definition for division_rings that sets 0^-n = 0?

view this post on Zulip Mario Carneiro (Jun 01 2018 at 15:56):

You could use the (tiny) library of proper division in mathlib though: units.mk0 a h where a : real and h : a != 0 is an element of units real, which is a group, so you can raise it to an integer power and coerce back to real

view this post on Zulip Johan Commelin (Jun 01 2018 at 16:44):

Ok, thanks. I will take a look at those functions.

view this post on Zulip Johan Commelin (Jun 01 2018 at 16:48):

Is it now easy to have the integers \cup infty? How about int \cup -\infty ? Including the order and addition on them. (Otherwise I could just take option int.

view this post on Zulip Mario Carneiro (Jun 01 2018 at 16:59):

Yes, with_top int has an addition operation and an order, and is defeq to option int

view this post on Zulip Johan Commelin (Jun 01 2018 at 17:08):

Hmm, but there is no with_bot for semigroups. I want to define a function f : nat \to (with_top int), and then another function nat \to real := \lam n, b^(- f(n)), where b is some fixed real number.

view this post on Zulip Johan Commelin (Jun 01 2018 at 17:09):

So then I need to extend - to - : with_top int \to with_bot int. And I need to explain to has_pow real that b^(-infty) = 0.

view this post on Zulip Mario Carneiro (Jun 01 2018 at 17:10):

eww

view this post on Zulip Mario Carneiro (Jun 01 2018 at 17:10):

that's a bit specialized

view this post on Zulip Johan Commelin (Jun 01 2018 at 17:10):

Ok, f(n) = infty \iff n = 0.

view this post on Zulip Mario Carneiro (Jun 01 2018 at 17:11):

You can define - as option.map (\lam x, -x), and b^o where o : with_bot int by cases

view this post on Zulip Johan Commelin (Jun 01 2018 at 17:11):

The other option is that I just use if-then-else everywhere... but I don't really like that either...

view this post on Zulip Mario Carneiro (Jun 01 2018 at 17:11):

no if-then

view this post on Zulip Mario Carneiro (Jun 01 2018 at 17:11):

it's an option, use cases

view this post on Zulip Johan Commelin (Jun 01 2018 at 17:12):

Right. (I meant avoiding option and just do dite (n = 0) in all the definitions.

view this post on Zulip Johan Commelin (Jun 01 2018 at 17:12):

(This stuff shows up everywhere in nonarchimedean valuations.)

view this post on Zulip Mario Carneiro (Jun 01 2018 at 17:12):

what n = 0 are you talking about?

view this post on Zulip Mario Carneiro (Jun 01 2018 at 17:13):

you said f returns an option

view this post on Zulip Mario Carneiro (Jun 01 2018 at 17:13):

well, a with_top

view this post on Zulip Johan Commelin (Jun 01 2018 at 17:13):

Yes, but I could also define f on pnat, and g with a dite.

view this post on Zulip Johan Commelin (Jun 01 2018 at 17:13):

Right?

view this post on Zulip Mario Carneiro (Jun 01 2018 at 17:14):

Oh, I misunderstood your iff statement

view this post on Zulip Johan Commelin (Jun 01 2018 at 17:15):

But I like your approach. I'll try to implement it when I'm back at Lean. (And should I just clone and dualise the with_top stuff to with_bot for semigroups?

view this post on Zulip Mario Carneiro (Jun 01 2018 at 17:15):

It's already there

view this post on Zulip Johan Commelin (Jun 01 2018 at 17:16):

Hmm, for with_bot I only see instances for partial orders and lattices. Not for semigroups.

view this post on Zulip Mario Carneiro (Jun 01 2018 at 17:17):

There is with_zero also, there are lots of ways to construe the added element in all the structures

view this post on Zulip Mario Carneiro (Jun 01 2018 at 17:18):

Oh, I see, with_top and with_bot are actually the same as add_semigroups

view this post on Zulip Johan Commelin (Jun 01 2018 at 17:19):

Ok, so maybe you can also give a hint on how to define f. It is the p-adic valuation (where p is a prime). So f(n) is the maximal e : nat such that p^e divides n.

view this post on Zulip Johan Commelin (Jun 01 2018 at 17:19):

Oh, I see, with_top and with_bot are actually the same as add_semigroups

Yes, but not as ordered add_semigroups.

view this post on Zulip Mario Carneiro (Jun 01 2018 at 17:19):

Yeah, I'll work on that

view this post on Zulip Reid Barton (Jun 01 2018 at 17:21):

@Johan Commelin see https://gist.github.com/rwbarton/599327954b01b2e840894189981172ea

view this post on Zulip Mario Carneiro (Jun 01 2018 at 17:21):

First, I would want a "prime count" function that takes a nat and finds the appropriate power of p. It is defined arbitrarily at zero, but for concreteness that means f 0 = 0

view this post on Zulip Reid Barton (Jun 01 2018 at 17:22):

I gave that to Kevin earlier and I think he has improved it some in the Fibonacci project

view this post on Zulip Johan Commelin (Jun 01 2018 at 17:22):

Yes, or f 0 = infty. And then you would be done.

view this post on Zulip Johan Commelin (Jun 01 2018 at 17:22):

Reid, thanks. I'll take a look.

view this post on Zulip Mario Carneiro (Jun 01 2018 at 17:22):

Then the valuation function is defined by cases on n

view this post on Zulip Mario Carneiro (Jun 01 2018 at 17:24):

actually, I just checked what I did in metamath for this and I used with_top as well. So past me seems to think that's a better idea

view this post on Zulip Mario Carneiro (Jun 01 2018 at 17:25):

I'm a bit worried about having to coerce all the time though

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 17:47):

I don't think I ever got the code completely working in the Fibonacci project, there was perhaps one sorry I never got rid of

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 17:48):

As it currently exists, it is written as a "race to the finish" which gets the job done without worrying about looking good while doing it, whereas I need "polished" code to go into mathlib. It's like the difference between research notes and a journal article or textbook. This process of bringing schemes in will take a lot of both of our time and right now I think you have bigger plans, so I would hold off on attempting this for the present.

Yes, this is exactly how I wrote it, and I put very little thought into how to make structures because I didn't really know how to make structures at the time. Here are my more long-term thoughts on these matters:

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 17:49):

I'm going to do perfectoid spaces because I think it would be funny to do them

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 17:49):

Some scheme stuff we will need e.g. sheaves

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 17:49):

but I was thinking about re-doing it

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 17:49):

doing it all for a second time in a perfectoid spaces directory

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 17:50):

and this time doing it better and checking with people like Mario along the way as to whether the structures looked sensible

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 17:50):

I understand now much better what I can do well and what I do badly

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 17:50):

and especially what I do so badly that it will take a lot of time to fix

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 17:50):

I make no apologies for the race to the finish with schemes -- this was simply a test to see if it could be done, and it could be done

view this post on Zulip Mario Carneiro (Jun 01 2018 at 17:51):

I thnk that's a good plan

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 17:52):

In the long term with schemes, I propose doing perfectoid spaces, seeing the parts which are common to both theories, using this commonality as an argument for inclusion in mathlib, and then spending some time writing these parts of the code properly

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 17:52):

so for example we will need sheaves of types at some point

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 17:52):

and when we need them in the perfectoid theory I will revisit what I did for schemes

view this post on Zulip Mario Carneiro (Jun 01 2018 at 17:52):

The second time around you will have a much better appreciation for the subtleties and design questions and can do it right

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 17:52):

(in fact we did these already and I even have a suggested definition from Mario somewhere in my starred messages)

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 17:53):

yes -- second time round much better

view this post on Zulip Mario Carneiro (Jun 01 2018 at 17:53):

Not to mention you are a better lean programmer now than last month (and the month before that etc)

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 17:53):

so second time round I think "this is important, I knocked up a definition in 10 minutes when I was doing schemes, here are the problems I had with it, let's fix those problems now and aim for mathlib"

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 17:53):

"and write a proper interface while we're here"

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 17:54):

so it's partly some random repo with random bits of people's papers formalised

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 17:54):

and then some directory called "mathlib_someday"

view this post on Zulip Mario Carneiro (Jun 01 2018 at 17:54):

When I look at dioph.lean I am ashamed of myself, I would write that so much better now and it's been only a year

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 17:54):

where we put files where someone has actually made an effort to make the file mathlib-worthy

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 17:55):

You're absolutely right that I get better every month. When I started schemes I had no idea how to use type class inference so never used it -- I would just supply all the missing proofs myself.

view this post on Zulip Scott Morrison (Jun 01 2018 at 22:15):

This all sounds like a great plan --- schemes absolutely deserve to be in mathlib (what would be the point of mathlib if we weren't aiming for it to cover the basic essentials?), and at the same time we should try to make sure code going into mathlib is good (not perfect, though).

view this post on Zulip Scott Morrison (Jun 01 2018 at 22:16):

My categories code (getting there! :-) is still abysmal, probably, and I appreciate it's going to be lots of work to get it into mathlib. :-)

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 00:08):

import algebra.archimedean

#check @abs_nonneg
-- abs_nonneg : ∀ {α : Type u_1}
--   [_inst_1 : decidable_linear_ordered_comm_group α] (a : α),
--   abs a ≥ 0

theorem abs_nonneg' (α : Type) [floor_ring α] [decidable_linear_ordered_comm_group α]
(r : α) : abs r  0 := abs_nonneg r -- fails

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 00:08):

My understanding of something Reid said a few days ago about the reals

view this post on Zulip Kenny Lau (Jun 03 2018 at 00:08):

diamond of death?

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 00:08):

was that I shouldn't be proving things about the reals

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 00:09):

I should just demand I'm a complete totally ordered field and deduce everything from that

view this post on Zulip Mario Carneiro (Jun 03 2018 at 00:09):

yeah, this is a diamond problem

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 00:09):

but the real problem was decidability I think

view this post on Zulip Mario Carneiro (Jun 03 2018 at 00:09):

you have two conflicting group structures on A

view this post on Zulip Kenny Lau (Jun 03 2018 at 00:09):

and order structure?

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 00:10):

I want to use this abs >= 0 lemma

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 00:10):

a floor_ring has an order

view this post on Zulip Mario Carneiro (Jun 03 2018 at 00:10):

Why do you have two typeclasses here? that's the question

view this post on Zulip Reid Barton (Jun 03 2018 at 00:11):

In this case I think you don't need decidable_linear_ordered_comm_group

view this post on Zulip Mario Carneiro (Jun 03 2018 at 00:11):

you do, to state abs

view this post on Zulip Mario Carneiro (Jun 03 2018 at 00:11):

but you don't need the floor_ring

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 00:16):

definition abs_expansion (r : α) [decidable_linear_ordered_comm_group α]:    :=
  expansion (abs r) (abs_nonneg r)

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 00:16):

that's what the problem becomes if I remove the floor_ring

view this post on Zulip Mario Carneiro (Jun 03 2018 at 00:17):

what's expansion

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 00:17):

type mismatch at application
  expansion (abs r) _
term
  abs_nonneg r
has type
  @ge α
    (@preorder.to_has_le α
       (@partial_order.to_preorder α
          (@ordered_comm_group.to_partial_order α
             (@decidable_linear_ordered_comm_group.to_ordered_comm_group α _inst_3))))
    (@abs α _inst_3 r)
    0
but is expected to have type
  @ge α
    (@preorder.to_has_le α
       (@partial_order.to_preorder α
          (@ordered_comm_monoid.to_partial_order α
             (@ordered_cancel_comm_monoid.to_ordered_comm_monoid α
                (@ordered_semiring.to_ordered_cancel_comm_monoid α
                   (@ordered_ring.to_ordered_semiring α
                      (@linear_ordered_ring.to_ordered_ring α (@floor_ring.to_linear_ordered_ring α _inst_2))))))))
    (@abs α _inst_3 r)
    0

view this post on Zulip Mario Carneiro (Jun 03 2018 at 00:17):

Again, conflicting typeclasses

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 00:17):

definition expansion (r : α) (H : r  0) :   
| 0 := int.to_nat (floor r)
| (n + 1) := int.to_nat (floor (chomp r n))

view this post on Zulip Mario Carneiro (Jun 03 2018 at 00:17):

inst_3 in one, inst_2 in the other

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 00:17):

But it's just a decidability issue

view this post on Zulip Mario Carneiro (Jun 03 2018 at 00:18):

no it's a conflicting typeclasses issue

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 00:18):

I just want to "switch decidability on"

view this post on Zulip Mario Carneiro (Jun 03 2018 at 00:18):

I assume you don't care about classical?

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 00:18):

right

view this post on Zulip Mario Carneiro (Jun 03 2018 at 00:18):

just local instance decidable_prop

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 00:18):

This is stuff for mathematicians

view this post on Zulip Mario Carneiro (Jun 03 2018 at 00:20):

Maybe you should just do this over \R instead of A

view this post on Zulip Mario Carneiro (Jun 03 2018 at 00:20):

or else use the noncomputable floor instance for archimedean A

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 00:21):

example (α : Type) [floor_ring α] : add_comm_group α := by apply_instance
example (α : Type) [floor_ring α] : linear_order α := by apply_instance

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 00:25):

I am a complete idiot

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 00:25):

I should just be proving a junk theorem

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 00:26):

I was defining decimal expansions of real numbers

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 00:26):

and being fussy about issues with negative numbers

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 00:27):

I should just let the function return some random result if the input is negative and then stop fussing

view this post on Zulip Kenny Lau (Jun 03 2018 at 00:28):

57

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 00:28):

I can't believe I'm going to prove a junk theorem

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 00:28):

I feel dirty

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 00:29):

This is the problem

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 00:29):

definition expansion (r : α) (H : r  0) :   
| 0 := int.to_nat (floor r)
| (n + 1) := int.to_nat (floor (chomp r n))

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 00:29):

I just have to drop H

view this post on Zulip Mario Carneiro (Jun 03 2018 at 00:30):

It's not even used

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 00:30):

and coerce a negative integer into nat

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 00:30):

that's not the point Mario

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 00:30):

it's all part of the mathematician's promise

view this post on Zulip Mario Carneiro (Jun 03 2018 at 00:30):

That goes in theorems, not definitions

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 00:30):

we don't quite model things in the same way

view this post on Zulip Mario Carneiro (Jun 03 2018 at 00:31):

I have never seen a mathematician write a function that has an additional proof argument

view this post on Zulip Mario Carneiro (Jun 03 2018 at 00:31):

I think they would have a hard time even understanding what that means

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 00:31):

It's not even used

it should be there on moral grounds

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 00:32):

there should be some tactic bringing it along

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 00:33):

"mathematicians promise that they will not run this programme on negative numbers"

view this post on Zulip Kenny Lau (Jun 03 2018 at 00:33):

@kevin just treat it like how you treat nat.sub

view this post on Zulip Mario Carneiro (Jun 03 2018 at 00:33):

You could use roption for partial functions too

view this post on Zulip Kenny Lau (Jun 03 2018 at 00:33):

"subtraction with a star"

view this post on Zulip Mario Carneiro (Jun 03 2018 at 00:34):

alternatively, you could actually make sense of expansions of negative numbers

view this post on Zulip Mario Carneiro (Jun 03 2018 at 00:34):

which of course makes perfect sense and generates p-adic numbers

view this post on Zulip Mario Carneiro (Jun 03 2018 at 00:35):

or two's complement for the CS folks

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 00:36):

It's not even used

It's used in int.to_nat

view this post on Zulip Mario Carneiro (Jun 03 2018 at 00:37):

Yet more alternatively, don't define it as a function, have an existence theorem

view this post on Zulip Mario Carneiro (Jun 03 2018 at 00:37):

the inverse to this is a lot easier to state

view this post on Zulip Mario Carneiro (Jun 03 2018 at 00:42):

def expansion (r : α) (n : ℕ) : ℕ :=
⌊r * (10 ^ n : ℕ)⌋.nat_mod 10

view this post on Zulip Mario Carneiro (Jun 03 2018 at 00:43):

I'm not sure why n is a nat here, there are both negative and positive exponent terms in the expansion

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 01:18):

least upper bounds etc as predicates are already there: https://github.com/leanprover/mathlib/blob/master/order/bounds.lean

I see that I did mine a different way around to you. I defined is_LUB x S and you is_lub S x. Is there a preference for yours over mine? I chose "x S" because I would say x before S ("x is a least upper bound for S")

view this post on Zulip Mario Carneiro (Jun 03 2018 at 01:20):

yes, this allows you to view is_lub S as a predicate by currying

view this post on Zulip Mario Carneiro (Jun 03 2018 at 01:21):

generally speaking, more "parameter" like things should come first

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 01:24):

I'm far more likely to be fixing S and trying various x's than I am to be fixing an x and seeing if it bounds any S's, this seems far more unlikely to occur in practice

view this post on Zulip Mario Carneiro (Jun 03 2018 at 01:30):

that's why I said that

view this post on Zulip Mario Carneiro (Jun 03 2018 at 01:30):

S is the parameter, x is the variable

view this post on Zulip Mario Carneiro (Jun 03 2018 at 01:30):

so S comes first

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 13:56):

that's why I said that

I know, I was just translating you into maths

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 22:53):

Hey @Kenny Lau

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 22:53):

I was playing with sups

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 22:54):

what do you think this is:

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 22:54):

⟨λ u Hu, let s,Hs,t,Ht,Hu := Hu in by rw Hu;exact add_le_add (HSb.1 s Hs) (HTc.1 t Ht),
 λ d Hd,add_le_of_le_sub_right $ HSb.2 (d - c) (λ s Hs,le_sub.1 ((λ s₁ Hs₁,HTc.2 _ (λ t Ht,le_sub_left_of_add_le $ Hd _ s₁,Hs₁,t,Ht,rfl -- the proof
   )) s Hs))

view this post on Zulip Kenny Lau (Jun 03 2018 at 22:54):

my constructive proof?

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 22:54):

right

view this post on Zulip Kenny Lau (Jun 03 2018 at 22:54):

yay

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 22:55):

here's an even better version

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 22:55):

I wrote it twice

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 22:55):

second time looked like this

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 22:55):

theorem lub_add'' (S T : set ) (b c : ) (HSb : is_lub S b) (HTc : is_lub T c) : is_lub (S + T) (b + c) :=
⟨λ u Hu, let s,Hs,t,Ht,Hu := Hu in by rw Hu;exact add_le_add (HSb.1 s Hs) (HTc.1 t Ht),
λ d Hd,add_le_of_le_sub_right $ HSb.2 _ $ λ s Hs,le_sub.1 $ HTc.2 _ $ λ t Ht,le_sub_left_of_add_le $ Hd _ s,Hs,t,Ht,rfl

view this post on Zulip Kenny Lau (Jun 03 2018 at 22:55):

more dollar signs?

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 22:55):

instance : has_add (set ℝ) := ⟨λ S T,{u | ∃ (s ∈ S) (t ∈ T), u = s + t}⟩

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 22:56):

import order.bounds

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 22:56):

and analysis.real

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 22:56):

and it will run

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 22:56):

I couldn't get that stupid triangle thing to work on the first line of the proof

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 22:56):

the \t triangle that Patrick and I both dread

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 22:57):

so I have to use rw;exact :-)

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 22:57):

so that can be golfed a bit more

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 22:57):

but the proof the other way I was extremely pleased with :-)

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 22:57):

I formulated the theorem

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 22:57):

I proved it in tactic mode

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 22:58):

I then translated my tactic mode proof into term mode

view this post on Zulip Kenny Lau (Jun 03 2018 at 22:58):

nice!

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 22:58):

and then I started again and proved it in term mode

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 22:58):

from scratch

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 22:58):

looking at my old term mode proof for hints about which arithmetic functions to use :-)

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 23:01):

in that last proof line, Lean was somehow always "on the last term" -- I never had to fill in a hole with a non-zero number of characters to the right of it (other than the close bracket)

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 23:01):

Kenny if you had given me that answer I would have had a hard time marking it.

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 23:02):

I mean the lambda

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 23:02):

it's become unreadable, right?

view this post on Zulip Kenny Lau (Jun 03 2018 at 23:02):

lol

view this post on Zulip Kenny Lau (Jun 03 2018 at 23:02):

but you can verify it

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 23:03):

that is a very different thing from understanding it


Last updated: May 10 2021 at 08:14 UTC