Zulip Chat Archive

Stream: general

Topic: fintype (units (zmod n))


Johan Commelin (Sep 10 2021 at 12:12):

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 (Sep 10 2021 at 12:15):

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

Eric Rodriguez (Sep 10 2021 at 12:17):

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

Mario Carneiro (Sep 10 2021 at 12:17):

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 (Sep 10 2021 at 12:18):

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 (Sep 10 2021 at 12:19):

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 (Sep 10 2021 at 12:19):

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

Yaël Dillies (Sep 10 2021 at 12:20):

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

Mario Carneiro (Sep 10 2021 at 12:21):

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 (Sep 10 2021 at 12:22):

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

Anne Baanen (Sep 10 2021 at 12:22):

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

Anne Baanen (Sep 10 2021 at 12:25):

Although docs#zmod.unit_of_coprime is already computable

Johan Commelin (Sep 10 2021 at 12:25):

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

Mario Carneiro (Sep 10 2021 at 12:25):

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

Johan Commelin (Sep 10 2021 at 12:26):

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 (Sep 10 2021 at 12:29):

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

Anne Baanen (Sep 10 2021 at 12:29):

docs#zmod.units_equiv_coprime already existed :P

Johan Commelin (Sep 10 2021 at 12:29):

Shouldn't we rather make units.fintype computable?

Johan Commelin (Sep 10 2021 at 12:30):

Or even better, create a Prop-valued alternative?

Johan Commelin (Sep 10 2021 at 12:31):

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 (Sep 10 2021 at 12:31):

So assuming fintype R all the time is overly restrictive.

Mario Carneiro (Sep 10 2021 at 12:32):

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 (Sep 10 2021 at 12:33):

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

Mario Carneiro (Sep 10 2021 at 12:33):

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

Mario Carneiro (Sep 10 2021 at 12:35):

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 (Sep 10 2021 at 12:41):

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 (Sep 10 2021 at 12:42):

nooo, my computability :cry:

Johan Commelin (Sep 10 2021 at 12:42):

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 (Sep 10 2021 at 12:43):

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 (Sep 10 2021 at 12:46):

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 (Sep 10 2021 at 12:47):

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

Mario Carneiro (Sep 10 2021 at 14:47):

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 (Sep 10 2021 at 15:08):

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

Mario Carneiro (Sep 10 2021 at 15:42):

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

Mario Carneiro (Sep 10 2021 at 15:43):

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

Johan Commelin (Sep 10 2021 at 17:01):

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

Johan Commelin (Sep 10 2021 at 17:02):

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

Mario Carneiro (Sep 10 2021 at 17:02):

ah, I was hoping there wasn't

Johan Commelin (Sep 10 2021 at 17:02):

It seems like a pretty useful instance to me.

Mario Carneiro (Sep 10 2021 at 17:02):

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

Mario Carneiro (Sep 10 2021 at 17:02):

they are defeq after all

Johan Commelin (Sep 10 2021 at 17:03):

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

Mario Carneiro (Sep 10 2021 at 17:03):

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

Mario Carneiro (Sep 10 2021 at 17:03):

so it wouldn't apply anyway

Mario Carneiro (Sep 10 2021 at 17:04):

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

Johan Commelin (Sep 10 2021 at 17:04):

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

Johan Commelin (Sep 10 2021 at 17:04):

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

Mario Carneiro (Sep 10 2021 at 17:04):

oof, what are all these fact instances

Johan Commelin (Sep 10 2021 at 17:06):

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

Johan Commelin (Sep 10 2021 at 17:07):

So that's the origin of all the facts.

Mario Carneiro (Sep 10 2021 at 17:08):

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 (Sep 10 2021 at 17:30):

@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 (Sep 10 2021 at 17:30):

Mario Carneiro said:

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

Yakov Pechersky (Sep 10 2021 at 23:02):

Fintype instances are subsingleton

Eric Wieser (Jul 31 2023 at 14:45):

#6266 adds the titular instance

Kevin Buzzard (Jul 31 2023 at 14:56):

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 (Jul 31 2023 at 14:57):

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 (Jul 31 2023 at 15:45):

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 (Jul 31 2023 at 17:56):

(edit: done)

Kevin Buzzard (Jul 31 2023 at 22:00):

Thanks! I tried and failed :-)

Jireh Loreaux (Aug 01 2023 at 21:31):

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

Kevin Buzzard (Aug 01 2023 at 21:59):

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 (Aug 01 2023 at 22:20):

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 (Aug 01 2023 at 22:21):

But probably you already knew that.

Kevin Buzzard (Aug 01 2023 at 22:32):

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


Last updated: Dec 20 2023 at 11:08 UTC