From 5d7bd2ea2a0a28fb275da8ba2e2c0dc5a33d1034 Mon Sep 17 00:00:00 2001 From: Georges Gonthier Date: Wed, 8 May 2019 09:43:34 +0200 Subject: refactor `seq` permutation theory - Change the naming of permutation lemmas so they conform to a consistent policy: `perm_eq` lemmas have a `perm_` (_not_ `perm_eq`) prefix, or sometimes a `_perm` suffix for lemmas that _prove_ `perm_eq` using a property when there is also a lemma _using_ `perm_eq` for the same property. Lemmas that do not concern `perm_eq` do _not_ have `perm` in their name. - Change the definition of `permutations` for a time- and space- back-to-front generation algorithm. - Add frequency tally operations `tally`, `incr_tally`, `wf_tally` and `tally_seq`, used by the improved `permutation` algorithm. - add deprecated aliases for renamed lemmas --- mathcomp/fingroup/gproduct.v | 14 +++++++------- mathcomp/fingroup/perm.v | 17 +++++++++-------- 2 files changed, 16 insertions(+), 15 deletions(-) (limited to 'mathcomp/fingroup') diff --git a/mathcomp/fingroup/gproduct.v b/mathcomp/fingroup/gproduct.v index 676daf0..853ffb6 100644 --- a/mathcomp/fingroup/gproduct.v +++ b/mathcomp/fingroup/gproduct.v @@ -614,19 +614,19 @@ Lemma perm_bigcprod (I : eqType) r1 r2 (A : I -> {set gT}) G x : \prod_(i <- r1) x i = \prod_(i <- r2) x i. Proof. elim: r1 r2 G => [|i r1 IHr] r2 G defG Ax eq_r12. - by rewrite perm_eq_sym in eq_r12; rewrite (perm_eq_small _ eq_r12) ?big_nil. -have /rot_to[n r3 Dr2]: i \in r2 by rewrite -(perm_eq_mem eq_r12) mem_head. + by rewrite perm_sym in eq_r12; rewrite (perm_small_eq _ eq_r12) ?big_nil. +have /rot_to[n r3 Dr2]: i \in r2 by rewrite -(perm_mem eq_r12) mem_head. transitivity (\prod_(j <- rot n r2) x j). rewrite Dr2 !big_cons in defG Ax *; have [[_ G1 _ defG1] _ _] := cprodP defG. rewrite (IHr r3 G1) //; first by case/allP/andP: Ax => _ /allP. - by rewrite -(perm_cons i) -Dr2 perm_eq_sym perm_rot perm_eq_sym. + by rewrite -(perm_cons i) -Dr2 perm_sym perm_rot perm_sym. rewrite -{-2}(cat_take_drop n r2) in eq_r12 *. -rewrite (eq_big_perm _ eq_r12) !big_cat /= !(big_nth i) !big_mkord in defG *. +rewrite (perm_big _ eq_r12) !big_cat /= !(big_nth i) !big_mkord in defG *. have /cprodP[[G1 G2 defG1 defG2] _ /centsP-> //] := defG. rewrite defG2 -(bigcprodW defG2) mem_prodg // => k _; apply: Ax. - by rewrite (perm_eq_mem eq_r12) mem_cat orbC mem_nth. + by rewrite (perm_mem eq_r12) mem_cat orbC mem_nth. rewrite defG1 -(bigcprodW defG1) mem_prodg // => k _; apply: Ax. -by rewrite (perm_eq_mem eq_r12) mem_cat mem_nth. +by rewrite (perm_mem eq_r12) mem_cat mem_nth. Qed. Lemma reindex_bigcprod (I J : finType) (h : J -> I) P (A : I -> {set gT}) G x : @@ -637,7 +637,7 @@ Proof. case=> h1 hK h1K; rewrite -!(big_filter _ P) filter_index_enum => defG Ax. rewrite -(big_map h P x) -(big_filter _ P) filter_map filter_index_enum. apply: perm_bigcprod defG _ _ => [i|]; first by rewrite mem_enum => /Ax. -apply: uniq_perm_eq (enum_uniq P) _ _ => [|i]. +apply: uniq_perm (enum_uniq P) _ _ => [|i]. by apply/dinjectiveP; apply: (can_in_inj hK). rewrite mem_enum; apply/idP/imageP=> [Pi | [j Phj ->//]]. by exists (h1 i); rewrite ?inE h1K. diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v index 33bf82c..b610c36 100644 --- a/mathcomp/fingroup/perm.v +++ b/mathcomp/fingroup/perm.v @@ -294,22 +294,22 @@ Proof. by apply/permP => z; rewrite -(permKV s z) permJ; apply/inj_tperm/perm_inj. Qed. -Lemma tuple_perm_eqP {T : eqType} {n} {s : seq T} {t : n.-tuple T} : +Lemma tuple_permP {T : eqType} {n} {s : seq T} {t : n.-tuple T} : reflect (exists p : 'S_n, s = [tuple tnth t (p i) | i < n]) (perm_eq s t). Proof. apply: (iffP idP) => [|[p ->]]; last first. rewrite /= (map_comp (tnth t)) -{1}(map_tnth_enum t) perm_map //. - apply: uniq_perm_eq => [||i]; rewrite ?enum_uniq //. + apply: uniq_perm => [||i]; rewrite ?enum_uniq //. by apply/injectiveP; apply: perm_inj. by rewrite mem_enum -[i](permKV p) image_f. case: n => [|n] in t *; last have x0 := tnth t ord0. - rewrite tuple0 => /perm_eq_small-> //. + rewrite tuple0 => /perm_small_eq-> //. by exists 1; rewrite [mktuple _]tuple0. -case/(perm_eq_iotaP x0); rewrite size_tuple => Is eqIst ->{s}. -have uniqIs: uniq Is by rewrite (perm_eq_uniq eqIst) iota_uniq. -have szIs: size Is == n.+1 by rewrite (perm_eq_size eqIst) !size_tuple. +case/(perm_iotaP x0); rewrite size_tuple => Is eqIst ->{s}. +have uniqIs: uniq Is by rewrite (perm_uniq eqIst) iota_uniq. +have szIs: size Is == n.+1 by rewrite (perm_size eqIst) !size_tuple. have pP i : tnth (Tuple szIs) i < n.+1. - by rewrite -[_ < _](mem_iota 0) -(perm_eq_mem eqIst) mem_tnth. + by rewrite -[_ < _](mem_iota 0) -(perm_mem eqIst) mem_tnth. have inj_p: injective (fun i => Ordinal (pP i)). by apply/injectiveP/(@map_uniq _ _ val); rewrite -map_comp map_tnth_enum. exists (perm inj_p); rewrite -[Is]/(tval (Tuple szIs)); congr (tval _). @@ -577,5 +577,6 @@ End LiftPerm. Prenex Implicits lift_perm lift_permK. - +Notation tuple_perm_eqP := + (deprecate tuple_perm_eqP tuple_permP) (only parsing). -- cgit v1.2.3