The real numbers

Stream: maths

[Kevin Buzzard]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

we mean that it exists

[Kevin Buzzard]

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

[Kenny Lau]

is R[ε] Dedekind-complete?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Andrew Ashworth]

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

[Kevin Buzzard]

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

[Kenny Lau]

I already proved the IVT ^^

[Kevin Buzzard]

Where Kenny?

[Kenny Lau]

in my own construction of the real numbers

[Kenny Lau]

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

[Andrew Ashworth]

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!)

[Andrew Ashworth]

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

[Kevin Buzzard]

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

[Kenny Lau]

no

[Kevin Buzzard]

Is it in mathlib?

[Kenny Lau]

no idea

[Andrew Ashworth]

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

[Johannes Hölzl]

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

[Johannes Hölzl]

and a lot of other people

[Johannes Hölzl]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

because even though infinity isn't a real number

[Johannes Hölzl]

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

[Kevin Buzzard]

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

[Johannes Hölzl]

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

[Johannes Hölzl]

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

[Johannes Hölzl]

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.

[Kevin Buzzard]

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?

[Kevin Buzzard]

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

[Kevin Buzzard]

that you are a Dedekind complete ordered field

[Kevin Buzzard]

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

[Kevin Buzzard]

Did you all do that?

[Mario Carneiro]

Uniqueness is overrated

[Kevin Buzzard]

rofl

[Kevin Buzzard]

you people

[Kevin Buzzard]

you don't understand equality

[Mario Carneiro]

It's really not needed for anything practical though

[Mario Carneiro]

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

[Kevin Buzzard]

it's needed for clear thinking

[Kevin Buzzard]

and so we have to teach it to computers

[Kevin Buzzard]

it makes the world a simpler place

[Mario Carneiro]

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

[Mario Carneiro]

a uniqueness statement doesn't help here

[Kevin Buzzard]

I just mean you can port theorems with the uniqueness statement

[Mario Carneiro]

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

[Kevin Buzzard]

I want to do more than port theorems

[Kevin Buzzard]

I want to identify them as one

[Mario Carneiro]

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

[Kenny Lau]

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)

[Kenny Lau]

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

[Kevin Buzzard]

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

[Kenny Lau]

we won't be constructing other real numbers

[Kenny Lau]

so I don't see why uniqueness is important

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kenny Lau]

i just did it for myself

[Mario Carneiro]

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

[Kenny Lau]

i did it privately

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

right

[Kevin Buzzard]

and then Kenny's

[Mario Carneiro]

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

[Kenny Lau]

rip filter construction 2017-2018

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

Yes, and that theorem is still there

[Kenny Lau]

no, you need a way to construct real numbers

[Kenny Lau]

like sqrt(2)

[Kenny Lau]

and filters are hard to work with

[Kevin Buzzard]

but if Johannes had made it to that pinnacle

[Kevin Buzzard]

you would never need to think about filters any more

[Kenny Lau]

how would you make sqrt(2)?

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

and then say that you're a complete field

[Mario Carneiro]

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

[Kevin Buzzard]

Chris did exp and sin and cos

[Kevin Buzzard]

did that ever make it into mathlib?

[Kevin Buzzard]

I need that for October!

[Kenny Lau]

it's still in PR i think

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kenny Lau]

you're on the wrong thread then

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

The quote from Spivak

[Kevin Buzzard]

[not the question itself]

[Kevin Buzzard]

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

[Kenny Lau]

(removed)

[Kevin Buzzard]

up to unique isomorphism

[Kevin Buzzard]

they are _the same_

[Kevin Buzzard]

they are equal

[Kevin Buzzard]

they are maths-equivalent

[Mario Carneiro]

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

[Reid Barton]

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

[Kevin Buzzard]

Don't prove a single theorem about the reals

[Kevin Buzzard]

just prove a theorem about complete totally ordered fields?

[Reid Barton]

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

[Reid Barton]

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

[Kenny Lau]

that one is mul_one :P

[Kevin Buzzard]

norm_num ftw

[Reid Barton]

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

[Kenny Lau]

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

[Reid Barton]

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

[Mario Carneiro]

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

[Reid Barton]

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

[Reid Barton]

Sure, and then norm_num can do that for you

[Kenny Lau]

so I said it's mul_one

[Andrew Ashworth]

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

[Kevin Buzzard]

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

[Kenny Lau]

but there is no computable version

[Mario Carneiro]

well, the current version is as computable as it gets

[Kevin Buzzard]

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

[Kevin Buzzard]

computations

[Mario Carneiro]

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

[Kenny Lau]

everything is about computation

[Kevin Buzzard]

which are of course important when you want to prove theorems

[Kevin Buzzard]

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

[Mario Carneiro]

well yes

[Kevin Buzzard]

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

[Kenny Lau]

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

[Mario Carneiro]

I did

[Andrew Ashworth]

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

[Mario Carneiro]

It's called divp

[Kevin Buzzard]

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

[Mario Carneiro]

It works on any ring

[Kenny Lau]

you won't want to formalize computable reals

[Andrew Ashworth]

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

[Kenny Lau]

are you going to set up turing machines now

[Mario Carneiro]

lol I'm actually typing out turing machines right now

[Mario Carneiro]

Actually I'm going via Wang B-machines

[Kevin Buzzard]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Kevin Buzzard]

Thanks Kenny.

