# Zulip Chat Archive

## Stream: general

### Topic: optional proofs for type class inference

#### Chris Hughes (Oct 13 2019 at 14:03):

At the moment we have two types for integers mod n `zmod`

and `zmodp`

depending on whether `n`

is `prime`

or not, so that the field instance can be synthesized. This means that a lot of proofs are duplicated. I think there are other places where this sort of problem could come up.

Here's an idea I came up with that might make this nicer

mport data.nat.prime inductive option' (α : Sort*) : Sort* | none {} : option' | some : α → option' def zmod (n : ℕ) (h : option' n.prime := option'.none) : Type := fin n

This way proofs that apply whether or not `n`

is prime can be stated in full generality in one statement, and the field instances can be put on the type `zmod n (some _)`

What do people think of this strategy?

#### Johan Commelin (Oct 13 2019 at 16:47):

Alternatively, we make a `coe`

from `nat.primes`

to `pnat`

. And we ditch `zmodp`

. Then just use `zmod`

.

#### Reid Barton (Oct 13 2019 at 16:57):

Then the idea is to put the instance on `zmod ((coe : primes -> pnat) p)`

?

#### Reid Barton (Oct 13 2019 at 16:57):

the field instance I mean

#### Johan Commelin (Oct 13 2019 at 16:59):

Exactly

#### Johan Commelin (Oct 13 2019 at 17:01):

Parts of the library are currently using `[nat.prime p]`

. But then, we can't write `instance : nat.prime (ring_char k)`

for finite fields `k`

. Because `nat.prime`

is not actually a class. There's still a bunch of things that have to be sorted out here.

#### Johan Commelin (Oct 13 2019 at 17:04):

Otoh, maybe `ring_char`

is actually bad. If you have 3 or more fields, it might be more practical to show that they all have `char_p _ p`

then showing that they all pairwise have the same `ring_char`

.

#### Chris Hughes (Oct 13 2019 at 17:18):

This seems sensible to me. Because you almost always have the assumption `p.prime`

as an assumption to the theorem, it shouldn't be as annoying as `pnat`

, because you never start with a natural number and then prove it's prime like you do with positivity. I think perhaps refactors like this should wait until Lean 4 when we know exactly what type class inference will be like

Last updated: Dec 20 2023 at 11:08 UTC