From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

(**
  ----
  ** Exercise 1 *)

(**
Try to define a next function over 'I_n that correspond to the
successor function over the natural plus the special case that
"n -1" is mapped to zero *)

Definition onext n (x : 'I_n) : 'I_n.
case: n x => [| n] x.
  exact: x.
exists (x.+1 %%n.+1).
  by apply: ltn_pmod.
Defined.

Eval compute in val (onext (Ordinal (isT : 2 < 4))).
Eval compute in val (onext (Ordinal (isT : 3 < 4))).

(**
  ----
  ** Exercise 2 
*)

(**
   Show that injectivity is decidable for a function f : aT -> rT
   with  aT a finite 
*) 

Module MyInj.

Check injective.

Definition injectiveb (aT : finType) (rT : eqType) (f : aT -> rT) : bool :=
 [forall x : aT, forall y : aT, (f x == f y) ==> (x == y)].

Lemma injectiveP (aT : finType) (rT : eqType) (f : aT -> rT) : 
  reflect (injective f) (injectiveb f).
Proof.
apply: (iffP forallP) => [Ibf x y Efxy|If x].
  by move: Ibf => /(_ x) /forallP /(_ y); rewrite Efxy eqxx => /eqP.
by apply/forallP=> y; apply/implyP => /eqP Efxy; apply/eqP; apply: If.
Qed.

End MyInj.

(** 
  ----
  ** Exercise 3 
*)

(** 
   Try to formalize the following problem 
*)

(** 
  Given a parking  where the boolean indicates if the slot is occupied or not 
*)

Definition parking n := 'I_n -> 'I_n -> bool.

(**
   Number of cars at line i 
*)               

Definition sumL n (p : parking n) i := \sum_(j < n) p i j.

(**
   Number of cars at column j 
*)

Definition sumC n (p : parking n) j := \sum_(i < n) p i j.

(**
   Show that if 0 < n there is always two lines, or two columns, or a column and a line
   that have the same numbers of cars 
*)

(* Two intermediate lemmas to use injectivity  *)

Lemma leq_sumL n (p : parking n) i : sumL p i < n.+1.
Proof.
have {2}<-: \sum_(i < n) 1 = n by rewrite -[X in _ = X]card_ord sum1_card.
by apply: leq_sum => k; case: (p _ _).
Qed.

Lemma leq_sumC n (p : parking n) j : sumC p j < n.+1.
Proof.
have {2}<-: \sum_(i < n) 1 = n by rewrite -[X in _ = X]card_ord sum1_card.
by apply: leq_sum => k; case: (p _ _).
Qed.

Lemma inl_inj {A B} : injective (@inl A B). Proof. by move=> x y []. Qed.
Lemma inr_inj {A B} : injective (@inr A B). Proof. by move=> x y []. Qed.

Lemma result n (p : parking n) : 0 < n ->
  exists i, exists j,
   [\/  (i != j) /\ (sumL p i = sumL p j),
        (i != j) /\ (sumC p i = sumC p j) | sumL p i = sumC p j].
Proof.
case: n p => [//|[|n]] p _ /=.
  exists ord0, ord0; apply: Or33.
  by rewrite /sumL /sumC !big_ord_recl !big_ord0.
pose sLC (i : 'I_n.+2 + 'I_n.+2) :=
  match i with
  | inl i => Ordinal (leq_sumL p i)
  | inr i => Ordinal (leq_sumC p i) end.
have [sC_inj | /injectivePn /=] := altP (injectiveP sLC).
  have := max_card (mem (codom sLC)); rewrite card_codom // card_sum !card_ord.
  by rewrite !addnS !addSn !ltnS -ltn_subRL subnn ltn0.
move=> [[i|i] [[j|j] //=]]; [| |move: i j => j i|];
rewrite ?(inj_eq inj_inl, inj_eq inj_inr) => neq_ij [];
by exists i, j; do ?[exact: Or31|exact: Or32|exact: Or33].
Qed.

(** 
  ----
  ** Exercise 4 
*)

(** 
   Prove the following state by induction and by following Gauss proof.
 *)

Lemma gauss_ex_p1 : forall n, (\sum_(i < n) i).*2 = n * n.-1.
Proof.
elim=> [|n IH]; first by rewrite big_ord0.
rewrite big_ord_recr /= doubleD {}IH.
case: n => [|n /=]; first by rewrite muln0.
by rewrite -muln2 -mulnDr addn2 mulnC.
Qed.

Lemma gauss_ex_p2 : forall n, (\sum_(i < n) i).*2 = n * n.-1.
Proof.
case=> [|n/=]; first by rewrite big_ord0.
rewrite -addnn.
have Hf i : n - i < n.+1.
  by apply: leq_trans (leq_subr _ _) _.
pose f (i : 'I_n.+1) := Ordinal (Hf i).
have f_inj : injective f.
  move=> x y /val_eqP/eqP H.
  apply/val_eqP => /=.
  rewrite -(eqn_add2l (n - x)) subnK -1?ltnS  //.
  by rewrite [n - x]H subnK -1?ltnS.
rewrite {1}(reindex_inj f_inj) -big_split /=.
rewrite -[X in _ = X * _]card_ord -sum_nat_const.
by apply: eq_bigr => i _; rewrite subnK // -ltnS.
Qed.

Lemma gauss_ex_p3 : forall n, (\sum_(i < n) i).*2 = n * n.-1.
Proof.
case=> [|n/=]; first by rewrite big_ord0.
rewrite -addnn {1}(reindex_inj rev_ord_inj) -big_split /=.
rewrite -[X in _ = X * _]card_ord -sum_nat_const.
by apply: eq_bigr => i _; rewrite subSS subnK // -ltnS.
Qed.

(** 
  ----
   ** Exercise 5 
*)

Lemma sum_odd1 : forall n, \sum_(i < n) (2 * i + 1) = n ^ 2.
Proof.
case=> [|n/=]; first by rewrite big_ord0.
rewrite big_split -big_distrr /= mul2n gauss_ex_p3 sum_nat_const.
by rewrite card_ord -mulnDr addn1 mulnn.
Qed.

(** 
  ----
  ** Exercise 6 
*)

Lemma sum_exp : forall x n, x ^ n.+1 - 1 = (x - 1) * \sum_(i < n.+1) x ^ i.
Proof.
move=> x n.
rewrite mulnBl big_distrr mul1n /=.
rewrite big_ord_recr [X in _ = _ - X]big_ord_recl /=.
rewrite [X in _ = _ - (_ + X)](eq_bigr (fun i : 'I_n =>  x * x ^ i))
      => [|i _]; last by rewrite -expnS.
rewrite [X in _ = X - _]addnC [X in _ = _ - X]addnC subnDA addnK.
by rewrite expnS expn0.
Qed.

(**
  ----
 ** Exercise 7 
*)

(** Prove the following state by induction and by using a similar trick
   as for Gauss noticing that n ^ 3 = n * (n ^ 2) *)

Lemma bound_square : forall n, \sum_(i < n) i ^ 2 <= n ^ 3.
Proof.
move=> n.
rewrite expnS -[X in _ <= X * _]card_ord -sum_nat_const /=.
elim/big_ind2: _ => // [* |i]; first exact: leq_add.
by rewrite leq_exp2r // ltnW.
Qed.

(**
  ----
  ** Exercise 8 
*)

(**
  building a monoid law 
*)

Section cex.

Variable op2 : nat -> nat -> nat.

Hypothesis op2n0 : right_id 0 op2.

Hypothesis op20n : left_id 0 op2.

Hypothesis op2A : associative op2.

Hypothesis op2add : forall x y, op2 x y = x + y.

Canonical Structure op2Mon : Monoid.law 0 :=
  Monoid.Law op2A op20n op2n0.

Lemma ex_op2 : \big[op2/0]_(i < 3) i = 3.
Proof. 
by rewrite !big_ord_recr big_ord0 /= !op2add. 
Qed.

End cex.