Defining instances using several implicit arguments

Stream: new members

[Jakob Scholbach]

Another newbie syntax question: why does this not work (the definition of the class does work, but the instance does not, it says failed to synthesize type class instance for.... If I omit the parts [q : ℕ] [char_p F q] (both in the class and the instance), it does work.

import data.polynomial.basic
import algebra.char_p
import field_theory.separable

class my_has_separable_contraction (F : Type) [field F] [q : ℕ] [char_p F q]
  (f : polynomial F) : Prop :=
  (has_separable_contraction' [] : ∃ m : ℕ, ∃ g : polynomial F,
  g.separable ∧ polynomial.expand F (3^m) g = f)

instance my_irreducible_has_separable_contraction
  (F : Type) [field F] [q : ℕ] [char_p F q]
  (f : polynomial F) (irred : irreducible f) (fn : f ≠ 0):
  my_has_separable_contraction F f :=
begin
  sorry
end

[Adam Topaz]

What are your imports?

[Adam Topaz]

Oh, you need to use (q : \nat)

[Adam Topaz]

But I can't know for sure without a #mwe

[Jakob Scholbach]

yes, sorry, I forgot to include the imports.

[Adam Topaz]

import data.polynomial.basic
import algebra.char_p
import field_theory.separable

class my_has_separable_contraction (F : Type) [field F] (q : ℕ) [char_p F q]
  (f : polynomial F) : Prop :=
  (has_separable_contraction' [] : ∃ m : ℕ, ∃ g : polynomial F,
  g.separable ∧ polynomial.expand F (3^m) g = f)

instance my_irreducible_has_separable_contraction
  (F : Type) [field F] (q : ℕ) [char_p F q]
  (f : polynomial F) (irred : irreducible f) (fn : f ≠ 0):
  my_has_separable_contraction F q f :=
begin
  sorry
end

[Adam Topaz]

[ .. ] is only used for classes.

[Jakob Scholbach]

OK -- is it possible to leave the q implicit by other means?

[Adam Topaz]

yeah, one sec.

[Alex J. Best]

Use {} instead

[Jakob Scholbach]

{ q : \N } ?

[Adam Topaz]

but he wants the field to have characteristic q

[Adam Topaz]

I would do this:

import data.polynomial.basic
import algebra.char_p
import field_theory.separable

class my_has_separable_contraction (F : Type) [field F] (f : polynomial F) : Prop :=
  (has_separable_contraction' [] : ∀ (q : ℕ) [char_p F q], ∃ m : ℕ, ∃ g : polynomial F,
  g.separable ∧ polynomial.expand F (3^m) g = f)

instance my_irreducible_has_separable_contraction
  (F : Type) [field F] (f : polynomial F) (irred : irreducible f) (fn : f ≠ 0):
  my_has_separable_contraction F  f :=
begin
  sorry
end

[Jakob Scholbach]

OK, what is the general rule? If I use { q ... } I cannot refer to it in any later [...] ?

import data.polynomial.basic
import algebra.char_p
import field_theory.separable

class my_has_separable_contraction (F : Type) [field F] {q : ℕ} [char_p F q]
  (f : polynomial F) : Prop :=
  (has_separable_contraction' [] : ∃ m : ℕ, ∃ g : polynomial F,
  g.separable ∧ polynomial.expand F (3^m) g = f)

instance my_irreducible_has_separable_contraction
  (F : Type) [field F] {q : ℕ} [char_p F q]
  (f : polynomial F) (irred : irreducible f) (fn : f ≠ 0):
  my_has_separable_contraction F f :=
begin
  sorry
end

does not work, with the same error message.

[Adam Topaz]

What's the name of the function which returns the characteristic of a ring?

[Jakob Scholbach]

char_ring

[Jakob Scholbach]

I believe

[Adam Topaz]

Wait, q doesn't appear at all after the : in your class, right?

[Adam Topaz]

Why do you need it at all?

[Jakob Scholbach]

Oh, for the purpose of testing I replaced q^m by 3^m. Sorry about this glitch in posting it, but I do need it in the definition of the class.

[Adam Topaz]

Oh I see.

[Adam Topaz]

So you could do something like this:

import data.polynomial.basic
import algebra.char_p
import field_theory.separable

class my_has_separable_contraction (F : Type) [field F] (f : polynomial F) : Prop :=
  (has_separable_contraction' [] : ∃ m : ℕ, ∃ g : polynomial F,
  g.separable ∧ polynomial.expand F ((ring_char F)^m) g = f)

instance my_irreducible_has_separable_contraction
  (F : Type) [field F] (f : polynomial F) (irred : irreducible f) (fn : f ≠ 0):
  my_has_separable_contraction F f :=
begin
  sorry
end

[Adam Topaz]

Note this works;

example {F : Type*} [field F] : char_p F (ring_char F) := by apply_instance

[Adam Topaz]

Which means that the typeclass system will automatically know that F has characteristic ring_char F (as it should be!)

[Jakob Scholbach]

OK, I see, thanks. This works in this special case; for the purpose of having a mwe, I also simplified the code in another respect. I have defined a class exp_char F p (which otherwise is identical to char_p, but it is about the exponential characteristic). I guess I could also adapt the definition of ring_char to this situation and produce a function like ring_exp_char. This would allow me to use your solution. But is there no other general smooth way of invoking [some_class some_structure some_natural_number] without this detour (or the detour with the forall q : that you also kindly suggested)?

[Adam Topaz]

The other option is to make q explicit, meaning that your class says "This is a polynomial which is a contraction of a separable polynomial, but you are only allowed to use it for fields of characteristic $q$".

[Adam Topaz]

I.e. the class itself will depend on $q$.

[Jakob Scholbach]

Yes, but it feels (to me newbie!) somehow unnatural: I leave the existence & assumption (concerning the characteristic) on the field implicit, but need to explicitly feed in the natural number.

[Adam Topaz]

Well, it's a theorem that a field has a unique characteristic :)

[Jakob Scholbach]

Yes, sure, I won't argue with you on that! :) , and of course all your solutions do work. Just to understand it also in general, let me ask one last time: is it not possible to have implicit assumptions involving an implicitly present natural number?

[Adam Topaz]

Oh, it's certainly possible in cases where lean can infer what that natural number must be from context.

[Adam Topaz]

The issue is that lean had no way of inferring what $q$ was supposed to be in my_has_separable_contraction, just because you declare [char_p F q as an assumption for my_irreducible_has_separable_contraction. That's the point I was trying to make above -- you can perfectly legally write
{F : Type} [field F] [char_p F 5] [char_p F 3]

[Adam Topaz]

How would lean know whether the characteristic of $F$ is $3$ or $5$?

[Adam Topaz]

(of course you can prove false with these assumptions, but that's another point altogether.)

[Jakob Scholbach]

OK, I understand your point. In some sense I would like to put [q : \N] both in the class, and also in the instance (prior to the char_p, so that this clause does know about the q). If I understand you correctly, the (only?) thing that makes this fail is the fact that a number is not a structure, so I guess I would like to find a syntax that overcome this hurdle.

[Adam Topaz]

Not quite. It's the fact that a number is not a typeclass. Typeclasses are things like field, ring, etc.

[Adam Topaz]

You can very well have a class that's a plain proposition (just like the one you made).

[Jakob Scholbach]

OK, yes. So: can I turn a number into a typeclass (and otherwise keep its nature as is)?

[Adam Topaz]

And you can make a class that is just a number, like this:

class foo :=
(n : ℕ)

example [foo] : ℕ := foo.n

[Adam Topaz]

This is a bit silly, but you can do this:

import algebra.char_p

class foo := (n : ℕ)

class bar (F : Type*) [field F] [foo] extends char_p F foo.n

example {F : Type*} [field F] [foo] [bar F] : char_p F foo.n := by apply_instance

[Jakob Scholbach]

OK, I see. Thank you very much for your advice -- I appreciate it! Just to record it for later readers: this solution would read like so:

import data.polynomial.basic
import algebra.char_p
import field_theory.separable

class foo :=
(n : ℕ)

class my_has_separable_contraction (F : Type) [field F] [foo] [char_p F foo.n]
  (f : polynomial F) : Prop :=
  (has_separable_contraction' [] : ∃ m : ℕ, ∃ g : polynomial F,
  g.separable ∧ polynomial.expand F (foo.n^m) g = f)

instance my_irreducible_has_separable_contraction
  (F : Type) [field F] [foo] [char_p F foo.n]
  (f : polynomial F) (irred : irreducible f) (fn : f ≠ 0):
  my_has_separable_contraction F f :=
begin
  sorry
end

[Adam Topaz]

Maybe it's worth mentioning that such a hack should not be done in practice.