order_of_refactor

Stream: general

[Julian Külshammer]

In #6587 I am trying to refactor the definition of order_of to make sense of infinite groups. The main file is compiling, but there are two issues that I'm unable to fix.

1) In the file group_theory.perm.cycles the proof breakes because somehow lean doesn't understand that order_of makes sense. It somehow doesn't recognise that perm \alpha being a fintype implies that order_of is well-defined. It gets a bit better if I add haveI := fintype_perm in that the second order_of now makes sense, but the first still doesn't. Any idea why that is?

2) The decidability-classical linter reports two problems in the order_of file, the first is in is_cyclic_of_order_of_eq_card, the second one is in is_cyclic.card_order_of_eq_totient. It reports that I should replace decidable_eq \alpha by classical in the proof. However, if I try that, the refl in the end don't seem to work although at least in the infoview the terms look the same.

Does someone have an idea what is going on in either of these?

[Kevin Buzzard]

You can always try congr' if refl is causing you trouble. This is the problem we see a lot when people try reasoning about finite types. The two ways to fix it are to either become an expert in constructive finiteness or switch to existential finiteness like I do in the fincard branch

[Kevin Buzzard]

Basically I would argue that someone like you would be better off with the hypothesis nonempty (fintype alpha) but then the problem is that some of the theorems you'll need are not proved in this generality, computable versions are proved instead so you have to port everything to a non-computable setting. I think elements of infinite order should have order 0 and one shouldn't even ask for any finiteness hypotheses. Then you prove the theorem saying that g^n=1 iff n is a multiple of the order.

[Kevin Buzzard]

This non-computable finiteness is something else which is long overdue, like ideals in noncommutative rings

[Mario Carneiro]

The definition of order_of has two decidability assumptions [Π a : α, decidable_pred (λ n, 0 < n ∧ a ^ n = 1)] [Π a : α, decidable (∃ n, 0 < n ∧ a ^ n = 1)] that should be axed

[Mario Carneiro]

If you want this to be computable, you should instead have a typeclass has_order_of so that you can supply an implementation and prove it equivalent to the real order_of

[Mario Carneiro]

it's very unrealistic to assume that [Π a : α, decidable (∃ n, 0 < n ∧ a ^ n = 1)] is directly decidable on concrete computable groups

[Julian Külshammer]

So, I understand correctly that I should make the definition noncomputable and remove the two assumptions and then it could be a second step to supply an implementation later?

[Mario Carneiro]

yeah, if you don't care to have a computable order_of now then just remove those assumptions and use by classical; exact local to the definition of order_of

[Mario Carneiro]

I don't think you should expose a theorem that talks about nat.find directly as in order_of_of_finite_order; instead expose the definitional axioms of nat.find rewritten for use with order_of

[Julian Külshammer]

I don't care about it being computable now, but @Johan Commelin remarked in the PR process that it would be nice to be able to use dec_trivial to compute orders of elements in finite groups of order less than 10 in the future. As far as I can see, this is not used in mathlib so far.

[Mario Carneiro]

I think it's worth specifically investigating this in its own PR, because the naive implementation is not at all practical

[Mario Carneiro]

In particular, decidable (∃ n, 0 < n ∧ a ^ n = 1) has no instance even in the case where A is a decidable fintype

[Mario Carneiro]

because it contains an unbounded existential nat quantifier

[Julian Külshammer]

Thanks for the advice. I'll go classical then for now.

[Kevin Buzzard]

There are two things pulling in different directions here. One is theoretical mathematicians like Julian and @Peter Nelson coming along and saying "we are finding fintype and finsetdifficult to use in practice", which can I believe be solved with this finsum approach, and then there's the other extreme where we'd like to be able to show off to the undergraduates by computing the order of some explicit element of S3 using dec_trivial. These are incompatible in some sense -- and I don't think we should be telling newcomer mathematicians that they need to learn all the arcane tricks in order to prove theorems about the order of an element of a finite group. But the dec_trivial proof is not the correct one, we all know that Lean will hang on the dihedral group D37 anyway with this approach. Telling students we can compute the order of elements in S3 but not S8 is not a good look when software like GAP is out there.

[Johan Commelin]

@Julian Külshammer Just to be clear: I don't consider the dec_trivial thing very important. So let's go classical.

[Johan Commelin]

But we'll need a way to easily show that -1 : units int has order 2

[Eric Wieser]

Mario, doesn't the linked PR provide such an instance?

[Julian Külshammer]

@Johan Commelin I'll keep that in mind and try to add an example or lemma about that.

[Mario Carneiro]

It does, but only in the trivial case where it is always true, in which case it may as well be a fact instead of a decidable assumption

[Mario Carneiro]

but really, a statement with this much quantifier complexity should be packed behind a definition if you actually want typeclass inference to work on it

[Julian Külshammer]

@Kevin Buzzard I don't think it was a particular issue with fintype in this case though. It was possible to make it work with some decidability assumption like: If it is possible to decide if the order of this element is finite, then you can use a computable definition. However, as Eric pointed out, there is then a problem with rewrites not working nicely, e.g. lean couldn't figure out that if a has finite order and a=1, then order of 1 makes sense and got stuck. Then I switched to the all-or-nothing approach according to Eric's advice: In practice, probably it is reasonable to ask that finite order is decidable for every element of a group (e.g. finite groups or free groups) rather than just a specific one. But this was also difficult to use (because of too many quantifiers according to Mario). So, now everything is noncomputable and works fine. Lean now reports that there are some unused arguments in dihedral: Since the dihedral group associated to 0 is defined to be the infinite dihedral group, the order of the elements can be given uniformly without assuming finite dihedral group, i.e. n>0.

[Julian Külshammer]

I wasn't able to fix problem 2 though, refl still doesn't work and I wasn't able to make congr' work either. If anyone has an advice there, let me know.

[Eric Wieser]

(deleted)

[Kevin Buzzard]

@Julian Külshammer yes this exactly the problem with fintype -- rewrites don't work nicely (experts can often work around individual problems). This is what the noncomputable approach solves in a far simpler way, by removing the issue completely.