Zulip Chat Archive

Johannes -- who do I credit if I take your polynomial stuff from mason-stothers? [or mason-stother as you seem to have called it]? Is it you or JWageM?

Kevin Buzzard (May 23 2018 at 14:15):

I firmly believe I could do this entire thing in 3 days

Kevin Buzzard (May 23 2018 at 14:15):

it's a bit unfortunate about the marking I still have to do though :-/

Kevin Buzzard (May 23 2018 at 14:16):

Chris and Kenny will have finished their exams by Friday afternoon UK time so this would be a perfect all-night binge for them to do afterwards.

Kevin Buzzard (May 23 2018 at 14:16):

;-)

Kevin Buzzard (May 23 2018 at 14:16):

OK now back to marking

Johannes Hölzl (May 23 2018 at 14:19):

Mason-stother's polynomials are from us both, most parts were done by Jens, some by me. Its okay to only credit Jens.

Nicholas Scheel (May 23 2018 at 15:01):

Hi! How can I help best? Maybe start building Z[(1+sqrt(5))/2] ? I have a little experience with field extensions from abstract algebra this past semester ...

Nicholas Scheel (May 23 2018 at 15:03):

that’s really just Z[sqrt(5)] right? field operations will get you (1+-sqrt(5))/2 from that

Patrick Massot (May 23 2018 at 15:03):

He wants a ring, not a field

Patrick Massot (May 23 2018 at 15:03):

And that's what this notation denotes

Kevin Buzzard (May 23 2018 at 15:10):

Right -- there is Q(sqrt(5)) = Q(alpha) [alpha := (1+sqrt(5))/2] and there is Z[sqrt(5)] which is strictly smaller than Z[alpha] [it has index 2]

Kevin Buzzard (May 23 2018 at 15:11):

The only reason I suggested the ring not the field was (1) rings have fewer axioms than fields and (2) my instinct was to construct the smallest object which was mathematically reasonable [so no semirings or distribs, thank you] and which contained enough to formalise the statement "u_m = (alpha^m - beta^m) / sqrt (5)"...oh crap

Kevin Buzzard (May 23 2018 at 15:11):

maybe a field is fine :-)

Kevin Buzzard (May 23 2018 at 15:11):

One could prove sqrt(5) * u_m = alpha^m - beta^m

Kevin Buzzard (May 23 2018 at 15:12):

and then mumble about integral domains

Kevin Buzzard (May 23 2018 at 15:12):

OK so @Nicholas Scheel if you want to take a look at how the complex numbers were built from the real numbers in mathlib (in some file called complex.lean probably) then you could just copy this and build Q(sqrt(5)) from Q by adjoining a square root of 5

Kevin Buzzard (May 23 2018 at 15:13):

The only difficulty will be in proving that if a+b*sqrt(5) is non-zero then a^2-5b^2 is non-zero, which you need for division

Kevin Buzzard (May 23 2018 at 15:13):

For the complexes the argument is that everything is positive, that doesn't work here

Kevin Buzzard (May 23 2018 at 15:13):

you need that 5 isn't the square of a rational

Kevin Buzzard (May 23 2018 at 15:13):

but modulo that, there's your Q(sqrt(5))

Kevin Buzzard (May 23 2018 at 15:13):

at some point one would need this anyway, to prove Z[alpha] is an integral domain, so there's no getting away from it

Chris Hughes (May 23 2018 at 15:33):

I've done some stuff on integers mod n which I'll send you when I get home.

Nicholas Scheel (May 23 2018 at 15:48):

Ah okay, I see ... I think I'll try to build Z[alpha], doesn't look like we'll need division

Chris Hughes (May 23 2018 at 16:52):

@Kevin Buzzard Very messy, but the most basic stuff about integers mod n is there. https://github.com/dorhinj/leanstuff/blob/master/Zmod1.lean

Chris Hughes (May 23 2018 at 16:53):

@Nicholas Scheel I also made a bit of a start on univariate polys, although I haven't done much more than copy Johannes stuff on multivariate polys.

Chris Hughes (May 23 2018 at 16:54):

I think Sean's finset.max would be a more appropriate definition of degree than sup

Nicholas Scheel (May 23 2018 at 16:57):

okay I have a commutative ring instance for Z[alpha]!

Johannes Hölzl (May 23 2018 at 16:59):

with sup you don't need to use iget. max is the better name but I think sup has the better behaviour.

Patrick Massot (May 23 2018 at 18:25):

Thanks, but I don't know how to use sup

Kenny Lau (May 23 2018 at 18:52):

@Kevin Buzzard have you pushed?

Kevin Buzzard (May 23 2018 at 18:56):

pushed what?

Kenny Lau (May 23 2018 at 18:56):

fibonacci

Kevin Buzzard (May 23 2018 at 18:56):

Chris -- Johannes and his student wrote some univariate poly stuff in their mason-stother repo

Kevin Buzzard (May 23 2018 at 18:57):

What Fibonacci is there for me to push?

Kevin Buzzard (May 23 2018 at 18:57):

I have epsilon

Kevin Buzzard (May 23 2018 at 18:57):

I proved luc (m + 3) = 2 * fib (m + 3) + fib m

Kevin Buzzard (May 23 2018 at 18:57):

I will push some stuff

Chris Hughes (May 23 2018 at 19:00):

They didn't do the theorem you need I don't think.

Kevin Buzzard (May 23 2018 at 19:11):

I pushed some stuff

Kevin Buzzard (May 23 2018 at 19:12):

I proved 2/3 of point 4

Kevin Buzzard (May 23 2018 at 19:55):

Is gcd (a + n * b) b = gcd a b in lean or mathlib somewhere? (everything a nat)]

Patrick Massot (May 23 2018 at 19:55):

If everything is a nat, this is almost certainly wrong in some edge case

Kenny Lau (May 23 2018 at 19:58):

there isn't, since gcd is well-defined for 0 in the real world

Patrick Massot (May 23 2018 at 20:00):

I knew it: edge case

Kenny Lau (May 23 2018 at 20:00):

#check nat.gcd_rec -- nat.gcd m n = nat.gcd (n % m) m
open nat
example (a n b : ℕ) : gcd (a + n * b) b = gcd a b :=
by rw [gcd_comm, gcd_rec, add_mul_mod_self_right, ← gcd_rec, gcd_comm]

Kenny Lau (May 23 2018 at 20:00):

there is no edge case!

Patrick Massot (May 23 2018 at 20:01):

This is an edge case to the general statement that every general statement about nat is wrong

Kevin Buzzard (May 23 2018 at 20:09):

of course one could argue that gcd 0 0 = 0 is already wrong

Kevin Buzzard (May 23 2018 at 20:09):

given that 7 divides both 0 and 0

Patrick Massot (May 23 2018 at 20:11):

To be honest, that one has nothing to do with nat. It's also a problem in integers

Kevin Buzzard (May 23 2018 at 20:12):

You know that $\frac{\zeta(1-k)}{2} + \Sigma_{n\geq1}\sigma_{k-1}(n)q^n$ is a modular form, right?

Kevin Buzzard (May 23 2018 at 20:13):

Here $\sigma_{k-1}(n)$ denotes the sum of the $k-1$ st powers of the positive divisors of $n$ .

Kevin Buzzard (May 23 2018 at 20:14):

but if you set $n=0$ in the sum you get the sum of the $k-1$ st powers of the positive divisors of $0$

Kevin Buzzard (May 23 2018 at 20:14):

so that's $1^{k-1} + 2 ^{k-1} + 3^{k-1} + \cdots$

Kevin Buzzard (May 23 2018 at 20:14):

which is $\zeta(1-k)$ by...erm...definition...or something

Kevin Buzzard (May 23 2018 at 20:15):

but the sum is only over half of the integers

Kevin Buzzard (May 23 2018 at 20:15):

so you should only take the term at zero half as seriously

Kevin Buzzard (May 23 2018 at 20:15):

which gives you $\zeta(1-k)/2$

Kevin Buzzard (May 23 2018 at 20:15):

and that's how I remember it

Patrick Massot (May 23 2018 at 20:16):

And we are surprised formalizing maths is hard...

Nicholas Scheel (May 23 2018 at 20:19):

@Kevin Buzzard Should I make a fork, or may I have commit access?

Kenny Lau (May 23 2018 at 20:19):

do I have commit access?

Kevin Buzzard (May 23 2018 at 20:21):

what is the most sensible idea?

Kevin Buzzard (May 23 2018 at 20:21):

nobody has commit access except me

Kevin Buzzard (May 23 2018 at 20:21):

but I am happy to give it to anybody

Kevin Buzzard (May 23 2018 at 20:21):

unless someone has a good reason why I shouldn't do this

Kevin Buzzard (May 23 2018 at 20:21):

I need to know your github usernames I guess

Kenny Lau (May 23 2018 at 20:22):

I'll kindly delete your alpha and beta :P (after proving points 4 and 6)

Patrick Massot (May 23 2018 at 20:22):

If I were you I would fear seeing constructive stuff invading my repo

Kevin Buzzard (May 23 2018 at 20:24):

OK Kenny and Nicholas you should have push access

Kenny Lau (May 23 2018 at 20:24):

thanks

Kenny Lau (May 23 2018 at 20:24):

If I were you I would fear seeing constructive stuff invading my repo

much fear of the unknown :P

Kevin Buzzard (May 23 2018 at 20:24):

but lemme push some stuff

Patrick Massot (May 23 2018 at 20:24):

Constructive madness on the way...

Kevin Buzzard (May 23 2018 at 20:24):

I need a job done

Patrick Massot (May 23 2018 at 20:25):

Selling your mathematician soul...

Kevin Buzzard (May 23 2018 at 20:26):

OK I am pushed

Kenny Lau (May 23 2018 at 20:27):

waitttt where did the Z alpha come from

Kenny Lau (May 23 2018 at 20:27):

oh Nicholas built it...

Kenny Lau (May 23 2018 at 20:27):

@Nicholas Scheel do you think we'll really need it?

Nicholas Scheel (May 23 2018 at 20:27):

oops sorry, did I step on your push?

Kenny Lau (May 23 2018 at 20:28):

I'm just doubting whether we need sqrt(5) at all

Kevin Buzzard (May 23 2018 at 20:28):

Here's the reason I think we might need sqrt(5)

Nicholas Scheel (May 23 2018 at 20:28):

I think this might help along the way ;) :

lemma αβsum : α + β = 1 := rfl
lemma αβprod : α * β = -1 := rfl

Kevin Buzzard (May 23 2018 at 20:28):

that looks really good

Kevin Buzzard (May 23 2018 at 20:29):

it's a little bit better than my method

Kenny Lau (May 23 2018 at 20:29):

