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):


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