Stream: new members

Topic: 2006 STEP 3 Question 8

Shing Tak Lam (Mar 23 2020 at 02:53):

Hello, I was trying to formalise my solution to this question in lean, but I'm getting an error saying the my result contains meta variables.

So far I have

import data.polynomial
data.real.basic

open polynomial

variable Δ : polynomial ℝ → polynomial ℝ
variables f g : polynomial ℝ
variable k : ℝ

axiom Δ1 : Δ X = C 1
axiom Δ2 : Δ(f + g) = Δ f + Δ g
axiom Δ3 : Δ(C k * f) = C k * Δ f
axiom Δ4 : Δ(f * g) = f * Δ g + g * Δ f

lemma ΔXcubed : Δ (X^3) = 3*X^2 := begin
have h1 : X^3 = X * X^2 := begin
have h11 : 3 = 2 + 1 := rfl,
rw h11,
rw pow_succ,
end -- Error Here
end


I've highlighted where the error is occuring, the error message is

tactic failed, result contains meta-variables
state:
no goals
state:
6 goals
Δ : polynomial ℝ → polynomial ℝ
⊢ Δ (X ^ 3) = 3 * X ^ 2

Δ : polynomial ℝ → polynomial ℝ
⊢ Type ?

Δ : polynomial ℝ → polynomial ℝ
⊢ comm_semiring ?m_1

Δ : polynomial ℝ → polynomial ℝ
⊢ has_pow (polynomial ?m_1) ℕ

Δ : polynomial ℝ → polynomial ℝ
⊢ has_mul (polynomial ?m_1)

Δ : polynomial ℝ → polynomial ℝ
⊢ has_pow (polynomial ?m_1) ℕ


I think I know why the error is occurring, as I didn't specify the type of X, so lean doesn't know that it has pow mul, etc. But I'm not sure how or where I could add the type annotations?

Also, when I use the axioms, rw \Delta4 doesn't work, I need to specify rw \Delta4 \Delta. Making \Delta a constant fixes this, but then it still doesn't fix the error message above. In this case, should \Delta be variable or constant? Since I don't care what Delta is, as long as it satisfies those axioms.

Mario Carneiro (Mar 23 2020 at 02:59):

those axioms should be variables. If you make them axioms then they will implicitly quantify over all Delta, meaning that you are adding an axiom to lean that says that all functions are derivations. Since this is false, the axiom will make lean inconsistent

Yury G. Kudryashov (Mar 23 2020 at 03:01):

And you probably want to include all these variables so that they will be available in tactic proofs.

Shing Tak Lam (Mar 23 2020 at 03:30):

Alright thank you, I've edited it with your suggestions. However, I still have an issue with the results contains meta-variables.

Yury G. Kudryashov (Mar 23 2020 at 03:33):

Can't help without looking at your code...

Shing Tak Lam (Mar 23 2020 at 03:36):

Apologies. The error message is basically the same after changing the axioms to variables. I've also changed f g and k to be in foralls instead of variables.

import data.polynomial
data.real.basic

open polynomial

variable Δ : polynomial ℝ → polynomial ℝ
include Δ

variable Δ1 : Δ X = C 1
variable Δ2 : ∀ (f g : polynomial ℝ), Δ(f + g) = Δ f + Δ g
variable Δ3 : ∀ (k : ℝ) (f : polynomial ℝ), Δ(C k * f) = C k * Δ f
variable Δ4 : ∀ (f g : polynomial ℝ), Δ(f * g) = f * Δ g + g * Δ f
include Δ1 Δ2 Δ3 Δ4

lemma ΔXcubed : Δ (X^3) = 3*X^2 := begin
have h1 : X^3 = X * X^2 := begin
have h11 : 3 = 2 + 1 := rfl,
rw h11,
rw pow_succ,
end -- ERROR HERE
end


Shing Tak Lam (Mar 23 2020 at 03:38):

Nevermind, I've figured it out. I needed to add the type annotation in the inner have statement, as the X in the inner statement is different to the one in the theorem statement.

Mario Carneiro (Mar 23 2020 at 03:41):