so, constructivism wins?

Kevin Buzzard (May 23 2018 at 20:29):

To prove something like luc (m + 3) = 2 * fib (m + 3) + fib m you can just do it by induction

Kevin Buzzard (May 23 2018 at 20:29):

but to prove luc (4 * n) = (luc (2 * n) ^ 2) - 2

Kevin Buzzard (May 23 2018 at 20:30):

the only method I know is to prove the general sqrt (5) formula

Kenny Lau (May 23 2018 at 20:30):

you just need the right lemmas

Kevin Buzzard (May 23 2018 at 20:30):

maybe some theorem of logic says you don't need square roots of 5

Kenny Lau (May 23 2018 at 20:30):

like the one I proved that day

Kenny Lau (May 23 2018 at 20:30):

variables (m n : ℕ)

local attribute [elab_as_eliminator] nat.strong_induction_on

theorem to_be_named : fib (m + n + 1) =
  fib m * fib n + fib (m + 1) * fib (n + 1) :=
nat.strong_induction_on n $ λ n, nat.cases_on n (λ _, by simp [fib]) $ λ n,
nat.cases_on n (λ _, by simp [fib]) $ λ n ih,
have H1 : _ := ih n (nat.lt_trans (nat.lt_succ_self n) (nat.lt_succ_self (n+1))),
have H2 : fib (m + n + 2) = _ + _ * (fib n + fib (n+1)) := ih (n+1) (nat.lt_succ_self (n+1)),
calc  fib (m + n + 1) + fib (m + n + 2)
    = fib m * (fib n + fib (n+1)) + fib (m+1) * (fib (n+1) + (fib n + fib (n+1))) :
  by rw [H1, H2, mul_add, mul_add, mul_add, mul_add]; ac_refl

Kevin Buzzard (May 23 2018 at 20:30):

but then you will end up defining some auxiliary function on Z x Z

Kevin Buzzard (May 23 2018 at 20:30):

Let me just read through the proof

Kevin Buzzard (May 23 2018 at 20:31):

Of course one might also argue that using sqrt(5) is a _natural_ thing to do

Kevin Buzzard (May 23 2018 at 20:31):

which might make it a good thing to do

Kenny Lau (May 23 2018 at 20:32):

I should add "building the algebraic numbers" to my want-to-do-but-god-knows-when list

Kevin Buzzard (May 23 2018 at 20:32):

Of course you could also take the ring Q[x] and quotient out by the ideal (x^2-5) right? ;-)

Kevin Buzzard (May 23 2018 at 20:33):

I will write comments about the proof in the issue

Patrick Massot (May 23 2018 at 20:35):

From an arithmetic point of view it makes much more sense than defining square root on nonnegative reals

Mario Carneiro (May 23 2018 at 20:39):

Hey, it might be too late for this remark but I built the ring Z[\sqrt n] in pell.lean. Not directly applicable, but it might be useful

Mario Carneiro (May 23 2018 at 20:43):

of course one could argue that gcd 0 0 = 0 is already wrong
given that 7 divides both 0 and 0

I think there are good reasons to believe that gcd 0 0 = 0 is right over both nat and int, and in traditional math, if you think about the integers in that calculation as representing their principal ideals. (gcd m n) = (m, n)

Mario Carneiro (May 23 2018 at 20:44):

so here "greatest" actually means greatest in the divisor order, putting 0 at the top not the bottom

Kenny Lau (May 23 2018 at 20:48):

@Kevin Buzzard 7 divides both 0 and 0, and 7 divides gcd(0,0) = 0, consistent with the UMP of GCD

Kenny Lau (May 23 2018 at 20:56):

@Kevin Buzzard can I push?

Kevin Buzzard (May 23 2018 at 20:57):

sure go ahead and push

Kevin Buzzard (May 23 2018 at 20:57):

I wrote a more detailed sketch of how to flesh out the argument in the issue

Kenny Lau (May 23 2018 at 20:58):

are you sure I have write access?

Kevin Buzzard (May 23 2018 at 20:58):

I need to go and steer my children towards their beds now. Thanks for the help all of you. Mario and Kenny, I see the advantages of the "zero bigger than everything" approach here! Of course it's just the ideal-theoretic way of thinking about it -- gcd(x,y) = ideal generated by x and y, and if it's principal then let's choose a canonical generator if we can.

Kevin Buzzard (May 23 2018 at 20:58):

Kenny I think I invited you. Did you check your email or did I fail?

Kenny Lau (May 23 2018 at 20:59):

oh, I need to accept the invitation

Kevin Buzzard (May 23 2018 at 20:59):

https://github.com/kbuzzard/lean-squares-in-fibonacci/issues/1

Kevin Buzzard (May 23 2018 at 20:59):

Note the last part -- point 12 is slightly delicate, it needs the following consequence of uniqueness of prime factorization: if gcd(x,y)=1 and x*y is a square then x and y are both squares (here x,y>0).

Kevin Buzzard (May 23 2018 at 21:01):

and for that you need: n square iff v_p(n) even for all primes p (v_p(n) = largest power of p dividing n) and gcd(x,y)=1 iff min(v_p(x),v_p(y))=0 for all primes p

Mario Carneiro (May 23 2018 at 21:03):

pretty sure that exact theorem is in my formalization

Mario Carneiro (May 23 2018 at 21:04):

and you don't need UFD for it

Kevin Buzzard (May 23 2018 at 21:05):

well you do need something

Kevin Buzzard (May 23 2018 at 21:05):

because it's not true in a general ring

Kevin Buzzard (May 23 2018 at 21:05):

well I suppose it depends on what you mean by gcd in a general ring

Mario Carneiro (May 23 2018 at 21:05):

you need nat.gcd facts and some induction

Mario Carneiro (May 23 2018 at 21:06):

I'm not saying it doesn't depend in a reverse mathematics way on UFD, but you don't need all that complexity for the proof

Kevin Buzzard (May 23 2018 at 21:06):

a bit like the proof of UFD ;-)

Kevin Buzzard (May 23 2018 at 21:06):

[I mean, you need nat.gcd facts and some induction for that too]

Kevin Buzzard (May 23 2018 at 21:07):

For a general comm ring there are two natural defs of gcd, one more general than the other

Kevin Buzzard (May 23 2018 at 21:07):

and the weaker version of coprime doesn't cut it

Kevin Buzzard (May 23 2018 at 21:07):

oh there are also issues with units

Kevin Buzzard (May 23 2018 at 21:07):

-4 and -9 are coprime and their product is a square etc etc

Kevin Buzzard (May 23 2018 at 21:08):

so there are issues in general

Kevin Buzzard (May 23 2018 at 21:08):

but I take your point that you are saying you don't have to go through v_p(x)

Mario Carneiro (May 23 2018 at 21:08):

right

Mario Carneiro (May 23 2018 at 21:08):

it's a nice way to conceptualize it, but it's technically complicated and not worth it for most problems IMO

Mario Carneiro (May 23 2018 at 21:10):

whenever you need a fact that would come from primality of the p in v_p(n), just use the coprime assumption instead, it's just as well for the purpose of the proof

Kenny Lau (May 23 2018 at 21:23):

@Mario Carneiro what's the fastest way to know that n=1 or n=2 given n divides 2?

Mario Carneiro (May 23 2018 at 21:23):

n | 2 implies n <= 2

Chris Hughes (May 23 2018 at 21:23):

2 is prime

Mario Carneiro (May 23 2018 at 21:23):

alternatively, 2 is prime

Kenny Lau (May 23 2018 at 21:23):

oh lol

Kenny Lau (May 23 2018 at 21:32):

Point 4 done!

Nicholas Scheel (May 23 2018 at 22:42):

I want to prove this but I don't know how? lemma Fib.is_fib (n : ℤ) : Fib (n+2) = Fib n + Fib (n + 1) :P

Nicholas Scheel (May 23 2018 at 22:42):

cases n, refl, induction n using nat.case_strong_induction_on with n ih, refl, cases n, refl, cases n, refl, have ih0 := ih n (nat.le_succ_of_le (nat.le_succ _)), have ih1 : Fib (-[1+n+1] + 2) = Fib -[1+n+1] + Fib -[1+n] := ih (n+1) (nat.le_succ _), have ih2 : Fib -[1+n] = Fib -[1+n+2] + Fib -[1+n+1] := ih (n+2) (le_refl _),

Kenny Lau (May 23 2018 at 22:43):

write x^(n+2) as x^n x^2?

Kenny Lau (May 23 2018 at 22:43):

you might find int.induction_on useful

Kenny Lau (May 24 2018 at 02:44):

Point 6 done except the last claim

Kevin Buzzard (May 24 2018 at 07:39):

OK this is great.

Kevin Buzzard (May 24 2018 at 07:39):

Looking at what has been already done

Kevin Buzzard (May 24 2018 at 07:39):

I already easily have enough material to fill the session.

Kevin Buzzard (May 24 2018 at 07:39):

So actually the time pressure is over.

Kevin Buzzard (May 24 2018 at 07:40):

These kids are smart kids (my audience of 8)

Kevin Buzzard (May 24 2018 at 07:40):

but the Lean session will last 90 minutes

Kevin Buzzard (May 24 2018 at 07:40):

and even talking about how to construct Z[alpha] and computing Fibonacci numbers mod n throws up so much stuff

Kevin Buzzard (May 24 2018 at 07:41):

that my talk is already written.

Kevin Buzzard (May 24 2018 at 07:41):

However I am definitely still interested in finishing the job :-)

Kevin Buzzard (May 24 2018 at 07:41):

Here's a question.

Kevin Buzzard (May 24 2018 at 07:42):

Oh -- before I start -- thanks to Kenny and Nicholas for their contributions!

Kevin Buzzard (May 24 2018 at 07:42):

I'm still mired in marking and preparing these talks for Sat was beginning to become a worry.

Kevin Buzzard (May 24 2018 at 07:43):

The question is how to express the following assertion in Lean

Kevin Buzzard (May 24 2018 at 07:43):

We need to compute the Fibonacci sequence mod 16

Kevin Buzzard (May 24 2018 at 07:44):

The theorem is that mod 16 it goes like this:

Kevin Buzzard (May 24 2018 at 07:44):

[0, 1, 1, 2, 3, 5, 8, 13, 5, 2, 7, 9, 0, 9, 9, 2, 11, 13, 8, 5, 13, 2, 15, 1]

Kevin Buzzard (May 24 2018 at 07:45):

And the proof is "trivial by induction"

Kevin Buzzard (May 24 2018 at 07:45):

(because each term in that list is the sum of the previous two terms mod 16, and at the end we have 15 + 1 = 0 and 1 + 0 = 1 so we wrap back)

