(* -------------------------------------------------------------------- *)
(* Copyright (c) - 2015--2016 - IMDEA Software Institute                *)
(* Copyright (c) - 2015--2018 - Inria                                   *)
(* Copyright (c) - 2016--2018 - Polytechnique                           *)

(* -------------------------------------------------------------------- *)
From mathcomp Require Import all_ssreflect all_algebra.
Notation "[ predI _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ predU _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ predD _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ predC _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ preim _ of _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
New coercion path [GRing.subring_closedM;
                   GRing.smulr_closedN] : GRing.subring_closed >-> GRing.oppr_closed is ambiguous with existing 
[GRing.subring_closedB; GRing.zmod_closedN] : GRing.subring_closed >-> GRing.oppr_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.subring_closed_semi;
                   GRing.semiring_closedM] : GRing.subring_closed >-> GRing.mulr_closed is ambiguous with existing 
[GRing.subring_closedM; GRing.smulr_closedM] : GRing.subring_closed >-> GRing.mulr_closed.
New coercion path [GRing.subring_closed_semi;
                   GRing.semiring_closedD] : GRing.subring_closed >-> GRing.addr_closed is ambiguous with existing 
[GRing.subring_closedB; GRing.zmod_closedD] : GRing.subring_closed >-> GRing.addr_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.sdivr_closed_div;
                   GRing.divr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed is ambiguous with existing 
[GRing.sdivr_closedM; GRing.smulr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.subalg_closedBM;
                   GRing.subring_closedB] : GRing.subalg_closed >-> GRing.zmod_closed is ambiguous with existing 
[GRing.subalg_closedZ; GRing.submod_closedB] : GRing.subalg_closed >-> GRing.zmod_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.divring_closed_div;
                   GRing.sdivr_closedM] : GRing.divring_closed >-> GRing.smulr_closed is ambiguous with existing 
[GRing.divring_closedBM; GRing.subring_closedM] : GRing.divring_closed >-> GRing.smulr_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.divalg_closedBdiv;
                   GRing.divring_closedBM] : GRing.divalg_closed >-> GRing.subring_closed is ambiguous with existing 
[GRing.divalg_closedZ; GRing.subalg_closedBM] : GRing.divalg_closed >-> GRing.subring_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.Pred.subring_smul;
                   GRing.Pred.smul_mul] : GRing.Pred.subring >-> GRing.Pred.mul is ambiguous with existing 
[GRing.Pred.subring_semi; GRing.Pred.semiring_mul] : GRing.Pred.subring >-> GRing.Pred.mul.
[ambiguous-paths,typechecker]
From mathcomp Require Export finmap.

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

Import Order.TTheory GRing.Theory Num.Theory.

Local Open Scope ring_scope.
Local Open Scope fset_scope.

(* -------------------------------------------------------------------- *)
Lemma uniq_fset_keys {K : choiceType} (J : {fset K}) : uniq (enum_fset J).
K: choiceType
J: {fset K}
uniq J
Proof.
2 by case: J => J /= /canonical_uniq. Qed.

#[global] Hint Resolve uniq_fset_keys : core.

(* -------------------------------------------------------------------- *)
Lemma enum_fset0 (T : choiceType) :
  enum [finType of fset0] = [::] :> seq (@fset0 T).
T: choiceType
enum [finType of fset0] = [::]
Proof.
a by rewrite enumT unlock. Qed.

