small generalizations and extensions in poly #202

CohenCyril · 2018-07-04T14:29:48Z

No description provided.

thery

quick review

thery · 2018-07-11T13:20:57Z

mathcomp/algebra/ssralg.v

@@ -1171,6 +1171,9 @@ Proof. by rewrite exprAC sqrrN !expr1n. Qed.
 Lemma signrMK n : @involutive R ( *%R ((-1) ^+ n)).
 Proof. by move=> x; rewrite mulrA -expr2 sqrr_sign mul1r. Qed.

+Lemma lastr_eq0 (s : seq R) x : x != 0 -> (last x s == 0) = (last 1 s == 0).
+Proof. by elim: s => [|y s ihs] /negPf // ->; rewrite oner_eq0. Qed.


case: s is sufficient

thery · 2018-07-11T13:22:11Z

mathcomp/algebra/ssralg.v

@@ -1171,6 +1171,9 @@ Proof. by rewrite exprAC sqrrN !expr1n. Qed.
 Lemma signrMK n : @involutive R ( *%R ((-1) ^+ n)).
 Proof. by move=> x; rewrite mulrA -expr2 sqrr_sign mul1r. Qed.

+Lemma lastr_eq0 (s : seq R) x : x != 0 -> (last x s == 0) = (last 1 s == 0).


Maybe this statement could be generalized to
Lemma lastr_eq (s : seq R) (x y z : R) : x != z -> y != z -> (last x s == z) = (last y s == z).

I am not sure it is desirable, as 1 is canonical for a R : ringType... However, maybe the theorem you mention has its place in seq.v

I added your last_eq to seq (for an eqType)

thery · 2018-07-11T13:27:38Z

mathcomp/algebra/poly.v

