Extracting constant from sum

Stream: general

[Bolton Bailey]

Not sure what's going on here, sort of long MWE below, sorry for that.

I am trying to make a simp attribute that puts mv_polynomials into a normal form which makes it easier to evaluate their coefficients. As a part of this, I want to rewrite expressions of the form (∑ x in r, X s * f x) into X s * (∑ x in r, f x). To do this, I make a lemma which is a straightforward application of the finset.mul_sum lemma.

But when I do make this lemma, I get that the tactic fails due to not finding instance of pattern. Strangely, <-finset.mul_sum itself works fine, but I'd rather this simplification be self-contained. (Is there a way to add <-lemma to a simp attribute?)

Am I making a dumb mistake here? What is the issue? I have tried set_option pp.notation false and set_option pp.implicit true but they make the output to verbose to read.

import data.mv_polynomial.basic
import algebra.polynomial.big_operators

open_locale big_operators classical

section

open mv_polynomial

noncomputable theory



universes u

parameter {F : Type u}
parameter [field F]

namespace mv_polynomial
variables {σ : Type*} {e : ℕ} {n m : σ} {s : σ →₀ ℕ}

variables {R : Type u}
variables [comm_semiring R] {p q : mv_polynomial σ R}



@[derive decidable_eq]
inductive vars : Type
| α : vars
| β : vars
| γ : vars
| δ : vars

run_cmd mk_simp_attr `polynomial_nf
run_cmd tactic.add_doc_string `simp_attr.polynomial_nf "Attribute for lemmas that are used in the conversion of mv_polynomial expressions to a normal form"

@[polynomial_nf]
lemma sum_X_mul {α : Type u} {r : finset α} {f : α -> mv_polynomial σ R} (s : σ) :
  (∑ x in r, X s * f x) = X s * (∑ x in r, f x)
:=
begin
  rw finset.mul_sum,
end

-- set_option pp.notation false
-- set_option pp.implicit true

lemma foo :
  ∑ (i : fin 3) in finset.fin_range 3,
    mv_polynomial.X vars.γ
    * ((mv_polynomial.C (i : polynomial F)) : mv_polynomial vars (polynomial F))
  =
  mv_polynomial.X vars.γ
  * ∑ (i : fin 4) in finset.fin_range 4,
    ((mv_polynomial.C (i : polynomial F)) : mv_polynomial vars (polynomial F))
   :=
begin
  -- simp only with polynomial_nf, -- failed to simplify
  rw sum_X_mul, -- rewrite tactic failed, did not find instance of the pattern
  -- rw <-finset.mul_sum, -- works fine
  -- simp only [<-finset.mul_sum], -- works fine
end

end mv_polynomial

end

[Kevin Buzzard]

simp is a rewrite system. It doesn't choose which way to rewrite -- if it could go in both directions it would loop. It only ever rewrites the LHS of a simp lemma into the RHS

[Bolton Bailey]

Yes, which is why I put the form I wanted on the right side in the lemma I made. There is no way for it to loop here

[Kevin Buzzard]

Oh ok sorry, I misunderstood your use of <- in your question

[Bolton Bailey]

Indeed, as you can see, putting simp aside entirely, rw <-finset.mul_sum works but rw sum_X_mul does not. I am wondering why this is the case.

[Yakov Pechersky]

Try making the r and f explicit args, and supplying them in the rw.

[Yakov Pechersky]

Then find where removing them leads to breakage

[Bolton Bailey]

type mismatch at application
  mv_polynomial.sum_X_mul (finset.fin_range 3) (λ (i : fin 3), ⇑C ↑i)
term
  λ (i : fin 3), ⇑C ↑i
has type
  fin 3 → mv_polynomial vars (polynomial F) : Type u
but is expected to have type
  fin 3 → mv_polynomial ?m_1 ?m_2 : Type ?

Is it a universe issue?

[Yakov Pechersky]

Are you explicitly writing coercion arrows?

[Bolton Bailey]

No, the above is the copy-pasted error message when I start putting in the arguments. this is what I wrote

lemma foo :
  ∑ (i : fin 3) in finset.fin_range 3,
    mv_polynomial.X vars.γ
    * ((mv_polynomial.C (i : polynomial F)) : mv_polynomial vars (polynomial F))
  =
  mv_polynomial.X vars.γ
  * ∑ (i : fin 4) in finset.fin_range 4,
    ((mv_polynomial.C (i : polynomial F)) : mv_polynomial vars (polynomial F))
   :=
begin
  -- simp only with polynomial_nf, -- failed to simplify
  rw sum_X_mul (finset.fin_range 3) (λ i, ((mv_polynomial.C (i : polynomial F)) : mv_polynomial vars (polynomial F))),
  -- rewrite tactic failed, did not find instance of the pattern
  -- rw <-finset.mul_sum, -- works fine
  -- simp only [<-finset.mul_sum], -- works fine
