coeff_mul

Stream: maths

[Johan Commelin]

I have just finished the proof of coeff_mul for `mv_polynomial:
https://gist.github.com/jcommelin/add8c8df8b3479c435d3f5ac34cdb1f7#file-mv_polynomial_coeff_mul-lean-L189-L298

[Johan Commelin]

lemma coeff_mul (φ ψ : mv_polynomial σ α) (n) :
coeff n (φ * ψ) = finset.sum (finsupp.nat_downset n) (λ m, coeff m φ * coeff (n - m) ψ) :=

[Johan Commelin]

I think this would fill a little gap in the API for polynomials.

[Johan Commelin]

Question: what should finsupp.nat_downset be called? Does this somehow generalise? Is there something like "partial orders with downsets that are finsets"?

[Johan Commelin]

Also... if people want a golfing challenge... currently the proof is a whopping 120 lines...

[Johan Commelin]

Another option is to sum over a finset in the product, so that we are even closer to mimicking $\sum_{i + j = n} c_i(\phi) \cdot c_j(\psi)$.

[Mario Carneiro]

It already exists, it's called multiset.diagonal I think

[Mario Carneiro]

(actually that's the subtraction free version - nat_downset is multiset.powerset)

[Mario Carneiro]

Just like with nat, I recommend avoiding subtraction here and indeed I suggest using a finset over the product as you've indicated

[Johan Commelin]

Ok, but multiset X is not defeq to finsupp X nat

[Johan Commelin]

@Mario Carneiro I think multiset.diagonal is very nice. But how should I apply it in the context of mv_polynomial? There is no obvious analogue for arbitrary finsupps. Should I use glue between multiset X and finsupp X nat?

[Mario Carneiro]

The analogue I think is to axiomatize it

[Mario Carneiro]

there are other examples, but I don't know a better way to say it than "the set of all elements below x is finite"

[Mario Carneiro]

In the case of finsupp X nat specifically, I think I would just prove it by transferring from multiset X

[Johan Commelin]

I'm still confused about what you would want the statement of coeff_mul to look like...

[Mario Carneiro]

lemma coeff_mul (φ ψ : mv_polynomial σ α) (n) :
coeff n (φ * ψ) = finset.sum (finsupp.diagonal n) (λ p, coeff p.1 φ * coeff p.2 ψ) :=

[Mario Carneiro]

here finsupp.diagonal n is something like (multiset.diagonal n.support).map (prod.map f f) where f m = \lam x, count x m

[Mario Carneiro]

and f is then shown to be one half of an order isomorphism, so that mem_diagonal holds also for finsupp

[Johan Commelin]

Aha... thanks for the suggestions!

[Johan Commelin]

@Mario Carneiro It's not a problem that finsupp.diagonal is only defined for ℕ?

[Mario Carneiro]

The generalization, like I said, is to have a typeclass for types that have a diagonal function; this is the instance for nat

[Mario Carneiro]

Another example of a type with this property (let's say "downward finite") is finsupp X A itself, when A is downward finite

[Kenny Lau]

Ok, but multiset X is not defeq to finsupp X nat

hey we have a natural isomorphism

[Mario Carneiro]

I would have thought you would be the first to point out that it's not constructively provable

[Kenny Lau]

which direction?

[Mario Carneiro]

finsupp -> multiset

[Kenny Lau]

but you have the support

[Mario Carneiro]

Oh you're right. As long as X is decidable both directions work

[Kenny Lau]

looks like I need to bring up my special category

[Kenny Lau]

@Mario Carneiro

-- ⟨s.to_finset, λ x, s.count x, λ x, multiset.mem_to_finset.trans $ multiset.count_pos.symm.trans $ nat.pos_iff_ne_zero⟩
-- faster but less idiomatic
def Multiset_Finsupp_nat : Multiset.{u} ≅ Finsupp_nat.{u} :=
{ hom :=
  { app := λ α s, (s.map $ λ x, finsupp.single x 1).sum,

[Kenny Lau]

which one would you choose?

[Kenny Lau]

import data.multiset data.finsupp
import category_theory.natural_isomorphism category_theory.types category_theory.opposites category_theory.concrete_category

universe u

open category_theory

namespace category_theory.instances

@[reducible] def DecEq := bundled decidable_eq

instance (x : DecEq) : decidable_eq x := x.str

instance DecEq_category : category DecEq :=
{ hom := λ x y, x → y,
  id := λ x, id,
  comp := λ x y z f g, g ∘ f }

end category_theory.instances

open category_theory.instances

@[reducible] def Multiset : DecEq.{u} ⥤ Type u :=
{ obj := λ α, multiset α,
  map := λ α β, multiset.map,
  map_id' := λ α, funext multiset.map_id,
  map_comp' := λ α β γ f g, funext $ λ s, (multiset.map_map g f s).symm }

@[reducible] def Finsupp_nat : DecEq.{u} ⥤ Type u :=
{ obj := λ α, α →₀ ℕ,
  map := λ α β, finsupp.map_domain,
  map_id' := λ α, funext $ λ s, finsupp.map_domain_id,
  map_comp' := λ α β γ f g, funext $ λ s, finsupp.map_domain_comp }

theorem multiset.map_repeat {α : Type u} {β : Type*} (f : α → β) (x : α) (n : ℕ) :
  multiset.map f (multiset.repeat x n) = multiset.repeat (f x) n :=
nat.rec_on n rfl $ λ n ih, by rw [multiset.repeat_succ, multiset.map_cons, ih, multiset.repeat_succ]

theorem multiset.repeat_add {α : Type u} (x : α) (m n : ℕ) :
  multiset.repeat x (m + n) = multiset.repeat x m + multiset.repeat x n :=
nat.rec_on n (by rw [multiset.repeat_zero, add_zero, add_zero]) $ λ n ih,
by rw [multiset.repeat_succ, nat.add_succ, multiset.repeat_succ, multiset.add_cons, ih]

-- ⟨s.to_finset, λ x, s.count x, λ x, multiset.mem_to_finset.trans $ multiset.count_pos.symm.trans $ nat.pos_iff_ne_zero⟩
-- faster but less idiomatic
def Multiset_Finsupp_nat : Multiset.{u} ≅ Finsupp_nat.{u} :=
{ hom :=
  { app := λ α s, (s.map $ λ x, finsupp.single x 1).sum,
    naturality' := λ α β f, funext $ λ s, finsupp.ext $ λ x,
      show ((multiset.map f s).map $ λ x, finsupp.single x 1).sum x = finsupp.map_domain f (s.map $ λ x, finsupp.single x 1).sum x,
      from multiset.induction_on s rfl $ λ a s ih, if h : f a = x
      then by rw [multiset.map_cons, multiset.map_cons, multiset.sum_cons, finsupp.add_apply, finsupp.single_apply, if_pos h,
          multiset.map_cons, multiset.sum_cons, finsupp.map_domain_add, finsupp.add_apply, finsupp.map_domain_single, finsupp.single_apply, if_pos h, ih]
      else by rw [multiset.map_cons, multiset.map_cons, multiset.sum_cons, finsupp.add_apply, finsupp.single_apply, if_neg h,
          multiset.map_cons, multiset.sum_cons, finsupp.map_domain_add, finsupp.add_apply, finsupp.map_domain_single, finsupp.single_apply, if_neg h, ih] },
  inv :=
  { app := λ α s, s.sum multiset.repeat,
    naturality' := λ α β f, funext $ λ s,
      show (s.map_domain f).sum multiset.repeat = (s.sum multiset.repeat).map f,
      from finsupp.induction s rfl $ λ x n s hsx hn ih, begin
        rw [finsupp.map_domain_add, finsupp.sum_add_index, finsupp.map_domain_single, finsupp.sum_single_index,
            finsupp.sum_add_index, finsupp.sum_single_index, multiset.map_add, multiset.map_repeat, ih],
        { refl }, { intros, refl }, { intros, rw multiset.repeat_add },
        { refl }, { intros, refl }, { intros, rw multiset.repeat_add }
      end },
  hom_inv_id' := nat_trans.ext $ λ α, funext $ λ s, by skip,
  inv_hom_id' := nat_trans.ext $ λ α, funext $ λ s, finsupp.ext $ by skip }

[Kenny Lau]

that's it for now

[Kenny Lau]

I think I was just aware of finsupp.of_multiset

[Kenny Lau]

import data.multiset data.finsupp
import category_theory.natural_isomorphism category_theory.types category_theory.opposites category_theory.concrete_category

universe u

open category_theory

namespace category_theory.instances

@[reducible] def DecEq := bundled decidable_eq

instance (x : DecEq) : decidable_eq x := x.str

instance DecEq_category : category DecEq :=
{ hom := λ x y, x → y,
  id := λ x, id,
  comp := λ x y z f g, g ∘ f }

end category_theory.instances

open category_theory.instances

@[reducible] def Multiset : DecEq.{u} ⥤ Type u :=
{ obj := λ α, multiset α,
  map := λ α β, multiset.map,
  map_id' := λ α, funext multiset.map_id,
  map_comp' := λ α β γ f g, funext $ λ s, (multiset.map_map g f s).symm }

@[reducible] def Finsupp_nat : DecEq.{u} ⥤ Type u :=
{ obj := λ α, α →₀ ℕ,
  map := λ α β, finsupp.map_domain,
  map_id' := λ α, funext $ λ s, finsupp.map_domain_id,
  map_comp' := λ α β γ f g, funext $ λ s, finsupp.map_domain_comp }

theorem multiset.map_repeat {α : Type u} {β : Type*} (f : α → β) (x : α) (n : ℕ) :
  multiset.map f (multiset.repeat x n) = multiset.repeat (f x) n :=
nat.rec_on n rfl $ λ n ih, by rw [multiset.repeat_succ, multiset.map_cons, ih, multiset.repeat_succ]

theorem multiset.repeat_add {α : Type u} (x : α) (m n : ℕ) :
  multiset.repeat x (m + n) = multiset.repeat x m + multiset.repeat x n :=
nat.rec_on n (by rw [multiset.repeat_zero, add_zero, add_zero]) $ λ n ih,
by rw [multiset.repeat_succ, nat.add_succ, multiset.repeat_succ, multiset.add_cons, ih]

-- ⟨s.to_finset, λ x, s.count x, λ x, multiset.mem_to_finset.trans $ multiset.count_pos.symm.trans $ nat.pos_iff_ne_zero⟩
-- faster but less idiomatic
def Multiset_Finsupp_nat : Multiset.{u} ≅ Finsupp_nat.{u} :=
{ hom :=
  { app := λ α s, (s.map $ λ x, finsupp.single x 1).sum,
    naturality' := λ α β f, funext $ λ s, finsupp.ext $ λ x,
      show ((multiset.map f s).map $ λ x, finsupp.single x 1).sum x = finsupp.map_domain f (s.map $ λ x, finsupp.single x 1).sum x,
      from multiset.induction_on s rfl $ λ a s ih, if h : f a = x
      then by rw [multiset.map_cons, multiset.map_cons, multiset.sum_cons, finsupp.add_apply, finsupp.single_apply, if_pos h,
          multiset.map_cons, multiset.sum_cons, finsupp.map_domain_add, finsupp.add_apply, finsupp.map_domain_single, finsupp.single_apply, if_pos h, ih]
      else by rw [multiset.map_cons, multiset.map_cons, multiset.sum_cons, finsupp.add_apply, finsupp.single_apply, if_neg h,
          multiset.map_cons, multiset.sum_cons, finsupp.map_domain_add, finsupp.add_apply, finsupp.map_domain_single, finsupp.single_apply, if_neg h, ih] },
  inv :=
  { app := λ α s, s.sum multiset.repeat,
    naturality' := λ α β f, funext $ λ s,
      show (s.map_domain f).sum multiset.repeat = (s.sum multiset.repeat).map f,
      from finsupp.induction s rfl $ λ x n s hsx hn ih, begin
        rw [finsupp.map_domain_add, finsupp.sum_add_index, finsupp.map_domain_single, finsupp.sum_single_index,
            finsupp.sum_add_index, finsupp.sum_single_index, multiset.map_add, multiset.map_repeat, ih],
        { refl }, { intros, refl }, { intros, rw multiset.repeat_add },
        { refl }, { intros, refl }, { intros, rw multiset.repeat_add }
      end },
  hom_inv_id' := nat_trans.ext $ λ α, funext $ λ s,
    show (s.map $ λ x, finsupp.single x 1).sum.sum multiset.repeat = s,
    from multiset.induction_on s rfl $ λ a s ih, begin
      rw [multiset.map_cons, multiset.sum_cons, finsupp.sum_add_index, finsupp.sum_single_index, multiset.repeat_one, ih, multiset.cons_add, zero_add],
      { refl }, { intros, refl }, { intros, rw multiset.repeat_add }
    end,
  inv_hom_id' := nat_trans.ext $ λ α, funext $ λ s,
    show ((s.sum multiset.repeat).map $ λ x, finsupp.single x 1).sum = s,
    from finsupp.induction s rfl $ λ y n s hsy hn ih, begin
      rw [finsupp.sum_add_index, finsupp.sum_single_index, multiset.map_add, multiset.sum_add, ih, multiset.map_repeat],
      { congr' 1, clear hn, induction n with n ih,
        { rw [finsupp.single_zero, multiset.repeat_zero, multiset.sum_zero] },
        { rw [multiset.repeat_succ, multiset.sum_cons, ih, ← nat.one_add, finsupp.single_add] } },
      { refl }, { intros, refl }, { intros, rw multiset.repeat_add }
    end }

[Johan Commelin]

Stuff got 90 lines shorter after @Mario Carneiro's suggestions: https://gist.github.com/jcommelin/add8c8df8b3479c435d3f5ac34cdb1f7

[Johan Commelin]

Still using - to subtract single s 1 but I think that can't be avoided.

[Patrick Massot]

This is still pretty frightening. It's really baffling to think the definition of multiplication does not make this lemma obvious...

[Johan Commelin]

Of course people shouldn't be discouraged to golf this down to a 5 line proof

[Johan Commelin]

I really feel like making this the definition of multiplication.

[Johan Commelin]

But I guess mv_polynomial inherits multiplication in a crazy way from ℕ being a add_monoid.

[Chris Hughes]

I'm surprised you didn't use multiset.count anywhere.

[Johan Commelin]

Maybe I should not have proven it by induction on the polynomials...

[Johan Commelin]

I don't know.

[Johan Commelin]

It seemed like an obvious thing to do. Maybe it is obviously bad.

[Johan Commelin]

lemma coeff_mul (φ ψ : mv_polynomial σ α) (n : σ →₀ ℕ) :
  coeff n (φ * ψ) = finset.sum (diagonal n) (λ p, coeff p.1 φ * coeff p.2 ψ) :=
begin
  rw mul_def,
  have := @finset.sum_sigma (σ →₀ ℕ) α _ _ φ.support (λ _, ψ.support)
    (λ x, if (x.1 + x.2 = n) then coeff x.1 φ * coeff x.2 ψ else 0),
  convert this.symm using 1; clear this,
  { rw [coeff],
    repeat {rw sum_apply, apply finset.sum_congr rfl, intros, dsimp only},
    exact single_apply },
  { have : (diagonal n).filter (λ x, x.1 ∈ φ.support ∧ x.2 ∈ ψ.support) ⊆ (diagonal n) :=
      finset.filter_subset _,
    rw [← finset.sum_sdiff this, finset.sum_eq_zero, zero_add], swap,
    { intros x hx, rw [finset.mem_sdiff, not_iff_not_of_iff (finset.mem_filter),
        not_and, not_and, not_mem_support_iff] at hx,
      by_cases H : x.1 ∈ φ.support,
      { rw [coeff, coeff, hx.2 hx.1 H, mul_zero] },
      { rw not_mem_support_iff at H, rw [coeff, H, zero_mul] } },
    symmetry,
    rw [← finset.sum_sdiff (finset.filter_subset _), finset.sum_eq_zero, zero_add], swap,
    { intros x hx, rw [finset.mem_sdiff, not_iff_not_of_iff (finset.mem_filter), not_and] at hx,
      replace hx := hx.2 hx.1, rw if_neg, exact hx },
    { apply finset.sum_bij, swap 5, { intros x hx, exact (x.1, x.2) },
      { intros x hx, rw [finset.mem_filter, finset.mem_sigma] at hx,
        rw [finset.mem_filter, mem_diagonal],
        dsimp, exact hx.symm },
      { intros x hx, rw finset.mem_filter at hx, rw if_pos hx.2 },
      { rintros ⟨i,j⟩ ⟨k,l⟩ hij hkl, simpa using and.intro },
      { rintros ⟨i,j⟩ hij, refine ⟨⟨i,j⟩, _, _⟩, { apply_instance },
        { rw [finset.mem_filter, mem_diagonal] at hij, rw [finset.mem_filter, finset.mem_sigma],
          exact hij.symm },
        { refl } } },
    all_goals { apply_instance } }
end

[Johan Commelin]

I hope this is a more reasonable length.