## Stream: maths

### Topic: strange rw behaviour with mv_polynomial

#### Kevin Buzzard (Mar 30 2020 at 15:06):

Shing Tak Lam managed to get rw zero_add to fail on a goal of the form 0 + p = p where p : mv_polynomial R S.

Working with multivariate polynomials rings, and not doing anything particularly fishy as far as I can see (but maybe I'm wrong), he created a zero which was a finsupp.has_zero. The first example below refuses to rewrite, which surprises me because the equality is an equality of mv_polynomials. The second example rewrites fine, which also surprises me because this time the equality is an equality of finsupps. @Gabriel Ebner how do I debug this one?

import data.mv_polynomial

open mv_polynomial

variables (R : Type) [comm_ring R] (S : Type) (p : mv_polynomial S R)

-- problematic proof of p = 0 + p with a funny zero which can show up
-- if you're working with mv_polynomials

-- set_option pp.all true
example : p =
-- zero
(@has_zero.zero.{0}
(@finsupp.{0 0} (@finsupp.{0 0} S nat nat.has_zero) R
(@mul_zero_class.to_has_zero.{0} R
(@semiring.to_mul_zero_class.{0} R
(@comm_semiring.to_semiring.{0} R
(@comm_ring.to_comm_semiring.{0} R _inst_1)))))
(@finsupp.has_zero.{0 0} (@finsupp.{0 0} S nat nat.has_zero) R
(@mul_zero_class.to_has_zero.{0} R
(@semiring.to_mul_zero_class.{0} R
(@comm_semiring.to_semiring.{0} R
(@comm_ring.to_comm_semiring.{0} R _inst_1))))))
+ p :=
begin
-- ⊢ p = 0 + p
symmetry,
-- ⊢ 0 + p = p (GOAL A)
-- rw zero_add, -- still fails
exact zero_add p -- closes goal
end

-- but with 0 + p = p the rewrite works

example : (@has_zero.zero.{0}
(@finsupp.{0 0} (@finsupp.{0 0} S nat nat.has_zero) R
(@mul_zero_class.to_has_zero.{0} R
(@semiring.to_mul_zero_class.{0} R
(@comm_semiring.to_semiring.{0} R
(@comm_ring.to_comm_semiring.{0} R _inst_1)))))
(@finsupp.has_zero.{0 0} (@finsupp.{0 0} S nat nat.has_zero) R
(@mul_zero_class.to_has_zero.{0} R
(@semiring.to_mul_zero_class.{0} R
(@comm_semiring.to_semiring.{0} R
(@comm_ring.to_comm_semiring.{0} R _inst_1))))))
+ p = p :=
begin
-- ⊢ 0 + p = p (GOAL B)
end

-- but this fails! So how did rw find the add_monoid instance?
example : add_monoid (@finsupp.{0 0} (@finsupp.{0 0} S nat nat.has_zero) R
(@mul_zero_class.to_has_zero.{0} R
(@semiring.to_mul_zero_class.{0} R
(@comm_semiring.to_semiring.{0} R
(@comm_ring.to_comm_semiring.{0} R _inst_1))))) := by apply_instance


#### Kevin Buzzard (Mar 30 2020 at 15:08):

GOAL A is @eq.{1} (@mv_polynomial.{0 0} S R (@comm_ring.to_comm_semiring.{0} R _inst_1)) and GOAL B is @eq.{1} (@finsupp.{0 0} (@finsupp.{0 0} S nat nat.has_zero) R ...

No

#### Kevin Buzzard (Mar 30 2020 at 15:09):

The one where the rewrite fails is mv_polynomial addition, the one that succeeds is finsupp addition.

#### Gabriel Ebner (Mar 30 2020 at 15:13):

Try rw zero_add after setting

set_option trace.type_context.is_def_eq true
set_option trace.type_context.is_def_eq_detail true


#### Gabriel Ebner (Mar 30 2020 at 15:14):

You should be able to make sense of the output, it's not very long.

Thanks!

#### Kevin Buzzard (Mar 30 2020 at 15:16):

The problem seems to be this:

[type_context.is_def_eq_detail] [3]: mv_polynomial S R =?= (S →₀ ℕ) →₀ R
[type_context.is_def_eq_detail] [4]: mv_polynomial =?= finsupp
[type_context.is_def_eq_detail] on failure: mv_polynomial =?= finsupp


Lean correctly asks whether the mv_polynomial is the finsupp, and this is true because this is literally the definition of mv_polynomial S R, but Lean fails to spot this.

#### Kevin Buzzard (Mar 30 2020 at 15:16):

Oh no wait, I am out of date

#### Gabriel Ebner (Mar 30 2020 at 15:17):

Now go to the definition of rewrite_cfg and check what the default value of md is.

#### Kevin Buzzard (Mar 30 2020 at 15:17):

As of ten days ago, mv_polynomial is defined to be add_monoid_algebra.

#### Kevin Buzzard (Mar 30 2020 at 15:17):

Gabriel Ebner said:

Now go to the definition of rewrite_cfg and check what the default value of md is.

I don't know what this means.

#### Gabriel Ebner (Mar 30 2020 at 15:18):

ctrl+p #tactic.rewrite_cfg

#### Gabriel Ebner (Mar 30 2020 at 15:18):

It's the default transparency setting for the rw tactic, which explains why Lean doesn't recognize these two types as definitionally equal.

#### Kevin Buzzard (Mar 30 2020 at 15:21):

You mean just look at the definition in core Lean? It's md := reducible

#### Kevin Buzzard (Mar 30 2020 at 15:21):

I have no idea what md means

#### Kevin Buzzard (Mar 30 2020 at 15:22):

-- TODO(Leo): improve documentation

#### Kevin Buzzard (Mar 30 2020 at 15:22):

Oh I see you just told me what it meant

#### Gabriel Ebner (Mar 30 2020 at 15:22):

md is the default reducibility setting. It tells Lean what definitions to unfold when unifying terms.

#### Gabriel Ebner (Mar 30 2020 at 15:22):

reducible means it will only unfold definitions marked as reducible.

#### Kevin Buzzard (Mar 30 2020 at 15:23):

All this X =?= Y trace output is Lean doing unification?

:+1:

#### Patrick Massot (Mar 30 2020 at 15:24):

Yes, =?= (or its fancy unicode version) is the symbol describing a unification problem.

#### Kevin Buzzard (Mar 30 2020 at 15:24):

example : mv_polynomial S R = ((S →₀ ℕ) →₀ R) := rfl but this isn't good enough

#### Gabriel Ebner (Mar 30 2020 at 15:26):

I've posted this another thread today, if you want a "reducible-only" rfl, you can use the following:

example : mv_polynomial S R = ((S →₀ ℕ) →₀ R) :=
by tactic.reflexivity tactic.transparency.reducible


#### Kevin Buzzard (Mar 30 2020 at 15:27):

and here we expect this to fail, and indeed it does fail.

#### Kevin Buzzard (Mar 30 2020 at 15:28):

So perhaps an interesting question is why we ended up with a finsupp zero.

#### Kevin Buzzard (Mar 30 2020 at 15:35):

because unless you are telling me to edit core Lean and change this md value, it seems that this is somehow the root of the problem.

#### Kevin Buzzard (Mar 30 2020 at 15:35):

import data.mv_polynomial

open mv_polynomial finsupp

variables (R : Type) [comm_ring R] (S : Type) (p : mv_polynomial S R)

set_option pp.all true
example (u : S →₀ ℕ) : monomial u (0 : R) = 0 :=
begin
rw monomial,
rw single_zero,
-- ⊢ 0 = 0
-- Lean does not close the goal
refl -- works
end


#### Gabriel Ebner (Mar 30 2020 at 15:36):

You can set the reducibility as an argument to the rw tactic:

rw zero_add at ⊢ {md := tactic.transparency.semireducible},


But you should probably avoid unfolding mv_polynomial in the first place.

#### Kevin Buzzard (Mar 30 2020 at 15:37):

Right. Shing wants to prove results about monomials which are defined as finsupp.singles.

#### Kevin Buzzard (Mar 30 2020 at 15:39):

In the proof above I'm showing $0X^u=0$ by unfolding the definition of monomial and reducing the question to showing that finsupp.single u 0 = 0, but the equality is still an equality of mv_polynomials.

#### Gabriel Ebner (Mar 30 2020 at 15:39):

I think you're supposed to write coeff 0 (monomial u) instead of monomial u 0.

#### Kevin Buzzard (Mar 30 2020 at 15:39):

I think that's something else

#### Gabriel Ebner (Mar 30 2020 at 15:40):

def coeff (m : σ →₀ ℕ) (p : mv_polynomial σ α) : α := p m


It seems like what we want?

#### Kevin Buzzard (Mar 30 2020 at 15:40):

monomial u r is $rX^u$

#### Kevin Buzzard (Mar 30 2020 at 15:41):

monomial u has type R -> mv_polynomial S R

Oh yes.

#### Kevin Buzzard (Mar 30 2020 at 15:41):

Lean went with the second one, where $rX^u$ is a monomial. The other definition only allows $X^u$

#### Kevin Buzzard (Mar 30 2020 at 15:42):

I have been thinking a lot about monomials over the past few days and I realised that Johannes made a really good decision to go with the second one.

#### Kevin Buzzard (Mar 30 2020 at 15:43):

The monomials span mv_polynomial R S as an additive abelian group, which is really helpful for induction principles because multiplication of mv_polynomials is a complete horrorshow, you don't want to prove anything about it directly.

#### Gabriel Ebner (Mar 30 2020 at 15:43):

Really? It seems like the second version needs lots of extra duplicate lemmas, which we don't even have (such as the example you've posted).

#### Kevin Buzzard (Mar 30 2020 at 15:44):

The crazy thing is that the monomials of the first kind, $X^u$, simply don't seem to play a role.

#### Kevin Buzzard (Mar 30 2020 at 15:44):

Sure you could prove that C r * monomial_of_first_kind u = monomial u r

#### Kevin Buzzard (Mar 30 2020 at 15:45):

but you may as well prove C r * monomial u s = monomial u (r * s)

#### Kevin Buzzard (Mar 30 2020 at 15:47):

But going back to the original question, it seems that because mv_polynomial is not marked as reducible (are there any plans to mark it reducible? @Johan Commelin ?) one should reprove a few finsupp lemmas about single such as single_zero in the mv_polynomial namespace and call them things likemonomial_zero. @Chris Hughes does this sound sane?

#### Kevin Buzzard (Mar 30 2020 at 15:48):

@Shing Tak Lam if you are planning an mv_polynomial PR then you might want to drop these in, unless someone pops up saying I've misunderstood what's going on.

#### Kevin Buzzard (Mar 30 2020 at 15:49):

@Gabriel Ebner is there any way I can look through a 200 line file with pp.all on and find all occurrences of finsupp in the pp.all output?

#### Gabriel Ebner (Mar 30 2020 at 15:49):

Run lean my_file.lean | grep finsupp on the command-line?

#### Chris Hughes (Mar 30 2020 at 15:49):

Kevin Buzzard said:

The monomials span mv_polynomial R S as an additive abelian group, which is really helpful for induction principles because multiplication of mv_polynomials is a complete horrorshow, you don't want to prove anything about it directly.

I don't think this is true unless $R = \mathbb{Z}$. They are a basis as an $R$ module though.

#### Kevin Buzzard (Mar 30 2020 at 15:50):

Chris, my point is exactly that this is true as an add_comm_group

#### Kevin Buzzard (Mar 30 2020 at 15:50):

because a monomial in Lean is defined to be $rX^u$ not $X^u$

#### Kevin Buzzard (Mar 30 2020 at 15:51):

This was really important for Shing when proving that partial derivatives satisfied the Leibniz rule.

#### Reid Barton (Mar 30 2020 at 15:51):

Isn't it just a question of whether you want to deal with Z-linear combinations or R-linear combinations?

#### Reid Barton (Mar 30 2020 at 15:51):

Neither really involves the multiplication in mv_polynomial

#### Chris Hughes (Mar 30 2020 at 15:51):

With the other one, they span as an $R$ module though, which seems to be okay as well.

#### Kevin Buzzard (Mar 30 2020 at 15:51):

The R-linear structure is defined by C r * ...

#### Kevin Buzzard (Mar 30 2020 at 15:52):

and this is mv_polynomial multiplication which is hugely inconvenient to deal with.

#### Chris Hughes (Mar 30 2020 at 15:52):

I think there are a bunch of induction principles on polynomials, and you probably want all of them.

#### Kevin Buzzard (Mar 30 2020 at 15:52):

For mv_polynomial we only found one!

#### Kevin Buzzard (Mar 30 2020 at 15:52):

@[recursor 5]
lemma induction_on {M : mv_polynomial σ α → Prop} (p : mv_polynomial σ α)
(h_C : ∀a, M (C a)) (h_add : ∀p q, M p → M q → M (p + q)) (h_X : ∀p n, M p → M (p * X n)) :
M p :=


is the one in mathlib

#### Kevin Buzzard (Mar 30 2020 at 15:53):

You can't use this to prove Leibniz very easily because one of the inputs is how things behave under multiplication by a variable

#### Kevin Buzzard (Mar 30 2020 at 15:54):

So I told Shing to use this:

theorem mv_polynomial.induction_on' {R : Type*} [comm_semiring R] {S : Type*}
{M : mv_polynomial S R → Prop} (p : mv_polynomial S R) :
(∀ (u : S →₀ ℕ), M (monomial u 1)) →
(∀ (p q : mv_polynomial S R), M p → M q → M (p + q)) →
(∀ (p : mv_polynomial S R) (r : R), M p → M (C r * p)) → M p :=


but even this wasn't good enough because we are still multiplying by C r and even proving Leibniz for the case of C r is awful because mv_polynomial multiplication is hellish.

#### Kevin Buzzard (Mar 30 2020 at 15:55):

Here's the definition:

def pderivative (var : S) (p : mv_polynomial S R) : mv_polynomial S R :=
p.sum (λ A B, monomial (erase var A + single var (A var - 1)) (B * (A var)))


Proving it's R-linear directly turned out to be much harder than I thought

#### Kevin Buzzard (Mar 30 2020 at 15:55):

The insight was to use this induction principle:

theorem mv_polynomial.induction_on'' {R : Type*} [comm_semiring R] {S : Type*}
{M : mv_polynomial S R → Prop} (p : mv_polynomial S R) :
(∀ (u : S →₀ ℕ) (r : R), M (monomial u r)) →
(∀ (p q : mv_polynomial S R), M p → M q → M (p + q)) → M p


#### Chris Hughes (Mar 30 2020 at 15:55):

There is an induction principle on polynomial based on the derivative. If you prove $P(f') \implies P(f)$ and $P(0)$, then you've proved it for all polynomials.

#### Kevin Buzzard (Mar 30 2020 at 15:56):

We don't have that for mv_polynomial yet because there is no derivative of any kind (until the PR hits some time tomorrow)

#### Chris Hughes (Mar 30 2020 at 15:57):

It's not there on polynomials yet, but I conjecture it might be useful to prove things about limits of polynomials.

#### Kevin Buzzard (Mar 30 2020 at 15:57):

pderivative is easily checked to be additive. The third induction principle then reduces Leibniz to checking it for monomials $rX^u$ and $sX^v$

#### Kevin Buzzard (Mar 30 2020 at 15:57):

and you can check this by hand, apart from the fact that rw add_zero sometimes randomly doesn't work ;-)

#### Kevin Buzzard (Mar 30 2020 at 15:58):

This gives you Leibniz and you can then deduce that pderivative is R-linear from it!

#### Kevin Buzzard (Mar 30 2020 at 16:17):

Oh look -- unification of finsupp and mv_polynomial sometimes works:

[type_context.is_def_eq_detail] [1]: (S →₀ ℕ) →₀ R =?= mv_polynomial S R
[type_context.is_def_eq_detail] unfold right: mv_polynomial
[type_context.is_def_eq_detail] [2]: (S →₀ ℕ) →₀ R =?= add_monoid_algebra R (S →₀ ℕ)
[type_context.is_def_eq] (S →₀ ℕ) →₀ R =?= mv_polynomial S R ... success  (approximate mode)


#### Kevin Buzzard (Mar 30 2020 at 16:18):

But also in the very same trace output

[type_context.is_def_eq_detail] [3]: (S →₀ ℕ) →₀ R =?= mv_polynomial S R
[type_context.is_def_eq_detail] [4]: finsupp =?= mv_polynomial
[type_context.is_def_eq_detail] on failure: finsupp =?= mv_polynomial


#### Kevin Buzzard (Mar 30 2020 at 16:19):

How come Lean sometimes goes for unfold right?

Last updated: May 12 2021 at 07:17 UTC