end

[Yakov Pechersky]

Ah, so rewrite works up to syntactic equality usually.

[Yakov Pechersky]

import data.mv_polynomial.basic
import algebra.polynomial.big_operators

open_locale big_operators classical

section

open mv_polynomial

noncomputable theory

universes u

parameter {F : Type u}
parameter [field F]

namespace mv_polynomial
variables {σ : Type*} {e : ℕ} {n m : σ} {s : σ →₀ ℕ}

variables {R : Type u}
variables [comm_semiring R] {p q : mv_polynomial σ R}

@[derive decidable_eq]
inductive vars : Type
| α : vars
| β : vars
| γ : vars
| δ : vars

lemma sum_X_mul {α : Type u} [fintype α] (f : α -> mv_polynomial σ R) (s : σ) :
  (∑ x, X s * f x) = X s * (∑ x, f x) :=
by rw finset.mul_sum

lemma foo :
  ∑ (i : fin 3),
    mv_polynomial.X vars.γ
    * ((mv_polynomial.C (i : polynomial F)) : mv_polynomial vars (polynomial F))
  =
  mv_polynomial.X vars.γ
  * ∑ (i : fin 4),
    ((mv_polynomial.C (i : polynomial F)) : mv_polynomial vars (polynomial F))
   :=
begin
  -- ∑ (i : fin 3), X vars.γ * ⇑C ↑i = X vars.γ * ∑ (i : fin 4), ⇑C ↑i
  rw sum_X_mul (mv_polynomial.C) vars.γ,
  -- rewrite tactic failed, did not find instance of the pattern in the target expression
  -- ∑ (x : ?m_1), X vars.γ * ⇑C x
  -- notice that here `x` is without a coercion arrow
end

end mv_polynomial

end

[Yakov Pechersky]

  simp [sum_X_mul (mv_polynomial.C) vars.γ],
``` will work

[Bolton Bailey]

Ah, was the issue that I was conflating finset with fintype?

[Yakov Pechersky]

No, I was just simplifying the lemma requirements. The issue is that your statement has ⇑C ↑i but rw is looking for ⇑C i. They are not syntactically the same.

[Bolton Bailey]

Ok, but none of this solves my problem of wanting to include this in a simp attribute, it seems. It still doesn't work as rw sum_X_mul

[Bolton Bailey]

It also doesn't explain why sum_mul works but sum_X_mul doesn't.

[Bolton Bailey]

Here's the mwe again with mul_sum.symm dragged into the file as mul_sum_2. It works fine, but my lemma does not. Why?

import data.mv_polynomial.basic
import algebra.polynomial.big_operators

open_locale big_operators classical

section

open mv_polynomial

noncomputable theory



universes u v

parameter {F : Type u}
parameter [field F]

namespace mv_polynomial
variables {σ : Type*} {e : ℕ} {n m : σ} {s : σ →₀ ℕ}

variables {R : Type u}
variables [comm_semiring R] {p q : mv_polynomial σ R}



@[derive decidable_eq]
inductive vars : Type
| α : vars
| β : vars
| γ : vars
| δ : vars

run_cmd mk_simp_attr `polynomial_nf
run_cmd tactic.add_doc_string `simp_attr.polynomial_nf "Attribute for lemmas that are used in the conversion of mv_polynomial expressions to a normal form"

variables {α : Type u} {β : Type v}

namespace finset
variables {s₁ s₂ : finset α} {a : α} {b : β}  {f g : α → β}


section semiring
variables [non_unital_non_assoc_semiring β]

lemma mul_sum_2 :
 ∑ x in s₁, b * f x
  = b * (∑ x in s₁, f x) :=
finset.mul_sum.symm


@[polynomial_nf]
lemma sum_X_mul (f : α -> mv_polynomial σ R) (s : σ) :
  (∑ x in s₁, X s * f x) = X s * (∑ x in s₁, f x) :=
by rw finset.mul_sum


-- set_option pp.notation false
-- set_option pp.implicit true

lemma foo :
  ∑ (i : fin 3),
    mv_polynomial.X vars.γ
    * ((mv_polynomial.C (i : polynomial F)) : mv_polynomial vars (polynomial F))
  =
  mv_polynomial.X vars.γ
  * ∑ (i : fin 4),
    ((mv_polynomial.C (i : polynomial F)) : mv_polynomial vars (polynomial F))
   :=
begin
  rw sum_X_mul, -- fails
  -- rw mul_sum_2, -- works
end

end semiring

end finset

end mv_polynomial

end