Lemma enum_fset1 (T : choiceType) (x : T) :
  enum [finType of [fset x]] = [:: [`fset11 x]].
d
x: T
enum [finType of [fset x]] = [:: [` fset11 x]]
Proof.
11
apply/perm_small_eq=> //; apply/uniq_perm => //.
13
uniq (enum [finType of [fset x]])
13
enum [finType of [fset x]] =i [:: [` fset11 x]]
  by apply/enum_uniq.
13
1d
case=> [y hy]; rewrite mem_seq1 mem_enum /in_mem /=.
d
x, y: T
hy: y \in [fset x]
true = ([` hy] == [` fset11 x])
by rewrite eqE /=; rewrite in_fset1 in hy.
Qed.

(* -------------------------------------------------------------------- *)
Section BigFSet.
Variable (R : Type) (idx : R) (op : Monoid.law idx).
Variable (I : choiceType).

Lemma big_fset0_cond (P : pred _) (F : _ -> R) :
  \big[op/idx]_(i : @fset0 I | P i) F i = idx :> R.
R: Type
idx: R
op: Monoid.law idx
I: choiceType
P: pred fset0
F: fset0 -> R
\big[op/idx]_(i | P i) F i = idx
Proof.
29 by apply: big_pred0 => -[j hj]; have := hj; rewrite in_fset0. Qed.

Lemma big_fset0 (F : @fset0 I -> R) :
  \big[op/idx]_(i : fset0) F i = idx.
2c
2d
2e
2f
31
\big[op/idx]_i F i = idx
Proof.
35 by rewrite /index_enum -enumT /= enum_fset0 big_nil. Qed.

Lemma big_fset1 (a : I) (F : [fset a] -> R) :
  \big[op/idx]_(i : [fset a]) F i = F (FSetSub (fset11 a)).
2c
2d
2e
2f
a: I
F: [fset a] -> R
\big[op/idx]_i F i = (F.[fset11 a])%fmap
Proof.
3b by rewrite /index_enum -enumT enum_fset1 big_seq1. Qed.
End BigFSet.

(* -------------------------------------------------------------------- *)
Section BigFSetCom.
Variable (R : Type) (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_fset_seq_cond (T : choiceType) (J : {fset T}) P F :
    \big[*%M/1]_(x : J | P (val x)) F (val x)
  = \big[*%M/1]_(x <- enum_fset J | P x) F x.
2c
2d
op: Monoid.com_law 1
d
J: {fset T}
P: T -> bool
F: T -> R
\big[*%M/1]_(x | P (val x)) F (val x) =
\big[*%M/1]_(x <- J | P x) F x
Proof.
43
case: J=> J c; rewrite -(big_map val) /index_enum.
2c
2d
46
d
48
49
J: seq T
c: canonical_keys J
\big[*%M/1]_(i <- [seq val i
                     | i <- locked_with index_enum_key
                              (Finite.enum
                                 (fset_sub_finType
                                    (mkFinSet c)))] | 
P i) F i = \big[*%M/1]_(x <- mkFinSet c | P x) F x
by rewrite !unlock val_fset_sub_enum ?canonical_uniq.
Qed.

Lemma big_fset_seq (T : choiceType) (J : {fset T}) F :
    \big[*%M/1]_(x : J) F (val x)
  = \big[*%M/1]_(x <- enum_fset J) F x.
2c
2d
46
d
47
49
\big[*%M/1]_x F (val x) = \big[*%M/1]_(x <- J) F x
Proof.
54 by apply/big_fset_seq_cond. Qed.

Lemma big_seq_fset_cond (T : choiceType) (s : seq T) P F : uniq s ->
    \big[*%M/1]_(x : [fset x in s] | P (val x)) F (val x)
  = \big[*%M/1]_(x <- s | P x) F x.
2c
2d
46
d
s: seq T
48
49
uniq s ->
\big[*%M/1]_(x | P (val x)) F (val x) =
\big[*%M/1]_(x <- s | P x) F x
Proof.
5a
move=> eq_s; rewrite big_fset_seq_cond; apply/perm_big.
2c
2d
46
d
5d
48
49
eq_s: uniq s
perm_eq [fset x | x in s] s
by apply/uniq_perm=> //= x; rewrite in_fset.
Qed.

Lemma big_seq_fset (T : choiceType) (s : seq T) F : uniq s ->
    \big[*%M/1]_(x : [fset x in s]) F (val x)
  = \big[*%M/1]_(x <- s) F x.
2c
2d
46
d
5d
49
uniq s ->
\big[*%M/1]_x F (val x) = \big[*%M/1]_(x <- s) F x
Proof.
67 by apply/big_seq_fset_cond. Qed.
End BigFSetCom.

Arguments big_fset_seq_cond [R idx op T J] P F.
Arguments big_fset_seq [R idx op T J] F.
Arguments big_seq_fset_cond [R idx op T s] P F _.
Arguments big_seq_fset [R idx op T s] F _.

(* -------------------------------------------------------------------- *)
Section BigFSetU.
Context {R : Type} {T : choiceType} (idx : R) (op : Monoid.com_law idx).

Lemma big_fsetU (A B : {fset T}) F : [disjoint A & B] ->
  \big[op/idx]_(j : A `|` B) F (val j) =
    op (\big[op/idx]_(j : A) F (val j))
       (\big[op/idx]_(j : B) F (val j)).
2c
d
2d
op: Monoid.com_law idx
A, B: {fset T}
49
[disjoint A & B] ->
\big[op/idx]_j F (val j) =
op (\big[op/idx]_j F (val j))
  (\big[op/idx]_j F (val j))
Proof.
6d
move=> dj_AB; rewrite !big_fset_seq -big_cat; apply/perm_big.
2c
d
2d
70
71
49
dj_AB: [disjoint A & B]
perm_eq (A `|` B) (A ++ B)
apply/uniq_perm=> //.
77
uniq (A ++ B)
77
A `|` B =i A ++ B
+
7b rewrite cat_uniq ?uniq_fset_keys !(andbT, andTb); apply/hasPn => x /=.
2c
d
2d
70
71
49
78
14
x \in B -> x \notin A
7e
  by apply/fdisjointP; rewrite fdisjoint_sym.
77
80
+
88 by move=> x; rewrite mem_cat in_fsetE.
Qed.
End BigFSetU.

(* -------------------------------------------------------------------- *)
Section BigFSetOrder.
Variable (R : realDomainType) (T : choiceType).

Lemma big_fset_subset (I J : {fset T}) (F : T -> R) :
  (forall x, 0 <= F x) -> {subset I <= J} ->
    \sum_(i : I) F (val i) <= \sum_(j : J) F (val j).
R: realDomainType
d
I, J: {fset T}
49
(forall x : T, 0 <= F x) ->
{subset I <= J} ->
\sum_i F (val i) <= \sum_j F (val j)
Proof.
8c
move=> ge0_F le_IJ; rewrite !big_fset_seq /=.
8f
d
90
49
ge0_F: forall x : T, 0 <= F x
le_IJ: {subset I <= J}
\sum_(x <- I) F x <= \sum_(x <- J) F x
rewrite [X in _<=X](bigID [pred j : T | j \in I]) /=.
96
\sum_(x <- I) F x <=
(\sum_(i <- J | i \in I) F i +
 \sum_(i <- J | i \notin I) F i)%R
rewrite ler_paddr ?sumr_ge0 // -[X in _<=X]big_filter.
96
\sum_(x <- I) F x <=
\sum_(i <- [seq i <- J | i \in I]) F i
rewrite le_eqVlt; apply/orP; left; apply/eqP/perm_big.
96
perm_eq I [seq i <- J | i \in I]
apply/uniq_perm; rewrite ?filter_uniq //; last move=> i.
8f
d
90
49
97
98
i: T
(i \in I) = (i \in [seq i <- J | i \in I])
rewrite mem_filter; case/boolP: (_ \in _) => //=.
a9
i \in I -> true = (i \in J)
by move/le_IJ => ->.
Qed.

Lemma big_nat_mkfset (F : nat -> R) n :
  \sum_(0 <= i < n) F i =
    \sum_(i : [fset x in (iota 0 n)]) F (val i).
8f
d
F: nat -> R
n: nat
\sum_(0 <= i < n) F i = \sum_i F (val i)
Proof.
b1
rewrite -(big_map val xpredT) /=; apply/perm_big.
b3
perm_eq (index_iota 0 n)
  [seq fsval i
     | i <- index_enum
              (fset_sub_finType
                 [fset x | x in iota 0 n])]
apply/uniq_perm; rewrite ?iota_uniq //.
b3
uniq
  [seq fsval i
     | i <- index_enum
              (fset_sub_finType
                 [fset x | x in iota 0 n])]
b3
index_iota 0 n
  =i [seq fsval i
        | i <- index_enum
                 (fset_sub_finType
                    [fset x | x in iota 0 n])]
  rewrite map_inj_uniq /=; last apply/val_inj.
b3
uniq
  (index_enum
     (fset_sub_finType [fset x | x in iota 0 n]))
c0
  by rewrite /index_enum -enumT enum_uniq.
b3
c2
by move=> i; rewrite /index_enum -enumT -enum_fsetE in_fset /index_iota subn0.
Qed.

Lemma big_ord_mkfset (F : nat -> R) n :
  \sum_(i < n) F i =
    \sum_(i : [fset x in (iota 0 n)]) F (val i).
b3
\sum_(i < n) F i = \sum_i F (val i)
Proof.
cb by rewrite -(big_mkord xpredT) big_nat_mkfset. Qed.
End BigFSetOrder.

(* -------------------------------------------------------------------- *)
Lemma enum_fsetT {I : finType} :
  perm_eq (enum [fset i | i in I]) (enum I).
I: finType
perm_eq (enum [fset i | i in I]) (enum I)
Proof.
d0
apply/uniq_perm; rewrite ?enum_uniq //.
d2
enum [fset i | i in I] =i enum I
by move=> i /=; rewrite !mem_enum in_imfset.
Qed.

(* -------------------------------------------------------------------- *)