Calculate the totaldegree of ((X + Y) ^ 2 + 3 * X + Y) / 2

Stream: new members

[Xitai Jiang]

Here I have that X : MvPolynomial (Fin 2) ℝ := MvPolynomial.X 0 and Y : MvPolynomial (Fin 2) ℝ := MvPolynomial.X 1,set f:= (MvPolynomial.C (1 / 2)) * ((X + Y) ^ 2 + (MvPolynomial.C 3) * X + Y), How to prove that Mvpolynomial.totalDegree f = 2？ Much thanks!

[Kevin Buzzard]

Can you write your question as a #mwe so that others don't have to work so hard to answer?

[Xitai Jiang]

import Mathlib
example (X Y f : MvPolynomial (Fin 2) ℝ)
(hX : X = MvPolynomial.X 0)
(hY : Y = MvPolynomial.X 1)
(hf : f = (MvPolynomial.C (1 / 2)) * ((X + Y) ^ 2 + (MvPolynomial.C 3) * X + Y))
: MvPolynomial.totalDegree f = 2 := by sorry

this may be an example of my question, thank you very much.

[Philippe Duchon]

Your example is missing the imports; most likely, import Mathlib. This is required in a "minimum working example", so one can just click to open it in the Lean playground.

[Xitai Jiang]

I'm sorry, and I have fixed it in the previous codes

[Kevin Buzzard]

