fintype (units (zmod n))

Stream: general

[Johan Commelin]

noncomputable def fintype_units : Π n, fintype (units (zmod n))
| 0     := show fintype (units ℤ), from infer_instance
| (n+1) := infer_instance

Can this be an instance? Why is this noncomputable? Both branches are computable.
Should we finally have a [is_finite X] typeclass that lives in Prop?

[Johan Commelin]

https://github.com/leanprover-community/mathlib/pull/8820/files#diff-7f686f5382f35c1cb9194c1e08521752e0518a07416ab32c400b4ad49e0372b6R39
Apparently @Mario Carneiro knows how to make this computable.

[Eric Rodriguez]

it causes some annoying diamonds, but maybe it's okay reducible. not too sure about the noncomputability

[Mario Carneiro]

It's noncomputable because being a unit is not decidable in general. Is there a clever way to enumerate the units of fin n?

[Mario Carneiro]

I suppose you can decide being a unit in a finite ring by brute force but surely we can do better than that

[Yaël Dillies]

Mario Carneiro said:

It's noncomputable because being a unit is not decidable in general. Is there a clever way to enumerate the units of fin n?

Euclid's algorithm?

[Yaël Dillies]

Once you've found one unit, you can take its powers to gain some time.

[Yaël Dillies]

(if you want to compute all of them at once)

[Mario Carneiro]

Hm, that makes sense. Does anyone want to try writing a function fin n -> option (units (fin n)) which computes the inverse and proves it is inverse?

[Mario Carneiro]

it sounds like you can get it from the extended euclidean algorithm

[Anne Baanen]

Sure! I already have xgcd in front of me :)

[Anne Baanen]

Although docs#zmod.unit_of_coprime is already computable

[Johan Commelin]

@Mario Carneiro but what about diamonds? Does such an instance-by-cases introduce a risk there?

[Mario Carneiro]

All instances on zmod n are written like this, because it is a type defined by cases

[Johan Commelin]

Hmmm, we shouldn't have an instance for just zmod n (n > 0) that does computable units, right? Because it would clash with the existing docs#units.fintype

[Anne Baanen]

instance : Π n, fintype (units (zmod n))
| 0 := show fintype (units ℤ), by apply_instance
| n@(_ + 1) := fintype.of_equiv _ units_equiv_coprime.symm

[Anne Baanen]

docs#zmod.units_equiv_coprime already existed :P

[Johan Commelin]

Shouldn't we rather make units.fintype computable?

[Johan Commelin]

Or even better, create a Prop-valued alternative?

[Johan Commelin]

I mean, I want a computable zmod n, don't get me wrong. But many arguments with finite monoids could be done with just a Prop-valued finiteness certificate.

[Johan Commelin]

So assuming fintype R all the time is overly restrictive.

[Mario Carneiro]

Johan Commelin said:

Shouldn't we rather make units.fintype computable?

Is that possible? It is not obvious to me how to compute the set of units without decidable_eq at least

[Mario Carneiro]

Also, none of this is any barrier to also adding an is_finite (units (zmod n)) or what have you

[Mario Carneiro]

You don't need to use fintypeif you don't want to

[Mario Carneiro]

Also, it isn't a non-instance because it is noncomputable; in fact I don't know why it's not an instance, the page you linked to says noncomputable instance

[Johan Commelin]

