strange rw behaviour with mv_polynomial

Stream: maths

[Kevin Buzzard]

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

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]

Is it the same addition?

[Kevin Buzzard]

No

[Kevin Buzzard]

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

[Gabriel Ebner]

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]

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

[Kevin Buzzard]

Thanks!

[Kevin Buzzard]

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]

Oh no wait, I am out of date

[Gabriel Ebner]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

ctrl+p #tactic.rewrite_cfg

[Gabriel Ebner]

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]

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

[Kevin Buzzard]

I have no idea what md means

[Kevin Buzzard]

-- TODO(Leo): improve documentation

[Kevin Buzzard]

Oh I see you just told me what it meant

[Gabriel Ebner]

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

[Gabriel Ebner]

reducible means it will only unfold definitions marked as reducible.

[Kevin Buzzard]

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

[Gabriel Ebner]

:+1:

[Patrick Massot]

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

[Kevin Buzzard]

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

[Gabriel Ebner]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

I think that's something else

[Gabriel Ebner]

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

It seems like what we want?

[Kevin Buzzard]

monomial u r is $rX^u$

[Kevin Buzzard]

monomial u has type R -> mv_polynomial S R

[Gabriel Ebner]

Oh yes.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

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

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

[Chris Hughes]

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]

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

[Kevin Buzzard]

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

[Chris Hughes]

Sorry, I misread

[Kevin Buzzard]

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

[Reid Barton]

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

[Reid Barton]

Neither really involves the multiplication in mv_polynomial

[Chris Hughes]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Chris Hughes]

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

[Kevin Buzzard]

For mv_polynomial we only found one!

[Kevin Buzzard]

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

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]

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]

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]

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]

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]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

How come Lean sometimes goes for unfold right?