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 uniq_fset_keysUsed by

• mathcomp.experimental_reals.realsum

---

Source code {KSource code : choiceType} (JSource code : {fset K}) : uniq (enum_fset J).

Proof.

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

#[global] Hint Resolve uniq_fset_keys : core.

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

Proof.

by rewrite enumT unlock. Qed.

Lemma enum_fset1Source code (TSource code : choiceType) (xSource code : 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 (RSource code : Type) (idxSource code : R) (opSource code : Monoid.law idx).
Variable (ISource code : choiceType).

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

Proof.

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

Lemma big_fset0Used by

• mathcomp.experimental_reals.distr
• mathcomp.experimental_reals.realsum

---

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

Proof.

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

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

Proof.

by rewrite /index_enum -enumT enum_fset1 big_seq1. Qed.

End BigFSet.

Section BigFSetCom.
Variable (RSource code : Type) (idxSource code : R).

Local Notation "1"Source code := idx.

Variable opSource code : Monoid.com_law 1.

Local Notation "'*%M'"Source code := op (at level 0).
Local Notation "x * y"Source code := (op x y).

Lemma big_fset_seq_condSource code (TSource code : choiceType) (JSource code : {fset T}) PSource code FSource code :
    \big[*%M/1]_(xSource code : J | P (val x)) F (val x)
  = \big[*%M/1]_(xSource code <- 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 big_fset_seqUsed by

• mathcomp.experimental_reals.distr
• mathcomp.experimental_reals.realsum

---

Source code (TSource code : choiceType) (JSource code : {fset T}) FSource code :
    \big[*%M/1]_(xSource code : J) F (val x)
  = \big[*%M/1]_(xSource code <- enum_fset J) F x.

Proof.

by apply/big_fset_seq_cond. Qed.

Lemma big_seq_fset_condSource code (TSource code : choiceType) (sSource code : seq T) PSource code FSource code : uniq s ->
    \big[*%M/1]_(xSource code : [fset xSource code in s] | P (val x)) F (val x)
  = \big[*%M/1]_(xSource code <- 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 big_seq_fsetUsed by

• mathcomp.experimental_reals.realsum

---

Source code (TSource code : choiceType) (sSource code : seq T) FSource code : uniq s ->
    \big[*%M/1]_(xSource code : [fset xSource code in s]) F (val x)
  = \big[*%M/1]_(xSource code <- 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 {RSource code : Type} {TSource code : choiceType} (idxSource code : R) (opSource code : Monoid.com_law idx).

Lemma big_fsetUSource code (ASource code BSource code : {fset T}) FSource code : [disjoint A & B] ->
  \big[op/idx]_(jSource code : A `|` B) F (val j) =
    op (\big[op/idx]_(jSource code : A) F (val j))
       (\big[op/idx]_(jSource code : 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 (RSource code : realDomainType) (TSource code : choiceType).

Lemma big_fset_subsetUsed by

• mathcomp.experimental_reals.realsum

---

Source code (ISource code JSource code : {fset T}) (FSource code : T -> R) :
  (forall xSource code, 0 <= F x) -> {subset I <= J} ->
    \sum_(iSource code : I) F (val i) <= \sum_(jSource code : J) F (val j).

Proof.

move=> ge0_F le_IJ; rewrite !big_fset_seq /=.
rewrite [X in _<=X](bigID [pred jSource code : 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 big_nat_mkfsetSource code (FSource code : nat -> R) nSource code :
  \sum_(0 <= iSource code < n) F i =
    \sum_(iSource code : [fset xSource code 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 big_ord_mkfsetUsed by

• mathcomp.experimental_reals.realsum

---

Source code (FSource code : nat -> R) nSource code :
  \sum_(iSource code < n) F i =
    \sum_(iSource code : [fset xSource code in (iota 0 n)]) F (val i).

Proof.

by rewrite -(big_mkord xpredT) big_nat_mkfset. Qed.

End BigFSetOrder.

Lemma enum_fsetTUsed by

• mathcomp.experimental_reals.realsum

---

Source code {ISource code : finType} :
  perm_eq (enum [fset i | iSource code in I]) (enum I).

Proof.

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