+  (p \Po q)`_n = \sum_(i < size p) p`_i * (q ^+ i)`_n.
+Proof.
+rewrite comp_polyE coef_sum.
+by elim/big_ind2: _ => [//|? ? ? ? -> -> //|i]; rewrite coefZ.


why using induction?
by apply: eq_bigr => i _; rewrite coefZ.

thery · 2018-07-11T14:19:16Z

mathcomp/algebra/poly.v

+by rewrite cardT /= size_enum_ord [in RHS]big_tnth.
+Qed.
+
+Lemma size_prod_eq1 (I : finType) (P : pred I) (F : I -> {poly R}) :


It seems reasonable to also add the mul version
Lemma size_mul_eq1 p q :
(size (p * q) == 1%N) = ((size p == 1%N) && (size q == 1%N)).

thery · 2018-07-11T14:20:10Z

mathcomp/algebra/poly.v

+by rewrite cardT /= size_enum_ord [in RHS]big_tnth.
+Qed.
+
+Lemma size_prod_eq1 (I : finType) (P : pred I) (F : I -> {poly R}) :


Why restrict this to finType and not prove the general statement

Lemma size_prod_eq1
(I : eqType) (s : seq I) (P : pred I) (F : I -> {poly R}) :
(size (\prod_(i <- s | P i) F i) == 1%N) =
(all (fun i => size (F i) == 1%N) [seq x <- s | P x]).

The proof for finType is way easier and not really restrictive (see the proof of size_prod_seq_eq1) and the phrasing in terms of [forall (i | P i) ...] is slightly more elegant. I'm quite convinced we want to keep size_prod_eq1 as such, but I am less sure about size_prod_seq_eq1

Could we have just one theorem?

thery · 2018-07-11T14:30:15Z

mathcomp/algebra/poly.v

+by elim/big_ind2: _ => // [[] [|n] [] [|m]|i Pi]; rewrite -?polySpred ?F_neq0.
+Qed.
+
+Lemma size_prod_seq_eq1 (I : choiceType) (s : seq I) (F : I -> {poly R}) :


should be eqType

thery · 2018-07-11T14:44:26Z

mathcomp/algebra/poly.v

@@ -4,7 +4,7 @@ Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp
 Require Import ssrbool ssrfun eqtype ssrnat seq div choice fintype.
 From mathcomp
-Require Import bigop ssralg binomial.
+Require Import bigop ssralg binomial tuple.


is this new import comes only because you are using big_tnth?

thery · 2018-07-14T08:37:44Z

mathcomp/algebra/poly.v

+Lemma size_mul_eq1 p q :
+  (size (p * q) == 1%N) = ((size p == 1%N) && (size q == 1%N)).
+Proof.
+by have := size_prod_seq_eq1 [:: p; q] id; rewrite unlock /= mulr1 andbT.


Kind of weird you would expect size_mul_eq1 to help proving the summation theorem not the other way around.

I know, but since the proof is not done by induction... (maybe it would be shorter? I did not try)

Lemma size_mul_eq1 p q :
(size (p * q) == 1%N) = ((size p == 1%N) && (size q == 1%N)).
Proof.
case: (p =P 0) => [->|/eqP pNZ]; first by rewrite mul0r size_poly0.
case: (q =P 0) => [->|/eqP qNZ]; first by rewrite mulr0 size_poly0 andbF.
rewrite size_mul //.
by move: pNZ qNZ; rewrite -!size_poly_gt0; (do 2 case: size) => //= n [|[|]].
Qed.

Lemma size_prod_seq_eq1 (I : eqType) (s : seq I) (P : pred I) (F : I -> {poly R}) :
(size (\prod_(i <- s | P i) F i) == 1%N) = (all [pred i | P i ==> (size (F i) == 1%N)] s).
Proof.
elim: s => [|a s IH /=]; first by rewrite big_nil size_poly1.
rewrite big_cons; case: (P a) => //=.
by rewrite size_mul_eq1 IH.
Qed.

but maybe size_prod_seq_eq1 should be expressed as a reflect

@pi8027

Added `permutations` and some `perm_eq` lemmas suggested by @MrSet in #299 (except the link to the coq lib `Permutation` predicate). Added support for casts on `map` comprehension general terms. Added `allpairs_map[lr]` suggested by @pi8027 in #314, but with equational proofs; changed `allpairs_comp` to its converse `map_allpairs` for consistency. Documented the `all2` predicate added in #224, and the view combinators added in #202. Renamed `seq2_ind` to `seq_ind2`, and weakened the induction hypothesis, adding a `size` equality assumption. Corrected the header to use `<=>` for `bool` predicate documentation, and `<->` for `Prop` predicates, following the library’s general convention. Replaced the `nosimpl` in `rev` with a `Arguments simpl never` directive, making it possible to merge the `Rev` section into the main `Sequences` section. Miscellaneous improvements to proof scripts and file organisation.

@pi8027

Added `permutations` and some `perm_eq` lemmas suggested by @MrSet in #299 (except the link to the coq lib `Permutation` predicate). Added support for casts on `map` comprehension general terms. Added `allpairs_map[lr]` suggested by @pi8027 in #314, but with equational proofs; changed `allpairs_comp` to its converse `map_allpairs` for consistency. Documented the `all2` predicate added in #224, and the view combinators added in #202. Renamed `seq2_ind` to `seq_ind2`, and weakened the induction hypothesis, adding a `size` equality assumption. Corrected the header to use `<=>` for `bool` predicate documentation, and `<->` for `Prop` predicates, following the library’s general convention. Replaced the `nosimpl` in `rev` with a `Arguments simpl never` directive, making it possible to merge the `Rev` section into the main `Sequences` section. Miscellaneous improvements to proof scripts and file organisation.

@pi8027

Added `permutations` and some `perm_eq` lemmas suggested by @MrSet in #299 (except the link to the coq lib `Permutation` predicate). Added support for casts on `map` comprehension general terms. Added `allpairs_map[lr]` suggested by @pi8027 in #314, but with equational proofs; changed `allpairs_comp` to its converse `map_allpairs` for consistency. Documented the `all2` predicate added in #224, and the view combinators added in #202. Renamed `seq2_ind` to `seq_ind2`, and weakened the induction hypothesis, adding a `size` equality assumption. Corrected the header to use `<=>` for `bool` predicate documentation, and `<->` for `Prop` predicates, following the library’s general convention. Replaced the `nosimpl` in `rev` with a `Arguments simpl never` directive, making it possible to merge the `Rev` section into the main `Sequences` section. Miscellaneous improvements to proof scripts and file organisation.

@pi8027

Added `permutations` and some `perm_eq` lemmas suggested by @MrSet in #299 (except the link to the coq lib `Permutation` predicate). Added support for casts on `map` comprehension general terms. Added `allpairs_map[lr]` suggested by @pi8027 in #314, but with equational proofs; changed `allpairs_comp` to its converse `map_allpairs` for consistency. Documented the `all2` predicate added in #224, and the view combinators added in #202. Renamed `seq2_ind` to `seq_ind2`, and weakened the induction hypothesis, adding a `size` equality assumption. Corrected the header to use `<=>` for `bool` predicate documentation, and `<->` for `Prop` predicates, following the library’s general convention. Replaced the `nosimpl` in `rev` with a `Arguments simpl never` directive, making it possible to merge the `Rev` section into the main `Sequences` section. Miscellaneous improvements to proof scripts and file organisation.

@pi8027

- Added `permutations` and some `perm_eq` lemmas suggested by @MrSet in math-comp#299 (except the link to the coq lib `Permutation` predicate). Use insertion rather than rotation to construct permutations This definition is closer to the one proposed by @MrSet. It adds one line to the definition of `permutations` but the proofs become a little simpler. - Added support for casts on `map` comprehension general terms. - Added `allpairs_map[lr]` suggested by @pi8027 in math-comp#314, but with equational proofs; changed `allpairs_comp` to its converse `map_allpairs` for consistency. Also improves `eq_in_allpairs_dep` proof with @CohenCyril’s proof, and renames `perm_eq_flatten` to `perm_flatten`, consistently with other `perm` lemmas. - Add `allpairs` extensionality lemmas - Added three lemmas, for the non-localised, dependent localised and non-dependent localised cases; as per `eq_in_map`, the latter two are equivalences. - Documented the `all2` predicate added in math-comp#224, and the view combinators added in math-comp#202. - Renamed `seq2_ind` to `seq_ind2`, and weakened the induction hypothesis, adding a `size` equality assumption. - Corrected the header to use `<=>` for `bool` predicate documentation, and `<->` for `Prop` predicates, following the library’s general convention. - Replaced the `nosimpl` in `rev` with a `Arguments simpl never` directive, making it possible to merge the `Rev` section into the main `Sequences` section. - Miscellaneous improvements to proof scripts and file organisation. - correct maximal implicits of `constant` - Fixes omitted `Prenex Implicit` declaration - Other implicits fixes - Fix apparent `done` regression It appears `done` now does a weaker form of intros, and this broke the `dtuple_onP` proof. Updated the proof to eliminate the issue.

@pi8027

- Added `permutations` and some `perm_eq` lemmas suggested by @MrSet in #299 (except the link to the coq lib `Permutation` predicate). Use insertions to construct permutations. This definition is closer to the one proposed by @MrSet, than one using rotations (it adds one line to the definition of `permutations` but the proofs become a little simpler.) - Added support for casts on `map` comprehension general terms. - Added `allpairs_map[lr]` suggested by @pi8027 in #314, but with equational proofs; changed `allpairs_comp` to its converse `map_allpairs` for consistency. - Add three `allpairs` extensionality lemmas: for the non-localised, dependent localised and non-dependent localised cases; as per `eq_in_map`, the latter two are equivalences. - Documented the `all2` predicate added in #224, and the view combinators added in #202. - Renamed `seq2_ind` to `seq_ind2`, and weakened the induction hypothesis, adding a `size` equality assumption. - Corrected the header to use `<=>` for `bool` predicate documentation, and `<->` for `Prop` predicates, following the library’s general convention. - Replaced the `nosimpl` in `rev` with a `Arguments simpl never` directive, making it possible to merge the `Rev` section into the main `Sequences` section. - Miscellaneous improvements to proof scripts and file organisation. - Correct maximal implicits of `constant`. - Fixes omitted `Prenex Implicit` declaration. - Other implicits fixes. - Fix apparent `done` regression It appears `done` now does a weaker form of intros, and this broke the `dtuple_onP` proof. Updated the proof to eliminate the issue. (Commit log edited by @CohenCyril during the squash.)

@pi8027

- Added `permutations` and some `perm_eq` lemmas suggested by @MrSet in #299 (except the link to the coq lib `Permutation` predicate). Use insertions to construct permutations. This definition is closer to the one proposed by @MrSet, than one using rotations (it adds one line to the definition of `permutations` but the proofs become a little simpler.) - Added support for casts on `map` comprehension general terms. - Added `allpairs_map[lr]` suggested by @pi8027 in #314, but with equational proofs; changed `allpairs_comp` to its converse `map_allpairs` for consistency. - Add three `allpairs` extensionality lemmas: for the non-localised, dependent localised and non-dependent localised cases; as per `eq_in_map`, the latter two are equivalences. - Documented the `all2` predicate added in #224, and the view combinators added in #202. - Renamed `seq2_ind` to `seq_ind2`, and weakened the induction hypothesis, adding a `size` equality assumption. - Corrected the header to use `<=>` for `bool` predicate documentation, and `<->` for `Prop` predicates, following the library’s general convention. - Replaced the `nosimpl` in `rev` with a `Arguments simpl never` directive, making it possible to merge the `Rev` section into the main `Sequences` section. - Miscellaneous improvements to proof scripts and file organisation. - Correct maximal implicits of `constant`. - Fixes omitted `Prenex Implicit` declaration. - Other implicits fixes. - Fix apparent `done` regression It appears `done` now does a weaker form of intros, and this broke the `dtuple_onP` proof. Updated the proof to eliminate the issue. (Commit log edited by @CohenCyril during the squash.)

@pi8027

- Added `permutations` and some `perm_eq` lemmas suggested by @MrSet in #299 (except the link to the coq lib `Permutation` predicate). Use insertions to construct permutations. This definition is closer to the one proposed by @MrSet, than one using rotations (it adds one line to the definition of `permutations` but the proofs become a little simpler.) - Added support for casts on `map` comprehension general terms. - Added `allpairs_map[lr]` suggested by @pi8027 in #314, but with equational proofs; changed `allpairs_comp` to its converse `map_allpairs` for consistency. - Add three `allpairs` extensionality lemmas: for the non-localised, dependent localised and non-dependent localised cases; as per `eq_in_map`, the latter two are equivalences. - Documented the `all2` predicate added in #224, and the view combinators added in #202. - Renamed `seq2_ind` to `seq_ind2`, and weakened the induction hypothesis, adding a `size` equality assumption. - Corrected the header to use `<=>` for `bool` predicate documentation, and `<->` for `Prop` predicates, following the library’s general convention. - Replaced the `nosimpl` in `rev` with a `Arguments simpl never` directive, making it possible to merge the `Rev` section into the main `Sequences` section. - Miscellaneous improvements to proof scripts and file organisation. - Correct maximal implicits of `constant`. - Fixes omitted `Prenex Implicit` declaration. - Other implicits fixes. - Fix apparent `done` regression It appears `done` now does a weaker form of intros, and this broke the `dtuple_onP` proof. Updated the proof to eliminate the issue. (Commit log edited by @CohenCyril during the squash.)

@pi8027

- Added `permutations` and some `perm_eq` lemmas suggested by @MrSet in math-comp#299 (except the link to the coq lib `Permutation` predicate). Use insertions to construct permutations. This definition is closer to the one proposed by @MrSet, than one using rotations (it adds one line to the definition of `permutations` but the proofs become a little simpler.) - Added support for casts on `map` comprehension general terms. - Added `allpairs_map[lr]` suggested by @pi8027 in math-comp#314, but with equational proofs; changed `allpairs_comp` to its converse `map_allpairs` for consistency. - Add three `allpairs` extensionality lemmas: for the non-localised, dependent localised and non-dependent localised cases; as per `eq_in_map`, the latter two are equivalences. - Documented the `all2` predicate added in math-comp#224, and the view combinators added in math-comp#202. - Renamed `seq2_ind` to `seq_ind2`, and weakened the induction hypothesis, adding a `size` equality assumption. - Corrected the header to use `<=>` for `bool` predicate documentation, and `<->` for `Prop` predicates, following the library’s general convention. - Replaced the `nosimpl` in `rev` with a `Arguments simpl never` directive, making it possible to merge the `Rev` section into the main `Sequences` section. - Miscellaneous improvements to proof scripts and file organisation. - Correct maximal implicits of `constant`. - Fixes omitted `Prenex Implicit` declaration. - Other implicits fixes. - Fix apparent `done` regression It appears `done` now does a weaker form of intros, and this broke the `dtuple_onP` proof. Updated the proof to eliminate the issue. (Commit log edited by @CohenCyril during the squash.)

small generalizations in poly

618c922

CohenCyril requested review from amahboubi and thery July 4, 2018 14:29

thery requested changes Jul 11, 2018

View reviewed changes

CohenCyril added 2 commits July 14, 2018 01:26

Laurent's simplifications

ededc37

updated proposition for big_prod_seq_eq1

cf1b112

thery reviewed Jul 14, 2018

View reviewed changes

CohenCyril added 2 commits July 19, 2018 17:11

poly_size_eq1 phrased with reflect + combinators

a4f1697

last_eq for exhaustivity

47831fd

thery merged commit 1897c99 into math-comp:master Jul 19, 2018

maximedenes added this to the 1.8.0 milestone Mar 22, 2019

CohenCyril deleted the improving-poly branch May 24, 2019 12:04

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

small generalizations and extensions in poly #202

small generalizations and extensions in poly #202

CohenCyril commented Jul 4, 2018

thery left a comment

thery Jul 11, 2018

CohenCyril Jul 13, 2018

thery Jul 11, 2018

CohenCyril Jul 13, 2018

CohenCyril Jul 19, 2018

thery Jul 11, 2018

thery Jul 11, 2018

thery Jul 11, 2018

CohenCyril Jul 14, 2018

thery Jul 14, 2018

thery Jul 11, 2018

thery Jul 11, 2018

CohenCyril Jul 13, 2018

thery Jul 14, 2018

CohenCyril Jul 14, 2018

thery Jul 14, 2018

small generalizations and extensions in poly #202

small generalizations and extensions in poly #202

Conversation

CohenCyril commented Jul 4, 2018

thery left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment