Rewrite: function expected

Stream: new members

[Pim Otte]

In the corresponding sample, I'm trying to get the 2 out of the (alphabeta2) multiplication on the right.

The lemma I've found does a little bit more, but I can't get the rewrite to work.

Could anyone help me understand why it's expecting a function? I sort of get this in the context of an iff rewrite, because then it is a function, but I'm also supposed to be able to rewrite with an equality lemma, right? Thanks in advance!

import data.mv_polynomial.basic
import data.complex.basic

noncomputable theory

example  (α β : ℂ): 5 = 5 :=
begin
    have fact': (mv_polynomial.monomial (finsupp.single 0 1 + finsupp.single 1 1)) (α * β) * 2 = (mv_polynomial.monomial (finsupp.single 0 1 + finsupp.single 1 1)) (α * β * 2),
      {
        rw ← (mv_polynomial.monomial_mul (finsupp.single 0 1) (finsupp.single 1 1) (α * β) 2),
        -- function expected at
        -- mv_polynomial.monomial_mul
        -- term has type
        -- ⇑(mv_polynomial.monomial ?m_4) ?m_5 * ⇑(mv_polynomial.monomial ?m_6) ?m_7 =
        -- ⇑(mv_polynomial.monomial (?m_4 + ?m_6)) (?m_5 * ?m_7)
        sorry,
      },
    sorry,
end

[Ruben Van de Velde]

It's not the rewrite, this gives the same error:

        have := mv_polynomial.monomial_mul (finsupp.single 0 1) (finsupp.single 1 1) (α * β) 2,

The issue is that mv_polynomial.monomial_mul's arguments are implicit, so you just need

        rw ← mv_polynomial.monomial_mul,

[Pim Otte]

Ahhhh, so if arguments are between { }, it doesn't just mean it'll infer them, it also means you can't supply them? Though it's not a problem per se, I can rw multiple times in this case; is there any way I can specify which instance of a pattern I'd like to rewrite when the arguments are implicit like this?

[Filippo A. E. Nuccio]

Yes, you can use @. If you call @mv.polynomial.monomial_mul it will expect all variables, both those in {} and those in [].

[Pim Otte]

Follow-up question. I'm failing at another rewrite, I've checked the whole expression in the hypothesis and goal and the brackets and such seem to match, so I'm guessing it's a type coercion thing or something of that sort.

Two questions: How do I fix this, but perhaps more importantly, how could I debug something like this?

import data.mv_polynomial.basic
import data.complex.basic
import ring_theory.polynomial.homogeneous

noncomputable theory

open_locale big_operators

def is_waring_decomposition {σ : Type*} {R : Type*} [comm_semiring R] (p : mv_polynomial σ R) (s : finset (ℕ × mv_polynomial.homogeneous_submodule σ R 1)) := (∑ i in s, (i.2 : mv_polynomial σ R)^i.1) = p

def waring_rank {σ : Type*} {R : Type*} [comm_semiring R] (p : mv_polynomial σ R) : nat := Inf ({n : ℕ | ∃ s : finset (ℕ × mv_polynomial.homogeneous_submodule σ R 1), is_waring_decomposition p s ∧ sizeof s = n} : set ℕ)


lemma simple_waring_rank (p ∈ mv_polynomial.homogeneous_submodule (fin 2) ℂ 2) : 2 ≤ waring_rank(p)  ↔ ((mv_polynomial.coeff (finsupp.single 0 1 + finsupp.single 1 1) p)^2 - 4*(mv_polynomial.coeff (finsupp.single 0 2) p)*(mv_polynomial.coeff (finsupp.single 1 2) p) ≠ 0 ∨ p = 0):=
begin
  split,
  {
    contrapose!,
    intro h,

    have choose_α_β : ∃ (α β : ℂ), (mv_polynomial.coeff (finsupp.single 0 1 + finsupp.single 1 1) p = 2*α*β ∧ mv_polynomial.coeff (finsupp.single 0 2) p = α^2 ∧ mv_polynomial.coeff (finsupp.single 1 2) p = β^2),
    {
      sorry,
    },

    cases choose_α_β with α h',
    cases h' with β hαβ,
    have fact₁ : (mv_polynomial.monomial (finsupp.single 0 1) α + mv_polynomial.monomial (finsupp.single 1 1) β)^2 = p,
    {
      ring_nf SOP,
      rw mv_polynomial.ext_iff,
      intros m,
      simp only [mv_polynomial.monomial_pow, mv_polynomial.monomial_mul, finsupp.smul_single', mul_one, mv_polynomial.coeff_add,
  mv_polynomial.coeff_monomial],
      cases hαβ with hmiddle h',
      cases h' with hfirst hlast,
      rw ← hfirst,
      rw ← hlast,

      have fact': (mv_polynomial.monomial (finsupp.single 0 1 + finsupp.single 1 1)) (α * β) * 2 = (mv_polynomial.monomial (finsupp.single 0 1 + finsupp.single 1 1)) (α * β * 2),
      {
        sorry,
      },
      -- Another rewrite failure?
      rw fact',


      sorry,
    },
    sorry,
  },
  sorry,
end

[Filippo A. E. Nuccio]

The problem is that in the goal the polynomails are supported on fin 2 and in fact' they are supported on nat.

[Filippo A. E. Nuccio]

You can click on the VSCode widget to see it.

[Pim Otte]

Thanks, that makes a ton of sense:)

[Filippo A. E. Nuccio]

You can use @again to force where they are supported in fact'.

[Pim Otte]

have fact': (mv_polynomial.monomial (finsupp.single (0 : (fin 2)) 1 + finsupp.single 1 1)) (α * β) * 2 = (mv_polynomial.monomial (finsupp.single 0 1 + finsupp.single 1 1)) (2 * α * β),
      {
        simp only [← mv_polynomial.monomial_mul, mv_polynomial.monomial_eq_C_mul_X],
        simp only [pow_one, mv_polynomial.C_mul, map_bit0, mv_polynomial.C_1],
        ring,
      },

I ended up squeezing in a type ascription in and that seems to do the trick too:)

[Ruben Van de Velde]

Looks like Filippo beat me to it, but yeah, I was suspicious of the twos, so I clicked on them:
Screenshot-from-2022-08-04-18-02-08.png

[Pim Otte]

Okay, so I'm now putting (fin 2) everywhere, but I'm stuck at a "failed to synthesize type class for mul_zero_one_class (fin 2)".

Any pointers for what I should put on the blank and/or how I could find that out?

import data.mv_polynomial.basic

noncomputable theory

example : 0 = 0 :=
begin
  have fact_disjoint_support : (finsupp.single (0 : (fin 2)) 1 + finsupp.single (1 : (fin 2)) 1).support = (finsupp.single (0 : (fin 2)) 1).support ∪ (finsupp.single (1 : (fin 2)) 1).support,
                {
                    exact finsupp.support_add_eq ((finsupp.support_single_disjoint one_ne_zero one_ne_zero).mpr (@zero_ne_one (fin 2)  _))
                },
end

[Eric Wieser]

That last fin 2 should be ℕ I think