From 618c9229fecbf6f1e85035aa0033943dcd4f3464 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Tue, 3 Jul 2018 13:07:16 +0200 Subject: small generalizations in poly --- mathcomp/algebra/poly.v | 92 +++++++++++++++++++++++++++++++++++++---------- mathcomp/algebra/ssralg.v | 3 ++ 2 files changed, 76 insertions(+), 19 deletions(-) (limited to 'mathcomp') diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v index f34ca2d..1c5de11 100644 --- a/mathcomp/algebra/poly.v +++ b/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. (******************************************************************************) (* This file provides a library for univariate polynomials over ring *) @@ -359,6 +359,9 @@ Proof. by apply: (iffP idP); rewrite size_poly_leq0; move/eqP. Qed. Lemma size_poly_gt0 p : (0 < size p) = (p != 0). Proof. by rewrite lt0n size_poly_eq0. Qed. +Lemma gt_size_poly_neq0 p n : (size p > n)%N -> p != 0. +Proof. by move=> /(leq_ltn_trans _) h; rewrite -size_poly_eq0 lt0n_neq0 ?h. Qed. + Lemma nil_poly p : nilp p = (p == 0). Proof. exact: size_poly_eq0. Qed. @@ -384,6 +387,9 @@ have def_p: p = (p`_0)%:P by rewrite -size1_polyC ?pC. by exists p`_0; rewrite // -polyC_eq0 -def_p -size_poly_eq0 pC. Qed. +Lemma size_polyC_leq1 (c : R) : (size c%:P <= 1)%N. +Proof. by rewrite size_polyC; case: (c == 0). Qed. + Lemma leq_sizeP p i : reflect (forall j, i <= j -> p`_j = 0) (size p <= i). Proof. apply: (iffP idP) => [hp j hij| hp]. @@ -461,6 +467,9 @@ move=> ltqp; rewrite /lead_coef coefD size_addl //. by rewrite addrC nth_default ?simp // -ltnS (ltn_predK ltqp). Qed. +Lemma lead_coefDr p q : size q > size p -> lead_coef (p + q) = lead_coef q. +Proof. by move/lead_coefDl<-; rewrite addrC. Qed. + (* Polynomial ring structure. *) Definition mul_poly_def p q := @@ -1939,6 +1948,13 @@ Proof. by rewrite [p \Po q]horner_poly; apply: eq_bigr => i _; rewrite mul_polyC. Qed. +Lemma coef_comp_poly p q n : + (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. +Qed. + Lemma polyOver_comp S (ringS : semiringPred S) (kS : keyed_pred ringS) : {in polyOver kS &, forall p q, p \Po q \in polyOver kS}. Proof. @@ -2216,6 +2232,38 @@ elim/big_rec2: _ => [|i d p /nzF nzFi IHp]; first by rewrite size_poly1. by rewrite size_mul // -?size_poly_eq0 IHp // addnS polySpred. Qed. +Lemma size_prod_seq (I : eqType) (s : seq I) (F : I -> {poly R}) : + (forall i, i \in s -> F i != 0) -> + size (\prod_(i <- s) F i) = ((\sum_(i <- s) size (F i)).+1 - size s)%N. +Proof. +move=> nzF; rewrite big_tnth size_prod; last by move=> i; rewrite nzF ?mem_tnth. +by rewrite cardT /= size_enum_ord [in RHS]big_tnth. +Qed. + +Lemma size_prod_eq1 (I : finType) (P : pred I) (F : I -> {poly R}) : + (size (\prod_(i | P i) F i) == 1%N) = [forall (i | P i), size (F i) == 1%N]. +Proof. +have [/forall_inP F_neq0|] := boolP [forall (i | P i), F i != 0]; last first. + rewrite negb_forall_in => /exists_inP [i Pi]; rewrite negbK => /eqP Fi_eq0. + rewrite (bigD1 i) //= Fi_eq0 mul0r size_poly0; symmetry. + by apply/existsP; exists i; rewrite Pi Fi_eq0 size_poly0. +rewrite size_prod // -sum1_card subSn; last first. + by rewrite leq_sum // => i Pi; rewrite size_poly_gt0 F_neq0. +rewrite (eq_bigr (fun i => (size (F i)).-1 + 1))%N; last first. + by move=> i Pi; rewrite addn1 -polySpred ?F_neq0. +rewrite big_split /= addnK -big_andE /=. +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}) : + reflect (forall i, i \in s -> size (F i) = 1%N) + (size (\prod_(i <- s) F i) == 1%N). +Proof. +rewrite big_tnth size_prod_eq1. +apply: (iffP forall_inP) => Fi i; last by rewrite Fi // mem_tnth. +by move=> /seq_tnthP [{i}i ->]; apply/eqP/Fi. +Qed. + Lemma size_exp p n : (size (p ^+ n)).-1 = ((size p).-1 * n)%N. Proof. elim: n => [|n IHn]; first by rewrite size_poly1 muln0. @@ -2255,31 +2303,33 @@ rewrite (leq_trans (size_scale_leq _ _)) // polySpred ?expf_neq0 //. by rewrite size_exp -(subnKC nc_q) ltn_pmul2l. Qed. -Lemma size_comp_poly2 p q : size q = 2 -> size (p \Po q) = size p. +Lemma lead_coef_comp p q : size q > 1 -> + lead_coef (p \Po q) = (lead_coef p) * lead_coef q ^+ (size p).-1. Proof. -have [/size1_polyC->| p_gt1] := leqP (size p) 1; first by rewrite comp_polyC. -move=> lin_q; have{lin_q} sz_pq: (size (p \Po q)).-1 = (size p).-1. - by rewrite size_comp_poly lin_q muln1. -rewrite -(ltn_predK p_gt1) -sz_pq -polySpred // -size_poly_gt0 ltnW //. -by rewrite -subn_gt0 subn1 sz_pq -subn1 subn_gt0. +move=> q_gt1; rewrite !lead_coefE coef_comp_poly size_comp_poly. +have [->|nz_p] := eqVneq p 0; first by rewrite size_poly0 big_ord0 coef0 mul0r. +rewrite polySpred //= big_ord_recr /= big1 ?add0r => [|i _]. + by rewrite -!lead_coefE -lead_coef_exp !lead_coefE size_exp mulnC. +rewrite [X in _ * X]nth_default ?mulr0 ?(leq_trans (size_exp_leq _ _)) //. +by rewrite mulnC ltn_mul2r -subn1 subn_gt0 q_gt1 /=. Qed. -Lemma comp_poly2_eq0 p q : size q = 2 -> (p \Po q == 0) = (p == 0). -Proof. by rewrite -!size_poly_eq0 => /size_comp_poly2->. Qed. +Lemma comp_poly_eq0 p q : size q > 1 -> (p \Po q == 0) = (p == 0). +Proof. +move=> sq_gt1; rewrite -!lead_coef_eq0 lead_coef_comp //. +rewrite mulf_eq0 expf_eq0 !lead_coef_eq0 -[q == 0]size_poly_leq0. +by rewrite [_ <= 0]leqNgt (leq_ltn_trans _ sq_gt1) ?andbF ?orbF. +Qed. -Lemma lead_coef_comp p q : - size q > 1 -> lead_coef (p \Po q) = lead_coef p * lead_coef q ^+ (size p).-1. +Lemma size_comp_poly2 p q : size q = 2 -> size (p \Po q) = size p. Proof. -move=> q_gt1; have nz_q: q != 0 by rewrite -size_poly_gt0 ltnW. -have [-> | nz_p] := eqVneq p 0; first by rewrite comp_poly0 !lead_coef0 mul0r. -rewrite comp_polyE polySpred //= big_ord_recr /= addrC -lead_coefE. -rewrite lead_coefDl; first by rewrite lead_coefZ lead_coef_exp. -rewrite size_scale ?lead_coef_eq0 // (polySpred (expf_neq0 _ nz_q)) ltnS. -apply/leq_sizeP=> i le_qp_i; rewrite coef_sum big1 // => j _. -rewrite coefZ (nth_default 0 (leq_trans _ le_qp_i)) ?mulr0 //=. -by rewrite polySpred ?expf_neq0 // !size_exp -(subnKC q_gt1) ltn_pmul2l. +move=> sq2; have [->|pN0] := eqVneq p 0; first by rewrite comp_polyC. +by rewrite polySpred ?size_comp_poly ?comp_poly_eq0 ?sq2 // muln1 polySpred. Qed. +Lemma comp_poly2_eq0 p q : size q = 2 -> (p \Po q == 0) = (p == 0). +Proof. by rewrite -!size_poly_eq0 => /size_comp_poly2->. Qed. + Theorem max_poly_roots p rs : p != 0 -> all (root p) rs -> uniq rs -> size rs < size p. Proof. @@ -2293,6 +2343,10 @@ move=> x xrs; rewrite epq rootM root_XsubC orbC; case: (altP (x =P r)) => // exr by move: rnrs; rewrite -exr xrs. Qed. +Lemma roots_geq_poly_eq0 p (rs : seq R) : all (root p) rs -> uniq rs -> + (size rs >= size p)%N -> p = 0. +Proof. by move=> ??; apply: contraTeq => ?; rewrite leqNgt max_poly_roots. Qed. + End PolynomialIdomain. Section MapFieldPoly. diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v index c0b3041..31579ce 100644 --- a/mathcomp/algebra/ssralg.v +++ b/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. + Lemma mulrI_eq0 x y : lreg x -> (x * y == 0) = (y == 0). Proof. by move=> reg_x; rewrite -{1}(mulr0 x) (inj_eq reg_x). Qed. -- cgit v1.2.3 From ededc3786a779f26303e9545dc68bd6006b4aae4 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Sat, 14 Jul 2018 01:26:16 +0100 Subject: Laurent's simplifications --- mathcomp/algebra/poly.v | 7 ++----- mathcomp/algebra/ssralg.v | 2 +- 2 files changed, 3 insertions(+), 6 deletions(-) (limited to 'mathcomp') diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v index 1c5de11..5019eda 100644 --- a/mathcomp/algebra/poly.v +++ b/mathcomp/algebra/poly.v @@ -1950,10 +1950,7 @@ Qed. Lemma coef_comp_poly p q n : (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. -Qed. +Proof. by rewrite comp_polyE coef_sum; apply: eq_bigr => i; rewrite coefZ. Qed. Lemma polyOver_comp S (ringS : semiringPred S) (kS : keyed_pred ringS) : {in polyOver kS &, forall p q, p \Po q \in polyOver kS}. @@ -2255,7 +2252,7 @@ rewrite big_split /= addnK -big_andE /=. 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}) : +Lemma size_prod_seq_eq1 (I : eqType) (s : seq I) (F : I -> {poly R}) : reflect (forall i, i \in s -> size (F i) = 1%N) (size (\prod_(i <- s) F i) == 1%N). Proof. diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v index 31579ce..9ccb92f 100644 --- a/mathcomp/algebra/ssralg.v +++ b/mathcomp/algebra/ssralg.v @@ -1172,7 +1172,7 @@ 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. +Proof. by case: s => [|y s] /negPf // ->; rewrite oner_eq0. Qed. Lemma mulrI_eq0 x y : lreg x -> (x * y == 0) = (y == 0). Proof. by move=> reg_x; rewrite -{1}(mulr0 x) (inj_eq reg_x). Qed. -- cgit v1.2.3 From cf1b1123f42d4c8b179d2a5bba557dec94de1888 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Sat, 14 Jul 2018 01:36:54 +0100 Subject: updated proposition for big_prod_seq_eq1 --- mathcomp/algebra/poly.v | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) (limited to 'mathcomp') diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v index 5019eda..2eba50d 100644 --- a/mathcomp/algebra/poly.v +++ b/mathcomp/algebra/poly.v @@ -2253,12 +2253,15 @@ by elim/big_ind2: _ => // [[] [|n] [] [|m]|i Pi]; rewrite -?polySpred ?F_neq0. Qed. Lemma size_prod_seq_eq1 (I : eqType) (s : seq I) (F : I -> {poly R}) : - reflect (forall i, i \in s -> size (F i) = 1%N) - (size (\prod_(i <- s) F i) == 1%N). + (size (\prod_(i <- s) F i) == 1%N) = (all [pred i | size (F i) == 1%N] s). Proof. -rewrite big_tnth size_prod_eq1. -apply: (iffP forall_inP) => Fi i; last by rewrite Fi // mem_tnth. -by move=> /seq_tnthP [{i}i ->]; apply/eqP/Fi. +by rewrite big_tnth size_prod_eq1 -big_all [in RHS]big_tnth big_andE. +Qed. + +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. Qed. Lemma size_exp p n : (size (p ^+ n)).-1 = ((size p).-1 * n)%N. -- cgit v1.2.3 From a4f169772ace822087c9ab6aaac3f81982560b97 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Thu, 19 Jul 2018 17:11:48 +0200 Subject: poly_size_eq1 phrased with reflect + combinators --- mathcomp/algebra/poly.v | 40 ++++++++++++++++++++++------------------ mathcomp/ssreflect/fintype.v | 17 +++++++++++++++-- mathcomp/ssreflect/seq.v | 13 +++++++++++++ 3 files changed, 50 insertions(+), 20 deletions(-) (limited to 'mathcomp') diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v index 2eba50d..0f97bb0 100644 --- a/mathcomp/algebra/poly.v +++ b/mathcomp/algebra/poly.v @@ -2237,31 +2237,35 @@ move=> nzF; rewrite big_tnth size_prod; last by move=> i; rewrite nzF ?mem_tnth. by rewrite cardT /= size_enum_ord [in RHS]big_tnth. Qed. -Lemma size_prod_eq1 (I : finType) (P : pred I) (F : I -> {poly R}) : - (size (\prod_(i | P i) F i) == 1%N) = [forall (i | P i), size (F i) == 1%N]. +Lemma size_mul_eq1 p q : + (size (p * q) == 1%N) = ((size p == 1%N) && (size q == 1%N)). Proof. -have [/forall_inP F_neq0|] := boolP [forall (i | P i), F i != 0]; last first. - rewrite negb_forall_in => /exists_inP [i Pi]; rewrite negbK => /eqP Fi_eq0. - rewrite (bigD1 i) //= Fi_eq0 mul0r size_poly0; symmetry. - by apply/existsP; exists i; rewrite Pi Fi_eq0 size_poly0. -rewrite size_prod // -sum1_card subSn; last first. - by rewrite leq_sum // => i Pi; rewrite size_poly_gt0 F_neq0. -rewrite (eq_bigr (fun i => (size (F i)).-1 + 1))%N; last first. - by move=> i Pi; rewrite addn1 -polySpred ?F_neq0. -rewrite big_split /= addnK -big_andE /=. -by elim/big_ind2: _ => // [[] [|n] [] [|m]|i Pi]; rewrite -?polySpred ?F_neq0. +have [->|pNZ] := eqVneq p 0; first by rewrite mul0r size_poly0. +have [->|qNZ] := eqVneq q 0; 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) (F : I -> {poly R}) : - (size (\prod_(i <- s) F i) == 1%N) = (all [pred i | size (F i) == 1%N] s). +Lemma size_prod_seq_eq1 (I : eqType) (s : seq I) (P : pred I) (F : I -> {poly R}) : + reflect (forall i, P i && (i \in s) -> size (F i) = 1%N) + (size (\prod_(i <- s | P i) F i) == 1%N). Proof. -by rewrite big_tnth size_prod_eq1 -big_all [in RHS]big_tnth big_andE. +have -> : (size (\prod_(i <- s | P i) F i) == 1%N) = + (all [pred i | P i ==> (size (F i) == 1%N)] s). + elim: s => [|a s IHs /=]; first by rewrite big_nil size_poly1. + by rewrite big_cons; case: (P a) => //=; rewrite size_mul_eq1 IHs. +apply: (iffP allP) => /= [/(_ _ _)/implyP /(_ _)/eqP|] sF_eq1 i. + by move=> /andP[Pi si]; rewrite sF_eq1. +by move=> si; apply/implyP => Pi; rewrite sF_eq1 ?Pi. Qed. -Lemma size_mul_eq1 p q : - (size (p * q) == 1%N) = ((size p == 1%N) && (size q == 1%N)). +Lemma size_prod_eq1 (I : finType) (P : pred I) (F : I -> {poly R}) : + reflect (forall i, P i -> size (F i) = 1%N) + (size (\prod_(i | P i) F i) == 1%N). Proof. -by have := size_prod_seq_eq1 [:: p; q] id; rewrite unlock /= mulr1 andbT. +apply: (iffP (size_prod_seq_eq1 _ _ _)) => Hi i. + by move=> Pi; apply: Hi; rewrite Pi /= mem_index_enum. +by rewrite mem_index_enum andbT; apply: Hi. Qed. Lemma size_exp p n : (size (p ^+ n)).-1 = ((size p).-1 * n)%N. diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v index 1446fbd..cb2f0a6 100644 --- a/mathcomp/ssreflect/fintype.v +++ b/mathcomp/ssreflect/fintype.v @@ -867,9 +867,13 @@ Proof. exact: 'forall_eqP. Qed. Lemma forall_inP D P : reflect (forall x, D x -> P x) [forall (x | D x), P x]. Proof. exact: 'forall_implyP. Qed. +Lemma forall_inPP D P PP : (forall x, reflect (PP x) (P x)) -> + reflect (forall x, D x -> PP x) [forall (x | D x), P x]. +Proof. by move=> vP; apply: (iffP (forall_inP _ _)) => /(_ _ _) /vP. Qed. + Lemma eqfun_inP D f1 f2 : reflect {in D, forall x, f1 x = f2 x} [forall (x | x \in D), f1 x == f2 x]. -Proof. by apply: (iffP 'forall_implyP) => eq_f12 x Dx; apply/eqP/eq_f12. Qed. +Proof. exact: (forall_inPP _ (fun=> eqP)). Qed. Lemma existsP P : reflect (exists x, P x) [exists x, P x]. Proof. exact: 'exists_idP. Qed. @@ -881,9 +885,13 @@ Proof. exact: 'exists_eqP. Qed. Lemma exists_inP D P : reflect (exists2 x, D x & P x) [exists (x | D x), P x]. Proof. by apply: (iffP 'exists_andP) => [[x []] | [x]]; exists x. Qed. +Lemma exists_inPP D P PP : (forall x, reflect (PP x) (P x)) -> + reflect (exists2 x, D x & PP x) [exists (x | D x), P x]. +Proof. by move=> vP; apply: (iffP (exists_inP _ _)) => -[x?/vP]; exists x. Qed. + Lemma exists_eq_inP D f1 f2 : reflect (exists2 x, D x & f1 x = f2 x) [exists (x | D x), f1 x == f2 x]. -Proof. by apply: (iffP (exists_inP _ _)) => [] [x Dx /eqP]; exists x. Qed. +Proof. exact: (exists_inPP _ (fun=> eqP)). Qed. Lemma eq_existsb P1 P2 : P1 =1 P2 -> [exists x, P1 x] = [exists x, P2 x]. Proof. by move=> eqP12; congr (_ != 0); apply: eq_card. Qed. @@ -928,6 +936,11 @@ Arguments exists_eqP [T rT f1 f2]. Arguments exists_inP [T D P]. Arguments exists_eq_inP [T rT D f1 f2]. +Notation "'exists_in_ view" := (exists_inPP _ (fun _ => view)) + (at level 4, right associativity, format "''exists_in_' view"). +Notation "'forall_in_ view" := (forall_inPP _ (fun _ => view)) + (at level 4, right associativity, format "''forall_in_' view"). + Section Extrema. Variables (I : finType) (i0 : I) (P : pred I) (F : I -> nat). diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 4347983..4bc704a 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -1004,6 +1004,10 @@ apply: (iffP IHs) => [] [x ysx ax]; exists x => //; first exact: mem_behead. by case: (predU1P ysx) ax => [->|//]; rewrite ay. Qed. +Lemma hasPP s aP : (forall x, reflect (aP x) (a x)) -> + reflect (exists2 x, x \in s & aP x) (has a s). +Proof. by move=> vP; apply: (iffP (hasP _)) => -[x?/vP]; exists x. Qed. + Lemma hasPn s : reflect (forall x, x \in s -> ~~ a x) (~~ has a s). Proof. apply: (iffP idP) => not_a_s => [x s_x|]. @@ -1020,6 +1024,10 @@ rewrite /= andbC; case: IHs => IHs /=. by right=> H; case IHs => y Hy; apply H; apply: mem_behead. Qed. +Lemma allPP s aP : (forall x, reflect (aP x) (a x)) -> + reflect (forall x, x \in s -> aP x) (all a s). +Proof. by move=> vP; apply: (iffP (allP _)) => /(_ _ _) /vP. Qed. + Lemma allPn s : reflect (exists2 x, x \in s & ~~ a x) (~~ all a s). Proof. elim: s => [|x s IHs]; first by right=> [[x Hx _]]. @@ -1038,6 +1046,11 @@ Qed. End Filters. +Notation "'has_ view" := (hasPP _ (fun _ => view)) + (at level 4, right associativity, format "''has_' view"). +Notation "'all_ view" := (allPP _ (fun _ => view)) + (at level 4, right associativity, format "''all_' view"). + Section EqIn. Variables a1 a2 : pred T. -- cgit v1.2.3 From 47831fdfcc1aa313b722232cebde2d3607f2e9b2 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Thu, 19 Jul 2018 17:11:59 +0200 Subject: last_eq for exhaustivity --- mathcomp/ssreflect/seq.v | 3 +++ 1 file changed, 3 insertions(+) (limited to 'mathcomp') diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 4bc704a..8938ac5 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -992,6 +992,9 @@ Proof. by move=> s0x; rewrite -(cat_take_drop n0 s) mem_cat /= s0x. Qed. Lemma mem_drop s x : x \in drop n0 s -> x \in s. Proof. by move=> s0'x; rewrite -(cat_take_drop n0 s) mem_cat /= s0'x orbT. Qed. +Lemma last_eq s z x y : x != y -> z != y -> (last x s == y) = (last z s == y). +Proof. by move=> /negPf xz /negPf yz; case: s => [|t s]//; rewrite xz yz. Qed. + Section Filters. Variable a : pred T. -- cgit v1.2.3