you can prove h1 by ring

Alright, Thanks!

Kevin Buzzard (Mar 23 2020 at 07:07):

Did you try recover?

This is a great question for Lean!

Kevin Buzzard (Mar 23 2020 at 07:45):

I think you might be better off proving lemma Δ_one : Δ 1 = 0 first, and then lemma ΔX_pow_succ (n : ℕ) : Δ (X ^ (n + 1)) = (n + 1) * X ^ n

Shing Tak Lam (Mar 23 2020 at 07:47):

I'm sorry, but I'm not sure what you mean by using recover.

Shing Tak Lam (Mar 23 2020 at 07:47):

I've already proved that \Delta c = 0 for all c.

Shing Tak Lam (Mar 23 2020 at 07:47):

I've already proved that \Delta c = 0 for all c.

Shing Tak Lam (Mar 23 2020 at 07:47):

I'm sorry, but I'm not sure what you mean by using recover.

Shing Tak Lam (Mar 23 2020 at 07:48):

And I did prove the general case of X^n, although I used X^n and not X^(n+1), which had an interesting base case

Kevin Buzzard (Mar 23 2020 at 07:48):

Oh, recover was when your goal contained metavariables.

Ah. I see

Kevin Buzzard (Mar 23 2020 at 07:49):

The problem with X^n directly is that when n=1 the inductive hypothesis involves 0 - 1 so has to be dealt with as a special case.

Shing Tak Lam (Mar 23 2020 at 07:50):

Yeah, when I was doing this question for STEP prep I thought it would be interesting to do in lean, as the steps revolved around these 4 rules. Now that no one even knows what's gonna happen with A Levels/STEP I had a bit of free time so I thought I'd give it a shot in Lean.

Kevin Buzzard (Mar 23 2020 at 07:51):

My son is in the same position -- sitting on a Cambridge offer with no idea what's going to happen next.

Shing Tak Lam (Mar 23 2020 at 07:51):

That makes sense, I did it on paper first and tried a direct translation. In retrospect X^(n+1) makes more sense. I'm gonna refactor it.

Shing Tak Lam (Mar 23 2020 at 07:52):

Yeah, Cambridge sent out an email like hours before the Government announcement, which wasn't that helpful.

(Not that any of my other Universities seem to know what is happening, do you know anything about Imperial?)

Kevin Buzzard (Mar 23 2020 at 07:52):

No decisions have been made yet.

Shing Tak Lam (Mar 23 2020 at 07:53):

Alright. Just that they haven't said anything since January, which was slightly worrying.

Shing Tak Lam (Mar 23 2020 at 07:53):

Thank you very much for all of your help

Kevin Buzzard (Mar 23 2020 at 08:17):

lemma Δ_one : Δ 1 = 0 :=
begin
-- the standard trick
suffices H : Δ 1 + Δ 1 = Δ 1,
conv begin to_rhs,
rw (show (1 : polynomial ℝ) = 1 * 1, by ring),
end,
rw Δ4,
ring,
end

