# Zulip Chat Archive

## 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