Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import ssrbool ssrfun ssrnat eqtype fintype choice seq.
From mathcomp Require Import finset bigop path binomial.

Set Implicit Arguments.


#[export] Hint Resolve nth_nil addn0 : core.

Lemma leq_addE m1 m2 n1 n2 :
  m1 <= m2 -> n1 <= n2 -> m1 + n1 = m2 + n2 -> m1 = m2 /\ n1 = n2.

Section SeqLemmas.

Variable (T : eqType).
Implicit Type s w : seq T.
Implicit Type a b : T.

Lemma drop_nilE s m :
  (drop m s == [::]) = (size s <= m).

Lemma cons_head_behead x s : (s != [::]) -> head x s :: behead s = s.

Lemma belast_behead_rcons x l s :
  belast (head x (rcons s l)) (behead (rcons s l)) = s.

Lemma last_behead_rcons x l s :
  last (head x (rcons s l)) (behead (rcons s l)) = l.

Lemma set_head_default b a s : s != [::] -> head a s = head b s.

Lemma rcons_set_nth a s l : set_nth a s (size s) l = rcons s l.

Lemma set_nth_rcons x0 s x n y :
  set_nth x0 (rcons s x) n y =
  if n < size s then rcons (set_nth x0 s n y) x
  else if n == size s then rcons s y
       else (rcons s x) ++ ncons (n - size s).-1 x0 [:: y].

Lemma rconsK a b u v : rcons u a = rcons v b -> u = v.

Lemma rcons_nilF s l : ((rcons s l) == [::]) = false.

Lemma cons_in_map_cons a b s w (l : seq (seq T)) :
  a :: s \in [seq b :: s1 | s1 <- l] -> a == b.

Lemma count_rcons w P l :
  count P (rcons w l) = count P w + P l.

Lemma set_nth_non_nil d s n y : set_nth d s n y != [::].

Lemma nth_set_nth_expand a b l i c j :
  (size l <= j < i) -> nth a (set_nth b l i c) j = b.

Lemma nth_set_nth_any a b l i c j :
  nth a (set_nth b l i c) j =
  if j == i then c else
    if j < size l then nth a l j else
      if j <= i then b else a.

Lemma eq_from_nth_notin x0 s1 s2 :
  x0 \notin s1 -> x0 \notin s2 ->
  (forall i : nat, nth x0 s1 i = nth x0 s2 i) -> s1 = s2.

End SeqLemmas.

Lemma minSS i j : minn i.+1 j.+1 = (minn i j).+1.

Lemma leq_sumn_in (sh : seq nat) i : i \in sh -> i <= sumn sh.

Lemma sumn_map_condE (T : Type) (s : seq T) (f : T -> nat) (P : pred T) :
  sumn [seq f i | i <- s & P i] = \sum_(i <- s | P i) f i.

Lemma sumn_mapE (T : Type) (s : seq T) (f : T -> nat) :
  sumn [seq f i | i <- s] = \sum_(i <- s) f i.

Lemma sum_minn s b :
  \sum_(l <- s) minn l b = sumn s - \sum_(l <- s) (l - b).

Lemma sum_take r s F :
  F 0 = 0 -> \sum_(l <- take r s) F l = \sum_(0 <= i < r) F (nth 0 s i).

Lemma sumn_take r s : sumn (take r s) = \sum_(0 <= i < r) nth 0 s i.
Lemma sumn_drop r s : sumn (drop r s) = \sum_(r <= i < size s) nth 0 s i.

Lemma sumn_nth_le l n :
  size l <= n -> sumn l = \sum_(0 <= i < n) nth 0 l i.

Lemma binomial_sumn_iota n : 'C(n, 2) = sumn (iota 0 n).

Lemma sumn_pred1_iota a b x :
  sumn [seq ((i == x) : nat) | i <- iota a b] = (a <= x < a + b).

Lemma count_mem_iota a b i :
  count_mem i (iota a b) = (a <= i < a + b).