Kevin Buzzard (May 24 2018 at 07:46):

The question is how one can prove this in Lean in a way which actually looks reasonable

Kevin Buzzard (May 24 2018 at 07:46):

This is not a question about how to do anything mod n, this is a specific question about mod 16 (there's an analogous one for mod 3 but I chose the most awkward one).

Kevin Buzzard (May 24 2018 at 07:46):

One issue is what to do the induction on.

Kevin Buzzard (May 24 2018 at 07:47):

You could do strong induction on m

Kevin Buzzard (May 24 2018 at 07:47):

or you could write m = 24 * n + t with 0 <= t < 24 and do induction on n

Kevin Buzzard (May 24 2018 at 07:48):

What I am (not really that) concerned about is that with either approach you end up writing essentially the same code block 24 or so times

Kevin Buzzard (May 24 2018 at 07:50):

In the direct strong induction argument you case on n mod 24 and I don't really know how to do that

Kevin Buzzard (May 24 2018 at 07:50):

hmm

Kevin Buzzard (May 24 2018 at 07:50):

maybe it's OK

Kevin Buzzard (May 24 2018 at 07:51):

if t < 22 it's some lemma of the form (a+b)%m = (a%m+b%m)%m -- is that in Lean/mathlib?

Kevin Buzzard (May 24 2018 at 07:51):

and in the induction case you end up with a statement of the form a0 and a1 and ... and a23

Kevin Buzzard (May 24 2018 at 07:51):

you would never write such a statement in python or whatever, you would somehow wrap everything up in a list

Kevin Buzzard (May 24 2018 at 07:52):

Hmm

Kevin Buzzard (May 24 2018 at 07:52):

I think my question is that I am seeing two competing methods for proving this and they book look a bit "trivial in maths but a bit ugly to write in Lean" at the minute. Anyone have any suggestions?

Chris Hughes (May 24 2018 at 07:55):

if t < 14 it's some lemma of the form (a+b)%m = (a%m+b%m)%m -- is that in Lean/mathlib?

int.modeq.modeq_add should help, since this is defeq to a + b \== a%m + b % m Although I forgot modeq_mod i.e. , so you'll have to prove that.
Why not just prove it as a lemma about integers mod n, and not naturals.

Kevin Buzzard (May 24 2018 at 07:57):

The problem with working with integers mod n is that if you want the _input_ to fib to be an integer mod n (n would be 24 here) then you have to prove that your definition is well-defined.

Kevin Buzzard (May 24 2018 at 07:57):

and that's basically the same question, or another way of writing it, as far as I can see. Am I missing your point?

Kevin Buzzard (May 24 2018 at 07:57):

Oh -- or are you just talking about the (a+b)%m lemma?

Chris Hughes (May 24 2018 at 07:58):

The definition is just quot.mk \circ fib

Kevin Buzzard (May 24 2018 at 07:58):

Chris I'm talking about the input not the output

Chris Hughes (May 24 2018 at 07:58):

I'm talking about the mod 16 lemma

Kevin Buzzard (May 24 2018 at 07:58):

I can get fib : N -> N / 16 fine

Kevin Buzzard (May 24 2018 at 07:58):

But fib : (N / 24) -> N / 16 is less fine

Kevin Buzzard (May 24 2018 at 07:58):

what am I saying

Kevin Buzzard (May 24 2018 at 07:58):

what has happened to me

Kevin Buzzard (May 24 2018 at 07:58):

(Z / 24)

Chris Hughes (May 24 2018 at 07:59):

Just do nat \r mod 16

Kevin Buzzard (May 24 2018 at 07:59):

what the hell is N mod 24

Kevin Buzzard (May 24 2018 at 07:59):

I understand how to build fib : N -> Z / 16

Kevin Buzzard (May 24 2018 at 07:59):

The issue is proving that fib (n + 24) = fib n

Kevin Buzzard (May 24 2018 at 08:00):

The only proof I know of that statement is

Kevin Buzzard (May 24 2018 at 08:00):

"consider n mod 24"

Kevin Buzzard (May 24 2018 at 08:00):

I realised I made a mistake above

Kevin Buzzard (May 24 2018 at 08:00):

I am going to edit a bunch of 16s and change them to 24s

Kevin Buzzard (May 24 2018 at 08:00):

input mod 24, output mod 16

Kevin Buzzard (May 24 2018 at 08:02):

OK fixed

Kevin Buzzard (May 24 2018 at 08:02):

So the issue is proving a = b mod 24 implies fib a = fib b mod 16

Kevin Buzzard (May 24 2018 at 08:02):

hmm

Kevin Buzzard (May 24 2018 at 08:03):

this is an idea

Kevin Buzzard (May 24 2018 at 08:03):

one can prove fib (n + 24) = fib n mod 16

Kevin Buzzard (May 24 2018 at 08:03):

by induction on n

Kevin Buzzard (May 24 2018 at 08:03):

and one has to hope that Lean has the firepower to compute fib 24

Kevin Buzzard (May 24 2018 at 08:03):

to get the induction started

Kevin Buzzard (May 24 2018 at 08:03):

OK so

Kevin Buzzard (May 24 2018 at 08:03):

actually

Kevin Buzzard (May 24 2018 at 08:04):

one can define fibmod16

Kevin Buzzard (May 24 2018 at 08:04):

I see

Kevin Buzzard (May 24 2018 at 08:04):

fibmod16 : N -> Z/16

Kevin Buzzard (May 24 2018 at 08:04):

then prove that forall n, fibmod16 (n + 24) = fibmod16 n by induction on n

Kevin Buzzard (May 24 2018 at 08:04):

and now no firepower needed

Kevin Buzzard (May 24 2018 at 08:05):

and now prove fib mod 16 is fibmod16 by induction on n

Kevin Buzzard (May 24 2018 at 08:05):

and you're done!

Kevin Buzzard (May 24 2018 at 08:05):

This is great!

Kevin Buzzard (May 24 2018 at 08:05):

Thanks Chris!

Kevin Buzzard (May 24 2018 at 08:05):

I could even make that discussion into 90 minutes, given that none of the kids will have seen Lean before

Chris Hughes (May 24 2018 at 08:06):

induction, bases case rfl, next case unfold 24 times, and hope things simplify

Kevin Buzzard (May 24 2018 at 08:08):

Yeah I think you've cracked it. Thanks Chris.

Kevin Buzzard (May 24 2018 at 08:08):

Now get back to stats revision ;-)

Kenny Lau (May 24 2018 at 09:05):

The correct way is to use the theorem I proved that day :P

Kevin Buzzard (May 24 2018 at 09:06):

Kenny

Kevin Buzzard (May 24 2018 at 09:06):

your comments are sometimes obscure

Kevin Buzzard (May 24 2018 at 09:06):

but "the theorem I proved that day" will take some beating

Kevin Buzzard (May 24 2018 at 09:06):

(a%m+b%m)%m=(a+b)%m is horrible

Kenny Lau (May 24 2018 at 09:06):

theorem to_be_named : fib (m + n + 1) =
  fib m * fib n + fib (m + 1) * fib (n + 1) :=
nat.strong_induction_on n $ λ n, nat.cases_on n (λ _, by simp [fib]) $ λ n,
nat.cases_on n (λ _, by simp [fib]) $ λ n ih,
have H1 : _ := ih n (nat.lt_trans (nat.lt_succ_self n) (nat.lt_succ_self (n+1))),
have H2 : fib (m + n + 2) = _ + _ * (fib n + fib (n+1)) := ih (n+1) (nat.lt_succ_self (n+1)),
calc  fib (m + n + 1) + fib (m + n + 2)
    = fib m * (fib n + fib (n+1)) + fib (m+1) * (fib (n+1) + (fib n + fib (n+1))) :
  by rw [H1, H2, mul_add, mul_add, mul_add, mul_add]; ac_refl

Kenny Lau (May 24 2018 at 09:06):

it's how it's done in proofwiki

Kenny Lau (May 24 2018 at 09:07):

this lemma, plus the fact that fib 16 and fib 17 are coprime

Kevin Buzzard (May 24 2018 at 09:07):

OK so I will now home in on the other part of your sentence

Kevin Buzzard (May 24 2018 at 09:07):

"The correct way"

Kenny Lau (May 24 2018 at 09:07):

it's more general

Kenny Lau (May 24 2018 at 09:07):

you can prove that fib m | fib n iff m | n

Kevin Buzzard (May 24 2018 at 09:07):

Oh so you're just talking about the correct way to do something random

Kevin Buzzard (May 24 2018 at 09:08):

I was rather hoping you were talking about the thing I was interested in :-)

Kenny Lau (May 24 2018 at 09:08):

m = 16?

Kevin Buzzard (May 24 2018 at 09:08):

Oh yeah!

Kevin Buzzard (May 24 2018 at 09:08):

Let's talk about that!

Kenny Lau (May 24 2018 at 09:08):

that's a special case lol

Chris Hughes (May 24 2018 at 09:08):

this lemma, plus the fact that fib 16 and fib 17 are coprime

Is this easy to prove, or are the numbers too big for lean to handle?

Kevin Buzzard (May 24 2018 at 09:08):

fib n is coprime to fib (n+1)

Kenny Lau (May 24 2018 at 09:08):

this lemma, plus the fact that fib 16 and fib 17 are coprime

Is this easy to prove, or are the numbers too big for lean to handle?

kevin already proved it

Kevin Buzzard (May 24 2018 at 09:08):

by Euclid's algorithm

Kevin Buzzard (May 24 2018 at 09:09):

I can't face (a%m+a%m)%m=(a+b)%m

Kevin Buzzard (May 24 2018 at 09:09):

I am going to work with Z/n

Kevin Buzzard (May 24 2018 at 09:09):

Where is this in Lean?

Kevin Buzzard (May 24 2018 at 09:09):

I currently have

Kevin Buzzard (May 24 2018 at 09:10):

definition fib_mod (m : ℕ) : ℕ → ℕ
| 0 := 0 % m
| 1 := 1 % m
| (n + 2) := ( (fib_mod n) + (fib_mod (n + 1)) ) % m

Kevin Buzzard (May 24 2018 at 09:10):

but I am going to go for a map from N to whatever Z/nZ is called

Kevin Buzzard (May 24 2018 at 09:10):

as long as it's an abelian group

Chris Hughes (May 24 2018 at 09:10):

https://github.com/dorhinj/leanstuff/blob/master/Zmod1.lean I did it.

Kevin Buzzard (May 24 2018 at 09:11):

oh so it's not in Lean?

Chris Hughes (May 24 2018 at 09:11):

No.

Kevin Buzzard (May 24 2018 at 09:11):

I mean mathlib

Kevin Buzzard (May 24 2018 at 09:11):

