Zulip Chat Archive

Stream: general

Topic: optional proofs for type class inference


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Reid Barton (Oct 13 2019 at 16:57):

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

view this post on Zulip Reid Barton (Oct 13 2019 at 16:57):

the field instance I mean

view this post on Zulip Johan Commelin (Oct 13 2019 at 16:59):

Exactly

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: May 08 2021 at 19:11 UTC