[Kevin Buzzard]

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?

[Kevin Buzzard]

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

[Kevin Buzzard]

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?

[Kevin Buzzard]

Is there some priority trick?

[Mario Carneiro]

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.

[Kevin Buzzard]

I see. Thanks.

[Kevin Buzzard]

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⟩

[Kevin Buzzard]

and then

[Kevin Buzzard]

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⟩

[Kevin Buzzard]

That's the same code again!

[Mario Carneiro]

sure is, less than 30 seconds copy paste work

[Kevin Buzzard]

That should be by math_trivial [add_lim_zero]

[Kevin Buzzard]

and then by math_trivial [neg_lim_zero]

[Mario Carneiro]

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

[Mario Carneiro]

6 or 7 times is not enough

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

"we laboriously transport structure"

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

Would this math_trivial tactic apply equally to real and pnat?

[Kevin Buzzard]

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

[Kevin Buzzard]

I found myself when doing schemes

[Kevin Buzzard]

wanting a tactic like this

[Kevin Buzzard]

and I know that when I start perfectoids

[Kevin Buzzard]

I'll find it again

[Mario Carneiro]

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

[Kevin Buzzard]

yeah isn't that interesting

[Kenny Lau]

lol

[Kenny Lau]

Kevin

[Kenny Lau]

the sky is blue

[Kevin Buzzard]

These guys need to make a proper mathematician

[Kevin Buzzard]

with the right kind of equals

[Kenny Lau]

it's foggy

[Kenny Lau]

relative humidity 98%

[Kevin Buzzard]

/- 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

[Kevin Buzzard]

Why do they make life better?

[Kevin Buzzard]

This is all in data/real/basic.lean

[Kenny Lau]

because beneath you is an uncomputable instance

[Kevin Buzzard]

those are the best kind IMO

[Kenny Lau]

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

[Kenny Lau]

so your definitions would have to be noncomputable

[Kenny Lau]

and it is used because it is declared the latest

[Kevin Buzzard]

none of this makes any sense to me

[Mario Carneiro]

no, that's not related

[Mario Carneiro]

those instances

short-circuit type class resolution

[Kevin Buzzard]

so they are creating new paths in the system

[Kenny Lau]

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

[Kevin Buzzard]

which are defeq to longer paths

[Mario Carneiro]

yes

[Kevin Buzzard]

and this is perhaps making the system better for some reason

[Kevin Buzzard]

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

[Mario Carneiro]

it means less time traversing the instance graph

[Kevin Buzzard]

then it would be much less time

[Mario Carneiro]

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

[Kevin Buzzard]

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))⟩⟩

[Kevin Buzzard]

They're getting quite tricky for my tactic now

[Mario Carneiro]

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

[Kevin Buzzard]

ha ha

[Mario Carneiro]

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

[Mario Carneiro]

so I set up the system to make that easier

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

I liked @Reid Barton 's comment about typeclasses.

[Kevin Buzzard]

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

[Kevin Buzzard]

You prefer yours?

[Kevin Buzzard]

@ and _ are a bit ugly maybe

[Kevin Buzzard]

but yours is shorter

[Mario Carneiro]

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

[Kevin Buzzard]

What is your preference? The mathlib one?

[Mario Carneiro]

I don't have a strong preference

[Kevin Buzzard]

In terms of Lean they're all presumably defeq

[Kevin Buzzard]

but in terms of readability some have more worth than others

[Mario Carneiro]

they are all syntactically equal

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

You've gone the wrong way

[Kevin Buzzard]

you can do has_le first and get has_lt for free!

[Mario Carneiro]

I know

[Kevin Buzzard]

You did it this way for a reason, presumably?

[Mario Carneiro]

the constructively natural one is lt

[Kevin Buzzard]

I see

[Kevin Buzzard]

it's all about computing

[Mario Carneiro]

it states that there is some epsilon separating them

[Mario Carneiro]

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

[Patrick Massot]

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"

[Patrick Massot]

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.

[Kevin Buzzard]

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 :-)

[Kevin Buzzard]

does Lean have decimal expansions??

[Kevin Buzzard]

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

[Kevin Buzzard]

with f(succ n)<=9

[Kenny Lau]

you can write that yourself

[Kenny Lau]

it's quite explicit using floor

[Kevin Buzzard]

you are right!

[Kenny Lau]

given a real number r

[Kevin Buzzard]

But I was just asking if someone had already written it

[Kevin Buzzard]

Kenny I can do it :-)

[Kevin Buzzard]

I even lecture it in M1F some years

[Kevin Buzzard]

Darn it

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kenny Lau]

Kevin

[Kenny Lau]

the fllor is there already

[Kevin Buzzard]

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

[Kenny Lau]

it's in archimedean

[Kevin Buzzard]

Thanks

[Kevin Buzzard]

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

[Kevin Buzzard]

Mario has answered this before

[Kevin Buzzard]

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

[Kenny Lau]

it's just a typeclass fallout

[Kevin Buzzard]

right

[Kevin Buzzard]

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

[Kenny Lau]

no idea

[Kevin Buzzard]

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

[Kevin Buzzard]

⌊10 / 3⌋ : ℤ

[Kevin Buzzard]

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

[Kevin Buzzard]

100% CPU usage!

[Mario Carneiro]

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

[Kevin Buzzard]

segv :-)

[Mario Carneiro]