lemma ΔX_pow_succ (n : ℕ) : Δ (X ^ (n + 1)) = (n + 1) * X ^ n := begin
induction n with d hd,
{ -- base case
rw [pow_one, Δ1, nat.cast_zero],
ring,
},
rw [nat.succ_eq_add_one, pow_succ, Δ4, Δ1, hd, pow_succ,
ring,
end


Kevin Buzzard (Mar 23 2020 at 08:22):

It helps a lot knowing what ring can and cannot do.

Shing Tak Lam (Mar 23 2020 at 08:31):

Again, thank you very much.

This (once again) reminds me I should probably read TPIL. show is nicer than what I've been doing, which is have then rw, which clutters up my local context a lot, and I end up with a lot of local hypotheses which are only used once.

For the final part of the question, the proof that \Delta f = df/dx for all polynomial f, I did it (on paper) by arguing that it's true for a polynomial of degree 1 (and 0), and then using induction, assuming that it is true for a polynomial of degree n then showing that it's true for a polynomial of degree n+1, therefore it is true for all polynomials. I've tried looking in data.polynomial, but I don't think I've seen this functionality in there. So I might have to do it another way.

I'm gonna look ring (and probably what a ring is first).

Mario Carneiro (Mar 23 2020 at 08:54):

This is just induction on natural numbers

Mario Carneiro (Mar 23 2020 at 08:55):

I'm pretty sure there is a degree function on polynomials

Mario Carneiro (Mar 23 2020 at 08:56):

The question I have about this problem is, do we have the definition of the derivative of a polynomial yet? Do we know it is a polynomial? I'm not sure how you intend to write the theorem statement

Johan Commelin (Mar 23 2020 at 08:58):

Mario Carneiro said:

I'm pretty sure there is a degree function on polynomials

Yes, and there is also nat_degree which is a natural number. (degree 0 is not natural)

Shing Tak Lam (Mar 23 2020 at 08:59):

So induction on degree p where p is the polynomial? The degree function returns an option nat though, so I'll have to look at that further.

I haven't written it yet, but there is a polynomial.derivative function, so I think it'll just be forall (p : polynomial R), derivative p = \Delta p.

Johan Commelin (Mar 23 2020 at 08:59):

We have the formal derivative of a polynomial, and also a proof that as a function it coincides with the analytical derivative (if you work over a normed field or something)

nice

Sebastien Gouezel (Mar 23 2020 at 09:26):

There is a function polynomial.induction_on that is designed precisely for this kind of induction. You can for instance have a look at analysis/calculus/deriv, line 1116.

Shing Tak Lam (Mar 23 2020 at 09:36):

Ok. Thank you all very much. I'll give that a shot when I have some more time to look at this.

Shing Tak Lam (Mar 23 2020 at 11:43):

I've had some free time just then and I tried Kevin's solution from above. However when i pasted it into lean I got a (deterministic) timeout. Seems like the rings are taking too long. I doubt my laptop is too slow, but that is a possibility.

Any suggestions to how I can fix this?

Mario Carneiro (Mar 23 2020 at 11:44):

ring performs very fast on almost all not-contrived examples, so that's not likely to be the problem

Mario Carneiro (Mar 23 2020 at 11:44):

it could be typeclass inference or something else

code plz

Shing Tak Lam (Mar 23 2020 at 11:47):

Minimum Working Example

import data.polynomial
data.real.basic
tactic

open polynomial

variable Δ : polynomial ℝ → polynomial ℝ
include Δ

variable Δ1 : Δ X = C 1
variable Δ2 : ∀ (f g : polynomial ℝ), Δ(f + g) = Δ f + Δ g
variable Δ3 : ∀ (k : ℝ) (f : polynomial ℝ), Δ(C k * f) = C k * Δ f
variable Δ4 : ∀ (f g : polynomial ℝ), Δ(f * g) = f * Δ g + g * Δ f
include Δ1 Δ2 Δ3 Δ4

lemma ΔXn (n : ℕ) : Δ (X^(n+1)) = (n+1)*X^n := begin
induction n with d hd,
{ -- base case
rw [pow_one, Δ1, nat.cast_zero],
ring,
},
rw [nat.succ_eq_add_one, pow_succ, Δ4, Δ1, hd, pow_succ,
ring,
end


The lemma is just the one Kevin posted above, so it probably worked on his machine.

Shing Tak Lam (Mar 23 2020 at 11:48):

It might be of use: #eval lean.version is (3, (6, 1)), mathlib is mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "093ac77ac9d27ce83ebf4e76ca5bd9b3eaebedaa"}

Shing Tak Lam (Mar 23 2020 at 11:49):

The lemma checks almost immediately if I comment out the ring in the inductive case (the one at the end of the lemma)

Mario Carneiro (Mar 23 2020 at 11:57):

The goal you gave to ring is

⊢ X * ((↑d + 1) * X ^ d) + X * X ^ d * C 1 = (↑d + 1 + 1) * (X * X ^ d)


which is not an equality that is valid from the axioms of rings alone (because of the C 1)

Mario Carneiro (Mar 23 2020 at 11:59):

I think ring is probably taking forever because it does some processing to see if different looking expressions are defeq, and it is unfolding C 1

Mario Carneiro (Mar 23 2020 at 12:00):

IIRC there is an option to disable that, but then it will just fail in this case

Mario Carneiro (Mar 23 2020 at 12:01):

This works

lemma ΔXn (n : ℕ) : Δ (X^(n+1)) = (n+1)*X^n := begin
induction n with d hd,
{ -- base case
rw [pow_one, Δ1, nat.cast_zero],
ring,
},
rw [nat.succ_eq_add_one, pow_succ, Δ4, Δ1, hd, pow_succ,
ring,
end


Shing Tak Lam (Mar 23 2020 at 12:01):

Huh... Alright. (I didn't write this).

Adding rw (show C (1:ℝ) = 1, by simp), before ring fixed this.

Thank you very much.

Mario Carneiro (Mar 23 2020 at 12:02):

Alternatively you can probably use simp instead of rw since half of those equations are simp lemmas

Shing Tak Lam (Mar 23 2020 at 12:03):

I see. I thought I saw somewhere that it's best to only use simp as the last tactic in a proof. That's why I didn't use it there.

That's right

Johan Commelin (Mar 23 2020 at 12:04):

But simp only is fine

Johan Commelin (Mar 23 2020 at 12:04):

Write squeeze_simp to get some help

Mario Carneiro (Mar 23 2020 at 12:04):

lemma ΔXn (n : ℕ) : Δ (X^(n+1)) = (n+1)*X^n := begin
induction n with d hd,
{ -- base case
rw [pow_one, Δ1, nat.cast_zero],
ring,
},
rw [pow_succ, Δ4, hd], simp [Δ1, pow_succ],
ring,
end


Mario Carneiro (Mar 23 2020 at 12:05):

using simp before a tactic that doesn't care too much about the shape of the input, like ring, is okay

Ok. Thank you.

Shing Tak Lam (Mar 23 2020 at 12:24):

Another question, when I try to rw ΔXn, it doesn't work. But rw ΔXn Δ works. But then it puts all of Δ1 Δ2 Δ3 Δ4 as new goals. Why? It's easy to solve (repeat {assumption}), but I'd still like to know why this is the case.

Kevin Buzzard (Mar 23 2020 at 13:16):

Because you used variables

Kevin Buzzard (Mar 23 2020 at 13:17):

The theorems you're proving are "if Delta satisfies all these axioms then..." and the proofs are hence all functions which demand proofs of all the axioms as input

Kevin Buzzard (Mar 23 2020 at 13:18):

One way around this would probably be to make some sort of structure to carry the variables around in

Mario Carneiro (Mar 23 2020 at 13:20):

You can probably also use parameters but it doesn't take much to stumble on places where they don't work very well

Kevin Buzzard (Mar 23 2020 at 13:22):

If you used parameters you would probably be able to avoid this issue in this one particular lean file, but if someone were to import your file because they wanted to use your work, the extra assumptions would be back by default

Kevin Buzzard (Mar 23 2020 at 13:22):

And the user could probably try to include them but then they have to remember to exclude them later. This set up happens very little in mathlib

Mario Carneiro (Mar 23 2020 at 13:23):

I think that's what you want in this case though. There are two or three intermediate lemmas and you don't want to refer to the assumptions since they are fixed, but once you reach the goal, you discharge everything and it becomes a regular theorem with a bunch of hypotheses

Kevin Buzzard (Mar 23 2020 at 13:24):

Here's how it would work with structures. You could define delta-structure on a ring R to be a function called Delta from polynomial R to polynomial R which satisfied the axioms. Just like the definition of a group in the group theory game.

Mario Carneiro (Mar 23 2020 at 13:25):

I think it has a name, it's called a derivation

Kevin Buzzard (Mar 23 2020 at 13:26):

And then you want to prove that if Delta is any delta-structure then the underlying map Delta.to_fun must agree with differentiation

Kevin Buzzard (Mar 23 2020 at 13:27):

A general derivation goes from R to another ring A and there is no Delta 1 axiom

Kevin Buzzard (Mar 23 2020 at 13:28):

The advantage of the structure approach is that you have easy access to the axioms: Delta.map_add is Delta2 for the function Delta.to_fun for example

Kevin Buzzard (Mar 23 2020 at 13:29):

Delta4 will be called Delta.map_mul

Kevin Buzzard (Mar 23 2020 at 13:30):

And someone better at knowing Lean's naming convention can figure out what Delta3 is called

Mario Carneiro (Mar 23 2020 at 13:30):

something with smul?

Kevin Buzzard (Mar 23 2020 at 13:34):

Oh is it not in canonical form??

Kevin Buzzard (Mar 23 2020 at 13:35):

I understand this canonical form/naming convention far worse than I would like to

Mario Carneiro (Mar 23 2020 at 13:43):

No, I think it's fine to write C k * p instead of k \bu p since it's an algebra

Mario Carneiro (Mar 23 2020 at 13:43):

I just meant that something like map_smul could be used for the name

Mario Carneiro (Mar 23 2020 at 13:43):

but since it isn't written with \bu that's a bit of a lie, so perhaps map_C_mul is better

Kevin Buzzard (Mar 23 2020 at 13:52):

The correct theorem from the point of view of derivations is that if we have a structure satisfying the last three axioms then there exists a unique polynomial g such that Delta (f) = g*f', and that g can be taken to be Delta(X)

Kevin Buzzard (Mar 23 2020 at 13:52):

This has the original question as a special case

Kevin Buzzard (Mar 23 2020 at 13:54):

Do we have a theory of derivations in Lean already? @Johan Commelin ?

Kevin Buzzard (Mar 23 2020 at 13:55):

I think it would be quite fun to prove the universal property of derivations in general.

Mario Carneiro (Mar 23 2020 at 13:59):

pretty sure we don't

Kevin Buzzard (Mar 23 2020 at 14:02):

@Shing Tak Lam so there's your homework while your teachers go through all the people in your year awarding them A-levels. I wonder if they'll do it anonymously?

Kevin Buzzard (Mar 23 2020 at 14:02):

Feel free to ask if you need help

Kevin Buzzard (Mar 23 2020 at 14:03):

But let's make a new thread because this one has a silly name. It can go in #maths

Shing Tak Lam (Mar 23 2020 at 14:05):

I had a meeting with my teachers earlier, and as I'm doing International A Levels, apparently my exams are still going ahead... It's just STEP that's a maybe...

Apparently the exam boards think that it's safe to go ahead (even though IB has cancelled for everyone as well).

Shing Tak Lam (Mar 23 2020 at 14:05):

So I guess I still have to revise...

(deleted)

Johan Commelin (Mar 23 2020 at 14:11):

Kevin Buzzard said:

Do we have a theory of derivations in Lean already? Johan Commelin ?

Not yet, but @Kenny Lau looked into it at some point, I htink.

Kenny Lau (Mar 23 2020 at 14:12):

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/derivation/near/170730598

Kevin Buzzard (Mar 23 2020 at 14:17):

Has enough API been extracted?

Johan Commelin (Mar 23 2020 at 14:17):

What are you thinking of?

Kevin Buzzard (Mar 23 2020 at 14:18):

Did we locate the characteristic predicate yet?

Kevin Buzzard (Mar 23 2020 at 14:18):

I think this has something to do with transfer.

Johan Commelin (Mar 23 2020 at 14:19):

No, I don't think much happened so far.

Johan Commelin (Mar 23 2020 at 14:19):

Also, didn't we switch to calling it the "characteristic predicate"?

Kevin Buzzard (Mar 23 2020 at 14:20):

Somehow the bare minimum API is the universal property, and then there is the problem of isolating the characteristic predicate and proving that a module satisfies the characteristic predicate iff it's the differentials

Kevin Buzzard (Mar 24 2020 at 13:47):

@Kenny Lau

import data.polynomial

open polynomial

structure delta_structure (R : Type) [comm_ring R] :=
(to_fun : polynomial R → polynomial R)
(map_X' : to_fun X = 1)
(map_add' : ∀ (f g : polynomial R), to_fun (f + g) = to_fun f + to_fun g)
(map_C_mul' : ∀ (k : R) (f : polynomial R), to_fun (C k * f) = C k * to_fun f)
(map_mul' : ∀ (f g : polynomial R), to_fun (f * g) = f * to_fun g + g * to_fun f)

namespace delta_structure

variables {R : Type} [comm_ring R] (Δ : delta_structure R)

instance : has_coe_to_fun (delta_structure R) := ⟨_, to_fun⟩

@[simp] theorem map_X (Δ : delta_structure R) : Δ X = 1 := Δ.map_X'

@[simp] theorem map_add (Δ : delta_structure R) : ∀ {f g : polynomial R}, Δ (f + g) = Δ f + Δ g := Δ.map_add'

@[simp] theorem map_C_mul : ∀ (k : R) (f : polynomial R), Δ (C k * f) = C k * Δ f := Δ.map_C_mul'

@[simp] theorem map_mul : ∀ (f g : polynomial R), Δ (f * g) = f * Δ g + g * Δ f := Δ.map_mul'

end delta_structure


What do you think of my structure?

Kevin Buzzard (Mar 27 2020 at 12:46):

@Shing Tak Lam now has a github repo where this question is solved using derivations on a polynomial ring. @Patrick Massot at the time of writing I see that he only has one branch, which is lean-3.4.2. Is this something to do with the tooling? Shing -- did you use leanproject to make this repo?

Kevin Buzzard (Mar 27 2020 at 12:50):

the linter doesn't like the simps above but now I have a much better understanding of what is going on there.

Shing Tak Lam (Mar 27 2020 at 12:58):

Yes I did use leanproject. Just to check I made a new project.

$leanproject new test > mkdir -p test > cd test > mkdir src > git init -q > git checkout -b lean-3.4.2 Switched to a new branch 'lean-3.4.2' configuring test 0.1 Adding mathlib  I'm kinda confused now as that shouldn't be happening... Looking at the repo at https://github.com/leanprover-community/mathlib-tools/blob/96734b3f6e7b1b6d69f86e18f4fee9c4c3e8bfff/mathlibtools/lib.py#L435 the branch should be called master. Shing Tak Lam (Mar 27 2020 at 12:59): For what it's worth $ pip list | grep mathlibtools
mathlibtools                       0.0.4


Kevin Buzzard (Mar 27 2020 at 12:59):

The tooling is brand new, much better than what we had before, but still contains a few minor glitches. It has already transformed my workflow though.

Kevin Buzzard (Mar 27 2020 at 12:59):

Yeah, that number is an indication of how new it is :-)

Patrick Massot (Mar 27 2020 at 13:35):

leanproject still uses leanpkg to create new projects. And leanpkg uses the default elan toolchain. We should change that, but that requires finding time to do it.

Patrick Massot (Mar 27 2020 at 13:36):

Also note that every complain or feature request about leanproject that is expressed here but not in a GitHub issue currently falls into a black hole.

Shing Tak Lam (Mar 27 2020 at 14:22):

Mhm... I found

https://github.com/leanprover-community/mathlib-tools/issues/26

and

https://github.com/leanprover-community/mathlib-tools/commit/5768b8fdf7de059eb8d4d663bd42fc8f9809190c

So this should be fixed...

Patrick Massot (Mar 27 2020 at 14:32):

The lean-3.4.2 exists in your repository, but the master branch also exist. Did you need to manually merge one branch into the other?

Shing Tak Lam (Mar 27 2020 at 14:36):

That was me renaming the branch locally from lean-3.4.2 to master then pushing it.

Shing Tak Lam (Mar 27 2020 at 14:37):

lean-3.4.2 now only exists on github but not on my local copy. I can probably delete it.

Patrick Massot (Mar 27 2020 at 14:50):

I'm sorry I can't reproduce this locally.

$leanproject new test$ git a leanpkg.toml
$git commit$ git branch
* master


Shing Tak Lam (Mar 27 2020 at 14:52):

No problem. I have a few ideas on what may have caused this, I'll give it a go tomorrow. If I find anything then I'll report back.

Last updated: May 08 2021 at 18:17 UTC