I will steal it

Kevin Buzzard (May 24 2018 at 09:11):

you only did Z mod 1?

Chris Hughes (May 24 2018 at 09:12):

The 1 is to distinguish it from another construction I did.

Kevin Buzzard (May 24 2018 at 09:12):

Oh OK :-)

Kevin Buzzard (May 24 2018 at 09:12):

That's a relief

Kevin Buzzard (May 24 2018 at 09:12):

I was hoping for Zmod16

Kevin Buzzard (May 24 2018 at 09:13):

wow

Kevin Buzzard (May 24 2018 at 09:13):

https://github.com/dorhinj/leanstuff

Kevin Buzzard (May 24 2018 at 09:13):

you have been pretty productive in the last 16 hours

Kevin Buzzard (May 24 2018 at 09:13):

about 50 lean files commited

Kenny Lau (May 24 2018 at 09:13):

lol

Kevin Buzzard (May 24 2018 at 09:14):

it's Chrislib

Kevin Buzzard (May 24 2018 at 09:14):

I like the look of kbuzzard.lean

Kevin Buzzard (May 24 2018 at 09:14):

Is that one of my theorems?

Kevin Buzzard (May 24 2018 at 09:14):

something about modular forms maybe?

Kevin Buzzard (May 24 2018 at 09:15):

Actually, hopefully, one of my theorems really _will_ be in Lean soon

Kevin Buzzard (May 24 2018 at 09:15):

Ellen is going to formalize my dots and boxes paper

Kevin Buzzard (May 24 2018 at 09:22):

If Z mod n isn't in mathlib and requires a bunch of Chris' local imports it might be easier to just go for def nat.mod_add (a b m : ℕ) : (a % m + b % m) % m = (a + b) % m := sorry

Kevin Buzzard (May 24 2018 at 09:22):

I am not enough of an expert in how to use % to see how to prove this

Kevin Buzzard (May 24 2018 at 09:22):

and it doesn't appear to be there already

Kevin Buzzard (May 24 2018 at 09:23):

KB <- professional number theorist who is not an expert in mod

Kevin Buzzard (May 24 2018 at 09:23):

:-/

Kevin Buzzard (May 24 2018 at 09:24):

I added the sorried assertion to https://github.com/kbuzzard/lean-squares-in-fibonacci/blob/master/src/definitions.lean

Chris Hughes (May 24 2018 at 09:27):

@[simp] lemma nat.mod_mod (n m : ℕ) : n % m % m = n % m :=
nat.cases_on m (by simp) (λ m, mod_eq_of_lt (mod_lt _ (succ_pos _)))

def nat.mod_add (a b m : ℕ) : (a % m + b % m) % m = (a + b) % m :=
nat.modeq.modeq_add (nat.mod_mod _ _) (nat.mod_mod _ _)

Patrick Massot (May 24 2018 at 09:28):

This is becoming slightly creepy

Patrick Massot (May 24 2018 at 09:28):

Kevin, what have you created?

Kenny Lau (May 24 2018 at 09:31):

import definitions

theorem fib_add (m n : ℕ) : fib (m + n + 1) =
  fib m * fib n + fib (m + 1) * fib (n + 1) :=
nat.rec_on_two n (by unfold fib; rw [mul_zero, zero_add, mul_one]; refl)
  (by unfold fib; rw [zero_add, mul_one, mul_one]; refl) $ λ n ih1 ih2,
calc  fib (m + n + 1) + fib (m + nat.succ n + 1)
    = fib m * (fib n + fib (n+1)) + fib (m+1) * (fib (n+1) + (fib n + fib (n+1))) :
  by rw [ih1, ih2, fib, mul_add, mul_add, mul_add, mul_add, nat.succ_eq_add_one]; ac_refl

attribute [refl] dvd_refl
attribute [trans] dvd_trans

theorem fib_dvd_mul (m n : ℕ) : fib m ∣ fib (m * n) :=
nat.cases_on m (by rw [zero_mul]; refl) $ λ m,
nat.rec_on n (dvd_zero _) $ λ n ih,
show fib (nat.succ m) ∣ fib (nat.succ m * n + m + 1),
by rw [fib_add]; apply dvd_add;
[apply dvd_mul_of_dvd_left ih, apply dvd_mul_left]

Kenny Lau (May 24 2018 at 09:31):

done

Kenny Lau (May 24 2018 at 09:31):

I don't need the fact that fib m and fib m+1 are coprime

Kenny Lau (May 24 2018 at 09:32):

I would need it to prove the converse though

Kevin Buzzard (May 24 2018 at 09:33):

Kevin, what have you created?

This is the new normal. Professors who can't prove things about mod so they ask the undergraduates

Kevin Buzzard (May 24 2018 at 09:34):

I really want that by December there are a bunch of undergraduates at my university asking their tutors questions which the tutors can't answer

Kevin Buzzard (May 24 2018 at 09:34):

or showing them code which the tutors can't understand

Kevin Buzzard (May 24 2018 at 09:34):

or saying "I typed up your problem sheet into Lean and you made an off by one error"

Kenny Lau (May 24 2018 at 09:34):

pushed

Kevin Buzzard (May 24 2018 at 09:34):

Thanks Kenny

Kevin Buzzard (May 24 2018 at 09:35):

I need a recursor for %

Kevin Buzzard (May 24 2018 at 09:35):

If I have a function F from nat to X

Kevin Buzzard (May 24 2018 at 09:35):

and a proof that F (n + 24) = F n

Kevin Buzzard (May 24 2018 at 09:35):

then I want a theorem that F n = F (n % 24)

Kevin Buzzard (May 24 2018 at 09:35):

Is that a recursor?

Kevin Buzzard (May 24 2018 at 09:35):

It's what I want, at any rate

Kenny Lau (May 24 2018 at 09:36):

ok a minute

Kevin Buzzard (May 24 2018 at 09:36):

what I don't want

Kevin Buzzard (May 24 2018 at 09:36):

is what I have to do

Kevin Buzzard (May 24 2018 at 09:36):

which is marking 150 scripts about sup S

Kevin Buzzard (May 24 2018 at 09:36):

I think I need to go offline for 7 hours

Kevin Buzzard (May 24 2018 at 09:36):

I will push too

Kevin Buzzard (May 24 2018 at 09:37):

Before I go

Kevin Buzzard (May 24 2018 at 09:37):

just let me make one thing clear to Kenny and Chris

Kevin Buzzard (May 24 2018 at 09:37):

Last night I was a bit worried about all this

Kevin Buzzard (May 24 2018 at 09:38):

because I still have 10 hours of marking and I wanted to give a good talk on Sat

Kevin Buzzard (May 24 2018 at 09:38):

but now I know I have enough material to give a good talk

Kevin Buzzard (May 24 2018 at 09:38):

so feel free to stop thinking about this and worry about your stats exam

Kevin Buzzard (May 24 2018 at 09:38):

and come back to it on Friday

Kevin Buzzard (May 24 2018 at 09:38):

I will be at Xena tonight by the way, from 6pm

Kevin Buzzard (May 24 2018 at 09:39):

Thanks to all of you, as ever

Kenny Lau (May 24 2018 at 09:42):

lemma nat.mod_rec (m n : ℕ) {C : ℕ → Sort*}
  (H : ∀ n, C n = C (n+m)) :
  C n = C (n%m) :=
have H1 : ∀ q r, C (r + m * q) = C r,
  from λ q, nat.rec_on q (λ r, by rw [mul_zero]; refl) $ λ n ih r,
    by rw [mul_succ, ← add_assoc, ← H, ih],
by conv in (C n) { rw [← mod_add_div n m, H1] }

Kenny Lau (May 24 2018 at 11:36):

theorem fib_gcd (m : ℕ) : ∀ n, nat.gcd (fib m) (fib n) = fib (nat.gcd m n) :=
[thing that works]

Kenny Lau (May 24 2018 at 11:36):

pushed

Kenny Lau (May 24 2018 at 11:49):

pushed

Kenny Lau (May 24 2018 at 11:49):

i'm going to eat and then revise statistics until tonight

Kevin Buzzard (May 26 2018 at 09:53):

What is the prettiest way to prove that there's a positive real number alpha with the property that alpha ^ 2 = alpha + 1?

Kenny Lau (May 26 2018 at 09:53):

not to.

Kenny Lau (May 26 2018 at 09:53):