I've seen this many times before

[Kevin Buzzard]

but it's only with reals

[Kevin Buzzard]

Lean is really good with most structures

[Kevin Buzzard]

Oh indpt of reals?

[Mario Carneiro]

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

[Kevin Buzzard]

I know

[Kevin Buzzard]

I assumed the problem was because reals always time out

[Kevin Buzzard]

but maybe you fixed that

[Kevin Buzzard]

and this is an independent timeout

[Mario Carneiro]

The major source of that was fixed a while ago

[Mario Carneiro]

this is just Z -> N timeout

[Kevin Buzzard]

What do you get with

[Kevin Buzzard]

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

[Mario Carneiro]

something horrible, don't do that

[Mario Carneiro]

What part of noncomputable don't you understand?

[Kevin Buzzard]

:-)

[Kevin Buzzard]

I thought there was no harm trying

[Mario Carneiro]

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

[Kevin Buzzard]

after all, schoolkid can do it

[Kevin Buzzard]

it's 1 Mario

[Mario Carneiro]

You can do it, but not like this

[Mario Carneiro]

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

[Kevin Buzzard]

this is going to be tough to explain to the mathematicians

[Kevin Buzzard]

I'm just being daft, I know about eval

[Mario Carneiro]

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

[Mario Carneiro]

#eval won't do any better

[Kevin Buzzard]

no but it could

[Mario Carneiro]

actually it will just complain up front

[Mario Carneiro]

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

[Kevin Buzzard]

the reduce gives me a segv (twice now)

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

That statement doesn't make sense

[Mario Carneiro]

noncomputability is a property of a term, not its denotation

[Kenny Lau]

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

[Kenny Lau]

it ain't no sheaf

[Kevin Buzzard]

is the obstruction finite?

[Mario Carneiro]

?

[Kenny Lau]

floor is computable iff halting problem can be solved

[Kenny Lau]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

So do that

[Kenny Lau]

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

[Kevin Buzzard]

so it can be computed in this case

[Kevin Buzzard]

Kenny -- doesn't it?

[Mario Carneiro]

floor (sqrt 2) is a computable number, yes

[Mario Carneiro]

but floor is not a computable function

[Mario Carneiro]

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

[Kenny Lau]

you need uniform computability without creativeness

[Kenny Lau]

informally

[Kenny Lau]

you need a canonical function

[Kevin Buzzard]

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

[Kenny Lau]

that works across everything

[Kevin Buzzard]

floor is daft. Give me exp any day

[Kevin Buzzard]

Is that computable?

[Mario Carneiro]

By the way, floor is computable on algebraic numbers

[Kevin Buzzard]

I reckon I can prove the sequence is Cauchy

[Kenny Lau]

everything is computable on algebraic numbers

[Mario Carneiro]

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

[Kenny Lau]

surprise

[Mario Carneiro]

exp is computable

[Kevin Buzzard]

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

[Kenny Lau]

I was uttering hyperbole

[Kevin Buzzard]

and so of the algebraic numbers

[Mario Carneiro]

I think real numbers are overrated in math

[Kenny Lau]

agree

[Kevin Buzzard]

They're just some random completion

[Kenny Lau]

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

[Kevin Buzzard]

that sometimes helps in physics

[Kevin Buzzard]

exactly

[Mario Carneiro]

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

[Kenny Lau]

but there's a problem @Mario Carneiro

[Kevin Buzzard]

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

[Mario Carneiro]

something like complete under computable sequences is more than enough

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

I'm sure it uses AC everywhere

[Kenny Lau]

I can't recall the name of the theroem

[Mario Carneiro]

it's not so different to doing categories in ZFC

[Kenny Lau]

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

[Kenny Lau]

algebraic numbers and exp

[Kenny Lau]

maybe some other things

[Kenny Lau]

maybe you'll know the name

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kenny Lau]

that's irrelevant

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

decidable equality doesn't mean decidable pi equality

[Kenny Lau]

pi equality meaning forall equality

[Kenny Lau]

not 3.14159

[Mario Carneiro]

I know, but rationality is decidable on algebraic numbers

[Kenny Lau]

oh is it

[Kenny Lau]

how do you define algebraic numbers?

[Mario Carneiro]

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

[Kenny Lau]

do you store the minimal polynomial?

[Mario Carneiro]

yes

[Kenny Lau]

I see

[Mario Carneiro]

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

[Kenny Lau]

agree

[Kevin Buzzard]

come on norm-num

[Kevin Buzzard]

↑⌊0⌋ * 10 = 0

[Kevin Buzzard]

you can do it

[Kevin Buzzard]

gaargh

[Kevin Buzzard]

stupid floor function

[Kevin Buzzard]

oh there is a lemma

[Kevin Buzzard]

I remember now

[Kevin Buzzard]

floor_coe

[Mario Carneiro]

I guess floor_zero and floor_one should be simp lemmas

[Mario Carneiro]

and theorems

[Kevin Buzzard]

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

[Kevin Buzzard]

that one of your other zeros

[Mario Carneiro]

it's defeq though, you can just apply floor_coe

[Kevin Buzzard]

not in a rewrite :-/

[Mario Carneiro]

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]

[Kenny Lau]

that one of your other zeros

lol

[Mario Carneiro]

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

[Mario Carneiro]

because the two 2's are represented differently

[Kevin Buzzard]

I've got interested in what needs names