Lemma iota_ltn a b : b <= a -> [seq i <- iota 0 a | i < b] = iota 0 b.

Lemma iota_geq a b : [seq i <- iota 0 a | b <= i] = iota b (a - b).

Section FinSet.

Variable T : finType.

Lemma setU1E (x : T) (S : {set T}) : (x \in S) = (x |: S == S).

End FinSet.

Lemma uniq_sum_count_mem (T : eqType) (P : pred T) l s :
  uniq s ->
  \sum_(i <- s | P i) (count_mem i) l = count (predI (mem s) P) l.

Lemma sumn_sort l S : sumn (sort S l) = sumn l.

Lemma map_filter_comp (T1 T2: Type) (l : seq T1) (PP : pred T2) (F : T1 -> T2) :
  [seq F i | i <- l & PP (F i)] = [seq i | i <- map F l & PP i ].

Lemma set1_disjoint (T : finType) (i j : T) :
  [set i] != [set j] -> [disjoint [set i] & [set j]].

Lemma subset_imsetK (T1 T2 : finType) (f : T1 -> T2) (s t : {set T1}):
  injective f -> f @: s \subset f @: t -> s \subset t.

Section SSRComplFinset.

Variables aT rT : finType.
Variables (f : aT -> rT).

Lemma imsetD (A B : {set aT}) :
  {in A :|: B &, injective f} -> f @: (B :\: A) = (f @: B) :\: (f @: A).

End SSRComplFinset.

Section ImsetInj.

Variables (T T1 T2 : finType) (f : T1 -> T2).

Lemma preimset_trivIset (P : {set {set T2}}) :
  trivIset P -> trivIset ((fun s : {set T2} => f @^-1: s) @: P).

Hypothesis (f_inj : injective f).

Lemma imset_inj : injective (fun s : {set T1} => imset f (mem s)).

Lemma imset_trivIset (P : {set {set T1}}) :
  trivIset P -> trivIset ((fun s : {set T1} => f @: s) @: P).

Lemma disjoint_imset (A B : {set T1}) :
  [disjoint A & B] -> [disjoint [set f x | x in A] & [set f x | x in B]].

End ImsetInj.

Lemma uniq_next (T : eqType) (p : seq T) : uniq p -> injective (next p).

Lemma mem_takeP (T : eqType) x0 x k (s : seq T) :
  reflect (exists2 i, i < minn k (size s) & x = nth x0 s i) (x \in take k s).

Lemma mem_take_enumI n (i : 'I_n) k : i \in take k (enum 'I_n) = (i < k).

Lemma take_enumI n k : take k (enum 'I_n) = filter ((gtn k) \o val) (enum 'I_n).

Lemma mem_drop_enumI n (i : 'I_n) k : i \in drop k (enum 'I_n) = (i >= k).

Lemma drop_enumI n k : drop k (enum 'I_n) = filter ((leq k) \o val) (enum 'I_n).

Lemma enum0 : enum 'I_0 = [::].

Section AbelianBigOp.

Import Monoid.Theory.

Variable R : Type.
Variable idx : R.
#[local] Notation "1" := idx.
Variable op : Monoid.com_law 1.
#[local] Notation "'*%M'" := op (at level 0).
#[local] Notation "x * y" := (op x y).

Lemma big_seq_sub (T : countType) (s : seq T) F :
  \big[op/idx]_(x : seq_sub s) F (ssval x) = \big[op/idx]_(x <- undup s) F x.

End AbelianBigOp.
Arguments partition_big [R idx op I s J P] p Q [F].

Section SetPartition.

Variable T : finType.
Implicit Types (X : {set T}) (P : {set {set T}}).

Lemma triv_part P X : X \in P -> partition P X -> P = [set X].

End SetPartition.

Notation "#{ x }" := #|(x : {set _})|
                      (at level 0, x at level 10, format "#{ x }").