(why can't we just use the Zalpha)

Kevin Buzzard (May 26 2018 at 09:54):

I would be really interested in an answer to this question before 2000 BST and ideally earlier

Kevin Buzzard (May 26 2018 at 09:54):

Kenny I am giving a talk to a bunch of schoolkids

Kevin Buzzard (May 26 2018 at 09:54):

I am going to give two talks

Mario Carneiro (May 26 2018 at 09:54):

square root, or FTA

Kevin Buzzard (May 26 2018 at 09:54):

In the first talk I will ask them to prove to me that alpha exists and I'll see what they come up with.

Kevin Buzzard (May 26 2018 at 09:54):

In the second talk I will show them how Lean does it

Kevin Buzzard (May 26 2018 at 09:54):

But I want it to look really sexy

Mario Carneiro (May 26 2018 at 09:55):

IVT works too

Kevin Buzzard (May 26 2018 at 09:55):

I want to define a real number alpha as $(1+5^{(1/2)})/2$ or something that looks as close to that as possible

Mario Carneiro (May 26 2018 at 09:55):

then use sqrt thm

Kevin Buzzard (May 26 2018 at 09:56):

I would like a square root symbol ideally. Is there one of them?

Kevin Buzzard (May 26 2018 at 09:56):

Oh I saw one in Pell maybe?

Mario Carneiro (May 26 2018 at 09:56):

I thought we did this a few months ago

Kevin Buzzard (May 26 2018 at 09:56):

I know how to solve it

Kevin Buzzard (May 26 2018 at 09:56):

I just want to make it look maximally sexy

Kevin Buzzard (May 26 2018 at 09:57):

I want to write a human-readable proof

Mario Carneiro (May 26 2018 at 09:57):

I think it is \surd

Mario Carneiro (May 26 2018 at 09:57):

it is in pell

Kevin Buzzard (May 26 2018 at 09:58):

i.e. something where you show the exact proof to a smart schoolkid and whilst they don't know any of the precise syntax they can still kind of see that it's a proof that if alpha is (1+sqrt(5))/2 then alpha^2=alpha+1.

Kevin Buzzard (May 26 2018 at 09:58):

I'll see what I can come up with

Kevin Buzzard (May 26 2018 at 10:00):

I fear becoming mired in div_muls and mul_adds when expanding everything out

Mario Carneiro (May 26 2018 at 10:00):

complete the square

Mario Carneiro (May 26 2018 at 10:01):

using ring

Kevin Buzzard (May 26 2018 at 13:30):

theorem root_5_squared : (sqrt 5) ^ 2 = 5 := by norm_num -- fails

Kevin Buzzard (May 26 2018 at 13:30):

Why can't it be easy

Kevin Buzzard (May 26 2018 at 13:30):

theorem root_5_squared : (sqrt 5) ^ 2 = 5 := by simp [(sqrt_prop 5).2] -- fails

Kevin Buzzard (May 26 2018 at 13:30):

I am so bad at reals

Kevin Buzzard (May 26 2018 at 13:30):

#check sqrt_prop -- ∀ (x : ℝ), 0 ≤ sqrt x ∧ sqrt x * sqrt x = max 0 x

Mario Carneiro (May 26 2018 at 13:32):

you want sqr_sqrt

Mario Carneiro (May 26 2018 at 13:32):

it's already a simp lemma, so you just have to supply a proof of 0 <= 5

Kevin Buzzard (May 26 2018 at 13:32):

why do I need to supply a proof of that?

Kevin Buzzard (May 26 2018 at 13:32):

It's clear it will yield to norm_num right?

Kevin Buzzard (May 26 2018 at 13:33):

Can I somehow add norm_num to simp?

Mario Carneiro (May 26 2018 at 13:33):

sure, but norm_num and simp don't talk back and forth like that

Kevin Buzzard (May 26 2018 at 13:33):

I am still a million miles away from writing a clear readable statement and proof that if alpha = (1+sqrt(5))/2 then alpha^2=alpha+1

Kevin Buzzard (May 26 2018 at 13:33):

I will keep trying

Mario Carneiro (May 26 2018 at 13:34):

norm_num doesn't know about square roots, and simp doesn't use norm_num as a discharger

Mario Carneiro (May 26 2018 at 13:34):

you could try simp {discharger := norm_num}, not sure if that works

Kevin Buzzard (May 26 2018 at 13:34):

completely unrelated -- why do I have imported file '/home/buzzard/lean-projects/lean-squares-in-fibonacci/_target/deps/mathlib/data/set/lattice.lean' uses sorry and several other mathlib errors? This looks really unprofessional :-/ Can you tell me a quick fix?

Mario Carneiro (May 26 2018 at 13:34):

still, I think simp (dec_trivial : 0 <= 5) is easy enough

Kevin Buzzard (May 26 2018 at 13:35):

That's enough? It goes from nats to reals?

Mario Carneiro (May 26 2018 at 13:35):

Oh wait no, le on real is not computable

Mario Carneiro (May 26 2018 at 13:35):

you need to use norm_num

Mario Carneiro (May 26 2018 at 13:35):

simp [(by norm_num : 0 <= 5)]

Kevin Buzzard (May 26 2018 at 13:36):

I don't understand what you are saying

Kevin Buzzard (May 26 2018 at 13:36):

I don't understand this stuff well enough

Kevin Buzzard (May 26 2018 at 13:36):

theorem root_5_squared : (sqrt 5) ^ 2 = 5 := by simp [sqr_sqrt,(dec_trivial : 0 <= 5)]-- fails

Kevin Buzzard (May 26 2018 at 13:36):

I am not even sure that's valid syntax

Mario Carneiro (May 26 2018 at 13:36):

it should be...

Mario Carneiro (May 26 2018 at 13:37):

the full proof is just sqr_sqrt (by norm_num : 0 <= 5)

Kevin Buzzard (May 26 2018 at 13:38):

theorem zero_le_5 : (0 : ℝ) ≤ 5 := by norm_num

theorem root_5_squared : (sqrt 5) ^ 2 = 5 := by simp [sqr_sqrt,zero_le_5]

Kevin Buzzard (May 26 2018 at 13:38):

First molehill conquered

Mario Carneiro (May 26 2018 at 13:38):

Oh, you might need to write simp [(by norm_num : (0:R) <= 5)]

Kevin Buzzard (May 26 2018 at 13:38):

Where?

Mario Carneiro (May 26 2018 at 13:39):

as a proof of the theorem

Mario Carneiro (May 26 2018 at 13:39):

that proves zero_le_5 inline, and uses it as a simp lemma in the main proof

Kevin Buzzard (May 26 2018 at 13:40):

It's really annoying to use Lean like this. Why do I have all these errors in mathlib?

Kevin Buzzard (May 26 2018 at 13:40):

imported file '/home/buzzard/lean-projects/lean-squares-in-fibonacci/_target/deps/mathlib/order/complete_lattice.lean' uses sorry
real_alpha.lean:1:0: warning

imported file '/home/buzzard/lean-projects/lean-squares-in-fibonacci/_target/deps/mathlib/order/bounded_lattice.lean' uses sorry
real_alpha.lean:1:0: warning

imported file '/home/buzzard/lean-projects/lean-squares-in-fibonacci/_target/deps/mathlib/data/finset.lean' uses sorry
real_alpha.lean:1:0: warning

imported file '/home/buzzard/lean-projects/lean-squares-in-fibonacci/_target/deps/mathlib/order/boolean_algebra.lean' uses sorry
real_alpha.lean:1:0: warning

imported file '/home/buzzard/lean-projects/lean-squares-in-fibonacci/_target/deps/mathlib/data/equiv.lean' uses sorry
real_alpha.lean:1:0: warning

imported file '/home/buzzard/lean-projects/lean-squares-in-fibonacci/_target/deps/mathlib/data/set/lattice.lean' uses sorry

Kevin Buzzard (May 26 2018 at 13:40):

What have I done wrong?

Mario Carneiro (May 26 2018 at 13:41):

maybe those files use sorry

Kevin Buzzard (May 26 2018 at 13:41):

I thought I was all up to date

Kevin Buzzard (May 26 2018 at 13:41):

They're all your files

Mario Carneiro (May 26 2018 at 13:41):

Look for an actual error

Mario Carneiro (May 26 2018 at 13:42):

Usually lean will have some error in a theorem, and then since the theorem failed it uses sorry instead, and then every other file that imports that file complains about the sorry so you get hundreds of sorry warnings

Kevin Buzzard (May 26 2018 at 13:42):

complete_lattice.lean:119:36: error

ambiguous overload, possible interpretations
  ⊥
  ⊥
Additional information:
/home/buzzard/lean-projects/lean-squares-in-fibonacci/_target/deps/mathlib/order/complete_lattice.lean:119:36: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because it failed to disambiguate overload using the expected type
  ?m_1
the following overloaded terms were applicable
  ⊥
  ⊥

Kevin Buzzard (May 26 2018 at 13:43):

Looks like much of a muchness to me

Kevin Buzzard (May 26 2018 at 13:44):

don't know how to synthesize placeholder
context:
α : Type u,
_inst_1 : lattice.complete_lattice.{u} α
⊢ Type ?l_1
complete_lattice.lean:120:36: error

ambiguous overload, possible interpretations
  @lattice.has_bot.bot.{?l_1} ?m_2 ?m_3
  @lattice.has_bot.bot.{?l_4} ?m_5 ?m_6
Additional information:
/home/buzzard/lean-projects/lean-squares-in-fibonacci/_target/deps/mathlib/order/complete_lattice.lean:120:36: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because it failed to disambiguate overload using the expected type
  ?m_1
the following overloaded terms were applicable
  @lattice.has_bot.bot.{?l_2} ?m_3 ?m_4
  @lattice.has_bot.bot.{?l_5} ?m_6 ?m_7

Kevin Buzzard (May 26 2018 at 13:44):

with pp_all on

Mario Carneiro (May 26 2018 at 13:44):

what about #print ⊥?

Kevin Buzzard (May 26 2018 at 13:45):

`⊥`:1024 :=
  | lattice.has_bot.bot _
  | lattice.has_bot.bot _

Mario Carneiro (May 26 2018 at 13:45):

some file somewhere has declared ⊥ as a global notation

Kevin Buzzard (May 26 2018 at 13:45):

Thanks

Mario Carneiro (May 26 2018 at 13:45):

I recently moved the location of the declaration of ⊥

Mario Carneiro (May 26 2018 at 13:46):

it's possible you have an old version of one of the files and so are getting a double declaration

Kevin Buzzard (May 26 2018 at 13:46):

Thanks

Kevin Buzzard (May 26 2018 at 13:46):

I can't see any of these symbols or bot in my file

Mario Carneiro (May 26 2018 at 13:46):

check lattice.lean

Kevin Buzzard (May 26 2018 at 13:47):

:~/lean-projects/lean-squares-in-fibonacci/_target/deps/mathlib$ git branch
* (HEAD detached at 6811f13)
  master

Kevin Buzzard (May 26 2018 at 13:47):

I don't know what detached head means

Mario Carneiro (May 26 2018 at 13:47):

or just search for notation `⊥`

Kevin Buzzard (May 26 2018 at 13:47):

Should I switch to master?

Mario Carneiro (May 26 2018 at 13:47):

it means you have a commit checked out, not a branch

Mario Carneiro (May 26 2018 at 13:48):

what does git status give?

Kevin Buzzard (May 26 2018 at 13:48):

That sounds right

Kevin Buzzard (May 26 2018 at 13:48):

shall I checkout a branch?

Kevin Buzzard (May 26 2018 at 13:48):

I did everything with leanpkg as far as I know

Mario Carneiro (May 26 2018 at 13:49):

leanpkg usually checks out commits, which is why it is like that

Kevin Buzzard (May 26 2018 at 13:49):

$ git status
HEAD detached at 6811f13
nothing to commit, working directory clean

Kevin Buzzard (May 26 2018 at 13:49):

Instead of trying to debug

Kevin Buzzard (May 26 2018 at 13:49):

can you just tell me how to install the latest mathlib and get it all working?

Mario Carneiro (May 26 2018 at 13:50):

You appear to have it already, from that status message

Kevin Buzzard (May 26 2018 at 13:50):

Is there just a brutal fix so I have a working version of mathlib? Should I just delete _target and run leanpkg something?

Kevin Buzzard (May 26 2018 at 13:50):

Or check out some other commit or branch?

Kevin Buzzard (May 26 2018 at 13:51):

I just want to get this fixed quickly, I am giving a talk in an hour

Mario Carneiro (May 26 2018 at 13:51):

yes probably, but I'm not a leanpkg expert

Kevin Buzzard (May 26 2018 at 13:51):

and then another one at 8 where I want to show Lean off

Kevin Buzzard (May 26 2018 at 13:51):

and all its erros

Kevin Buzzard (May 26 2018 at 13:51):

errors

Mario Carneiro (May 26 2018 at 13:51):

maybe back up the directory first, but sure just remove _target and do the usual leanpkg incantations

Mario Carneiro (May 26 2018 at 13:52):

that folder only has cached stuff so it should be fine

Kevin Buzzard (May 26 2018 at 13:52):

I'm on a train :-/

Mario Carneiro (May 26 2018 at 13:53):

try removing .olean files

Mario Carneiro (May 26 2018 at 13:53):

and rebuild

Kevin Buzzard (May 26 2018 at 13:53):

i did that already

Mario Carneiro (May 26 2018 at 13:54):

did you search for notation bot like I said?

Kevin Buzzard (May 26 2018 at 13:54):

git is working

Kevin Buzzard (May 26 2018 at 13:54):

really good

Kevin Buzzard (May 26 2018 at 13:54):

patchy 3g phone and hotspot

Mario Carneiro (May 26 2018 at 13:54):

this line

notation `⊥` := has_bot.bot _

should appear exactly once in mathlib, in bounded_lattice.lean

Kevin Buzzard (May 26 2018 at 13:55):

I got bored trying to work out why it was broken

Kevin Buzzard (May 26 2018 at 13:55):

I am under time pressure

Mario Carneiro (May 26 2018 at 13:55):

I'm hoping that the location of the second hit will hint at why you have old files

Kevin Buzzard (May 26 2018 at 13:55):

had

Mario Carneiro (May 26 2018 at 13:56):

that's why I'm giving suggestions that are fast to check

Kevin Buzzard (May 26 2018 at 13:58):

you could try simp {discharger := norm_num}, not sure if that works

I can't get it to work

Chris Hughes (May 26 2018 at 13:59):

How about this for a readable proof?

example : (((1 : ℝ) + √5) / 2) ^ 2 = ((1 : ℝ) + √5 ) / 2 + 1 :=
have h : (0 : ℝ) ≤ 5 := by norm_num,
begin
  rw [pow_two, div_mul_div, mul_add, mul_one, add_mul, one_mul, ← pow_two, sqr_sqrt h],
  ring,
end

Kevin Buzzard (May 26 2018 at 13:59):

import analysis.real tactic.norm_num tactic.ring

namespace real
noncomputable theory

def α := (real.sqrt 5 + 1) / 2
def β := 1 - α

theorem root_5_squared : (sqrt 5) ^ 2 = 5 := by simp [sqr_sqrt,(by norm_num : (0:ℝ) <= 5)]

lemma αβsum : α + β = 1 := begin
  unfold β,
  unfold α,
  norm_num, -- ;-)