[Kevin Buzzard]

I would vote for floor_zero

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

and you have to copy paste

[Mario Carneiro]

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

[Kevin Buzzard]

I know archimedean.lean so I could fix it up

[Kevin Buzzard]

I've been reading some of the real code recently

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

I was just thinking I should do the same

[Kevin Buzzard]

but for me it's much harder

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kenny Lau]

does that mean you finished Q1?

[Mario Carneiro]

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

[Kevin Buzzard]

no

[Kevin Buzzard]

I liked Q2 better

[Kevin Buzzard]

right

[Mario Carneiro]

also, the theorem you stated is false

[Mario Carneiro]

the floor of s is zero

[Kevin Buzzard]

:-)

[Kevin Buzzard]

oh too many 10s

[Kevin Buzzard]

sorry

[Kevin Buzzard]

I have to work out the full decimal expansion

[Kevin Buzzard]

so i need a fair few floors

[Mario Carneiro]

You really want to do this on rat

[Mario Carneiro]

then you can just compute

[Mario Carneiro]

just take your real number and map it to rat

[Kevin Buzzard]

I didn't know to what extent that mattered

[Kevin Buzzard]

now I need some theorem that says that the floors agree

[Kevin Buzzard]

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

[Mario Carneiro]

I am already on it

[Kenny Lau]

by unfold s; norm_num

[Kevin Buzzard]

thanks

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

I did...

[Kevin Buzzard]

and then again in the proof

[Kevin Buzzard]

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

[Kevin Buzzard]

what do you think about all this haveI stuff?

[Kevin Buzzard]

Aren't things worse than they used to be?

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

haveI is the compromise position

[Mario Carneiro]

...but it's not unreasonable here

[Mario Carneiro]

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

[Kevin Buzzard]

Thanks.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

but proof is id

[Mario Carneiro]

It's up to you

[Kevin Buzzard]

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

[Kenny Lau]

who the .... cares

[Kevin Buzzard]

it's the interface Kenny

[Kenny Lau]

proofs are irrelevant

[Kevin Buzzard]

id sometimes deserves a name :-)

[Kevin Buzzard]

proofs are irrelevant but names are important

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

I would say "use in moderation"

[Kevin Buzzard]

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

[Kevin Buzzard]

Rubbish lean code but it's a proof

[Kevin Buzzard]

What tricks am I missing?

[Kenny Lau]

le_floor?

[Kenny Lau]

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

[Kevin Buzzard]

here's the reals back to their old tricks

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

and then le_antisymm

[Kevin Buzzard]

noncomputable definition s : ℝ := 71/100

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

[Kevin Buzzard]

deterministic timeout

[Kenny Lau]

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

[Kevin Buzzard]

I did it by contradiction :-)

[Kevin Buzzard]

you always want to do things constructively

[Kenny Lau]

?

[Kenny Lau]

I see

[Kenny Lau]

to each their own

[Kenny Lau]

I have no time

[Kenny Lau]

I need to learn what the Weil group is

[Kevin Buzzard]

oh the coercion to R is done before the division

[Mario Carneiro]

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]

[Kenny Lau]

lol

[Kenny Lau]

two lines vs 100 lines

[Kevin Buzzard]

very nice

[Kevin Buzzard]

but I never got stuck

[Kevin Buzzard]

I just proved it and enjoyed it

[Kevin Buzzard]

walking around the gardens of mathematics

[Mario Carneiro]

oh you proved by contradiction

[Mario Carneiro]

that's a bit roundabout

[Kevin Buzzard]

it's inbuilt

[Kevin Buzzard]

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

[Mario Carneiro]

you have so many cases in this proof...

[Kevin Buzzard]

and about 80 did it

[Kenny Lau]

really

[Kevin Buzzard]

and 79 did it by contradiction

[Kenny Lau]

such a simple theorem

[Kenny Lau]

only 80 out of 250

[Kevin Buzzard]

it's about that

[Kevin Buzzard]

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

[Kenny Lau]

@Mario Carneiro and the 1 is me lol

[Kevin Buzzard]

maybe more

[Mario Carneiro]

I recall this story

[Kenny Lau]

like seriously

[Kenny Lau]

the UMPs of sup is all you need

[Kevin Buzzard]

contradiction is the most powerful method of proof

[Kevin Buzzard]

you get to assume the most stuff

[Kenny Lau]

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

[Kenny Lau]

rounded down to the nearest percent

[Mario Carneiro]

I'm not even against it on intuitionistic grounds

[Kevin Buzzard]

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

[Kenny Lau]

cleansed

[Mario Carneiro]

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

[Kevin Buzzard]

right

[Kevin Buzzard]

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

[Kevin Buzzard]

people writing

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

because it's what it is

[Kenny Lau]

it's the UMP

[Kevin Buzzard]

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

[Kevin Buzzard]

"

[Kenny Lau]

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

[Mario Carneiro]

For things like timed tests it's a good strategy

[Kenny Lau]

I find UMPs easier

[Mario Carneiro]

where you just write and write until you get the answer

[Kenny Lau]

I just use 100 UMPs until I get the answer

[Kenny Lau]

and I always get it

[Kenny Lau]

because it's universal

[Mario Carneiro]

Also resolution theorem proving is based on this idea

[Kenny Lau]

solve_by_elim ain't

[Mario Carneiro]

