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

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

Section test.

Variables (op1 : nat -> nat -> nat) (v : nat).

Lemma cmp_op3 : \big[op1/v]_(1 <= i < 3) i = op1 1 (op1 2 v).
Proof.
rewrite big_ltn.
  rewrite big_ltn; last by [].
  rewrite big_geq.
    by [].
  by [].  
by [].
Qed.

End test.

Lemma s3' : \sum_(i < 3) i = 3.
Proof.
rewrite big_ord_recr.
rewrite big_ord_recr /=.
rewrite big_ord_recr /=.
rewrite big_ord0.
by [].
Qed.

Lemma sumnP : forall n, \sum_(i < n) i = (n * n.-1) %/2.
Proof. 
move => n.
suff <- : (2 * \sum_(i < n) i) = n * n.-1 by rewrite mulKn.
rewrite mulSn mul1n.
rewrite {2}(reindex_inj rev_ord_inj) -big_split /=.
rewrite (eq_bigr (fun i => n.-1)).
  by rewrite sum_nat_const card_ord.
by move => i _; rewrite -[_ + _]succnK -addSn subnKC.
Qed.

Lemma sum_sq_leq : forall n, \sum_(i < n) i^2 <= n^3.
move => n.
apply: leq_trans (_ : \sum_(i < n) n^2 <= n^3).
  elim/big_rel: _ => //.
    by move => *; apply: leq_add.
  by move => [i il] _; rewrite leq_sqr ltnW.
by rewrite sum_nat_const card_ord -expnS.
Qed.

Lemma geq_max : forall n p f, 0 < p -> (forall i : 'I_n, f i < p) -> \max_i f i < p.
move => n p f p0 fp.
have pm : {morph (fun u => u < p) : x y / maxn x y >-> x && y}.
  move => x y /=.
Search _ maxn andb.
  rewrite -leq_maxl.
  rewrite /maxn.
  rewrite ltnS.
  by case : (x < y).
rewrite (big_morph _ pm p0).
Search _ (\big[andb/true]_(_ <- _ | _) _).
rewrite big_andE.
apply/forallP.
rewrite /=.
by [].
Qed.


Section canonical_example.

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 cmp_op3' : \big[op2/0]_(i < 3) i = 3.
Proof.
rewrite big_ord_recr /=.
rewrite big_ord_recr /=.
rewrite big_ord_recr /=.
rewrite big_ord0.
by rewrite !op2add.
Qed.

End canonical_example.