Cubics

Stream: general

[Yaël Dillies]

@David Kurniadi Angdinata, why did you not define docs#cubic as polynomial.degree_le R 3 (docs#polynomial.degree_le)?

[Riccardo Brasca]

I remember a PR about something similar, let me search.

[Riccardo Brasca]

It's #6428, but the only explanation is "Working directly with specific polynomials (like X^n - X - 1) is really painful, since whenever you try to do something simple like checking that the polynomial is monic or computing its degree, you have to prove a bunch of trivial inequalities. Bundling solves this problem".

[Kevin Buzzard]

right -- proving that the degree of x^2+1 is 2 is surprisingly annoying right now (as one of my UG students found out a few weeks ago)

[Kevin Buzzard]

(and it's not even true if R is the zero ring ;-) )

[Damiano Testa]

I find that working with nat_degree_le is way better.

[Yaël Dillies]

What Riccardo is describing sounds like a case for a strong dedicated API, but not really a case for a dedicated structure.

[Thomas Browning]

Damiano Testa said:

I find that working with nat_degree_le is way better.

Certainly, but proving the other inequality is still painful.

[Thomas Browning]

Yaël Dillies said:

What Riccardo is describing sounds like a case for a strong dedicated API, but not really a case for a dedicated structure.

I also came to this conclusion for the trinomials project. I hope to return to it at some point, and see if I can avoid bundled trinomials.

[David Ang]

@Yaël Dillies I just thought it was easier to work with four coefficients than with a submodule of R[X], and I was really just following the quadratic_discriminant file that’s already present (PS: can an admin kick my other account? I don’t have access to that one anymore and want to receive the right pings)

[David Ang]

When I wrote this I really only needed cubics that aren’t quadratic/linear/constant (so the four coefficients are kinda natural to start from), but I was told to include the degenerate cases as well, so now R[X] <= 3 seems more natural

[Damiano Testa]

Just a follow-up on the difficulty of computing explicit nat_degrees, I gave it a shot! Below is my attempt: it has not been easy! But I was indeed able to prove that the degree of X^2 + 1 is 2 in any non-trivial semiring! :upside_down:

Computing degrees

import data.polynomial.degree.definitions

open polynomial
open_locale polynomial classical

variables {R : Type*} [semiring R]

lemma C_X_pow_add_C_X_pow1 {r s : R} {m n : ℕ} (mn : m < n) :
  C r * (1 * X) ^ n + C s * (1 * X) ^ m = C s * (1 * X) ^ m + C r * (1 * X) ^ n :=
add_comm _ _

lemma nat_degree_monomial_le (n : ℕ) (r : R) : (monomial n r).nat_degree ≤ n :=
by { rw nat_degree_monomial, split_ifs, simp }

lemma nat_degree_add_add {m n : ℕ} (r s : R) (s0 : s ≠ 0) (f : R[X]) (hf : f.nat_degree ≤ m)
  (mn : m < n) :
  (f + monomial m r + monomial n s).nat_degree = n :=
begin
  rwa [nat_degree_add_eq_right_of_nat_degree_lt, nat_degree_monomial, if_neg s0],
  refine (nat_degree_add_le _ _).trans_lt _,
  apply max_lt,
  refine hf.trans_lt (mn.trans_le (le_of_eq _)),
  rw [nat_degree_monomial, if_neg s0],
  refine (nat_degree_monomial_le _ _).trans_lt (mn.trans_le (le_of_eq _)),
  rw [nat_degree_monomial, if_neg s0],
end

lemma nat_degree_add_once {m n : ℕ} (r s : R) (s0 : s ≠ 0)
  (mn : m < n) :
  (monomial m r + monomial n s).nat_degree = n :=
begin
  rwa [nat_degree_add_eq_right_of_nat_degree_lt, nat_degree_monomial, if_neg s0],
  rw [nat_degree_monomial, nat_degree_monomial, if_neg s0],
  split_ifs,
  exact (nat.zero_le _).trans_lt mn,
  assumption,
end

variable [nontrivial R]
--  my test polynomial: C u * X + X ^ 5 + C s + C t * X ^ 2 + X ^ 8
-- {r s t u : R} (r0 : t ≠ 0)
--  Kevin's example
lemma nat_degree_le :
  (X ^ 2 + 1 : R[X]).nat_degree ≤ 2 :=
begin
  -- First, make sure that all summands are `monomial`s
  try { rw X },
  try { rw ← C_1 },
  repeat { rw ← monomial_zero_left },
  repeat { rw monomial_pow },
  repeat { rw monomial_mul_monomial },
  -- and clean up various add_zeros, mul_ones,...
  try { simp [-monomial_zero_left] },
  -- We peel off each summand and produce goals where we need to show that each summand has
  -- degree bounded by our target
  repeat { refine (nat_degree_add_le _ _).trans (max_le _ _) },
  -- since our summands are monomials, we know that their degrees are at most their exponents
  any_goals { apply (nat_degree_monomial_le _ (_ : R)).trans _ },
  -- therefore, `norm_num` should be able to prove the inequalities.
  all_goals { norm_num },
end

-- {r s t u : R} (r0 : t ≠ 0) (z0 : (1 : R) ≠ 0)
lemma le_nat_degree :
  2 ≤ (X ^ 2 + 1 : R[X]).nat_degree :=
begin
  -- First, make sure that all summands are `monomial`s
  try { rw X },
  try { rw ← C_1 },
  repeat { rw ← monomial_zero_left },
  repeat { rw monomial_pow },
  repeat { rw monomial_mul_monomial },
  -- and clean up various add_zeros, mul_ones,...
  try { simp [-monomial_zero_left] },
  -- Now that all summands are monomials, we convert them to the form `C r * X ^ n`,
  -- with possibly `r = 1` and `n = 0` or `n = 1`, for uniformity.
  repeat { rw [monomial_eq_C_mul_X] },
  -- we also rearrange parentheses, just in case
  repeat { rw ← add_assoc },

  -- mark each summand with a `1 * X`: later on, we will remove these markers, to go deeper into
  -- the various summands.  The presence of a `1 *` in a term is our cue that we have not yet
  -- rearranged it.
  rw ← one_mul (X : R[X]),

  --  This block sorts the summands in ascending degree of exponent.
  --  The number of iterations should be adapted to each case -- this choice works for small cases.
  --  We visit each pair of consecutive summands and decide whether we swap them or not.
  --  The number of times that we visit all the summands is determined by the first `iterate`.
  --  The visits to the summands happens in the second `iterate`.
  iterate 2
  -- The inner loop visits each consecutive pairs of summands and swaps them, if the swap makes the
  -- sequence of exponents decrease.
  { iterate 3
    { -- We focus on the first pair.  `C_X_pow_add_C_X_pow1` will swap the two summands
      -- creating a proof obligation of showing that the new order is strictly monotone increasing.
      -- `norm_num` will try to solve side goal and if it does not succeed, then `refl` fails and
      -- the swap does not occur.
      -- If `norm_num` succeeds, we have straightened a little, otherwise, the two first terms are
      -- in correct order.
      --  In either case, after the `try`, we have not increased the number of inversions among the
      --  exponents of our summands and it could have decreased.
      try { work_on_goal 1 { rw C_X_pow_add_C_X_pow1, rotate, norm_num; refl } },
      -- so we shift parentheses around isolating the not-yet-visited terms (highlighted by the `1`)
      repeat { rw add_assoc (C _ * (1 * X) ^ _) },
      -- we mark as straightened the term that was just (possibly) rearranged
      try { nth_rewrite 0 one_mul X },
      -- and we prepare to start again with the next pair
      repeat { rw ← add_assoc (C _ * (1 * X) ^ _) } },
      -- We are now outside of the first `iterate`.
      -- we clear and replace the markers
      try { rw [one_mul] }, try { rw [← one_mul (X : R[X])] },
      -- we rearrange parentheses
      repeat { rw ← add_assoc } },

  -- Unless we made mistakes (or we looped too little), our expression has exponents sorted in
  -- strictly increasing order.
  -- We clear the leftover markers
  try { rw [one_mul X] },
  -- We re-express everything in terms of `monomial`s
  repeat { rw [← monomial_eq_C_mul_X] },
  -- Now we strip off each summand from the right-most one back
  -- remember that the further right we go, the higher the exponent.
  -- Lemma `nat_degree_add_add` creates proof obligations of checking that the ordering is
  -- correct and that the various coefficients are non-zero
  -- (really, we only need the highest coefficient to be non-zero, the remaining ones might well
  -- be zero, but I decided that this was enough!)
  repeat { rw nat_degree_add_add },
  try { rw nat_degree_add_once },
  -- Finally, we try to prove these proof obligations using `norm_num` or `assumptions that might
  -- be floating around.
  any_goals { norm_num },
  all_goals { assumption },
end

[Kevin Buzzard]

Thanks Damiano -- I think you've made my point quite well :-/

[Damiano Testa]

Btw, the challenge is now to find a polynomial written as a sum of terms with distinct exponents and non-zero coefficients, for which the above code does not compute the degree!

[Eric Rodriguez]

I don't see the issue:

import data.polynomial.degree.definitions

open polynomial

example {R} [semiring R] [nontrivial R] : (X ^ 2 + 1 : polynomial R).nat_degree = 2 :=
begin
  rw [nat_degree_add_eq_left_of_nat_degree_lt, nat_degree_X_pow],
  simp,
end

[Damiano Testa]

Sure, I was just giving a general procedure to compute natdegrees of explicit polynomials

[Eric Rodriguez]

Oh, does this work for any polynomial? That's exciting!

[Damiano Testa]

Well, it works on 2...

[Patrick Massot]

It would be nice to make it a norm_num extension

[Damiano Testa]

Patrick, I'm happy to try, but I'm not even entirely sure what is a norm_num extension.

Moreover, I think that all the code above could be much simpler if I only knew some metaprogramming. I would need a lot of help with that.

[Eric Rodriguez]

norm_num essentially works in an "extendable" way, I'm not really sure how. but it means that if you have some definition that you want to evaluate, you don't have to edit the core tactic, you can just do it in a separate file

[Eric Rodriguez]

cc @Mario Carneiro, he made most of this I think

[Damiano Testa]

Thanks Eric, I'll look a little at the various norm_num files and will ask questions.

[Damiano Testa]

By the way, most of the structure above is about sorting a sum of monomials by degree, which is independent of computing degrees. I can see if abel or ring works there.