optional proofs for type class inference

Stream: general

[Chris Hughes]

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]

Alternatively, we make a coe from nat.primes to pnat. And we ditch zmodp. Then just use zmod.

[Reid Barton]

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

[Reid Barton]

the field instance I mean

[Johan Commelin]

Exactly

[Johan Commelin]

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]

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]

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