end

lemma αβprod : α * β = -1 := begin
  unfold β,
  unfold α,
  rw [mul_sub,mul_one,add_div,mul_add,add_mul,add_mul], -- meh
  simp [root_5_squared],
  norm_num, -- unknown exception while type-checking theorem
end

Kevin Buzzard (May 26 2018 at 13:59):

I got an achievement -- "unknown exception while type-checking theorem"

Kevin Buzzard (May 26 2018 at 14:00):

Why isn't this easy

Kevin Buzzard (May 26 2018 at 14:00):

simp wants facts from norm_num but I don't know what facts

Kevin Buzzard (May 26 2018 at 14:00):

goal after simp is

Kevin Buzzard (May 26 2018 at 14:00):

⊢ 2⁻¹ +
      (sqrt 5 / 2 +
         (-(2⁻¹ * 2⁻¹) + (-(2⁻¹ * (sqrt 5 / 2)) + (-(sqrt 5 / 2 * 2⁻¹) + -(sqrt 5 / 2 * (sqrt 5 / 2)))))) =
    -1

Kevin Buzzard (May 26 2018 at 14:01):

I must have taken a wrong turn

Kevin Buzzard (May 26 2018 at 14:01):

I am not a competent driver when it comes to the reals

Mario Carneiro (May 26 2018 at 14:01):

simp on its own will not know how to finish the job

Mario Carneiro (May 26 2018 at 14:01):

you need ring for all that

Kevin Buzzard (May 26 2018 at 14:02):

All I want to do is prove that if alpha is (1+sqrt(5))/2 then alpha^2=alpha+1

Kevin Buzzard (May 26 2018 at 14:02):

in R

Kevin Buzzard (May 26 2018 at 14:02):

because if that's not easy

Kevin Buzzard (May 26 2018 at 14:02):

then what kind of an R have you got here

Kevin Buzzard (May 26 2018 at 14:02):

a computer scientist's one but not a mathematican's one

Kevin Buzzard (May 26 2018 at 14:03):

I completely understand the other approach

Kevin Buzzard (May 26 2018 at 14:03):

but for pedagogical reasons I would like to see this happening in R

Kevin Buzzard (May 26 2018 at 14:03):

I can always fall back on Nicholas' construction

Kevin Buzzard (May 26 2018 at 14:03):

which indeed I will ultimately fall back on

Kevin Buzzard (May 26 2018 at 14:04):

but my goal was not to explain how incredibly difficult it was to even the most trivial things

Mario Carneiro (May 26 2018 at 14:04):

I get it

Mario Carneiro (May 26 2018 at 14:04):

1 sec

Kevin Buzzard (May 26 2018 at 14:04):

Sorry to moan

Kevin Buzzard (May 26 2018 at 14:04):

I am giving an important talk

Kevin Buzzard (May 26 2018 at 14:05):

and I want it to be _really good_

Mario Carneiro (May 26 2018 at 14:05):

I believe it can be done with a short tactic invoke

Kevin Buzzard (May 26 2018 at 14:05):

so I want to make a really professional job of it

Mario Carneiro (May 26 2018 at 14:05):

I think you can use ring to get it down to an expression involving (sqrt 5)^2, and then use simp and norm_num to finish

Kevin Buzzard (May 26 2018 at 14:07):

Removed target and re-installed everything and I'm back up to speed :-)

Kevin Buzzard (May 26 2018 at 14:07):

one further step towards professional

Kevin Buzzard (May 26 2018 at 14:07):

No more errors

Kevin Buzzard (May 26 2018 at 14:08):

aargh that's a lie

Kevin Buzzard (May 26 2018 at 14:09):

I will sort this out later -- I've got until 8pm

Mario Carneiro (May 26 2018 at 14:09):

what time is it now?

Kenny Lau (May 26 2018 at 14:09):

I will sort this out later -- I've got until 8pm

what do you need to sort out?

Kevin Buzzard (May 26 2018 at 14:10):

I have loads of errors in mathlib

Kevin Buzzard (May 26 2018 at 14:10):

I've tried everything

Kevin Buzzard (May 26 2018 at 14:10):

I might reboot my computer

Kevin Buzzard (May 26 2018 at 14:10):

and recompile all .olean files

Kenny Lau (May 26 2018 at 14:10):

are you trying to prove anything?

Kevin Buzzard (May 26 2018 at 14:10):

but that's all I can think of

Kevin Buzzard (May 26 2018 at 14:11):

I'm tyring to prove that two real numbers are equal

Kevin Buzzard (May 26 2018 at 14:11):

I'll push

Kevin Buzzard (May 26 2018 at 14:12):

https://github.com/kbuzzard/lean-squares-in-fibonacci/blob/master/src/real_alpha.lean

Kevin Buzzard (May 26 2018 at 14:12):

But I want it to look sexy

Mario Carneiro (May 26 2018 at 14:13):

you could import data.real.basic instead

Mario Carneiro (May 26 2018 at 14:22):

import data.real.basic tactic.norm_num tactic.ring

open real
noncomputable theory

prefix `√`:90 := sqrt

def α := (√5 + 1) / 2
def β := 1 - α

theorem root_5_squared : √5 ^ 2 = 5 :=
by simp {discharger := `[norm_num]}

lemma αβsum : α + β = 1 := begin
  unfold α β,
  ring
end

lemma αβprod : α * β = -1 := begin
  unfold α β,
  ring,
  simp {discharger := `[norm_num]},
  ring
end

Kenny Lau (May 26 2018 at 14:22):

what

Kenny Lau (May 26 2018 at 14:27):

import data.real.basic tactic.norm_num

noncomputable theory

prefix `√`:90 := real.sqrt

def α := (1 + √5) / 2
def β := 1 - α

theorem root_5_squared : √5 * √5 = 5 :=
real.mul_self_sqrt $ show (0:ℝ) ≤ 5, by norm_num

lemma αβsum : α + β = 1 :=
show α + (1 - α) = 1,
from add_sub_cancel'_right α 1

lemma αβprod : α * β = -1 :=
calc  α * β
    = ((1 + √5) / 2) * (1 - (1 + √5) / 2) : rfl
... = ((1 + √5) / 2) * ((1 + 1) / 2 - (1 + √5) / 2) : by rw add_self_div_two
... = ((1 + √5) / 2) * (((1 + 1) - (1 + √5)) / 2) : by rw div_sub_div_same
... = ((1 + √5) / 2) * ((1 - √5) / 2) : by rw add_sub_add_left_eq_sub
... = ((1 + √5) * (1 - √5)) / (2 * 2) : by rw div_mul_div
... = (1 * 1 - √5 * √5) / (2 * 2) : by rw mul_self_sub_mul_self_eq
... = (1 * 1 - 5) / (2 * 2) : by rw root_5_squared
... = -1 : by norm_num

Kenny Lau (May 26 2018 at 14:27):

@Kevin Buzzard do you like direct proofs?

Mario Carneiro (May 26 2018 at 14:28):

You could also half-cheat and write a plausible-looking sequence of equalities all proven by ring

Kenny Lau (May 26 2018 at 14:28):

but that defeats the purpose of the presentation

Kevin Buzzard (May 26 2018 at 14:28):

This is somehow awful

Mario Carneiro (May 26 2018 at 14:28):

it makes it look nice and readable

Kevin Buzzard (May 26 2018 at 14:28):

but it's much better than nothing

Kevin Buzzard (May 26 2018 at 14:28):

But I don't want it to be readable

Kevin Buzzard (May 26 2018 at 14:28):

I want it to be trivial

Kenny Lau (May 26 2018 at 14:28):

what

Kevin Buzzard (May 26 2018 at 14:28):

An obscure one-liner?

Mario Carneiro (May 26 2018 at 14:28):

you didn't like my ring solution?

Kenny Lau (May 26 2018 at 14:29):

I thought you're teaching rigour

Kenny Lau (May 26 2018 at 14:29):

if you asked me in m1f to prove that alpha * beta = -1, that is exactly what I would write down

Kenny Lau (May 26 2018 at 14:29):

minus the by rw ... things

Kevin Buzzard (May 26 2018 at 14:29):

I don't understand -- what ring solution?

Kenny Lau (May 26 2018 at 14:29):

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/subject/Largest.20Square.20in.20the.20Fibonacci.20Sequence/near/127129776

