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: Dec 20 2023 at 11:08 UTC