Module mathcomp.experimental_reals.xfinmap

From mathcomp Require Import boot order algebra.
From mathcomp Require Export finmap.

Unset SsrOldRewriteGoalsOrder.
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 { : choiceType} ( : {fset K}) : uniq (enum_fset J).

Proof.

by case: J => J /= /canonical_uniq. Qed.

#[global] Hint Resolve uniq_fset_keys : core.

Lemma ( : choiceType) :
enum (fset0 : finType) = [::] :> seq (@fset0 T).

Proof.

by rewrite enumT unlock. Qed.

Lemma ( : choiceType) ( : T) :
enum ([fset x] : finType) = [:: [`fset11 x]].

Proof.

apply/perm_small_eq=> //; apply/uniq_perm => //.
by apply/enum_uniq.
case=> [y hy]; rewrite mem_seq1 mem_enum /in_mem /=.
by rewrite eqE /=; rewrite in_fset1 in hy.
Qed.

Section BigFSet.
Variable ( : Type) ( : R) ( : Monoid.law idx).
Variable ( : choiceType).

Lemma ( : pred _) ( : _ -> R) :
\big[op/idx]_( : @fset0 I | P i) F i = idx :> R.

Proof.

by apply: big_pred0 => -[j hj]; have := hj; rewrite in_fset0. Qed.

Lemma ( : @fset0 I -> R) :
\big[op/idx]_( : fset0) F i = idx.

Proof.

by rewrite /index_enum -enumT /= enum_fset0 big_nil. Qed.

Lemma ( : I) ( : [fset a] -> R) :
\big[op/idx]_( : [fset a]) F i = F (FSetSub (fset11 a)).

Proof.

by rewrite /index_enum -enumT enum_fset1 big_seq1. Qed.

End BigFSet.

Section BigFSetCom.
Variable ( : Type) ( : R).

Local Notation := idx.

Variable : Monoid.com_law 1.

Local Notation := op (at level 0).
Local Notation := (op x y).

Lemma ( : choiceType) ( : {fset T}) :
\big[*%M/1]_( : J | P (val x)) F (val x)
= \big[*%M/1]_( <- enum_fset J | P x) F x.

Proof.

case: J=> J c; rewrite -(big_map val) /index_enum.
by rewrite !unlock val_fset_sub_enum ?canonical_uniq.
Qed.

Lemma ( : choiceType) ( : {fset T}) :
\big[*%M/1]_( : J) F (val x)
= \big[*%M/1]_( <- enum_fset J) F x.

Proof.

by apply/big_fset_seq_cond. Qed.

Lemma ( : choiceType) ( : seq T) : uniq s ->
\big[*%M/1]_( : [fset in s] | P (val x)) F (val x)
= \big[*%M/1]_( <- s | P x) F x.

Proof.

move=> eq_s; rewrite big_fset_seq_cond; apply/perm_big.
by apply/uniq_perm=> //= x; rewrite in_fset.
Qed.

Lemma ( : choiceType) ( : seq T) : uniq s ->
\big[*%M/1]_( : [fset in s]) F (val x)
= \big[*%M/1]_( <- s) F x.

Proof.

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 { : Type} { : choiceType} ( : R) ( : Monoid.com_law idx).

Lemma ( : {fset T}) : [disjoint A & B] ->
  \big[op/idx]_( : A `|` B) F (val j) =
    op (\big[op/idx]_( : A) F (val j))
       (\big[op/idx]_( : B) F (val j)).

Proof.

move=> dj_AB; rewrite !big_fset_seq -big_cat; apply/perm_big.
apply/uniq_perm=> //.
+ rewrite cat_uniq ?uniq_fset_keys !(andbT, andTb); apply/hasPn => x /=.
by apply/fdisjointP; rewrite fdisjoint_sym.
+ by move=> x; rewrite mem_cat in_fsetE.
Qed.

End BigFSetU.

Section BigFSetOrder.
Variable ( : realDomainType) ( : choiceType).

Lemma ( : {fset T}) ( : T -> R) :
(forall , 0 <= F x) -> {subset I <= J} ->
\sum_( : I) F (val i) <= \sum_( : J) F (val j).

Proof.

move=> ge0_F le_IJ; rewrite !big_fset_seq /=.
rewrite [X in _<=X](bigID [pred : T | j \in I]) /=.
rewrite ler_wpDr ?sumr_ge0 // -[X in _<=X]big_filter.
rewrite le_eqVlt; apply/orP; left; apply/eqP/perm_big.
apply/uniq_perm; rewrite ?filter_uniq //; last move=> i.
rewrite mem_filter; case/boolP: (_ \in _) => //=.
by move/le_IJ => ->.
Qed.

Lemma ( : nat -> R) :
\sum_(0 <= < n) F i =
\sum_( : [fset in (iota 0 n)]) F (val i).

Proof.

rewrite -(big_map val xpredT) /=; apply/perm_big.
apply/uniq_perm; rewrite ?iota_uniq //.
rewrite map_inj_uniq /=; first apply/val_inj.
by rewrite /index_enum -enumT enum_uniq.
by move=> i; rewrite /index_enum -enumT -enum_fsetE in_fset /index_iota subn0.
Qed.

Lemma ( : nat -> R) :
\sum_( < n) F i =
\sum_( : [fset in (iota 0 n)]) F (val i).

Proof.

by rewrite -(big_mkord xpredT) big_nat_mkfset. Qed.

End BigFSetOrder.

Lemma { : finType} :
perm_eq (enum [fset i | in I]) (enum I).

Proof.

apply/uniq_perm; rewrite ?enum_uniq //.
by move=> i /=; rewrite !mem_enum in_imfset.
Qed.