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/algebra/ssrnum.v | 3 +-- mathcomp/algebra/vector.v | 6 +++--- 2 files changed, 4 insertions(+), 5 deletions(-) (limited to 'mathcomp/algebra') diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 97afdfb..12fcecb 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -4384,8 +4384,7 @@ have sz_p: size p = n.+1. pose r := sort argCle r0; have r_arg: sorted argCle r by apply: sort_sorted. have{Dp} Dp: p = \prod_(z <- r) ('X - z%:P). rewrite Dp lead_coefE sz_p coefB coefXn coefC -mulrb -mulrnA mulnb lt0n andNb. - rewrite subr0 eqxx scale1r; apply: eq_big_perm. - by rewrite perm_eq_sym perm_sort. + by rewrite subr0 eqxx scale1r; apply/esym/perm_big; rewrite perm_sort. have mem_rP z: (n > 0)%N -> reflect (z ^+ n = x) (z \in r). move=> n_gt0; rewrite -root_prod_XsubC -Dp rootE !hornerE hornerXn n_gt0. by rewrite subr_eq0; apply: eqP. diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v index e73ca33..87ca0f4 100644 --- a/mathcomp/algebra/vector.v +++ b/mathcomp/algebra/vector.v @@ -1004,7 +1004,7 @@ Proof. by rewrite /free span_seq1 dim_vline; case: (~~ _). Qed. Lemma perm_free X Y : perm_eq X Y -> free X = free Y. Proof. -by move=> eqX; rewrite /free (perm_eq_size eqX) (eq_span (perm_eq_mem eqX)). +by move=> eqXY; rewrite /free (perm_size eqXY) (eq_span (perm_mem eqXY)). Qed. Lemma free_directv X : free X = (0 \notin X) && directv (\sum_(v <- X) <[v]>). @@ -1061,7 +1061,7 @@ Proof. by rewrite cat_free => /and3P[]. Qed. Lemma filter_free p X : free X -> free (filter p X). Proof. -rewrite -(perm_free (etrans (perm_filterC p X _) (perm_eq_refl X))). +rewrite -(perm_free (etrans (perm_filterC p X _) (perm_refl X))). exact: catl_free. Qed. @@ -1170,7 +1170,7 @@ Qed. Lemma perm_basis X Y U : perm_eq X Y -> basis_of U X = basis_of U Y. Proof. move=> eqXY; congr ((_ == _) && _); last exact: perm_free. -by apply/eq_span; apply: perm_eq_mem. +by apply/eq_span; apply: perm_mem. Qed. Lemma vbasisP U : basis_of U (vbasis U). -- cgit v1.2.3