missing 'noncomputable' modifier

Stream: new members

[Michael Wahlberg]

What does this error mean? I was trying to define a special type of additive character :

def add_char'(x : F) (ζ_p : ℂˣ) ( hζ_p : is_primitive_root ζ_p p ) : ℂˣ  :=
  ζ_p^( zmod.val (algebra.trace (zmod (ring_char F)) F x)

And the error I got was:-
def add_char'(x : F) (ζ_p : ℂˣ) ( hζ_p : is_primitive_root ζ_p p ) : ℂˣ :=

[Alex J. Best]

Can you post a full #mwe with imports? That doesn't look like you've pasted the error there either

[Michael Wahlberg]

My bad. Here is the stuff I used :-

import number_theory.legendre_symbol.add_character
import number_theory.legendre_symbol.zmod_char
import algebra.char_p.char_and_card
import field_theory.finite.trace
import number_theory.cyclotomic.basic
import data.zmod.basic

universes u v w
variables {f : ℕ}
variables {F : Type u} [field F] [fintype F]
variables {p : ℕ} [fact p.prime] [char_p F p]

def add_char'(x : F) (ζ_p : ℂˣ) ( hζ_p : is_primitive_root ζ_p p ) : ℂˣ  :=
  ζ_p^( zmod.val (algebra.trace (zmod (ring_char F)) F x))

and the error was :-
`
missing 'noncomputable' modifier, definition 'add_char'' depends on 'ring_char'

`

[Eric Wieser]

Looks like your clipboard is betraying you

[Eric Wieser]

Because the error message looks missing still

[Michael Wahlberg]

Oh, I got it now, probably need the noncomputable modifier.

[Michael Stoll]

I think everything involving real or complex numbers is noncomputable (and Lean insists it be marked as such).

[Kyle Miller]

You can put noncomputable theory at the top of your module to automatically mark anything that Lean detects is noncomputable with noncomputable.

[Kyle Miller]

(Lean always knows the answer; needing to write noncomputable is a formality.)

[Eric Wieser]

Michael Stoll said:

I think everything involving real or complex numbers is noncomputable (and Lean insists it be marked as such).

That's not the case, it's just that docs#ring_char is noncomputable

[Kevin Buzzard]

It's just most things involving real or complex numbers which are noncomputable (e.g. sqrt, sin, exp, ...)

[Eric Wieser]

And you could argue that even the cases that are computable aren't meaningfully computable

[Michael Wahlberg]

But I think it's straightforward to calculate the character of any finite field. For that what function should I use?

[Eric Wieser]

I think using ring_char is fine

[Eric Wieser]

If you wanted it to be computable, you could use nat.find with an appropriate predicate

[Eric Wieser]

Or perhaps the algorithm you have in mind is to look at the factors of fintype.card F?

[Michael Wahlberg]

yup
Eric Wieser said:

Or perhaps the algorithm you have in mind is to look at the factors of fintype.card F?

[Kevin Buzzard]

I think that you might be using a different concept of "calculate" than this computable stuff. I think that polynomial addition might not be computable, but you can still calculate additions easily using the ring tactic.

[Eric Wieser]

Proving nat.min_fac (fintype.card F) = ring_char F would be a reasonable thing to do

[Eric Wieser]

Oh, here's a better spelling of ring_char F; just use p

[Eric Wieser]

You already wrote [char_p F p] which says "p is the characteristic of F"

[Eric Wieser]

There is no need to then re-compute p

[Eric Wieser]

(docs#ring_char.eq is a proof that they coincide)

[Michael Wahlberg]

Is there a way to simplify match tactics in our tactic state?

[Eric Wieser]

Can you give an example of the tactic state?

[Michael Wahlberg]

here: -
α: Type u n: ℕ v: Vec α n n✝: ℕ x: α xs: Vec α n✝ ⊢ ofVector (n✝ + 1) (match Vec.toVector n✝ xs with | { val := l, property := h } => { val := x :: l, property := (_ : List.length (x :: l) = n✝ + 1) }) = cons x xs

[Michael Wahlberg]

And here is my function :-

def Vec.toVector {α : Type u}: (n : ℕ) →  Vec α n → Vector α n
| _, v =>
  match v with
  | Vec.nil =>
    ⟨[], rfl⟩
  | Vec.cons x xs =>
    match Vec.toVector _ xs with
    | ⟨l, h⟩ =>
      ⟨x :: l, by
        rw[List.length_cons]
        rw[h]
        ⟩

[Eric Wieser]

Oh, so this is now Lean4 rather than your previous question which was Lean 3?

[Michael Wahlberg]

yup

[Notification Bot]

Michael Wahlberg has marked this topic as resolved.

[Notification Bot]

Michael Wahlberg has marked this topic as unresolved.

[Michael Wahlberg]

Okay, I am trying to define a particular type of additive character that inherits all the properties of a general additive character. How do we implement it?

[Michael Wahlberg]

If I want this function to inherit all the properties of an additive character, how should I go on about it?

def add_char'(x : F) : ℂˣ  :=
  ζ_p^( zmod.val (algebra.trace (zmod (ring_char F)) F x)

[Michael Wahlberg]

Because it's giving me type errors when I try to define my new gauss_sum using it:-

def gauss_sum' (χ : mul_char F ℂ ) : ℂ := ∑ x : F,  -(add_char' x)* (χ x)

[Eric Wieser]

What's the error you get?

[Michael Wahlberg]

Okay my whole code is this :-

import number_theory.legendre_symbol.add_character
import number_theory.legendre_symbol.zmod_char
import algebra.char_p.char_and_card
import field_theory.finite.trace
import number_theory.cyclotomic.basic
import data.zmod.basic
noncomputable theory
open add_char
open_locale big_operators

universes u v w
variables {f : ℕ}
variables {F : Type u} [field F] [fintype F]
variables {p : ℕ} [fact p.prime] [char_p F p]
variables {ζ_p : ℂˣ} [ is_primitive_root ζ_p p ]
def add_char'(x : F) : ℂˣ  :=
  ζ_p^( zmod.val (algebra.trace (zmod (ring_char F)) F x)

def gauss_sum' (χ : mul_char F ℂ ) : ℂ := ∑ x : F,  (add_char' x)* (χ x)

[Michael Wahlberg]

and the error I got was :-
don't know how to synthesize placeholder context: F : Type u, _inst_1 : field F, _inst_2 : fintype F, χ : mul_char F ℂ, x : F ⊢ ℂˣ

[Kevin Buzzard]

Lean wants to know what complex number ζ_p is. It can't be inferred from what you've given it.

[Kevin Buzzard]

You need to either fix one or pass in a value to the def.

[Kevin Buzzard]

Right now the type of add_char' is

add_char' : Π {F : Type u} [_inst_1 : field F] [_inst_2 : fintype F] {ζ_p : ℂˣ}, F → ℂˣ

which means "the unifier will figure out zeta_p despite being given no information about it", and the unifier is indeed getting stuck.

Contrast this with the fact that the unifier has to figure out F too (becuase it's also in {} brackets) but in the use case you give x to the function so it looks at the type of x and figures out that this should be what F is.

[Michael Wahlberg]

But now it's giving me this error :-
failed to synthesize type class instance for F : Type u, _inst_1 : field F, _inst_2 : fintype F, χ : mul_char F ℂ, x : F ⊢ ℂˣ

[Kevin Buzzard]

That error means that the type class inference system (the square bracket system) can't find the complex number you have asked it to find, which is not surprising because the units of the complex numbers are not a typeclass so the typeclass inference system doesn't know anything about them.

[Kevin Buzzard]

How about we answer the mathematical question first. Do you want the user to be inputting a primitive p'th root of unity, or do you want to be using a fixed one such as $e^{2\pi i/p}$? That is the design decision which was not made in your initial code.

[Kevin Buzzard]

In your initial code you ask the unification system to find one for you, and this is not its job, and in the new variant which you didn't post, I'm guessing from the error message that you instead asked the typeclass system to find one for you, and it's not the typeclass system's job either. Your options are either to specify one yourself in code (if you want to use a fixed one) or get the user to specify one as an input (if you want it to vary).

[Michael Wahlberg]

So, right now, I am trying to prove the properties of my add_char',
But I am stuck here because I cannot rewrite this particular equality in my lemma:-

lemma add_char'_mul_property (a : F) (x : F )(p : ℕ )[fact p.prime] [char_p F p] [ fact (is_primitive_root ζ_p p) ]: add_char' ζ_p (a + x) = add_char' ζ_p a * add_char' ζ_p x := by
begin
  unfold add_char',
  simp,
  have h1 : ring_char F = p := by apply ring_char.eq,
  rw [zmod.val_add ],
  rw [h1],

and the tactic state is :-
F : Type u, _inst_1 : field F, _inst_2 : fintype F, ζ_p : ℂˣ, a x : F, p : ℕ, _inst_6 : fact (nat.prime p), _inst_7 : char_p F p, _inst_8 : fact (is_primitive_root ζ_p p), h1 : ring_char F = p ⊢ ζ_p ^ (((⇑(algebra.trace (zmod (ring_char F)) F) a).val + (⇑(algebra.trace (zmod (ring_char F)) F) x).val) % ring_char F) = ζ_p ^ (⇑(algebra.trace (zmod (ring_char F)) F) a).val * ζ_p ^ (⇑(algebra.trace (zmod (ring_char F)) F) x).val
and my error is :-

`
rewrite tactic failed, motive is not type correct
λ (_a : ℕ),
ζ_p ^
(((⇑(algebra.trace (zmod (ring_char F)) F) a).val + (⇑(algebra.trace (zmod (ring_char F)) F) x).val) %
ring_char F) =
ζ_p ^ (⇑(algebra.trace (zmod (ring_char F)) F) a).val * ζ_p ^ (⇑(algebra.trace (zmod (ring_char F)) F) x).val =
(ζ_p ^ (((⇑(algebra.trace (zmod _a) F) a).val + (⇑(algebra.trace (zmod _a) F) x).val) % _a) =
ζ_p ^ (⇑(algebra.trace (zmod _a) F) a).val * ζ_p ^ (⇑(algebra.trace (zmod _a) F) x).val)

`

[Eric Wieser]

What's the reason for using ring_char F at all here instead of p?

[Michael Wahlberg]

Eric Wieser said:

What's the reason for using ring_char F at all here instead of p?

It's inherently used in the lemma used for breaking up addition inside the trace function

[Eric Wieser]

I don't understand what you mean. Let me make my question more clear; why did you write

def add_char'(x : F) : ℂˣ  :=
  ζ_p^( zmod.val (algebra.trace (zmod (ring_char F)) F x)

instead of the simpler

def add_char'(x : F) : ℂˣ  :=
  ζ_p^( zmod.val (algebra.trace (zmod p) F x)

[Michael Wahlberg]

Eric Wieser said:

I don't understand what you mean. Let me make my question more clear; why did you write

def add_char'(x : F) : ℂˣ  :=
  ζ_p^( zmod.val (algebra.trace (zmod (ring_char F)) F x)

Then it asks me to input the value of p again in the function along with all of its instance assumptions.
It complicates my gauss sum summation and what not,
instead of the simpler

def add_char'(x : F) : ℂˣ  :=
  ζ_p^( zmod.val (algebra.trace (zmod p) F x)

[Michael Wahlberg]

Also, another problem that I am facing is that despite introducing p as a global variable with all of its instance assumptions, why do I still need to use it every time. For more information, let me show you my whole code:-

import number_theory.legendre_symbol.add_character
import number_theory.legendre_symbol.zmod_char
import algebra.char_p.char_and_card
import field_theory.finite.trace
import number_theory.cyclotomic.basic
import data.zmod.basic
import data.complex.basic
import ring_theory.roots_of_unity
noncomputable theory

open add_char
open_locale big_operators

universes u v w
-- variables (f : ℕ)
variables {F : Type u} [field F] [fintype F] (p : ℕ) [fact p.prime] [char_p F p](ζ_p : ℂˣ) [ fact (is_primitive_root ζ_p p) ]


def add_char'(x : F) : ℂˣ  :=
  ζ_p^( zmod.val (algebra.trace (zmod (ring_char F)) F x))

def gauss_sum' (χ : mul_char F ℂ ) : ℂ := ∑ x : F,  (add_char' ζ_p x)* (χ x)

instance char_p_non_zero(p : ℕ )[fact p.prime][char_p F p] : ne_zero (ring_char F) :=
{out :=  begin
  intro h,
  have h1 : ring_char F = p :=
  begin
    apply ring_char.eq ,
  end,
  rw h1 at h,
  exact nat.prime.ne_zero (fact.out p.prime) h,
end}


lemma ζ_p_pow_eq_one (n : ℤ  ) : ζ_p^(n % p) = ζ_p^n := by
begin
  rw ←  mul_inv_eq_one,
  rw ← zpow_neg ζ_p n,
  rw ← zpow_add ζ_p,
  rw  is_primitive_root.zpow_eq_one_iff_dvd (fact.out (is_primitive_root ζ_p p)) ,
  rw ← int.modeq_zero_iff_dvd,
  have h1 : 0 = n + -n := by ring,
  rw h1,
  apply int.modeq.add_right,
  apply int.mod_modeq,
end


lemma add_char'_mul_property (a : F) (x : F )(p : ℕ )[fact p.prime] [char_p F p] [ fact (is_primitive_root ζ_p p) ]: add_char' ζ_p (a + x) = add_char' ζ_p a * add_char' ζ_p x := by
begin
  unfold add_char',
  simp,
  have h1 : ring_char F = p := by apply ring_char.eq,
  rw [zmod.val_add ],

end

[Michael Stoll]

Did you look at docs#add_char.primitive_char_finite_field ?

[Michael Wahlberg]

Michael Stoll said:

Did you look at docs#add_char.primitive_char_finite_field ?

Okay this looks promising

[Eric Wieser]

Can you edit your above message with #backticks?

[Notification Bot]

This topic was moved here from #new members > Common Error Thread by Heather Macbeth.