yeah, looks like compute_degree only works for single variable polynomials :-(

import Mathlib

example (X Y f : MvPolynomial (Fin 2) ℝ)
    (hX : X = MvPolynomial.X 0)
    (hY : Y = MvPolynomial.X 1)
    (hf : f = (MvPolynomial.C (1 / 2)) * ((X + Y) ^ 2 + (MvPolynomial.C 3) * X + Y)) :
    MvPolynomial.totalDegree f = 2 := by
  rw [hf, hX, hY]
  compute_degree -- doesn't work :-(

[Kevin Buzzard]

Probably right now the thing to do is to do it manually

import Mathlib

example (X Y f : MvPolynomial (Fin 2) ℝ)
    (hX : X = MvPolynomial.X 0)
    (hY : Y = MvPolynomial.X 1)
    (hf : f = (MvPolynomial.C (1 / 2)) * ((X + Y) ^ 2 + (MvPolynomial.C 3) * X + Y)) :
    MvPolynomial.totalDegree f = 2 := by
  rw [hf, hX, hY]
  apply le_antisymm
  · refine le_trans (MvPolynomial.totalDegree_mul _ _) ?_
    simp
    refine le_trans (MvPolynomial.totalDegree_add _ _) ?_
    simp
    refine le_trans (MvPolynomial.totalDegree_add _ _) ?_
    simp
    constructor
    · -- etc etc
      sorry
    · sorry
  · sorry

and then optionally learn how to write tactics and then write the tactic which does these manual steps for you.

[Luigi Massacci]

It seems to me @Xitai Jiang the main pain point is that all theorems about docs@MvPolynomial.totalDegree are over arbitrary docs#CommSemiring, so proving equality of anything is a nightmare the moment you have a multiplication. I would first prove a couple of theorems like this:

import Mathlib

lemma MvPolynomial.totalDegree_mul_const_ne_zero {R σ : Type*} [CommSemiring R] [IsDomain R]
 (a : R) (P : MvPolynomial σ R) (ha : a ≠ 0):
 ((C a) * P).totalDegree = P.totalDegree := by
  rw [totalDegree_eq, totalDegree_eq, C_mul', MvPolynomial.support_smul_eq ha]

and then it should be quite quick, if labour intensive

[Kevin Buzzard]

Yeah this is why I applied le_antisymm first, all of the API is proving inequalities for this kind of reason.

[Kevin Buzzard]

I'm about to get on the tube to go to work, I'll see if I can do it during the commute!

[Luigi Massacci]

right, but then how do you get past the second part? When you need to prove that the degrees are greater than the constants you get (so 0, 1, 2)

[Kevin Buzzard]

yeah I hadn't got to that bit yet :-/ Let's see if the Picadilly line inspires me!

[Luigi Massacci]

I guess you can do it by contradiction maybe, and then essentially re-repeat the top part in a very lengthy proof : ( nvm I don’t think this will help you, the lemmas in the library will still be in the “wrong” direction

[Damiano Testa]

I can look into making compute_degree work with totalDegree: I suspect that the same strategy used for degree can be used without too much extra machinery, just more lemmas.

[Damiano Testa]

As Kevin said, compute_degree works exclusively with Polynomial, so at the moment it will immediately stop processing any "degree" computation involving MvPolynomial.

[Luigi Massacci]

I got to here:

import Mathlib
import Mathlib.Data.Finset.Lattice.Basic
open MvPolynomial Finset Lattice

set_option autoImplicit false

variable {R σ : Type*} [CommSemiring R] [IsDomain R]

lemma MvPolynomial.totalDegree_mul_const_ne_zero (a : R) (P : MvPolynomial σ R) (ha : a ≠ 0):
 ((C a) * P).totalDegree = P.totalDegree := by
  rw [totalDegree_eq, totalDegree_eq, C_mul', MvPolynomial.support_smul_eq ha]

lemma MvPolynomial.totalDegree_mul_left_ne_zero (a b : MvPolynomial σ R) (ha : a ≠ 0) :
  (a * b).totalDegree = a.totalDegree + b.totalDegree := by
  sorry


lemma MvPolynomial.totalDegree_mul_right_ne_zero (a b : MvPolynomial σ R) (ha : a ≠ 0) :
  (b * a).totalDegree = a.totalDegree + b.totalDegree := by
  rw [mul_comm, totalDegree_mul_left_ne_zero]; assumption

lemma MvPolynomial.totalDegree_pow_of_ne_zero (a : MvPolynomial σ R) (ha : a ≠ 0) (n : ℕ):
  (a ^ n).totalDegree = n * a.totalDegree := by
  induction' n with n ih
  · simp only [pow_zero, totalDegree_one, zero_mul]
  · rw [pow_succ, totalDegree_mul_right_ne_zero _ _ ha, ih]
    ring


example (X Y f : MvPolynomial (Fin 2) ℝ)
(hX : X = MvPolynomial.X 0)
(hY : Y = MvPolynomial.X 1)
(hf : f = (MvPolynomial.C (1 / 2)) * ((X + Y) ^ 2 + (MvPolynomial.C 3) * X + Y))
: MvPolynomial.totalDegree f = 2 := by
  have hXY : X + Y ≠ 0 := by
    simp [hX, hY]
    intro h
    rw [MvPolynomial.eq_zero_iff] at h
    sorry
  have hXY_deg : (X+Y).totalDegree = 1 := by
    apply le_antisymm
    · rw [show 1 = max X.totalDegree Y.totalDegree by simp [hX, hY]]
      apply MvPolynomial.totalDegree_add X Y
    · have : (X+Y).totalDegree ≠ 0 := by
        intro h
        rw [MvPolynomial.totalDegree_eq_zero_iff_eq_C] at h
        simp [hX, hY] at h
        simp [hX, hY] at hXY
        contradiction
      exact Nat.one_le_iff_ne_zero.2 this
  rw [hf]
  rw [totalDegree_mul_const_ne_zero (1/2 : ℝ) _ (by norm_num)]
  · rw [totalDegree_add_eq_left_of_totalDegree_lt]
    · rw [totalDegree_add_eq_left_of_totalDegree_lt]
      · rw [totalDegree_pow_of_ne_zero _ hXY, hXY_deg]
      · rw [totalDegree_mul_const_ne_zero (3 : ℝ) _ (by norm_num)]
        rw [totalDegree_pow_of_ne_zero _ hXY, hXY_deg]
        simp only [hX, Fin.isValue, totalDegree_X, mul_one, Nat.one_lt_ofNat]
    · calc
      _ < ((X+Y)^2).totalDegree := by
        rw [totalDegree_pow_of_ne_zero _ hXY, hXY_deg]
        simp only [hY, Fin.isValue, totalDegree_X, mul_one, Nat.one_lt_ofNat]
      _ = _ := by
        rw [totalDegree_add_eq_left_of_totalDegree_lt]
        rw [totalDegree_mul_const_ne_zero (3 : ℝ) _ (by norm_num)]
        rw [totalDegree_pow_of_ne_zero _ hXY, hXY_deg]
        simp only [hX, Fin.isValue, totalDegree_X, mul_one, Nat.one_lt_ofNat]

[Luigi Massacci]

But I have to stop now, if anyone wants to fill those last two sorries (the second one is dumb)

[Luigi Massacci]

Note that for docs#Polynomial.degree there is a whole file with the equalities in the case of domains, so I assume it should be worthwile to add the same lemmas for docs#MvPolynomial

[Damiano Testa]

This is how I think that the non-existing tactic would work here:

import Mathlib

open MvPolynomial

example (X Y f : MvPolynomial (Fin 2) ℝ)
    (hX : X = MvPolynomial.X 0)
    (hY : Y = MvPolynomial.X 1)
    (hf : f = (MvPolynomial.C (1 / 2)) * ((X + Y) ^ 2 + (MvPolynomial.C 3) * X + Y)) :
    MvPolynomial.totalDegree f = 2 := by
  subst f hX hY
  apply le_antisymm
  · apply (totalDegree_mul ..).trans
    rw [add_assoc]
    simp
    apply (totalDegree_add ..).trans
    simp
    constructor
    apply (totalDegree_pow ..).trans
    simp
    apply (totalDegree_add ..).trans
    simp
    apply (totalDegree_add ..).trans
    simp
    apply (totalDegree_mul ..).trans
    simp
  -- insert proof that the relevant coefficient is non-zero
  sorry

[Damiano Testa]

This follows the exact same strategy that compute_degree follows for Polynomial. The simp-interlacing would be avoided by writing appropriate lemmas that already return the "correct" goal.

[Damiano Testa]

The final non-zero proof would be passed to norm_num + assumption and, if that does not close the goal, returned to the user.

[Kevin Buzzard]

I got to here but I'm at work now so need to get back to serious stuff.

import Mathlib

namespace MvPolynomial

lemma totalDegree_mul_const_ne_zero {R σ : Type*} [CommSemiring R] [IsDomain R]
 {a : R} (P : MvPolynomial σ R) (ha : a ≠ 0):
 ((C a) * P).totalDegree = P.totalDegree := by
  rw [totalDegree_eq, totalDegree_eq, C_mul', MvPolynomial.support_smul_eq ha]

-- missing API, and name `totalDegree_pow` is already taken
-- probably fiddly to prove, not entirely sure I have a plan
theorem totalDegree_pow' {R σ : Type*} [CommSemiring R] [IsDomain R]
    (a : MvPolynomial σ R) (n : ℕ) :
    (a ^ n).totalDegree = n * a.totalDegree := by sorry

-- should be much easier
theorem totalDegree_eq_max_of_disjoint_support {R σ : Type*} [CommSemiring R]
    (f g : MvPolynomial σ R) (h : Disjoint f.support g.support) :
    (f + g).totalDegree = max f.totalDegree g.totalDegree := sorry

example (X Y f : MvPolynomial (Fin 2) ℝ)
    (hX : X = MvPolynomial.X 0)
    (hY : Y = MvPolynomial.X 1)
    (hf : f = (MvPolynomial.C (1 / 2)) * ((X + Y) ^ 2 + (MvPolynomial.C 3) * X + Y)) :
    MvPolynomial.totalDegree f = 2 := by
  rw [hf, mul_add, mul_add, add_assoc, add_comm]
  have foo : (C (1 / 2) * (X + Y) ^ 2).totalDegree = 2 := by
    rw [totalDegree_mul_const_ne_zero]
    · rw [totalDegree_pow']
      simp [hX, hY]
      rw [totalDegree_eq_max_of_disjoint_support]
      · simp
      · sorry
    · norm_num
  rwa [totalDegree_add_eq_right_of_totalDegree_lt]
  rw [foo, Nat.lt_succ, ← mul_add]
  refine le_trans (MvPolynomial.totalDegree_mul _ _) ?_
  simp
  refine le_trans (MvPolynomial.totalDegree_add _ _) ?_
  simp [hX, hY]
  refine le_trans (MvPolynomial.totalDegree_mul _ _) ?_
  simp

Comparing with Luigi's work: they got much further (but I've also walked through Hyde Park): they've reduced my totalDegree_pow' (which looks like it's missing a nonzero hypothesis) to totalDegree_mul_left_ne_zero which should be in the API for totalDegree, but I think I like my approach for (X+Y).totalDegree = 1 better.

[Luigi Massacci]

Damiano Testa said:

This is how I think that the non-existing tactic would work here:

import Mathlib

open MvPolynomial

example (X Y f : MvPolynomial (Fin 2) ℝ)
    (hX : X = MvPolynomial.X 0)
    (hY : Y = MvPolynomial.X 1)
    (hf : f = (MvPolynomial.C (1 / 2)) * ((X + Y) ^ 2 + (MvPolynomial.C 3) * X + Y)) :
    MvPolynomial.totalDegree f = 2 := by
  subst f hX hY
  apply le_antisymm
  · apply (totalDegree_mul ..).trans
    rw [add_assoc]
    simp
    apply (totalDegree_add ..).trans
    simp
    constructor
    apply (totalDegree_pow ..).trans
    simp
    apply (totalDegree_add ..).trans
    simp
    apply (totalDegree_add ..).trans
    simp
    apply (totalDegree_mul ..).trans
    simp
  -- insert proof that the relevant coefficient is non-zero
  sorry

Ah that is clever, but the relevant lemma for the coefficients appears to be missing for MvPolynomial

[Kevin Buzzard]

Aah yes, that does the other direction. I can tell you thought about this sort of thing before :-)

[Xitai Jiang]

I have read all answers and they impressed me a lot. For me, I have proved that the totalDegree is no more that 2 and it remained to show the no less than side. By using MvPolynomial.degreeOf_le_totalDegree tactic, it suffices to show that
MvPolynomial.degreeOf 0 f = 2 (or equivalently, to show that MvPolynomial.degrees f = {0, 0, 1, 1}), which is hard for me.

example (X Y f : MvPolynomial (Fin 2) ℝ)
    (hX : X = MvPolynomial.X 0)
    (hY : Y = MvPolynomial.X 1)
    (hf : f = (MvPolynomial.C (1 / 2)) * ((X + Y) ^ 2 + (MvPolynomial.C 3) * X + Y)) :
    MvPolynomial.totalDegree f = 2 := by
    -- this can be proved by expanding f as a sum of monomials and use the MvPolynomial.totalDegree_mul and MvPolynomial.totalDegree_add tactic, which is omited here for simplicity
    have hle2 : MvPolynomial.totalDegree f  \le 2:= by sorry
    -- I have tried to prove the \ge 2 inequality by MvPolynomial.degreeOf_le_totalDegree tactic, and I haven't finished it
    have hge2 : MvPolynomial.totalDegree f  \ge 2:= by sorry