2006 STEP 3 Question 8

Stream: new members

[Shing Tak Lam]

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.

image.png

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]

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]

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

[Shing Tak Lam]

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]

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

[Shing Tak Lam]

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]

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]

you can prove h1 by ring

[Shing Tak Lam]

Alright, Thanks!

[Kevin Buzzard]

Did you try recover?

This is a great question for Lean!

[Kevin Buzzard]

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]

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

[Shing Tak Lam]

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

[Shing Tak Lam]

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

[Shing Tak Lam]

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

[Shing Tak Lam]

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]

Oh, recover was when your goal contained metavariables.

[Shing Tak Lam]

Ah. I see

[Kevin Buzzard]

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]

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]

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

[Shing Tak Lam]

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]

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]

No decisions have been made yet.

[Shing Tak Lam]

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

[Shing Tak Lam]

Thank you very much for all of your help

[Kevin Buzzard]

lemma Δ_one : Δ 1 = 0 :=
begin
  -- the standard trick
  suffices H : Δ 1 + Δ 1 = Δ 1,
    rwa add_left_eq_self at H,
  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,
    nat.cast_add, nat.cast_one],
  ring,
end

[Kevin Buzzard]

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

[Shing Tak Lam]

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]

This is just induction on natural numbers

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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]

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)

[Mario Carneiro]

nice

[Sebastien Gouezel]

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]

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]

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]

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

[Mario Carneiro]

it could be typeclass inference or something else

[Mario Carneiro]

code plz

[Shing Tak Lam]

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,
    nat.cast_add, nat.cast_one],
  ring,
end

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

[Shing Tak Lam]

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]

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]

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]

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]

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

[Mario Carneiro]

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,
    nat.cast_add, nat.cast_one, C_1],
  ring,
end

[Shing Tak Lam]

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]

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

[Shing Tak Lam]

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.

[Johan Commelin]

That's right

[Johan Commelin]

But simp only is fine

[Johan Commelin]

Write squeeze_simp to get some help

[Mario Carneiro]

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]

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

[Shing Tak Lam]

Ok. Thank you.

[Shing Tak Lam]

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]

Because you used variables

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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]

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]

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]

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]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

Delta4 will be called Delta.map_mul

[Kevin Buzzard]

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

[Mario Carneiro]

something with smul?

[Kevin Buzzard]

Oh is it not in canonical form??

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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]

This has the original question as a special case

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

pretty sure we don't

[Kevin Buzzard]

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

Feel free to ask if you need help

[Kevin Buzzard]

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

[Shing Tak Lam]

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]

So I guess I still have to revise...

[Shing Tak Lam]

(deleted)

[Johan Commelin]

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]

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

[Kevin Buzzard]

Has enough API been extracted?

[Johan Commelin]

What are you thinking of?

[Kevin Buzzard]

Did we locate the characteristic predicate yet?

[Kevin Buzzard]

I think this has something to do with transfer.

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

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]

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

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

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]

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]

For what it's worth

$ pip list | grep mathlibtools
mathlibtools                       0.0.4

[Kevin Buzzard]

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]

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

[Patrick Massot]

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]

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]

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]

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]

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

[Shing Tak Lam]

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

[Patrick Massot]

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

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

[Shing Tak Lam]

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.