From Ssreflect Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype. From MathComp Require Import path div tuple finfun bigop. Lemma big_cat_example f : \sum_(1 <= n < 11) f(n) = \sum_(1 <= n < 6) f(n) + \sum_(6 <= n < 11) f(n). Proof. by rewrite -big_cat. Qed. (* hint: use big_nat_recr and big_nil *) Lemma exo34 : forall n : nat, 2 * (\sum_(0 <= x < n.+1) x) = n * n.+1. Proof. Abort. Lemma exo35 n : (6 * \sum_(k < n.+1) k ^ 2)%nat = n * n.+1 * (n.*2).+1. Proof. Abort. Lemma exo36 (x n : nat) : 1 < x -> (x - 1) * (\sum_(k < n.+1) x ^ k) = x ^ n.+1 - 1. Proof. Abort. Lemma exo37 (v : nat -> nat) (v0 : v 0 = 1) (vn : forall n, v n.+1 = \sum_(k < n.+1) v k) (n : nat) : n != 0 -> v n = 2 ^ n.-1. Proof. Abort. Parameter n : nat. Parameters a b : 'I_n. (* use bigA_distr_big to prove the following *) Lemma bigA_distr_big_test : (a + b)^2 = a^2 + 2 * a * b + b^2. Proof. case: (boolP (a == b)) => [/eqP -> | ab]. ring. transitivity (\prod_(j : 'I_2) (\sum_(i in [predU (pred1 a) & (pred1 b)]) i)). rewrite big_ord_recr /=. rewrite big_ord_recr /=. rewrite big_ord0. rewrite mul1n. rewrite expnS. rewrite expn1. rewrite bigU /=; last first. by rewrite disjoint1. rewrite (big_pred1 a) //. by rewrite (big_pred1 b). rewrite bigA_distr_big /=. pose f1 := [ffun x : 'I_2 => match x with Ordinal O _ => a | Ordinal 1 _ => a | _ => a end]. pose f2 := [ffun x : 'I_2 => match x with Ordinal O _ => a | Ordinal 1 _ => b | _ => a end]. pose f3 := [ffun x : 'I_2 => match x with Ordinal O _ => b | Ordinal 1 _ => a | _ => a end]. pose f4 := [ffun x : 'I_2 => match x with Ordinal O _ => b | Ordinal 1 _ => b | _ => a end]. have f1f2 : f1 != f2. apply/eqP/ffunP. move/(_ (@Ordinal _ 1 _)). move/(_ erefl). rewrite !ffunE. by apply/eqP. have f1f3 : f1 != f3. apply/eqP/ffunP. move/(_ (@Ordinal _ 0 _)). move/(_ erefl). rewrite !ffunE. by apply/eqP. have f1f4 : f1 != f4. apply/eqP/ffunP. move/(_ (@Ordinal _ 0 _)). move/(_ erefl). rewrite !ffunE. by apply/eqP. have f2f3 : f2 != f3. apply/eqP/ffunP. move/(_ (@Ordinal _ 0 _)). move/(_ erefl). rewrite !ffunE. by apply/eqP. have f2f4 : f2 != f4. apply/eqP/ffunP. move/(_ (@Ordinal _ 0 _)). move/(_ erefl). rewrite !ffunE. by apply/eqP. have f3f4 : f3 != f4. apply/eqP/ffunP. move/(_ (@Ordinal _ 1 _)). move/(_ erefl). rewrite !ffunE. by apply/eqP. set tmp := ffun_on _. transitivity (\sum_(f in [predU (pred1 f1) & [predU (pred1 f2) & [predU (pred1 f3) & (pred1 f4)]]]) \prod_(i < 2) f i). apply eq_bigl => /= f. move H : (f \in tmp) => [|]. apply/esym. rewrite !inE /=. move/familyP : (H). move/(_ (@Ordinal _ O _)). move/(_ erefl). rewrite /= !inE. case/orP => /eqP H1. - move/familyP : (H). move/(_ (@Ordinal _ 1 _)). move/(_ erefl). rewrite /= !inE. case/orP => /eqP H2. + rewrite (_ : f == f1) //. apply/eqP/ffunP. case. case => [i|]. rewrite ffunE /= -H1. congr (f (Ordinal _)). by apply eq_irrelevance. case=> i //. rewrite ffunE /= -H2. congr (f (Ordinal _)). by apply eq_irrelevance. + rewrite (_ : f == f2). by rewrite orbC. apply/eqP/ffunP. case. case => [i|]. rewrite ffunE /= -H1. congr (f (Ordinal _)). by apply eq_irrelevance. case=> i //. rewrite ffunE /= -H2. congr (f (Ordinal _)). by apply eq_irrelevance. - move/familyP : (H). move/(_ (@Ordinal _ 1 _)). move/(_ erefl). rewrite /= !inE. case/orP => /eqP H2. + rewrite (_ : f == f3). by rewrite orbA /= orbC. apply/eqP/ffunP. case. case => [i|]. rewrite ffunE /= -H1. congr (f (Ordinal _)). by apply eq_irrelevance. case=> i //. rewrite ffunE /= -H2. congr (f (Ordinal _)). by apply eq_irrelevance. + rewrite (_ : f == f4). by rewrite 2!orbA orbC. apply/eqP/ffunP. case. case => [i|]. rewrite ffunE /= -H1. congr (f (Ordinal _)). by apply eq_irrelevance. case=> i //. rewrite ffunE /= -H2. congr (f (Ordinal _)). by apply eq_irrelevance. apply/esym/negbTE. rewrite !inE /=. move/negbT: H; apply contra => H. apply/familyP. case/orP : H. move/eqP => ->. case. case => [i|]. by rewrite !inE ffunE eqxx. case=> // i. by rewrite !inE ffunE eqxx. case/orP. move/eqP => ->. case. case=> [i|]. by rewrite !inE ffunE eqxx. case=> // i. by rewrite !inE ffunE eqxx orbC. case/orP. move/eqP => ->. case. case=> [i|]. by rewrite !inE ffunE eqxx orbC. case=> // i. by rewrite !inE ffunE eqxx. move/eqP => ->. case. case=> [i|]. by rewrite !inE ffunE eqxx orbC. case=> // i. by rewrite !inE ffunE eqxx orbC. rewrite bigU /=; last first. by rewrite disjoint1 !inE /= negb_or f1f2 /= negb_or f1f3 f1f4. rewrite bigU /=; last first. by rewrite disjoint1 !inE /= negb_or /= f2f3 f2f4. rewrite bigU /=; last first. by rewrite disjoint1 !inE /=. rewrite (big_pred1 f1) // (big_pred1 f2) // (big_pred1 f3) // (big_pred1 f4) //. rewrite !big_ord_recr /= !big_ord0 !mul1n !ffunE /=. ring. Qed.