bigop.v

From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop seq div ssrfun.

[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]

[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]

[Loading ML file ring_plugin.cmxs (using legacy method) ... done]

[Loading ML file coq-elpi.elpi ... done]

Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing,default]

Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing,default]

Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing,default]

Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing,default]

Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing,default]

Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing,default]

Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing,default]

Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing,default]

Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing,default]

Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing,default]

Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing,default]

(** Consider a sequence of unique elements [xs], an element [x0], and a predicate [P := λ x => x == x0]. Then, any "bigop" over the sequence [xs] w.r.t. the predicate and a function [F] is equal to [F x0]. *) Lemma big_pred1_seq : forall [R : Type] [idx : R] [op : Monoid.law idx] [X : eqType] [P : pred X] [F : X -> R] (xs : seq X) (i : X), (i \in xs) -> (uniq xs) -> P =1 pred1 i -> \big[op/idx]_(j <- xs | P j) F j = F i.

forall (R : Type) (idx : R) (op : Monoid.law idx) (X : eqType) (P : pred X) (F : X -> R) (xs : seq X) (i : X), i \in xs -> uniq xs -> P =1 pred1 i -> \big[op/idx]_(j <- xs | P j) F j = F i

Proof.

forall (R : Type) (idx : R) (op : Monoid.law idx) (X : eqType) (P : pred X) (F : X -> R) (xs : seq X) (i : X), i \in xs -> uniq xs -> P =1 pred1 i -> \big[op/idx]_(j <- xs | P j) F j = F i

move=> R idx op X P F xs i IN UNI Pi.

R: Type
idx: R
op: Monoid.law idx
X: eqType
P: pred X
F: X -> R
xs: seq X
i: X
IN: i \in xs
UNI: uniq xs
Pi: P =1 pred1 i
\big[op/idx]_(j <- xs | P j) F j = F i

have HAS: has P xs by apply /hasP; exists i => //=; rewrite (Pi i) pred1E.

R: Type
idx: R
op: Monoid.law idx
X: eqType
P: pred X
F: X -> R
xs: seq X
i: X
IN: i \in xs
UNI: uniq xs
Pi: P =1 pred1 i
HAS: has P xs
\big[op/idx]_(j <- xs | P j) F j = F i

move: UNI; have [j s1 s2 Pj nPs1] := (split_find HAS) => UNI.

R: Type
idx: R
op: Monoid.law idx
X: eqType
P: pred X
F: X -> R
xs: seq X
i: X
IN: i \in xs
Pi: P =1 pred1 i
HAS: has P xs
j: X
s1, s2: seq X
Pj: P j
nPs1: ~~ has P s1
UNI: uniq (rcons s1 j ++ s2)
\big[op/idx]_(j <- (rcons s1 j ++ s2) | P j) F j = F i

have nPs2 : ~~ has P s2.

R: Type
idx: R
op: Monoid.law idx
X: eqType
P: pred X
F: X -> R
xs: seq X
i: X
IN: i \in xs
Pi: P =1 pred1 i
HAS: has P xs
j: X
s1, s2: seq X
Pj: P j
nPs1: ~~ has P s1
UNI: uniq (rcons s1 j ++ s2)
~~ has P s2

R: Type
idx: R
op: Monoid.law idx
X: eqType
P: pred X
F: X -> R
xs: seq X
i: X
IN: i \in xs
Pi: P =1 pred1 i
HAS: has P xs
j: X
s1, s2: seq X
Pj: P j
nPs1: ~~ has P s1
UNI: uniq (rcons s1 j ++ s2)
nPs2: ~~ has P s2
\big[op/idx]_(j <- (rcons s1 j ++ s2) | P j) F j = F i

