Zulip Chat Archive

Stream: maths

Topic: coeff_mul


Johan Commelin (Jul 09 2019 at 06:42):

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 (Jul 09 2019 at 06:43):

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

Johan Commelin (Jul 09 2019 at 06:43):

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

Johan Commelin (Jul 09 2019 at 06:44):

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 (Jul 09 2019 at 06:44):

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

Johan Commelin (Jul 09 2019 at 06:46):

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

Mario Carneiro (Jul 09 2019 at 07:02):

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

Mario Carneiro (Jul 09 2019 at 07:03):

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

Mario Carneiro (Jul 09 2019 at 07:05):

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 (Jul 09 2019 at 07:19):

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

Johan Commelin (Jul 09 2019 at 07:22):

@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 (Jul 09 2019 at 07:24):

The analogue I think is to axiomatize it

Mario Carneiro (Jul 09 2019 at 07:25):

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 (Jul 09 2019 at 07:26):

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

Johan Commelin (Jul 09 2019 at 07:27):

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

Mario Carneiro (Jul 09 2019 at 07:28):

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

Mario Carneiro (Jul 09 2019 at 07:30):

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 (Jul 09 2019 at 07:32):

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

Johan Commelin (Jul 09 2019 at 07:33):

Aha... thanks for the suggestions!

Johan Commelin (Jul 09 2019 at 07:34):

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

Mario Carneiro (Jul 09 2019 at 07:35):

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 (Jul 09 2019 at 07:38):

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 (Jul 09 2019 at 07:41):

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

hey we have a natural isomorphism

Mario Carneiro (Jul 09 2019 at 07:43):

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

Kenny Lau (Jul 09 2019 at 07:45):

which direction?

Mario Carneiro (Jul 09 2019 at 07:46):

finsupp -> multiset

Kenny Lau (Jul 09 2019 at 07:47):

but you have the support

Mario Carneiro (Jul 09 2019 at 07:48):

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

Kenny Lau (Jul 09 2019 at 07:48):

looks like I need to bring up my special category

Kenny Lau (Jul 09 2019 at 10:12):

@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 (Jul 09 2019 at 10:12):

which one would you choose?

Kenny Lau (Jul 09 2019 at 11:20):

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 (Jul 09 2019 at 11:20):

that's it for now

Kenny Lau (Jul 09 2019 at 13:25):

I think I was just aware of finsupp.of_multiset

Kenny Lau (Jul 09 2019 at 13:31):

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 (Jul 09 2019 at 14:20):

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

Johan Commelin (Jul 09 2019 at 14:20):

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

Patrick Massot (Jul 09 2019 at 14:23):

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

Johan Commelin (Jul 09 2019 at 14:23):

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

Johan Commelin (Jul 09 2019 at 14:46):

I really feel like making this the definition of multiplication.

Johan Commelin (Jul 09 2019 at 14:46):

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

Chris Hughes (Jul 09 2019 at 14:56):

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

Johan Commelin (Jul 09 2019 at 14:57):

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

Johan Commelin (Jul 09 2019 at 14:57):

I don't know.

Johan Commelin (Jul 09 2019 at 14:57):

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

Johan Commelin (Jul 11 2019 at 09:19):

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 (Jul 11 2019 at 09:19):

I hope this is a more reasonable length.


Last updated: Dec 20 2023 at 11:08 UTC