From fbeec199e65fe7e9fd96ddd74e31aa0461c22927 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Tue, 1 Sep 2020 15:44:13 +0200 Subject: Lemmas reindex_omap and bigD1_ord + eq_liftF and lift_eqF + proof simplificaions --- mathcomp/ssreflect/bigop.v | 38 ++++++++++++++++++++++++++++++-------- mathcomp/ssreflect/finset.v | 16 ++++++---------- mathcomp/ssreflect/fintype.v | 6 ++++++ 3 files changed, 42 insertions(+), 18 deletions(-) (limited to 'mathcomp/ssreflect') diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index 1b580c0..ee3aedb 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -1464,18 +1464,29 @@ Lemma big_image_id (J : finType) (h : J -> R) (A : pred J) : \big[*%M/1]_(i <- [seq h j | j in A]) i = \big[*%M/1]_(j in A) h j. Proof. exact: big_image. Qed. -Lemma reindex_onto (I J : finType) (h : J -> I) h' (P : pred I) F : - (forall i, P i -> h (h' i) = i) -> +Lemma reindex_omap (I J : finType) (h : J -> I) h' (P : pred I) F : + (forall i, P i -> omap h (h' i) = some i) -> \big[*%M/1]_(i | P i) F i = - \big[*%M/1]_(j | P (h j) && (h' (h j) == j)) F (h j). + \big[*%M/1]_(j | P (h j) && (h' (h j) == some j)) F (h j). Proof. move=> h'K; have [n lePn] := ubnP #|P|; elim: n => // n IHn in P h'K lePn *. case: (pickP P) => [i Pi | P0]; last first. by rewrite !big_pred0 // => j; rewrite P0. -rewrite (bigD1 i Pi) (bigD1 (h' i)) h'K ?Pi ?eqxx //=; congr (_ * _). -rewrite {}IHn => [|j /andP[]|]; [|by auto | by rewrite (cardD1x i) in lePn]. -apply: eq_bigl => j; rewrite andbC -andbA (andbCA (P _)); case: eqP => //= hK. -by congr (_ && ~~ _); apply/eqP/eqP=> [<-|->] //; rewrite h'K. +have := h'K i Pi; case h'i_eq : (h' i) => [/= j|//] [hj_eq]. +rewrite (bigD1 i Pi) (bigD1 j) hj_eq ?Pi ?h'i_eq ?eqxx //=; congr (_ * _). +rewrite {}IHn => [|k /andP[]|]; [|by auto | by rewrite (cardD1x i) in lePn]. +apply: eq_bigl => k; rewrite andbC -andbA (andbCA (P _)); case: eqP => //= hK. +congr (_ && ~~ _); apply/eqP/eqP => [|->//]. +by move=> /(congr1 h'); rewrite h'i_eq hK => -[]. +Qed. +Arguments reindex_omap [I J] h h' [P F]. + +Lemma reindex_onto (I J : finType) (h : J -> I) h' (P : pred I) F : + (forall i, P i -> h (h' i) = i) -> + \big[*%M/1]_(i | P i) F i = + \big[*%M/1]_(j | P (h j) && (h' (h j) == j)) F (h j). +Proof. +by move=> h'K; rewrite (reindex_omap h (some \o h'))//= => i Pi; rewrite h'K. Qed. Arguments reindex_onto [I J] h h' [P F]. @@ -1493,6 +1504,15 @@ Lemma reindex_inj (I : finType) (h : I -> I) (P : pred I) F : Proof. by move=> injh; apply: reindex (onW_bij _ (injF_bij injh)). Qed. Arguments reindex_inj [I h P F]. +Lemma bigD1_ord n j (P : pred 'I_n) F : + P j -> \big[*%M/1]_(i < n | P i) F i + = F j * \big[*%M/1]_(i < n.-1 | P (lift j i)) F (lift j i). +Proof. +move=> Pj; rewrite (bigD1 j Pj) (reindex_omap (lift j) (unlift j))/=. + by under eq_bigl do rewrite liftK eq_sym eqxx neq_lift ?andbT. +by move=> i; case: unliftP => [k ->|->]; rewrite ?eqxx ?andbF. +Qed. + Lemma big_enum_val_cond (I : finType) (A : pred I) (P : pred I) F : \big[op/idx]_(x in A | P x) F x = \big[op/idx]_(i < #|A| | P (enum_val i)) F (enum_val i). @@ -1656,7 +1676,9 @@ Arguments bigID [R idx op I r]. Arguments bigU [R idx op I]. Arguments bigD1 [R idx op I] j [P F]. Arguments bigD1_seq [R idx op I r] j [F]. +Arguments bigD1_ord [R idx op n] j [P F]. Arguments partition_big [R idx op I J P] p Q [F]. +Arguments reindex_omap [R idx op I J] h h' [P F]. Arguments reindex_onto [R idx op I J] h h' [P F]. Arguments reindex [R idx op I J] h [P F]. Arguments reindex_inj [R idx op I h P F]. @@ -1749,7 +1771,7 @@ Proof. have [j _ | J0] := pickP J; first by rewrite (big_distr_big_dep j). have Q0 i: Q i =i pred0 by move=> /J0/esym/notF[]. transitivity (iter #|I| ( *%M 0) 1). - by rewrite -big_const; apply/eq_bigr=> i; have /(big_pred0 _)-> := Q0 i. + by rewrite -big_const; apply/eq_bigr=> i; have /(big_pred0 _)-> := Q0 i. have [i _ | I0] := pickP I. rewrite (cardD1 i) //= mul0m big_pred0 // => f. by apply/familyP=> /(_ i); rewrite Q0. diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v index 9bd8c1f..4262ed7 100644 --- a/mathcomp/ssreflect/finset.v +++ b/mathcomp/ssreflect/finset.v @@ -1453,17 +1453,13 @@ Lemma big_imset h (A : {pred I}) G : {in A &, injective h} -> \big[aop/idx]_(j in h @: A) G j = \big[aop/idx]_(i in A) G (h i). Proof. move=> injh; pose hA := mem (image h A). -have [x0 Ax0 | A0] := pickP A; last first. - by rewrite !big_pred0 // => x; apply/imsetP=> [[i]]; rewrite unfold_in A0. rewrite (eq_bigl hA) => [|j]; last exact/imsetP/imageP. -pose h' j := if insub j : {? j | hA j} is Some u then iinv (svalP u) else x0. -rewrite (reindex_onto h h') => [|j hAj]; rewrite {}/h'; last first. - by rewrite (insubT hA hAj) f_iinv. -apply: eq_bigl => i; case: insubP => [u -> /= def_u | nhAhi]. - set i' := iinv _; have Ai' : i' \in A := mem_iinv (svalP u). - by apply/eqP/idP=> [<- // | Ai]; apply: injh; rewrite ?f_iinv. -symmetry; rewrite (negbTE nhAhi); apply/idP=> Ai. -by case/imageP: nhAhi; exists i. +pose h' := omap (fun u : {j | hA j} => iinv (svalP u)) \o insub. +rewrite (reindex_omap h h') => [|j hAj]; rewrite {}/h'/= ?insubT/= ?f_iinv//. +apply: eq_bigl => i; case: insubP => [u -> /= def_u | nhAhi]; last first. + by apply/andP/idP => [[]//| Ai]; case/imageP: nhAhi; exists i. +set i' := iinv _; have Ai' : i' \in A := mem_iinv (svalP u). +by apply/eqP/idP => [[<-] // | Ai]; congr Some; apply: injh; rewrite ?f_iinv. Qed. Lemma big_imset_cond h (A : {pred I}) (P : pred J) G : {in A &, injective h} -> diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v index 88d0f92..3472a1d 100644 --- a/mathcomp/ssreflect/fintype.v +++ b/mathcomp/ssreflect/fintype.v @@ -2074,6 +2074,12 @@ Qed. Lemma neq_lift n (h : 'I_n) i : h != lift h i. Proof. exact: neq_bump. Qed. +Lemma eq_liftF n (h : 'I_n) i : (h == lift h i) = false. +Proof. exact/negbTE/neq_lift. Qed. + +Lemma lift_eqF n (h : 'I_n) i : (lift h i == h) = false. +Proof. by rewrite eq_sym eq_liftF. Qed. + Lemma unlift_none n (h : 'I_n) : unlift h h = None. Proof. by case: unliftP => // j Dh; case/eqP: (neq_lift h j). Qed. -- cgit v1.2.3