## Stream: new members

### Topic: What is going wrong here

#### Bolton Bailey (Jan 07 2021 at 08:11):

I am having trouble proving the lemma in the code in the mwe below

-- import data.polynomial.basic
import data.mv_polynomial.basic

noncomputable theory

section

universes u

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

parameters {m n_stmt n_wit : ℕ}

inductive vars : Type
| X : vars
| Y : vars
| Z : vars

def X_poly : mv_polynomial vars F := mv_polynomial.X vars.X

parameters {b : fin m → F}

lemma coeff_powers (j : ℕ) : (λ x : fin m, mv_polynomial.coeff (finsupp.single vars.X j) (b x • X_poly ^ (x : ℕ))) = (λ x : fin m, b x * ite (finsupp.single vars.X (x : ℕ) = finsupp.single vars.X j) 1 0)
:=
begin
apply funext,
intro x,
rw X_poly,
rw mv_polynomial.X_pow_eq_single,
rw mv_polynomial.smul_eq_C_mul,
rw mv_polynomial.coeff_C_mul,
rw mv_polynomial.coeff_monomial,
end

end


With the proof so far, the goal reduces to

⊢ b x * ite (finsupp.single vars.X ↑x = finsupp.single vars.X j) 1 0 = b x * ite (finsupp.single vars.X ↑x = finsupp.single vars.X j) 1 0


In the vs code lean infoview. Yet refl does not work. Even trying by_cases on finsupp.single vars.X ↑x = finsupp.single vars.X j leads to errors when I try to rewrite. What is going on and how do I finish this proof?

#### Kenny Lau (Jan 07 2021 at 08:12):

Have you tried congr? It's a "spot the difference" tactic.

#### Kenny Lau (Jan 07 2021 at 08:13):

my guess is that the decidable instances for the ite are different, in which case split_ifs; refl should work

#### Mario Carneiro (Jan 07 2021 at 08:14):

if it's decidable instances then congr alone should kill it

#### Bolton Bailey (Jan 07 2021 at 08:33):

Yes, the decidable instances may be different somehow - congr closes the proof. Thanks.

#### Eric Wieser (Jan 07 2021 at 08:38):

The noncomputable theory is probably what is causing the problem

#### Eric Wieser (Jan 07 2021 at 08:39):

I think you can just put @[derive decidable_eq] on your inductive type

#### Bolton Bailey (Jan 07 2021 at 09:02):

Removing noncomputable theory raises errors

import data.mv_polynomial.basic

section

-- noncomputable theory

universes u

/-- An inductive type from which to index the variables of the 3-variable polynomials the proof manages -/
@[derive decidable_eq]
inductive vars : Type
| X : vars
| Y : vars
| Z : vars

/-- The finite field parameter of our SNARK -/
parameter {F : Type u}
parameter [field F]

/-- Helpers for representing X, Y, Z as 3-variable polynomials -/
def X_poly : mv_polynomial vars F := mv_polynomial.X vars.X
def Y_poly : mv_polynomial vars F := mv_polynomial.X vars.Y
def Z_poly : mv_polynomial vars F := mv_polynomial.X vars.Z

end


complains of definition 'X_poly' is noncomputable, it depends on 'mv_polynomial.X'

Any work around for this?

#### Eric Wieser (Jan 07 2021 at 09:03):

Yes, add the word noncomputable before def X_poly. But maybe this doesn't help as much as I'd hoped

#### Eric Wieser (Jan 07 2021 at 09:04):

In fact, I think my comment is just wrong, and I'm confusing noncomputable theory with open_locale classical

Last updated: May 14 2021 at 07:19 UTC