polynomial ext with degree bound

Stream: Is there code for X?

[Heather Macbeth]

Is there a way to reduce an equality of polynomials that are both "obviously" of degree at most (say) 3, to a finite number of goals: proving equality of each of the coefficients up to three?

Concretely, say I have

import data.polynomial.basic
open polynomial

example {K : Type*} [field K] {p q a b c : K} :
  X ^ 3 + C p * X - C q = (X - C a) * (X - C b) * (X - C c) :=
begin
  admit,
end

Can I reduce this to the four goals

(X ^ 3 + C p * X - C q).coeff i = ((X - C a) * (X - C b) * (X - C c)).coeff i

for i from 0 to 3? (After this simp [coeff_mul, coeff_one, coeff_C, pow_succ, finset.nat.antidiagonal_succ] is enough to make the above goals more concrete.)

[Heather Macbeth]

Is this kind of thing the motivation for @Damiano Testa's polynomial-degree automation?

[Damiano Testa]

Currently, the "compute_degree" tactics make the implicit assumption that the "visibly leading term" is unique. While this is still the case in your example, it would not be true for the smaller degree terms. This is of course easy to adapt. However, it might be easier to follow this workflow:

• show that the degree is at most n;
• prove that if the degree is at most n, then the polynomials coincide if and only if their coeffs up to n coincide;
• bash away at the left-over cases.

[Damiano Testa]

This is still somewhat far from what the tactics can do!

[Damiano Testa]

But is a good motivational example to keep in mind. I already have a guess_degree function, which does "the obvious"!

[Heather Macbeth]

Thanks Damiano!

Damiano Testa said:

• prove that if the degree is at most n, then the polynomials coincide if and only if their coeffs up to n coincide;

Is there existing code for this, do you know?

[Heather Macbeth]

Maybe written for finsupp rather than polynomial?

[Damiano Testa]

This must be there, though I'm not at my computer now.

[Damiano Testa]

Btw, the compute_degree_le tactic is already PRed: #14762.

[Ruben Van de Velde]

Couldn't find a lemma for the second bullet, but not too hard to prove:

example (K : Type*) [field K] (p q : polynomial K) :
  (∀ n ≤ max p.nat_degree q.nat_degree, p.coeff n = q.coeff n) ↔ p = q :=
