Some more lemmas on permutations

[hivert]

I'm offering to contribute various lemmas which can be of general interest about permutations. Maybe you'll find some of them too specialized. Those are used in https://github.com/hivert/Coq-Combi/blob/master/theories/SymGroup/cycles.v where I'm showing that any permutation has a unique (upto order) decomposition in cyclic permutation with disjoint support:

https://github.com/hivert/Coq-Combi/blob/018368517a5c96ebe4c4992892d3fed5fef3605b/theories/SymGroup/cycles.v#L624-L630

This whole development could also be contributed to mathcomp later if there is sufficiently enough interest.

[amahboubi]

Nice PR thanks! It seems it brings welcomed complements to the theory of permutations over finite types.

[amahboubi]

Indeed, this third variant was missing... thanks! If I remember correctly, @thery wrote his own in alt.v...
It seems to me though that the present proof is going into some low level (point-level) details when it shouldn't. May be is this because we should use the fact that:

Lemma Sn_perm_onT n (x : 'S_n) : perm_on setT x

I could not find it but this should be a trivial fact. I tried to prove it but my memory of the finset lib is a bit rusty and I had the following problem: I would like to write

Lemma Sn_perm_onT n (x : 'S_n) : perm_on setT x.    
Proof. by rewrite /perm_on; apply: my_subsetT. Qed.

but then I need this generalization of subsetT:

Lemma my_subsetT  (T : finType) (A : pred T) : A \subset [set: T].
Proof. by apply/subsetP=> x; rewrite inE. Qed.

Can someone tell me what idiom I should use instead?
And now we can get the following proof for card_Sn:

Lemma card_Sn n : #|'S_(n)| = n`!.
Proof.
have /eq_card -> : 'S_(n) =1 perm_on [set: 'I_n] by move=> x; rewrite Sn_perm_onT.
by rewrite card_perm cardsT card_ord. 
Qed.

[hivert]

I completely agree that one shouldn't need to go to low level. I didn't manage to avoid it. If I remember correctly, there are at least a dozen of instances of this problem in my code. Either I'm missing some shortcut in the library... I'll try to extract another instance of this problem.

[amahboubi]

Great! It would be super useful indeed to collect some examples, so as to complete the infrastructure material with the missing pieces.

[hivert]

Here is one instance:

Notation "#{ x }" :=  #|(x : {set _})|
Variable T : finType.
Implicit Types (A B X : {set T}) (P Q : {set {set T}}).

Lemma count_set_of_card (p : pred nat) P :
  count p [seq #{x} | x in P] = #|P :&: [set x | p #{x}]|.
Proof using.
rewrite cardE -size_filter /enum_mem -enumT /=.
rewrite filter_map size_map; congr size.
rewrite -filter_predI -enumT /=; apply eq_filter.
by move=> S; rewrite !inE andbC.
Qed.

[ggonthier]

This contribution addresses an important gap in the finite group library, namely the lack of support for the symmetry groups Sym(X). This is a historical accident: permutations were initially implemented to support matrix operations (mainly, determinants), then support for group automorphism Aut(X) was developed, skipping over Sym(X) as this was not required for the Odd Order proof. The study of Alt(X) was primarily intended as an application, and thus never fully integrated in the library.
This is too important a topic to be handled piecewise; I suggest we work on a comprehensive PR that fully addresses it, and is consistent with the rest of the library. This means including your results on the decomposition in cycles, as well as support for cycle notation and structure, and n-transitivity. Some work will have to go in renaming: perm_ong should really be called Sym, pcycle in perm.v should really be called porbit, for instance.

[hivert]

Dear Georges,

I'm quite happy that you consider this part of the development worthwhile being included in MathComp. Right now my main question is how to proceed further. I considered the few lemma proposed here as a requirement for the inclusion (in whatever form) of the cycle.v file.

[CohenCyril]

Hi @hivert, if I am right, @ggonthier suggests you put all of your contributions to the symmetric group in one single PR (you may amend this one), so as to review and extend it globally rather than bits by bits.

[ggonthier]

Dear Florian, @CohenCyril is right. Peaking at Coq-combi, I think we'll need a few more results (see above) in order to do the topic justice. The finite group library mostly follows Aschbacher's Finite Group Theory textbook, so I'd like to use chapter 5 as a source for results and notation.
It's clear that some notation from both perm.v and your own cycle.v will need to be changed. I must confess I didn't put enough thought into names in perm.v because I viewed perm_on, pcycle and cycles as mere stepping stones to get to Aut and odd_perm.
Reviewing the textbook, a "cycle" is a permutation (not its support), so I should have used 'Sym', 'porbit' and 'porbits'. The text uses Fix(A) and Mov(A) to describe the fixed and moved points of a set of permutations, but we could also use psupport s for the moved points of a single permutation
(support s would conflict with an ssralg definition that is used for characters). We should also avoid cyclic, which is heavily used for groups; luckily it seems the more modern term is circular, which doesn't conflict with anything.
Finally, I'd like to unify as much as possible the group isomorphism construction, and generalise the one given in automorphism.v rather than creating a new one from scratch. We can still have a variety of isomorphism lemmas; my experience is that these are more useful in practice, because it
is usually more efficient to use isogP to get a new isomorphism constant than to mess around with explicit instances of a generic construction.

[amahboubi]

Hi @hivert! We discussed your PR at the MathcompDev meeting today. How
can we help this PR progress? For instance, would an explicit todo list
help? Also, it's absolutely fine if you have no more time left to devote
to this particular PR, in which case we (the devs) could also take over
the finalization of the work entirely.

[amahboubi]

Hi @hivert ! @ybertot told us today that the two of you discussed in person, and that you agreed to let us take over this PR. Many thanks!

[hivert]

@amahboubi Sure ! Please take what you want from my code. Sorry, I forgot to reply...

[amahboubi]

No worries, once again, thanks for your contribution.

[affeldt-aist]

I tried to address in a minimal way comments about this PR.

• @amahboubi suggested a simplification of card_Sn, which requires an
  intermediate lemma, relying on a generalization of subsetT (for all
  pred instead of all set) but this generalization requires the
  addition of pred_of_set here and there in the library
• @ggonthier suggested to work on a comprehensive PR to address the
  lack of support for the symmetry group Sym(X). See his comments for
  details. In a nutshell:
  • source for results and notations: Aschbacher's Finite Group Theory Chap. 5
  • use psupport s for the moved points of a single permutation
  • use circular instead of cyclic
  • generalize the group isomorphism construction from automorphism.v

[affeldt-aist]

Regarding the suggestion by @ggonthier to work on a comprehensive PR, we would like to reproduce part of the discussion that happened here as a new issue to keep track and eventually trigger a PR.

[ybertot]

@CohenCyril, can we conclude?

[CohenCyril]

@CohenCyril, can we conclude?

Some proofs are not in the mathcomp ssreflect style, please merge first and I will quickly submit a PR to fix them.

[affeldt-aist]

I have recorded the suggestion by @ggonthier as issue #478 for the sake of visibility.

[amahboubi]

@affeldt-aist @ybertot: you have both recently contacted me offline but I would prefer to discuss here. What are you expecting from my side concerning this PR?

[affeldt-aist]

@affeldt-aist @ybertot: you have both recently contacted me offline but I would prefer to discuss here. What are you expecting from my side concerning this PR?

We did address several of your comments but not all of them.
We wanted to tell you and make sure whether you think it is reasonable.

Here are details:
You suggested a simplification of card_Sn, which requires an
intermediate lemma, relying on a generalization of subsetT (for all
preds instead of all sets) but this generalization requires the
addition of pred_of_set here and there in the library so we did not implement it.
(We addressed your other comments about documentation and renamings.)

Regarding the suggestion by @ggonthier we decided not to address it in this
PR and to record it as an issue for later:
#478
(However, we did address the comments about renamings and moved lemmas around
following new suggestions by @CohenCyril .)

[amahboubi]

@affeldt-aist thanks for clarifying. Is there a reason why not creating an issue for my unaddresed suggestion as well? In case no, I just created one using github's facility.
I do not have enough time to allocate to this right now and this should not block the release process.

[amahboubi]

Note that the link automatically created does not work properly, does anyone know how to properly point to the entire conversation?

[CohenCyril]

Note that the link automatically created does not work properly, does anyone know how to properly point to the entire conversation?

I did it. (You can click on the "..." symbol and then "copy link" to get the permalink to any comment in any thread)

[affeldt-aist]

Is there a reason why not creating an issue for my unaddresed suggestion as well?
In case no, I just created one using github's facility.

I did not create an issue right away because I was hoping that a solution might have emerged out of this discussion. At this point, recording the issue is the right thing to do imho.

[CohenCyril]

@affeldt-aist you removed my last commits

[amahboubi]

Note that the link automatically created does not work properly, does anyone know how to properly point to the entire conversation?

I did it. (You can click on the "..." symbol and then "copy link" to get the permalink to any comment in any thread)

Thanks, and thanks for the tip!