Zulip Chat Archive

Stream: maths

Topic: coeff_mul


view this post on Zulip 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

view this post on Zulip 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) ψ) :=

view this post on Zulip Johan Commelin (Jul 09 2019 at 06:43):

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

view this post on Zulip 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"?

view this post on Zulip Johan Commelin (Jul 09 2019 at 06:44):

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

view this post on Zulip 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).

view this post on Zulip Mario Carneiro (Jul 09 2019 at 07:02):

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

view this post on Zulip Mario Carneiro (Jul 09 2019 at 07:03):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jul 09 2019 at 07:19):

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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jul 09 2019 at 07:24):

The analogue I think is to axiomatize it

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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 ψ) :=

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jul 09 2019 at 07:33):

Aha... thanks for the suggestions!

view this post on Zulip Johan Commelin (Jul 09 2019 at 07:34):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jul 09 2019 at 07:45):

which direction?

view this post on Zulip Mario Carneiro (Jul 09 2019 at 07:46):

finsupp -> multiset

view this post on Zulip Kenny Lau (Jul 09 2019 at 07:47):

but you have the support

view this post on Zulip Mario Carneiro (Jul 09 2019 at 07:48):

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

view this post on Zulip Kenny Lau (Jul 09 2019 at 07:48):

looks like I need to bring up my special category

view this post on Zulip 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,

view this post on Zulip Kenny Lau (Jul 09 2019 at 10:12):

which one would you choose?

view this post on Zulip 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 }

view this post on Zulip Kenny Lau (Jul 09 2019 at 11:20):

that's it for now

view this post on Zulip Kenny Lau (Jul 09 2019 at 13:25):

I think I was just aware of finsupp.of_multiset

view this post on Zulip 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 }

view this post on Zulip Johan Commelin (Jul 09 2019 at 14:20):

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

view this post on Zulip Johan Commelin (Jul 09 2019 at 14:20):

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

view this post on Zulip 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...

view this post on Zulip Johan Commelin (Jul 09 2019 at 14:23):

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

view this post on Zulip Johan Commelin (Jul 09 2019 at 14:46):

I really feel like making this the definition of multiplication.

view this post on Zulip Johan Commelin (Jul 09 2019 at 14:46):

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

view this post on Zulip Chris Hughes (Jul 09 2019 at 14:56):

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

view this post on Zulip Johan Commelin (Jul 09 2019 at 14:57):

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

view this post on Zulip Johan Commelin (Jul 09 2019 at 14:57):

I don't know.

view this post on Zulip Johan Commelin (Jul 09 2019 at 14:57):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jul 11 2019 at 09:19):

I hope this is a more reasonable length.


Last updated: May 10 2021 at 06:13 UTC