Kenny Lau (May 26 2018 at 14:29):

Kenny Lau (May 26 2018 at 14:30):

I can't delete my own messages...

Kevin Buzzard (May 26 2018 at 14:30):

I want as many solutions as I can

Kevin Buzzard (May 26 2018 at 14:31):

And we vote for the most beautiful

Kenny Lau (May 26 2018 at 14:31):

beauty is in the eye of the beholder

Kenny Lau (May 26 2018 at 14:31):

in this case, you

Kenny Lau (May 26 2018 at 14:31):

it's you who is/are presenting

Mario Carneiro (May 26 2018 at 14:33):

semi-explicit, only one ring

lemma αβprod : α * β = -1 := begin
  unfold α β,
  ring,
  rw sqr_sqrt; norm_num
end

Kenny Lau (May 26 2018 at 14:33):

I still don't know what @Kevin Buzzard wants

Kenny Lau (May 26 2018 at 14:33):

what is the goal of this?

Reid Barton (May 26 2018 at 14:36):

or an intermediate one, still using calc

lemma αβsum : α + β = 1 := by dsimp [β]; ring

lemma αβprod : α * β = -1 :=
calc  α * β
    = ((1 + √5) / 2) * (1 - (1 + √5) / 2) : rfl
... = (1 * 1 - √5^2) / (2 * 2) : by ring
... = -1 : by rw real.sqr_sqrt; norm_num

Mario Carneiro (May 26 2018 at 14:37):

I guess you could write the middle line as (1 - √5^2) / 4 for extra clean

Kenny Lau (May 26 2018 at 14:37):

low-tech one-liners:

Kenny Lau (May 26 2018 at 14:37):

import data.real.basic tactic.norm_num

noncomputable theory

prefix `√`:90 := real.sqrt

def α := (1 + √5) / 2
def β := (1 - √5) / 2

theorem root_5_squared : √5 * √5 = 5 :=
real.mul_self_sqrt $ show (0:ℝ) ≤ 5, by norm_num

lemma αβsum : α + β = 1 :=
by rw [α, β, ← add_div]; simp

lemma αβprod : α * β = -1 :=
by rw [α, β, div_mul_div, ← mul_self_sub_mul_self_eq, root_5_squared]; norm_num

Kenny Lau (May 26 2018 at 14:38):

(is changing the definition allowed?)

Mario Carneiro (May 26 2018 at 14:40):

lemma αβprod : α * β = -1 :=
calc ((√5 + 1) / 2) * (1 - (√5 + 1) / 2)
    = (1 - √5^2) / 4 : by ring
... = -1 : by rw sqr_sqrt; norm_num

Kenny Lau (May 26 2018 at 14:40):

not very different from the one above...

Mario Carneiro (May 26 2018 at 14:41):

it's based on reid's

Kenny Lau (May 26 2018 at 14:42):

import data.real.basic tactic.norm_num

noncomputable theory

prefix `√`:90 := real.sqrt

def α := (1 + √5) / 2
def β := (1 - √5) / 2

lemma sqrt_5_mul_self : √5 * √5 = 5 :=
real.mul_self_sqrt $ show (0:ℝ) ≤ 5, by norm_num

lemma αβsum : α + β = 1 :=
by simp [α, β, add_div, neg_div, -one_div_eq_inv]

lemma αβprod : α * β = -1 :=
by simp [α, β, div_mul_div, add_mul, mul_add, sqrt_5_mul_self]; norm_num

Reid Barton (May 26 2018 at 14:42):

And I just took Kenny's long calc and deleted all the intermediate steps that could be handled by ring.

Reid Barton (May 26 2018 at 14:43):

I like calc here because the fact α * β = -1 is actually not immediately obvious to a human, and you'd write out about the same number of intermediate steps to explain the calculation to a human.

Kenny Lau (May 26 2018 at 14:43):

still avoiding ring as usual :P

Kenny Lau (May 26 2018 at 14:44):

I like my new definition

Kenny Lau (May 26 2018 at 14:44):

who likes my new definition

Mario Carneiro (May 26 2018 at 14:44):

I think your definition is nicer if you are going to define both alpha and beta

Mario Carneiro (May 26 2018 at 14:45):

In a human proof I would probably have an additional step in the middle with all four terms and cross out the cross terms

Kenny Lau (May 26 2018 at 14:46):

that's what I did with the add_mul and mul_add

Kenny Lau (May 26 2018 at 14:46):

import data.real.basic tactic.norm_num

noncomputable theory

prefix `√`:90 := real.sqrt

def α := (1 + √5) / 2
def β := (1 - √5) / 2

lemma sqrt_5_mul_self : √5 * √5 = 5 :=
real.mul_self_sqrt $ show (0:ℝ) ≤ 5, by norm_num1

lemma αβsum : α + β = 1 :=
by simp [α, β, add_div, neg_div, -one_div_eq_inv]

lemma αβprod : α * β = -1 :=
by simp [α, β, div_mul_div, add_mul, mul_add, sqrt_5_mul_self]; norm_num1

Kenny Lau (May 26 2018 at 14:46):

low-tech :P

Mario Carneiro (May 26 2018 at 14:46):

A long rw proof is hard to read though

Mario Carneiro (May 26 2018 at 14:47):

unless you step through it

Kenny Lau (May 26 2018 at 14:47):

I thought @Kevin Buzzard wants a one-liner

Mario Carneiro (May 26 2018 at 14:47):

and you can't even do that for a simp proof

Mario Carneiro (May 26 2018 at 14:47):

I think we have that already

Mario Carneiro (May 26 2018 at 14:48):