hmm, then we should make this an instance (-;
But we should use the noncomputable version. The one by @Anne Baanen causes a clash with units.fintype.

[Anne Baanen]

nooo, my computability :cry:

[Johan Commelin]

Mario Carneiro said:

Johan Commelin said:

Shouldn't we rather make units.fintype computable?

Is that possible? It is not obvious to me how to compute the set of units without decidable_eq at least

Why doesn't fintype include decidable_eq? I would guess that you would almost always want that if you care about computability, right?

[Anne Baanen]

More seriously, why don't we make a computable def version of docs#units.fintype, even keeping the instance classical if we're so inclined?

[Yakov Pechersky]

Fintype doesn't include decidable_eq because nodup on lists is definable without decidable_eq. That's because it relies on the inductive pairwise ne. I can for sure know that my list of reals [0, 1, 2] is nodup by checking the first digit. Checking that it is not nodup is what's hard.

[Yakov Pechersky]

Similarly, nothing in the quotienting by list.perm to generate a multiset requires decidable_eq, because list.perm is also inductively defined.

[Mario Carneiro]

Johan Commelin said:

hmm, then we should make this an instance (-;
But we should use the noncomputable version. The one by Anne Baanen causes a clash with units.fintype.

I don't think it does, because there is no instance of fintype (zmod n)

[Johan Commelin]

Sure, but what happens after cases n in the succ branch?

[Mario Carneiro]

I don't follow, you were talking about conflicting instances

[Mario Carneiro]

The way that this instance is proved doesn't matter, since it's not competing with anything

[Johan Commelin]

@Mario Carneiro There is an instance of fintype (zmod (n+1))

[Johan Commelin]

So then we can get competing instances for fintype (units (zmod (n+1)))

[Mario Carneiro]

ah, I was hoping there wasn't

[Johan Commelin]

It seems like a pretty useful instance to me.

[Mario Carneiro]

Is it possible to just use fin (n+1) instead?

[Mario Carneiro]

they are defeq after all

[Johan Commelin]

Lemmas about finite fields should apply to zmod p, shouldn't they?

[Mario Carneiro]

that's not of the form zmod (n+1)

[Mario Carneiro]

so it wouldn't apply anyway

[Mario Carneiro]

I'm inclined to just live with the diamond if all these instances are used

[Johan Commelin]

Well... there is [fact (0 < n)] -> fintype (zmod n)

[Johan Commelin]

and [fact p.prime] -> [fact (0 < p)]

[Mario Carneiro]

oof, what are all these fact instances

[Johan Commelin]

Well, we want [fact p.prime] -> field (zmod p). Don't we?

[Johan Commelin]

So that's the origin of all the facts.

[Mario Carneiro]

As long as there aren't any fact instances, it should be okay to have instances with fact hypotheses since they won't be satisfied

[Johan Commelin]

@Mario Carneiro I'm afraid there's also a fact (0 < (n+1)) instance. It's quite a useful one, in fact.
It's one of the 2 or 3 global fact instances.

[Mario Carneiro]

Mario Carneiro said:

I'm inclined to just live with the diamond if all these instances are used

[Yakov Pechersky]

Fintype instances are subsingleton

[Eric Wieser]

#6266 adds the titular instance

[Kevin Buzzard]

Oh nice find Eric! Yeah it conflicts with instance [Monoid α] [Fintype α] [DecidableEq α] : Fintype αˣ := ... when Lean somehow knows that n>0 e.g. if n is prime and this is Facted.

[Kevin Buzzard]

I'd like to say that if we just moved to finite types then none of this would be an issue, but my attempts to wipe out constructivism in mathlib completely have failed when it comes to finset and fintype.

[Eric Wieser]

Can you add an example to your PR that replicates the failure, something like:

example : your_inst = old_inst := by
   success_if_fail rfl -- unavoidable diamond
   exact Subsingleton.elim _ _

[Eric Wieser]

(edit: done)

[Kevin Buzzard]

Thanks! I tried and failed :-)

[Jireh Loreaux]

@Kevin Buzzard why do we want Fintype here as opposed to Finite (ZMod q)ˣ?

[Kevin Buzzard]

Because the student who wanted this instance wanted to use a lemma which asked for Fintype. Now I've understood that this PR introduces a diamond I am definitely open to the idea of changing the PR so that it uses Finite instead.

[Jireh Loreaux]

Did the statement the student is working on need a fintype instance? If not, and instead they only want to apply a lemma that needs a fintype hypothesis, they can use a Finite instance to conjure a Fintype instance within the proof.

[Jireh Loreaux]

But probably you already knew that.

[Kevin Buzzard]

Yeah I'm sure you're right. Right now I'm still kind of torn between whether they should be working with ZMod n with n :PNat or [NeZero n] or just plain nats. Some of these suggestions make the fintype issue go away