{

R: Type
idx: R
op: Monoid.law idx
X: eqType
P: pred X
F: X -> R
xs: seq X
i: X
IN: i \in xs
Pi: P =1 pred1 i
HAS: has P xs
j: X
s1, s2: seq X
Pj: P j
nPs1: ~~ has P s1
UNI: uniq (rcons s1 j ++ s2)
~~ has P s2

apply: contraT => /negPn => hPs2; exfalso.

R: Type
idx: R
op: Monoid.law idx
X: eqType
P: pred X
F: X -> R
xs: seq X
i: X
IN: i \in xs
Pi: P =1 pred1 i
HAS: has P xs
j: X
s1, s2: seq X
Pj: P j
nPs1: ~~ has P s1
UNI: uniq (rcons s1 j ++ s2)
hPs2: has P s2
False

move: UNI; rewrite cat_uniq //= => /andP [UNI1 /andP [/negP NE UNI2]].

R: Type
idx: R
op: Monoid.law idx
X: eqType
P: pred X
F: X -> R
xs: seq X
i: X
IN: i \in xs
Pi: P =1 pred1 i
HAS: has P xs
j: X
s1, s2: seq X
Pj: P j
nPs1: ~~ has P s1
hPs2: has P s2
UNI1: uniq (rcons s1 j)
NE: ~ has (in_mem^~ (mem (rcons s1 j))) s2
UNI2: uniq s2
False

move: hPs2 => /hasP [j' IN' Pj'].

R: Type
idx: R
op: Monoid.law idx
X: eqType
P: pred X
F: X -> R
xs: seq X
i: X
IN: i \in xs
Pi: P =1 pred1 i
HAS: has P xs
j: X
s1, s2: seq X
Pj: P j
nPs1: ~~ has P s1
UNI1: uniq (rcons s1 j)
NE: ~ has (in_mem^~ (mem (rcons s1 j))) s2
UNI2: uniq s2
j': X
IN': j' \in s2
Pj': P j'
False

apply/NE/hasP; exists j' => //.

R: Type
idx: R
op: Monoid.law idx
X: eqType
P: pred X
F: X -> R
xs: seq X
i: X
IN: i \in xs
Pi: P =1 pred1 i
HAS: has P xs
j: X
s1, s2: seq X
Pj: P j
nPs1: ~~ has P s1
UNI1: uniq (rcons s1 j)
NE: ~ has (in_mem^~ (mem (rcons s1 j))) s2
UNI2: uniq s2
j': X
IN': j' \in s2
Pj': P j'
j' \in rcons s1 j

move: Pj' Pj; rewrite (Pi j') (Pi j) !pred1E => /eqP -> /eqP ->.

R: Type
idx: R
op: Monoid.law idx
X: eqType
P: pred X
F: X -> R
xs: seq X
i: X
IN: i \in xs
Pi: P =1 pred1 i
HAS: has P xs
j: X
s1, s2: seq X
nPs1: ~~ has P s1
UNI1: uniq (rcons s1 j)
NE: ~ has (in_mem^~ (mem (rcons s1 j))) s2
UNI2: uniq s2
j': X
IN': j' \in s2
j \in rcons s1 j

by rewrite mem_rcons mem_head. }

R: Type
idx: R
op: Monoid.law idx
X: eqType
P: pred X
F: X -> R
xs: seq X
i: X
IN: i \in xs
Pi: P =1 pred1 i
HAS: has P xs
j: X
s1, s2: seq X
Pj: P j
nPs1: ~~ has P s1
UNI: uniq (rcons s1 j ++ s2)
nPs2: ~~ has P s2
\big[op/idx]_(j <- (rcons s1 j ++ s2) | P j) F j = F i

rewrite -cats1 big_catl // big_catr // big_cons big_nil.

R: Type
idx: R
op: Monoid.law idx
X: eqType
P: pred X
F: X -> R
xs: seq X
i: X
IN: i \in xs
Pi: P =1 pred1 i
HAS: has P xs
j: X
s1, s2: seq X
Pj: P j
nPs1: ~~ has P s1
UNI: uniq (rcons s1 j ++ s2)
nPs2: ~~ has P s2
(if P j then op (F j) idx else idx) = F i

rewrite ifT // Monoid.simpm.

R: Type
idx: R
op: Monoid.law idx
X: eqType
P: pred X
F: X -> R
xs: seq X
i: X
IN: i \in xs
Pi: P =1 pred1 i
HAS: has P xs
j: X
s1, s2: seq X
Pj: P j
nPs1: ~~ has P s1
UNI: uniq (rcons s1 j ++ s2)
nPs2: ~~ has P s2
F j = F i

by move: Pj; rewrite (Pi j) pred1E //= => /eqP ->. Qed.