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/perm.v | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) (limited to 'mathcomp/fingroup/perm.v') 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