What is going wrong here

Stream: new members

[Bolton Bailey]

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]

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

[Kenny Lau]

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

[Mario Carneiro]

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

[Bolton Bailey]

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

[Eric Wieser]

The noncomputable theory is probably what is causing the problem

[Eric Wieser]

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

[Bolton Bailey]

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]

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

[Eric Wieser]

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