Zulip Chat Archive

Stream: maths

Topic: strange rw behaviour with mv_polynomial


view this post on Zulip 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
  -- 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

view this post on Zulip 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 ...

view this post on Zulip Gabriel Ebner (Mar 30 2020 at 15:08):

Is it the same addition?

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 15:09):

No

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Gabriel Ebner (Mar 30 2020 at 15:14):

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

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 15:14):

Thanks!

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 15:16):

Oh no wait, I am out of date

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 15:17):

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

view this post on Zulip 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.

view this post on Zulip Gabriel Ebner (Mar 30 2020 at 15:18):

ctrl+p #tactic.rewrite_cfg

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 15:21):

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

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 15:21):

I have no idea what md means

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 15:22):

-- TODO(Leo): improve documentation

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 15:22):

Oh I see you just told me what it meant

view this post on Zulip Gabriel Ebner (Mar 30 2020 at 15:22):

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

view this post on Zulip Gabriel Ebner (Mar 30 2020 at 15:22):

reducible means it will only unfold definitions marked as reducible.

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 15:23):

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

view this post on Zulip Gabriel Ebner (Mar 30 2020 at 15:23):

:+1:

view this post on Zulip Patrick Massot (Mar 30 2020 at 15:24):

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

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 15:24):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 15:27):

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

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 15:28):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 15:37):

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

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 15:39):

In the proof above I'm showing 0Xu=00X^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.

view this post on Zulip Gabriel Ebner (Mar 30 2020 at 15:39):

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

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 15:39):

I think that's something else

view this post on Zulip Gabriel Ebner (Mar 30 2020 at 15:40):

def coeff (m : σ  ) (p : mv_polynomial σ α) : α := p m

It seems like what we want?

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 15:40):

monomial u r is rXurX^u

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 15:41):

monomial u has type R -> mv_polynomial S R

view this post on Zulip Gabriel Ebner (Mar 30 2020 at 15:41):

Oh yes.

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 15:41):

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

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 15:41):

Lean went with the second one, where rXurX^u is a monomial. The other definition only allows XuX^u

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 15:44):

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

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 15:44):

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

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 15:45):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Gabriel Ebner (Mar 30 2020 at 15:49):

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

view this post on Zulip 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=ZR = \mathbb{Z}. They are a basis as an RR module though.

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 15:50):

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

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 15:50):

because a monomial in Lean is defined to be rXurX^u not XuX^u

view this post on Zulip Chris Hughes (Mar 30 2020 at 15:50):

Sorry, I misread

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 15:51):

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

view this post on Zulip 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?

view this post on Zulip Reid Barton (Mar 30 2020 at 15:51):

Neither really involves the multiplication in mv_polynomial

view this post on Zulip Chris Hughes (Mar 30 2020 at 15:51):

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

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 15:51):

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

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 15:52):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 15:52):

For mv_polynomial we only found one!

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Chris Hughes (Mar 30 2020 at 15:55):

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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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 rXurX^u and sXvsX^v

view this post on Zulip 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 ;-)

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 15:58):

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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