where you whittle down a counterexample until it is impossible

[Mario Carneiro]

but the resulting proof looks ugly I think

[Kenny Lau]

(whatever)

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kenny Lau]

so don't unfold them?

[Kevin Buzzard]

norm_num times out too

[Kenny Lau]

did you use div lemmas?

[Kenny Lau]

div_nonneg

[Kevin Buzzard]

oh I need to feed those in

[Kenny Lau]

you just need that one

[Kenny Lau]

the rest should be norm_num

[Kevin Buzzard]

do I put it in the context?

[Kenny Lau]

no, you apply it

[Kevin Buzzard]

you want me to actually prove it by hand??

[Kevin Buzzard]

what is this -- the 1980s?

[Kevin Buzzard]

we have norm_num!

[Kenny Lau]

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

[Kevin Buzzard]

refine div_nonneg _ _, times out

[Kevin Buzzard]

everything times out

[Kevin Buzzard]

my goal is corrupted

[Kenny Lau]

code

[Kevin Buzzard]

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

[Kevin Buzzard]

all this fuss about 0.71

[Kevin Buzzard]

I should have been in bed hours ago

[Kevin Buzzard]

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

[Kevin Buzzard]

it was only a 2 hour exam

[Kenny Lau]

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

[Mario Carneiro]

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

[Kevin Buzzard]

So using rat.cast_floor was a bad idea

[Kevin Buzzard]

Even though my instinct is to get out of R ASAP

[Kenny Lau]

there's a box

[Mario Carneiro]

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

[Kenny Lau]

think out of it

[Kenny Lau]

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

[Mario Carneiro]

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

[Kenny Lau]

lol

[Kenny Lau]

71 is too big for the kernel

[Kenny Lau]

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

[Mario Carneiro]

that's VM computation though

[Mario Carneiro]

or would be if it were lean

[Mario Carneiro]

python doesn't have to bother proving it is correct

[Mario Carneiro]

and it also doesn't use a braindead representation

[Kevin Buzzard]

Kenny I did it:

[Kevin Buzzard]

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

[Kevin Buzzard]

0.71 has no 8's in its decimal expansion

[Johan Commelin]

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

Would it help if we compute in base $r$ (with $r = 10$ or $16$)? 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

[Johan Commelin]

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

[Johan Commelin]

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.

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

well, those last two don't matter anyway

[Mario Carneiro]

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

[Mario Carneiro]

because computable reals are not like regular reals

[Johan Commelin]

I am not suggesting that rnum be computable

[Johan Commelin]

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

[Mario Carneiro]

That's the whole point

[Mario Carneiro]

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

[Johan Commelin]

Right

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

so there are valid reasons to keep both around

[Mario Carneiro]

nat is actually the faster one in the VM, because lean replaces it with GMP bignums or C ints if small enough

[Mario Carneiro]

while num is just a regular inductive type so it's implemented as a linked list of digits

[Mario Carneiro]

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

[Johan Commelin]

Yes, I understand. So, are things like Karatsuba or Tom-Cook implemented for num?

[Mario Carneiro]

If you are using norm_num or simp, you want VM-efficient data types

[Mario Carneiro]

No, the numbers have not got that big (yet)

[Mario Carneiro]

That requires significant size before it pays off

[Johan Commelin]

I guess another problem is that for big numbers the conversion between nat and num will become the bottle-neck. Right?

[Mario Carneiro]

You can't do anything that even mentions nat in the kernel with big numbers

[Mario Carneiro]

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

[Johan Commelin]

