Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype.
Require Import tuple finfun div path bigop prime.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

(* The following lemma is already proved as in the examples file, but you may
  want to prove it in a different way, by induction on n.

  This lemma also exists in the library (part of binomial.v) *)

Lemma sumP' : forall n, \sum_(i < n) i = (n * n.-1) ./2.
Proof.
move => n.
suff <- : (2 * \sum_(i < n) i) = n * n.-1 by rewrite -divn2 mulKn.
elim: n => [ | n h].
  by rewrite big_ord0 mul0n muln0.
rewrite succnK big_ord_recr muln_addr h.
rewrite /ord_max /=.
case : n {h} => [| n] /=.
  by rewrite !muln0 addn0.
rewrite mulnC !mulSn mul0n.
by rewrite addnC addn0 !addnA.
Qed.

(* You can prove this one in two fashions.
   1/ by induction on n.
   2/ by spliting and distributivity, then re-using sumP'.  But division by
   two is a pain in the neck.  *)
Lemma sum_odd1 : forall n, \sum_(i < n) (2 * i + 1) = n ^ 2.
Proof.
move => n; rewrite big_split -big_distrr /= sumP'.
rewrite sum_nat_const card_ord.
case: n => [ | n].
  by rewrite expnS !mul0n muln0.
rewrite muln1 succnK mul2n -[_.*2]add0n -{1}(_ : odd(n.+1 * n) = 0 :> nat).
  by rewrite odd_double_half expnS expn1 [_ * n.+1]mulSn addnC mulnC.
Search _ odd S.
Search _ odd muln.
rewrite odd_mul.
case h : (odd n.+1) => //.
by move: h => /=; move/negb_true_iff => ->.
(* Alternative solution
elim => [ | n h].
  by rewrite big_ord0 exp0n.
rewrite big_ord_recr h. rewrite /= !expnS !expn0. ring.
*)
Qed.

Lemma ex1 : forall n f, \sum_(i < n) (f i + 1) = n + \sum_(i < n) f i.
Proof.
move => n f; apply/eqP; rewrite big_split /= addnC eqn_addr.
by rewrite big_const_ord; elim : n {f} => [ | n]//.
(* alternative ending: by rewrite sum_nat_const card_ord muln1. *)
Qed.

Lemma fact_big : forall n, n`! = \prod_(1 <= i < n.+1) i.
Proof.
elim => [ | n h].
  by rewrite fact0 big_geq.
rewrite big_add1 /=.
rewrite factS h big_add1 /=.
by rewrite big_nat_recr mulnC.
Qed.

(* use the previous lemma for this proof. This is an opportunity to use big_prop. *)
Lemma prime_lt_Ndiv_fact :
  forall p n, prime p -> n < p -> ~~ (p %| n`!).
Proof.
move => p n pp np.
rewrite fact_big.
rewrite big_cond_seq.
elim/big_prop : _ => //.
    by rewrite euclid1.
  by move => x y px py; rewrite euclid // (negPf px) (negPf py).
Search _ (_ \in index_iota _ _).
move => i /=; rewrite mem_index_iota => /andP. move => [h1 h2].
rewrite gtnNdvd //.
by apply: leq_trans np.
Qed.

Lemma sum_exp : forall x n, 0 < x -> x ^ n.+1 - 1 = (x - 1) * \sum_(i < n.+1) x ^ i.
move => x n x0; elim: n => [| n h].
  by rewrite big_ord_recl expn0 big_ord0 addn0 muln1 expn1.
rewrite expnS.
  have h' : x ^ n.+1 = (x ^ n.+1 - 1) + 1.
  by rewrite subnK // expn_gt0 x0.
rewrite h' h mulnC muln_addl mul1n.
rewrite -addn_subA // -{2}[x - 1]muln1 -mulnA -muln_addr addnC -{2}(expn0 x).
rewrite big_distrl /=.
have -> : (\sum_(i < n.+1) x ^ i * x) = \sum_(i < n.+1) x ^ (lift ord0 i).
apply: eq_bigr.
  by move => i _; rewrite expnS mulnC.
by rewrite [X in _ = _ * X]big_ord_recl.
Qed.

Section abstract.

Variable A : Type.
Variables ad mu : A -> A -> A.
Variable op : A -> A.
Variables a0 a1 : A.

Hypothesis adC : commutative ad.
Hypothesis muC : commutative mu.
Hypothesis adA : associative ad.
Hypothesis muA : associative ad.
Hypothesis ad0a : left_id a0 ad.
Hypothesis ada0 : right_id a0 ad.
Hypothesis mu0a : left_zero a0 mu.
Hypothesis mua0 : right_zero a0 mu.
Hypothesis mu1a : left_id a1 mu.
Hypothesis mua1 : right_id a1 mu.
Hypothesis mu_adl : left_distributive mu ad.
Hypothesis mu_adr : right_distributive mu ad.
Hypothesis adN : forall a, ad a (op a) = a0.

Variable exp : A -> nat -> A.
Hypothesis exp0 : forall x, exp x 0 = a1.
Hypothesis expS : forall x n, exp x n.+1 = mu x (exp x n).
Hypothesis muVop1 : forall x, op x = mu (op a1) x.

Local Notation "x ^ n" := (exp x n).
Local Notation "a + b" := (ad a b).
Local Notation "a * b" := (mu a b).
Local Notation "a - b" := (ad a (op b)).

(* Add the relevant canonical structures to allow using natural operations on
  this addition, and multiplication.  *)


Canonical adMon : Monoid.law a0 :=
  Monoid.Law adA ad0a ada0.

Canonical Structure adCom : Monoid.com_law a0 :=
  Monoid.ComLaw adC.

Canonical Structure adadd : Monoid.add_law a0 mu:=
  Monoid.AddLaw mu_adl mu_adr.

Canonical Structure mumul : Monoid.mul_law a0 :=
  Monoid.MulLaw mu0a mua0.

Lemma sum_exp' : forall x n,  x ^ n.+1 - a1 = (x - a1) * \big[ad/a0]_(i < n.+1) x ^ i.
move => x n.
rewrite big_distrr /=.
rewrite (eq_bigr (fun i : 'I_n.+1 => x ^ i.+1 + (op a1) * x ^ i)); last first.
  by move => i _; rewrite mu_adl expS.
rewrite big_split /= -big_distrr /=.
rewrite big_ord_recr big_ord_recl /=.
rewrite [_ + x ^ n.+1]adC -!adA; congr ad.
rewrite exp0 adC mu_adr mua1.
(* rewrite (eq_bigr (fun i : 'I_n => x ^ i.+1)) // *)
rewrite /bump /=.
by rewrite -adA -{2}[\big[_ /_]_(_ <- _) _]mu1a -mu_adl [_ + a1]adC adN mu0a ada0.
Qed.

End abstract.