lemma αβprod : α * β = -1 :=
by unfold α β; ring; simp {discharger := `[norm_num]}; ring

Mario Carneiro (May 26 2018 at 14:51):

ooh, with this modification to norm_num:

meta def norm_num (loc : parse location) : tactic unit :=
let t := orelse' (norm_num1 loc) $
  simp_core {} (norm_num1 (interactive.loc.ns [none])) ff [] [] loc in
t >> repeat t

you can get away with just by unfold α β; ring; norm_num

Kevin Buzzard (May 26 2018 at 15:01):

I just want to explain to kids who don't know any better, what maths is

Kenny Lau (May 26 2018 at 15:02):

then why wouldn't you write down every step

Kevin Buzzard (May 26 2018 at 15:02):

All of this stuff is great

Kevin Buzzard (May 26 2018 at 15:02):

Because what is a step when you are 16 years old?

Kevin Buzzard (May 26 2018 at 15:02):

You have never thought about steps

Kevin Buzzard (May 26 2018 at 15:03):

You just answer the question

Mario Carneiro (May 26 2018 at 15:03):

I presume that will be part of the talk

Mario Carneiro (May 26 2018 at 15:03):

at least, the idea that math is built on axioms and rules

Mario Carneiro (May 26 2018 at 15:03):

and you have to use those rules to prove things

Mario Carneiro (May 26 2018 at 15:03):

the sense of "step" is not far from this

Kevin Buzzard (May 26 2018 at 15:09):

Yes exactly

Kevin Buzzard (May 26 2018 at 15:09):

I will be here at 8pm UK time (i.e. now + 3h50m) asking more stupid questions about real numbers

Nicholas Scheel (May 26 2018 at 16:37):

lemma α_sqr : α^2 = α + 1 := rfl in ℤα ;)

Kenny Lau (May 26 2018 at 16:37):

but he doesn't want to use Zalpha in the presentation lol

Nicholas Scheel (May 26 2018 at 16:38):

btw I proved point 3, should I leave it in Zalpha or move it to a point3.lean?

Kenny Lau (May 26 2018 at 16:38):

move it to point3.lean

Nicholas Scheel (May 26 2018 at 16:40):

done!

Nicholas Scheel (May 26 2018 at 16:43):

I tried and failed to prove that it is an integral domain, got any tips?

Kenny Lau (May 26 2018 at 16:44):

where are you stuck in?

Nicholas Scheel (May 26 2018 at 16:49):

it’s something like
a * c + b * d = 0 AND a * d + b * c + b * d = 0 IMPLIES THAT (a, b) = 0 OR (c, d) = 0

Nicholas Scheel (May 26 2018 at 16:52):

I understand that it’s equivalent to the fact that α is not an integer, and equivalent to the fact that 1 and α are linearly independent, but I don’t see how to do that from the definition of multiplication

Johan Commelin (May 26 2018 at 17:08):

Well, you could define an embedding of Zalpha into R.

Johan Commelin (May 26 2018 at 17:09):

I think we now have about a dozen proofs of why that works :wink:

Kenny Lau (May 26 2018 at 17:09):

proving that it is injective needs work also

Johan Commelin (May 26 2018 at 17:10):

That is the linear independence of 1 and alpha

Nicholas Scheel (May 26 2018 at 17:15):

sure, why not ;D

Kenny Lau (May 26 2018 at 17:15):

oh right you need to prove that sqrt(5) is irrational

Kevin Buzzard (May 26 2018 at 21:09):

Yeah, that's the analogue of showing that if $z=x+iy$ is a complex number which isn't zero, then you can divide by $z$ , by multiplying by $\overline{z}$ and then dividing by the non-zero real $z\overline{z}$ .

Kevin Buzzard (May 26 2018 at 21:10):

In this instance it boils down to proving that the product of $a+b\surd{5}$ and its Galois conjugate $a-b\surd{5}$ is non-zero if at least one of $a$ and $b$ is non-zero

Kevin Buzzard (May 26 2018 at 21:10):

\surdfor square roots in maths mode, not \sqrt

Kevin Buzzard (May 26 2018 at 21:10):

So as Kenny says it's precisely the irrationality of $\surd 5$ , or, more precisely, it's the statement that no rational number squared is $5$ (rather than any statement about real numbers not being rational)

Kevin Buzzard (May 26 2018 at 21:10):

So one way to do it is to prove that if $a+b\surd 5$ is non-zero then the rational $a^2-5b^2$ is non-zero and then use that a non-zero rational has an inverse.

Kevin Buzzard (May 26 2018 at 21:15):

I've just been telling some kids about Lean. Some of them got into it. We were doing induction on nat and on or and on false and stuff

Kevin Buzzard (May 26 2018 at 21:15):

I did some Fibonacci stuff

Kevin Buzzard (May 26 2018 at 21:15):

and some logic stuff

Kevin Buzzard (May 26 2018 at 21:15):

and we looked at why induction was a theorem in Lean

Nicholas Scheel (May 26 2018 at 21:28):

Well, you could define an embedding of Zalpha into R.

Thanks @Johan Commelin I think that worked ;) https://github.com/kbuzzard/lean-squares-in-fibonacci/blob/master/src/Zalpha_real.lean
again, ugly code, but it typechecks

Nicholas Scheel (May 26 2018 at 21:36):

and thanks @Chris Hughes for the alpha squared proof, such a time saver! :D

Kenny Lau (May 26 2018 at 22:41):

hmm, I wonder if we can shorten it

Kenny Lau (May 26 2018 at 22:58):

@Nicholas Scheel do you mind if I edit your files?

Nicholas Scheel (May 26 2018 at 22:58):

go for it!

Nicholas Scheel (May 26 2018 at 22:58):

I think I’m done for now, have to spend time on other things now

Nicholas Scheel (May 26 2018 at 22:59):

but I’m curious: what is norm_num? I haven’t found much documentation for it

Kevin Buzzard (May 26 2018 at 23:03):

It proves identities between explicit real numbers

Kevin Buzzard (May 26 2018 at 23:03):

And inequalities etc

Nicholas Scheel (May 26 2018 at 23:05):

cool :simple_smile:

Kenny Lau (May 26 2018 at 23:16):

theorem α_fib (n : ℕ) : α^(n+1) = ⟨Fib n, Fib (n+1)⟩ :=
begin
  induction n with n ih, { refl },
  change α*α^(n + 1) = ⟨Fib (n+1), Fib (n+2)⟩,
  rw ih, apply ext; simp [-add_comm],
  exact int.coe_nat_inj'.2 rfl
end

Kenny Lau (May 26 2018 at 23:16):

I golfed off a lot of lines from here

Nicholas Scheel (May 26 2018 at 23:18):

that’s great :smiley:

Kenny Lau (May 26 2018 at 23:20):

theorem α_fib (n : ℕ) : α^(n+1) = ⟨Fib n, Fib (n+1)⟩ :=
begin
  induction n with n ih, { refl },
  change α*α^(n + 1) = ⟨Fib (n+1), Fib (n+2)⟩,
  rw ih, apply ext; simp [-add_comm, Fib.is_fib]
end

Nicholas Scheel (May 26 2018 at 23:22):

🤯 change sounds amazing, funny that I hadn’t run across it before

Kenny Lau (May 26 2018 at 23:23):

do you realize that the show in tactic mode is different from the show in term mode

Kenny Lau (May 26 2018 at 23:23):

and then change is a generalization of that, that allows you to change the hypotheses as well

Nicholas Scheel (May 26 2018 at 23:29):

I haven’t used show in term mode, what’s the difference?

Kenny Lau (May 26 2018 at 23:30):

well there's not a huge difference

Reid Barton (May 26 2018 at 23:38):

I haven't used show in tactic mode!

Nicholas Scheel (May 26 2018 at 23:39):

that moment when computer programs understand analogies better than we expect :wink:

Kenny Lau (May 27 2018 at 01:27):

@Nicholas Scheel I hope you don't mind

Kenny Lau (May 27 2018 at 01:28):

https://github.com/kbuzzard/lean-squares-in-fibonacci/commit/7ba981070187c25d322b0e8de14021ec7214ddb9#diff-44f4839567c6f9e6617b4e04801b926a

Kenny Lau (May 27 2018 at 01:33):

TODO: incorporate this

Nicholas Scheel (May 27 2018 at 01:42):

not at all, that’s cool! thanks!

Kenny Lau (May 27 2018 at 02:00):

https://github.com/kbuzzard/lean-squares-in-fibonacci/commit/9106996916442e8f17239323d5a6cbe3e236efd3#diff-44f4839567c6f9e6617b4e04801b926a

Kenny Lau (May 27 2018 at 02:00):

done

Chris Hughes (May 27 2018 at 11:56):

I'm working on polys. I've just done the remainder theorem.

Kevin Buzzard (May 27 2018 at 12:01):

Polys in 1 variable need to go in mathlib so perhaps keep this in mind

Kevin Buzzard (May 27 2018 at 12:02):

When I write code now, I realise that sometimes it's code for me and sometimes it's stuff I think should be in mathlib

Kevin Buzzard (May 27 2018 at 12:02):

And I've started separating the two

Kevin Buzzard (May 27 2018 at 12:09):

I think this is an interesting consequence of proving "random" things like 144 being the largest square in the Fibonacci sequence.

Kevin Buzzard (May 27 2018 at 12:10):

I am pretty sure (am I right @Mario Carneiro ?) that mathlib has no interest in keeping and maintaining a proof of the curiosity that 144 is the largest square in the Fibonacci sequence.

Kevin Buzzard (May 27 2018 at 12:10):

However

Kevin Buzzard (May 27 2018 at 12:11):

When a mathematician looks at the proof, they expect to have to work in some areas

Kevin Buzzard (May 27 2018 at 12:11):

but conversely they expect some "standard tools" to be there

Kevin Buzzard (May 27 2018 at 12:11):

and this can be used to guide development of mathlib

Kevin Buzzard (May 27 2018 at 12:11):

For example, at some point someone is going to need quadratic reciprocity

Kevin Buzzard (May 27 2018 at 12:12):

and we will end up developing some of the tools needed to prove QR in this 144 proof

Kevin Buzzard (May 27 2018 at 12:12):

and I think there's a strong argument for QR going into mathlib as it's one of the jewels in the crown of mathematics

Kevin Buzzard (May 27 2018 at 12:13):

[as well as being a special case of Langlands Reciprocity ;-) ]

Kevin Buzzard (May 27 2018 at 12:13):

In the 144 proof we don't need full QR

Kevin Buzzard (May 27 2018 at 12:13):

but we need Gauss' Lemma and Euler's Criterion

Kevin Buzzard (May 27 2018 at 12:14):

so we're starting along the road to QR with these.

Kenny Lau (May 27 2018 at 12:29):

instance : decidable_linear_ordered_comm_ring ℤα :=

Kenny Lau (May 27 2018 at 12:29):

https://github.com/kbuzzard/lean-squares-in-fibonacci/blob/master/src/Zalpha_Zsqrt5.lean#L38

Kenny Lau (May 27 2018 at 12:29):

@Nicholas Scheel @Kevin Buzzard I find embedding into ℤ√5 a better idea than embedding into the reals

Kevin Buzzard (May 27 2018 at 12:43):

Mario's $\mathbb{Z}[\surd{5}]$ ?

Kevin Buzzard (May 27 2018 at 12:43):

(why doesn't sqrt work in LaTeX?)

Kevin Buzzard (May 27 2018 at 12:43):

He proved it was an ID?

Kenny Lau (May 27 2018 at 12:45):

He proved it was an ID?

yes

Kenny Lau (May 27 2018 at 12:45):

(althought I didn't use that)

Kenny Lau (May 27 2018 at 12:45):

(I used norm to prove that Zalpha is ID)

Kevin Buzzard (May 27 2018 at 12:45):

So how do you deduce ID from norm? You need that if norm is 0 then term is 0, right?

Kenny Lau (May 27 2018 at 12:46):

yes

Kenny Lau (May 27 2018 at 12:46):

which is tantamount to proving that sqrt5 is irrational

Kevin Buzzard (May 27 2018 at 12:46):

and so you need to prove irrationality#

Kevin Buzzard (May 27 2018 at 12:46):

right

Kenny Lau (May 27 2018 at 12:46):

on hindsight I should have used the embedding

Kenny Lau (May 27 2018 at 12:46):

but I still want to have the norm

Kevin Buzzard (May 27 2018 at 12:46):

I was suggesting that Mario might have done that already

Kenny Lau (May 27 2018 at 12:46):

the norm is useful

Kevin Buzzard (May 27 2018 at 12:46):

Sure

Kenny Lau (May 27 2018 at 12:46):

sure

Kevin Buzzard (May 27 2018 at 12:46):

And your norm commutes with Mario's

Kevin Buzzard (May 27 2018 at 12:47):

so you could have deduced your norm result from Mario's

Kevin Buzzard (May 27 2018 at 12:47):

and this would have saved you the trouble of proving irrationality of sqrt(5)

Kenny Lau (May 27 2018 at 12:47):

you see, in my embedding, I multiply the "real value" by 2

Kenny Lau (May 27 2018 at 12:47):

because alpha is not an element of Z[sqrt5]

Kenny Lau (May 27 2018 at 12:47):

and this would have saved you the trouble of proving irrationality of sqrt(5)

I know

Kenny Lau (May 27 2018 at 12:48):

I'll do it when I finish lunch

Kevin Buzzard (May 27 2018 at 12:48):

but I guess it's nice to check it every now and then

Nicholas Scheel (May 27 2018 at 12:53):

that’s cool! I’ll have to see how Zsqrt is decidable, I just avoided it because it’s irrational xD

Nicholas Scheel (May 27 2018 at 12:55):

oh duh: def sq_le (a c b d : ℕ) : Prop := c*a*a ≤ d*b*b

Kenny Lau (May 27 2018 at 15:35):

done

Kenny Lau (May 27 2018 at 15:35):

now the long proof that 5 is irrational is gone

Kenny Lau (May 27 2018 at 15:50):

theorem char_eq (z : ℤα) (H : z * z - z - 1 = 0) : z = α ∨ z = β :=
have H1 : (z - α) * (z - β) = 0,
  by rw [← H, α, β]; ring,
(eq_zero_or_eq_zero_of_mul_eq_zero H1).cases_on
  (or.inl ∘ eq_of_sub_eq_zero)
  (or.inr ∘ eq_of_sub_eq_zero)

Kenny Lau (May 27 2018 at 15:50):

completely pointless theorem

Kenny Lau (May 27 2018 at 15:50):

Gal(Zalpha/Z) = C2

Mario Carneiro (May 27 2018 at 15:51):

I guess z * z - z - 1 = (z - α) * (z - β) is also a way to prove alpha*beta = -1

Kenny Lau (May 27 2018 at 15:51):

sure

Kenny Lau (May 27 2018 at 16:24):

theorem gal (f : ℤα → ℤα) [is_ring_hom f] : f = id ∨ f = conj :=

Kenny Lau (May 27 2018 at 16:24):

lol I did it

Kevin Buzzard (May 27 2018 at 16:37):

nice!

Kevin Buzzard (May 27 2018 at 16:37):

Did you develop any tools for proving polys of degree n have at most n roots?

Kenny Lau (May 27 2018 at 17:12):

local notation `α` := Zalpha.units.α

#eval α^(-3:ℤ) -- -3 +   2α
#eval α^(-2:ℤ) --  2 +  -1α
#eval α^(-1:ℤ) -- -1 +   1α
#eval α^( 0:ℤ) --  1 +   0α
#eval α^( 1:ℤ) --  0 +   1α
#eval α^( 2:ℤ) --  1 +   1α
#eval α^( 3:ℤ) --  1 +   2α
#eval α^(12:ℤ) -- 89 + 144α