O.o (-;

[Mario Carneiro]

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

[Johan Commelin]

Ok, I don't follow this anymore... but I think it means that I can relax (-;

[Mario Carneiro]

You just have theorems saying bit0 \u x = \u bit0 x where \u : nat -> num

[Johan Commelin]

I thought that the VM cheated... and you would lose verification

[Mario Carneiro]

and you have a tactic (running in the VM) that selectively chooses to apply this theorem

[Mario Carneiro]

by looking at the term in the goal

[Mario Carneiro]

with regular lean functions you can only look at the value that is given, but tactics can decompose the expr that represents the value

[Mario Carneiro]

so something like bit0 (bit0 ... 1) has reasonable size as a term but not as a value

[Mario Carneiro]

and you can apply log(n) bit0 \u x = \u bit0 x theorems to get it down to a theorem just about num

[Mario Carneiro]

and then you prove by rfl or whatever

[Mario Carneiro]

and the kernel never has to evaluate big nats

[Johan Commelin]

Ok, I see the strategy.

[Johan Commelin]

I think Kevin is going to like that if at some point he wants to do some modular form stuff...

[Johan Commelin]

Because their coefficients explode

[Mario Carneiro]

So norm_num is also working in binary, I guess

[Mario Carneiro]

it produces a theorem that is longer for larger numbers though

[Mario Carneiro]

while a kernel proof is always just rfl

[Mario Carneiro]

For the most part, kernel computation is discouraged because it's not particularly optimized for that

[Mario Carneiro]

But I think it's amusing that in dependent type theory you can write down a very short proof of almost anything

[Johan Commelin]

What do you mean with that last statement?

[Mario Carneiro]

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

[Johan Commelin]

Right, but that proof will require a lot of prerequisite work

[Johan Commelin]

(Which I consider part of the proof.)

[Mario Carneiro]

The only work that needs to be done is the setup, stating the problem

[Mario Carneiro]

the "hard part" is completely absent from the accounting, except in the length bound

[Mario Carneiro]

but I can write functions that grow ridiculously fast in DTT so that's not saying much

[Johan Commelin]

Ok, so we can prove that RH doesn't have a short proof.

[Johan Commelin]

And neither has Fermat's Last Theorem

[Mario Carneiro]

Okay, fermat is a good example, since we know that one is true

[Johan Commelin]

For otherwise they would already have been in mathlib with a rfl proof.

[Mario Carneiro]

I can prove Fermat's last theorem by rfl

[Johan Commelin]

I would love to see that done.

[Johan Commelin]

The statement is already there

[Johan Commelin]

And that is all the setup you need.

[Mario Carneiro]

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

[Johan Commelin]

Right. And of course Lean will never finish running.

[Mario Carneiro]

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

[Mario Carneiro]

Of course the problem with this kind of analysis is that lean will run (almost) forever on such a proof

[Mario Carneiro]

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

[Johan Commelin]

Yes, and that's why we still dont have FLT in mathlib (-;

[Johan Commelin]

No, but compile-time is still a good measure

[Mario Carneiro]

Yes. Or number of proof steps including definitional reductions

[Mario Carneiro]

This doesn't come up in ZFC since there's no definitional reduction, what you see is what you get

[Mario Carneiro]

anyway, this "feature" of DTT should be thought of as abuse of lean, so don't be surprised if it starts to sweat

[Mario Carneiro]

when you try to #reduce 71 / 100

[Johan Commelin]

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.

[Mario Carneiro]

I think there are some pretty reasonable upper bounds based on physical considerations

[Mario Carneiro]

i.e. the proof appears to fit in the universe, so it's shorter than Graham's number

[Johan Commelin]

ok, fair enough

[Johan Commelin]

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?

[Kevin Buzzard]

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.

[Kevin Buzzard]

@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

[Johan Commelin]

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.

[Johan Commelin]

Or can we have multiple instances, depending on whether r has type nat or int or rat or real.

[Kevin Buzzard]

this is exactly the problem with pow

[Johan Commelin]

@Kevin Buzzard Isn't Sup already on line 316 of data.real.basic?

[Kevin Buzzard]

Chris Hughes wrote exp : C -> C but it's still not in mathlib

[Kevin Buzzard]

That's CS sup

[Kevin Buzzard]

sup(S)+sup(T) = sup(S+T) is not true for that sup

[Kevin Buzzard]

let S have one element and let T be empty

[Kevin Buzzard]

(deleted)

[Kevin Buzzard]

it returns 37 if the set has no sup

[Kevin Buzzard]

This is philosophy not mathematics

[Kevin Buzzard]

but if you're going to define sup globally

[Kevin Buzzard]

then it should be taking values in -infty + R + infty

[Kevin Buzzard]

not just spewing out 37s when it's stuck

[Kevin Buzzard]

You see how my predicate solves this problem?

[Kevin Buzzard]

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

[Johan Commelin]

Ok, so I read too quickly (-;

[Kevin Buzzard]

My question is how to formalize that statement in mathlib

[Kevin Buzzard]

and my predicates make it look nice and easy

[Kevin Buzzard]

whereas I can't quite do it with what we have

[Kevin Buzzard]

however I am unclear about whether "what I want as someone who wants to formulate elementary lemmas about sup"

[Kevin Buzzard]

has anything to do with "what should be in mathlib"

[Kevin Buzzard]

I am very unclear about what the boundaries of mathlib are

[Kevin Buzzard]

Look, watch this:

[Kevin Buzzard]

@Mario Carneiro -- should I put schemes in mathlib? Let me know. I don't care either way but you never answer

[Kevin Buzzard]

he never answers

[Kevin Buzzard]

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"

[Kevin Buzzard]

"this will need some thought"

[Kevin Buzzard]

I'll try another approach

[Kevin Buzzard]

@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)

[Kevin Buzzard]

I believe @Scott Morrison thinks they should be in mathlib

[Johannes Hölzl]

least upper bounds etc as predicates are already there: https://github.com/leanprover/mathlib/blob/master/order/bounds.lean

[Sebastien Gouezel]

You can also have a look at https://github.com/leanprover/mathlib/blob/master/order/conditionally_complete_lattice.lean

[Mario Carneiro]

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

[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?

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.

[Mario Carneiro]

@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

[Mario Carneiro]

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?

[Mario Carneiro]

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

[Johan Commelin]

Ok, thanks. I will take a look at those functions.

[Johan Commelin]

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.

[Mario Carneiro]

Yes, with_top int has an addition operation and an order, and is defeq to option int

[Johan Commelin]

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.

[Johan Commelin]

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.

[Mario Carneiro]

eww

[Mario Carneiro]

that's a bit specialized

[Johan Commelin]

Ok, f(n) = infty \iff n = 0.

[Mario Carneiro]

You can define - as option.map (\lam x, -x), and b^o where o : with_bot int by cases

[Johan Commelin]

The other option is that I just use if-then-else everywhere... but I don't really like that either...

[Mario Carneiro]

no if-then

[Mario Carneiro]

it's an option, use cases

[Johan Commelin]

Right. (I meant avoiding option and just do dite (n = 0) in all the definitions.

[Johan Commelin]

(This stuff shows up everywhere in nonarchimedean valuations.)

[Mario Carneiro]

what n = 0 are you talking about?

[Mario Carneiro]

you said f returns an option

[Mario Carneiro]

well, a with_top

[Johan Commelin]

Yes, but I could also define f on pnat, and g with a dite.

[Johan Commelin]

Right?

[Mario Carneiro]

Oh, I misunderstood your iff statement

[Johan Commelin]

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?

[Mario Carneiro]

It's already there

[Johan Commelin]

Hmm, for with_bot I only see instances for partial orders and lattices. Not for semigroups.

[Mario Carneiro]

There is with_zero also, there are lots of ways to construe the added element in all the structures

[Mario Carneiro]

Oh, I see, with_top and with_bot are actually the same as add_semigroups

[Johan Commelin]

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.

[Johan Commelin]

Oh, I see, with_top and with_bot are actually the same as add_semigroups

Yes, but not as ordered add_semigroups.

[Mario Carneiro]

Yeah, I'll work on that

[Reid Barton]

@Johan Commelin see https://gist.github.com/rwbarton/599327954b01b2e840894189981172ea

[Mario Carneiro]

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

[Reid Barton]

I gave that to Kevin earlier and I think he has improved it some in the Fibonacci project

[Johan Commelin]

Yes, or f 0 = infty. And then you would be done.

[Johan Commelin]

Reid, thanks. I'll take a look.

[Mario Carneiro]

Then the valuation function is defined by cases on n

[Mario Carneiro]

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

[Mario Carneiro]

I'm a bit worried about having to coerce all the time though

[Kevin Buzzard]

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

[Kevin Buzzard]

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:

[Kevin Buzzard]

I'm going to do perfectoid spaces because I think it would be funny to do them

[Kevin Buzzard]

Some scheme stuff we will need e.g. sheaves

[Kevin Buzzard]

but I was thinking about re-doing it

[Kevin Buzzard]

doing it all for a second time in a perfectoid spaces directory

[Kevin Buzzard]

and this time doing it better and checking with people like Mario along the way as to whether the structures looked sensible

[Kevin Buzzard]

I understand now much better what I can do well and what I do badly

[Kevin Buzzard]

and especially what I do so badly that it will take a lot of time to fix

[Kevin Buzzard]

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

[Mario Carneiro]

I thnk that's a good plan

[Kevin Buzzard]

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

[Kevin Buzzard]

so for example we will need sheaves of types at some point

[Kevin Buzzard]

and when we need them in the perfectoid theory I will revisit what I did for schemes

[Mario Carneiro]

The second time around you will have a much better appreciation for the subtleties and design questions and can do it right

[Kevin Buzzard]

(in fact we did these already and I even have a suggested definition from Mario somewhere in my starred messages)

[Kevin Buzzard]

yes -- second time round much better

[Mario Carneiro]

Not to mention you are a better lean programmer now than last month (and the month before that etc)

[Kevin Buzzard]

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"

[Kevin Buzzard]

"and write a proper interface while we're here"

[Kevin Buzzard]

so it's partly some random repo with random bits of people's papers formalised

[Kevin Buzzard]

and then some directory called "mathlib_someday"

[Mario Carneiro]

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

[Kevin Buzzard]

where we put files where someone has actually made an effort to make the file mathlib-worthy

[Kevin Buzzard]

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.

[Scott Morrison]

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

[Scott Morrison]

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. :-)

[Kevin Buzzard]

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

[Kevin Buzzard]

My understanding of something Reid said a few days ago about the reals

[Kenny Lau]

diamond of death?

[Kevin Buzzard]

was that I shouldn't be proving things about the reals

[Kevin Buzzard]

I should just demand I'm a complete totally ordered field and deduce everything from that

[Mario Carneiro]

yeah, this is a diamond problem

[Kevin Buzzard]

but the real problem was decidability I think

[Mario Carneiro]

you have two conflicting group structures on A

[Kenny Lau]

and order structure?

[Kevin Buzzard]

I want to use this abs >= 0 lemma

[Kevin Buzzard]

a floor_ring has an order

[Mario Carneiro]

Why do you have two typeclasses here? that's the question

[Reid Barton]

In this case I think you don't need decidable_linear_ordered_comm_group

[Mario Carneiro]

you do, to state abs

[Mario Carneiro]

but you don't need the floor_ring

[Kevin Buzzard]

definition abs_expansion (r : α) [decidable_linear_ordered_comm_group α]: ℕ → ℕ :=
  expansion (abs r) (abs_nonneg r)

[Kevin Buzzard]

that's what the problem becomes if I remove the floor_ring

[Mario Carneiro]

what's expansion

[Kevin Buzzard]

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

[Mario Carneiro]

Again, conflicting typeclasses

[Kevin Buzzard]

definition expansion (r : α) (H : r ≥ 0) : ℕ → ℕ
| 0 := int.to_nat (floor r)
| (n + 1) := int.to_nat (floor (chomp r n))

[Mario Carneiro]

inst_3 in one, inst_2 in the other

[Kevin Buzzard]

But it's just a decidability issue

[Mario Carneiro]

no it's a conflicting typeclasses issue

[Kevin Buzzard]

I just want to "switch decidability on"

[Mario Carneiro]

I assume you don't care about classical?

[Kevin Buzzard]

right

[Mario Carneiro]

just local instance decidable_prop

[Kevin Buzzard]

This is stuff for mathematicians

[Mario Carneiro]

Maybe you should just do this over \R instead of A

[Mario Carneiro]

or else use the noncomputable floor instance for archimedean A

[Kevin Buzzard]

example (α : Type) [floor_ring α] : add_comm_group α := by apply_instance
example (α : Type) [floor_ring α] : linear_order α := by apply_instance

[Kevin Buzzard]

I am a complete idiot

[Kevin Buzzard]

I should just be proving a junk theorem

[Kevin Buzzard]

I was defining decimal expansions of real numbers

[Kevin Buzzard]

and being fussy about issues with negative numbers

[Kevin Buzzard]

I should just let the function return some random result if the input is negative and then stop fussing

[Kenny Lau]

57

[Kevin Buzzard]

I can't believe I'm going to prove a junk theorem

[Kevin Buzzard]

I feel dirty

[Kevin Buzzard]

This is the problem

[Kevin Buzzard]

definition expansion (r : α) (H : r ≥ 0) : ℕ → ℕ
| 0 := int.to_nat (floor r)
| (n + 1) := int.to_nat (floor (chomp r n))

[Kevin Buzzard]

I just have to drop H

[Mario Carneiro]

It's not even used

[Kevin Buzzard]

and coerce a negative integer into nat

[Kevin Buzzard]

that's not the point Mario

[Kevin Buzzard]

it's all part of the mathematician's promise

[Mario Carneiro]

That goes in theorems, not definitions

[Kevin Buzzard]

we don't quite model things in the same way

[Mario Carneiro]

I have never seen a mathematician write a function that has an additional proof argument

[Mario Carneiro]

I think they would have a hard time even understanding what that means

[Kevin Buzzard]

It's not even used

it should be there on moral grounds

[Kevin Buzzard]

there should be some tactic bringing it along

[Kevin Buzzard]

"mathematicians promise that they will not run this programme on negative numbers"

[Kenny Lau]

@kevin just treat it like how you treat nat.sub

[Mario Carneiro]

You could use roption for partial functions too

[Kenny Lau]

"subtraction with a star"

[Mario Carneiro]

alternatively, you could actually make sense of expansions of negative numbers

[Mario Carneiro]

which of course makes perfect sense and generates p-adic numbers

[Mario Carneiro]

or two's complement for the CS folks

[Kevin Buzzard]

It's not even used

It's used in int.to_nat

[Mario Carneiro]

Yet more alternatively, don't define it as a function, have an existence theorem

[Mario Carneiro]

the inverse to this is a lot easier to state

[Mario Carneiro]

def expansion (r : α) (n : ℕ) : ℕ :=
⌊r * (10 ^ n : ℕ)⌋.nat_mod 10

[Mario Carneiro]

I'm not sure why n is a nat here, there are both negative and positive exponent terms in the expansion

[Kevin Buzzard]

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

[Mario Carneiro]

yes, this allows you to view is_lub S as a predicate by currying

[Mario Carneiro]

generally speaking, more "parameter" like things should come first

[Kevin Buzzard]

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

[Mario Carneiro]

that's why I said that

[Mario Carneiro]

S is the parameter, x is the variable

[Mario Carneiro]

so S comes first

[Kevin Buzzard]

that's why I said that

I know, I was just translating you into maths

[Kevin Buzzard]

Hey @Kenny Lau

[Kevin Buzzard]

I was playing with sups

[Kevin Buzzard]

what do you think this is:

[Kevin Buzzard]

⟨λ 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))⟩

