Library mathcomp.analysis.altreals.xfinmap

(* -------------------------------------------------------------------- 
 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.
From mathcomp Require Export finmap.

Set Implicit Arguments.

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).

#[global] Hint Resolve uniq_fset_keys : core.

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

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

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.

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

Lemma big_fset1 (a : I) (F : [fset a] → R) :
  \big[op/idx]_(i : [fset a]) F i = F (FSetSub (fset11 a)).
End BigFSet.

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


Variable op : Monoid.com_law 1.


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.

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.

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.

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.
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)).
End BigFSetU.

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

Lemma big_fset_subset (I J : {fset T}) (F : T → R) :
  (∀ x, 0 ≤ F x) → {subset I ≤ J} →
    \sum_(i : I) F (val i) ≤ \sum_(j : J) F (val j).

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).

Lemma big_ord_mkfset (F : nat → R) n :
  \sum_(i < n) F i =
    \sum_(i : [fset x in (iota 0 n)]) F (val i).
End BigFSetOrder.

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