begin
  rw [polynomial.ext_iff],
  refine forall_congr (λ n, ⟨λ h, _, λ h _, h⟩),
  refine (le_or_lt n (max p.nat_degree q.nat_degree)).elim h (λ h', _),
  rw [polynomial.coeff_eq_zero_of_nat_degree_lt ((le_max_left _ _).trans_lt h'),
    polynomial.coeff_eq_zero_of_nat_degree_lt ((le_max_right _ _).trans_lt h')],
end

[Ruben Van de Velde]

I suspect fin_cases or interval_cases could take it from there?

[Damiano Testa]

Probably, semiring K is enough?

[Ruben Van de Velde]

Yeah, I didn't check

[Damiano Testa]

If you go to branch#adomani_poleq then this works:

import tactic.poleq

open polynomial

example {K : Type*} [field K] {p q a b c : K} :
  X ^ 3 + C p * X - C q = (X - C a) * (X - C b) * (X - C c) :=
begin
  show_deg_le,
/-
K: Type ?
_inst_1: field K
p q a b c : K
i: ℕ
H: i ≤ 3
⊢ (X ^ 3 + ⇑C p * X - ⇑C q).coeff i = ((X - ⇑C a) * (X - ⇑C b) * (X - ⇑C c)).coeff i
-/
  admit,
end

[Damiano Testa]

As you can imagine, the example above is almost the only test I made, so there are likely lots of bugs!

If you end up experimenting with this tactic, please report all the bugs that you find!

[Yakov Pechersky]

A proof with a weaker hypothesis:

import data.polynomial.basic
open polynomial

example {K : Type*} [semiring K] (p q : polynomial K) :
  (∀ n ∈ p.support ∪ q.support, p.coeff n = q.coeff n) ↔ p = q :=
begin
  rw [polynomial.ext_iff],
  refine forall_congr (λ n, ⟨λ h, _, λ h _, h⟩),
  by_cases hp : n ∈ p.support,
  { exact h (finset.mem_union_left _ hp) },
  by_cases hq : n ∈ q.support,
  { exact h (finset.mem_union_right _ hq) },
  { rw [not_mem_support_iff] at hp hq,
    rw [hp, hq] }
end

[Yakov Pechersky]

For some concrete polynomials, p.support will be much sparser than range p.nat_degree.

[Ruben Van de Velde]

Certainly, but that statement seems harder to transform to individual goals than the degree one, no?

[Damiano Testa]

Currently, I used this adaptation of Ruben's version:

lemma nat_degree_le_max {R : Type*} [semiring R] (n : ℕ) {p q : polynomial R}
  (pn : p.nat_degree ≤ n) (qn : q.nat_degree ≤ n) :
  (∀ i ≤ n, p.coeff i = q.coeff i) ↔ p = q :=
begin
  refine iff.trans _ ext_iff.symm,
  refine forall_congr (λ i, ⟨λ h, _, λ h _, h⟩),
  refine (le_or_lt i n).elim h (λ k, _),
  refine (coeff_eq_zero_of_nat_degree_lt (pn.trans_lt k)).trans
    (coeff_eq_zero_of_nat_degree_lt (qn.trans_lt k)).symm
end

The advantage is that it bypasses having the nat_degree "alone", but only uses nat_degree ≤, which is easier to deal with.

[Damiano Testa]

The tactic (really compute_degree_le) does not try to figure out which coefficients are zero or not: it simply assumes that everything is "generic" and guesses the degree. For instance, this happens:

example {R : Type*} [semiring R] (a : R) :
  C a = 0 * X ^ 100 + C a :=
begin
  show_deg_le,
/-
R: Type ?
_inst_1: semiring R
a: R
i: ℕ
H: i ≤ 100
⊢ (⇑C a).coeff i = (0 * X ^ 100 + ⇑C a).coeff i
-/
  simp,
end

and note that the range for i is i ≤ 100.

[Damiano Testa]

@Yakov Pechersky I think that if working with sparse polynomials is important, then they should probably get special support, not just from this tactic, but more generally. I think that this is also what happens with computer algebra packages that sometimes have a special "class" of "sparse whatever" with optimized algorithms.

Another point: computing the actual support might be trickier than computing a superset of the union of the supports.

[Yakov Pechersky]

Here's a pretty mechanical proof that is meant to be similar to what meta code would do:

import data.polynomial.degree.definitions
import tactic.swap_var

open polynomial

variables {K : Type*} [semiring K]

lemma ext_support (p q : polynomial K) :
  (∀ n ∈ p.support ∪ q.support, p.coeff n = q.coeff n) ↔ p = q :=
begin
  rw [polynomial.ext_iff],
  refine forall_congr (λ n, ⟨λ h, _, λ h _, h⟩),
  by_cases hp : n ∈ p.support,
  { exact h (finset.mem_union_left _ hp) },
  by_cases hq : n ∈ q.support,
  { exact h (finset.mem_union_right _ hq) },
  { rw [not_mem_support_iff] at hp hq,
    rw [hp, hq] }
end

lemma support_add_eq (p q : polynomial K) (hd : disjoint p.support q.support) :
  (p + q).support = p.support ∪ q.support :=
begin
  refine le_antisymm support_add _,
  intros i h,
  simp only [coeff_add, mem_support_iff, ne.def],
  simp only [finset.mem_union, mem_support_iff] at h,
  cases h with h h, swap, swap_var p q,
  all_goals { have : q.coeff i = 0,
    { rw ←not_mem_support_iff,
      rw ←mem_support_iff at h,
      intro H,
      exact hd (finset.mem_inter_of_mem h H) <|> exact hd (finset.mem_inter_of_mem H h) },
    simpa [this] }
end

example (p q : polynomial K) (hp : p = C 1 + monomial 3 1 + monomial 5 1)
  (hq : q = monomial 5 1 + monomial 3 1 + C 1) : p = q :=
begin
  have hps : p.support ⊆ {0, 3, 5},
  swap,
  have hqs : q.support ⊆ {0, 3, 5},
  swap,
  any_goals { simp only [hp, hq],
    rw [support_add_eq],
    any_goals { rw [support_add_eq] },
    { intro i,
      simp only [map_one, finset.union_assoc, finset.mem_union, finset.mem_insert,
                finset.mem_singleton],
      rintro?;
      { have : i ∈ singleton _ := support_monomial' _ _ ‹_›,
        simp only [finset.mem_singleton] at this,
        simp [this] } },
    try { any_goals { rw finset.disjoint_union_left, split } },
    try { any_goals { rw finset.disjoint_union_right, split } },
    any_goals { refine finset.disjoint_of_subset_left (support_monomial' _ _) _,
        refine finset.disjoint_of_subset_right (support_monomial' _ _) _,
        intro,
        simp } },
  rw ←ext_support,
  intros n hn,
  replace hn : n ∈ {0, 3, 5},
  { rw finset.mem_union at hn,
    cases hn with hn hn;
    exact hps hn <|> exact hqs hn },
  simp only [finset.mem_insert, finset.mem_singleton] at hn,
  rcases? hn;
  simp [hp, hq, coeff_monomial, add_comm, add_assoc, add_left_comm]
end

[Yakov Pechersky]

Yes, I just did what your message ended on, used the superset of the union of supports.

[Yakov Pechersky]

It is possible we are in a ring where the coefficient of one of the monomials is actually zero and we don't know.

[Yakov Pechersky]

That's what I mean by superset here.

[Damiano Testa]

Yes, for instance the zero ring...

[Yakov Pechersky]

You can imagine a tactic that collects all the powers it sees. It then makes the {0, 3, 5} that I have, but with the powers it found. It uses the tactic proof I have here to show that this finset of powers is a superset of the union of the supports.

[Yakov Pechersky]

The rcases? takes care of the "fin_cases" equivalent on that finset that we've constructed.

[Damiano Testa]

Yakov Pechersky said:

You can imagine a tactic that collects all the powers it sees. It then makes the {0, 3, 5} that I have, but with the powers it found. It uses the tactic proof I have here to show that this finset of powers is a superset of the union of the supports.

Such a tactic essentially already exists in #14762: it needs a small amount of glue, since I did not need the support.

[Damiano Testa]

Btw, discounting optimizations, this also works:

example {K : Type*} [semiring K] :
  C 1 + monomial 3 1 + monomial 5 1 = monomial 5 1 + monomial 3 1 + C 1 :=
begin
  show_deg_le,
  simp only [coeff_monomial, coeff_one, eq_nat_cast, nat.cast_one, coeff_add],
  split_ifs;
  refl,
end

[Damiano Testa]

In #14762 there is the function guess_degree which does what you probably imagine. Combining this with list_binary_operands `((+)) (or whatever the right syntax for quoting is), you map guess_degree over the previous one and you obtain a list of degrees of the terms of your expression.

Still, there is no support for expanding products of sums, though.

[Heather Macbeth]

@Damiano Testa Would it make sense to bundle interval_cases or fin_cases into the tactic? Presumably that will be the desired next step in almost every case.

[Heather Macbeth]

Actually, not in this example of yours, I guess.

[Damiano Testa]

I think that this is one of the differences between the "sparse vs range" approach: for a range, you would enumerate everything up to the top degree, while for the sparse case, you would single out the terms that actually appear.

[Damiano Testa]

I am happy either way: at the moment, the tactic simply calls norm_num on the range, to make it look pretty.

[Xavier Roblot]

There was some discussion in this thread about the following result

import ring_theory.polynomial.basic

open polynomial

example {F : Type*} [comm_ring F] (d : ℕ) {f g : polynomial F} (hf : f.nat_degree ≤ d)
  (hg : g.nat_degree ≤ d) (h : ∀ i, i ≤ d → f.coeff i = g.coeff i) :
  f = g :=
begin
  ext,
  by_cases hn : n ≤ d,
  { exact h n hn, },
  { rw [coeff_eq_zero_of_nat_degree_lt, coeff_eq_zero_of_nat_degree_lt],
    linarith, linarith, },
end

but it didn't seem like the result made it into mathlib. I would need something along these lines...

[Riccardo Brasca]

I don't know if this is in mathlib, but you can surely golf the second part using docs#polynomial.coeff_eq_zero_of_nat_degree_lt

[Riccardo Brasca]

Ops, you're already using it

[Riccardo Brasca]

I mean that there is no need to use a powerful tactic as linarith, but it doesn't matter.

[Riccardo Brasca]

In any case if it isn't around docs#polynomial.coeff_eq_zero_of_nat_degree_lt I guess it's not there.

[Damiano Testa]

Further up in this thread, there is a proof of the "iff" version of this result. However, I think that the PR in which this is contained has not been merged. Given that the PR introduces some new tactic, it may not get merged: if you need the result, feel free to PR it!

[Xavier Roblot]

Damiano Testa said:

Further up in this thread, there is a proof of the "iff" version of this result. However, I think that the PR in which this is contained has not been merged. Given that the PR introduces some new tactic, it may not get merged: if you need the result, feel free to PR it!

Indeed, I'll PR the "iff" version then. Thanks!