[Kenny Lau]

my constructive proof?

[Kevin Buzzard]

right

[Kenny Lau]

yay

[Kevin Buzzard]

here's an even better version

[Kevin Buzzard]

I wrote it twice

[Kevin Buzzard]

second time looked like this

[Kevin Buzzard]

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⟩
⟩

[Kenny Lau]

more dollar signs?

[Kevin Buzzard]

instance : has_add (set ℝ) := ⟨λ S T,{u | ∃ (s ∈ S) (t ∈ T), u = s + t}⟩

[Kevin Buzzard]

import order.bounds

[Kevin Buzzard]

and analysis.real

[Kevin Buzzard]

and it will run

[Kevin Buzzard]

I couldn't get that stupid triangle thing to work on the first line of the proof

[Kevin Buzzard]

the \t triangle that Patrick and I both dread

[Kevin Buzzard]

so I have to use rw;exact :-)

[Kevin Buzzard]

so that can be golfed a bit more

[Kevin Buzzard]

but the proof the other way I was extremely pleased with :-)

[Kevin Buzzard]

I formulated the theorem

[Kevin Buzzard]

I proved it in tactic mode

[Kevin Buzzard]

I then translated my tactic mode proof into term mode

[Kenny Lau]

nice!

[Kevin Buzzard]

and then I started again and proved it in term mode

[Kevin Buzzard]

from scratch

[Kevin Buzzard]

looking at my old term mode proof for hints about which arithmetic functions to use :-)

[Kevin Buzzard]

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)

[Kevin Buzzard]

Kenny if you had given me that answer I would have had a hard time marking it.

[Kevin Buzzard]

I mean the lambda

[Kevin Buzzard]

it's become unreadable, right?

[Kenny Lau]

lol

[Kenny Lau]

but you can verify it

[Kevin Buzzard]

that is a very different thing from understanding it