# Zulip Chat Archive

## 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_polynomial`

s. 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 -- rw zero_add, -- fails 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) rw zero_add -- works 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 ...`

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

Is it the same addition?

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

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.

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

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?

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

:+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.single`

s.

#### 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_polynomial`

s.

#### 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`

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

Oh yes.

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

I was surprised about this. There are two definitions of the word monomial on Wikipedia

#### 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 like`monomial_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$

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

Sorry, I misread

#### 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_detail] unfold right: add_monoid_algebra [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