# Library GraphTheory.setoid_bigop

Require Import RelationClasses Morphisms Relation_Definitions.
From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.

# Bigops over Setoids

This file generalizes various lemmas from mathcomp.ssreflect.bigop to the setting where monoid laws only hold up to the equivalence of some setoid.

## setoids

From HB Require Import structures.

HB.mixin Record Setoid_of_Type A :=
{ eqv : relation A; Eqv : Equivalence eqv }.

HB.structure Definition Setoid := { A of Setoid_of_Type A }.
Notation setoid := Setoid.type.

Declare Scope setoid_scope.
Open Scope setoid_scope.
Infix "≡" := eqv (at level 79) : setoid_scope.
Notation "x ≡ y :> X" := ((x : X) (y : X))
(at level 79, y at next level, only parsing) : setoid_scope.
Global Existing Instance Eqv.

Definition flat (A : Type) := A.
Definition flat_setoid_mixin (A : Type) :=
Setoid_of_Type.Build A (@eq_equivalence A).
Section A.

TODO: Remove the section wrapper once HB supports this
Variable (A : Type).
HB.instance (flat A) (flat_setoid_mixin A).
End A.
HB.instance unit (flat_setoid_mixin unit).

Lemma eqvxx (X : setoid) (x : X) : x x. reflexivity. Qed.
Arguments eqvxx {X x}.

This allows trivia (and hence done) to solve x x.
Hint Extern 0 ⇒ reflexivity : core.

Class monoidLaws {X : setoid} (mon0 : X) (mon2 : X X X) :=
MonoidLaws {
mon_eqv: Proper (eqv ==> eqv ==> eqv) mon2;
monA: x y z, mon2 x (mon2 y z) mon2 (mon2 x y) z;
monU: x, mon2 x mon0 x;
monUl: x, mon2 mon0 x x
}.
Global Existing Instance mon_eqv.

Class comMonoidLaws {X:setoid} (mon0 : X) (mon2 : X X X) :=
ComMonoidLaws {
mon_of_com :> monoidLaws mon0 mon2;
monC : x y, mon2 x y mon2 y x
}.

Section SetoidTheory.
Variables (X : setoid) (mon0 : X) (mon2 : X X X).
Local Notation "1" := mon0.
Local Notation "*%M" := mon2 (at level 0).
Notation "x ⊗ y" := (mon2 x y) (left associativity, at level 25).

Lemma monUl_of_com :
( x, mon2 x mon0 x) ( x y, mon2 x y mon2 y x) x, mon2 mon0 x x.
Proof. movemonU monC x. by rewrite monC monU. Qed.

Definition mkComMonoidLaws
(mon_eqv: Proper (eqv ==> eqv ==> eqv) mon2)
(monA: x y z, mon2 x (mon2 y z) mon2 (mon2 x y) z)
(monC : x y, mon2 x y mon2 y x)
(monU: x, mon2 x mon0 x) :=
ComMonoidLaws (MonoidLaws mon_eqv monA monU (monUl_of_com monU monC)) monC.

Section MonoidTheory.
Context {X_monoid : monoidLaws mon0 mon2}.

Lemma eqv_bigr (I : Type) (r : seq I) (P : pred I) (F1 F2 : I X) :
( i : I, P i F1 i F2 i) \big[*%M/1]_(i <- r | P i) F1 i \big[*%M/1]_(i <- r | P i) F2 i.
Proof. elim/big_rec2 : _ ⇒ // i x y Pi H1 H2. by rewrite H2 ?H1. Qed.

Lemma eqv_bigl I r (P1 P2 : pred I) (F : I X) :
P1 =1 P2
\big[*%M/1]_(i <- r | P1 i) F i \big[*%M/1]_(i <- r | P2 i) F i.
Proof. by moveeqP12; rewrite -!(big_filter r) (eq_filter eqP12). Qed.

Lemma eqv_big I (r:seq I) (P1 P2 : pred I) (F1 F2 : I X) :
P1 =1 P2 ( i, P1 i F1 i F2 i)
\big[*%M/1]_(i <- r | P1 i) F1 i \big[*%M/1]_(i <- r | P2 i) F2 i.
Proof. by move/eqv_bigl <-; move/eqv_bigr→. Qed.

Lemma big_mkcond (I : eqType) (r : seq I) (P : pred I) (F : I X) :
\big[*%M/1]_(i <- r | P i) F i \big[*%M/1]_(i <- r) (if P i then F i else 1).
Proof. rewrite unlock. elim: r ⇒ //= i r H. by case P; rewrite H ?monUl. Qed.

Lemma big_cat (I : eqType) (r1 r2 : seq I) (P : pred I) (F : I X) :
\big[*%M/1]_(i <- (r1 ++ r2) | P i) F i
(\big[*%M/1]_(i <- r1 | P i) F i) (\big[*%M/1]_(i <- r2 | P i) F i).
Proof.
rewrite !(big_mkcond _ P). elim: r1 ⇒ /= [|i r1 IH]; first by rewrite big_nil monUl.
by rewrite !big_cons IH monA.
Qed.

Lemma big_seq1 (I : Type) (i : I) (F : I X) : \big[*%M/1]_(j <- [:: i]) F j F i.
Proof. by rewrite big_cons big_nil monU. Qed.

Lemma big_pred1_eq (I : finType) (i : I) (F : I X) :
\big[*%M/1]_(j | j == i) F j F i.
Proof.
rewrite -big_filter filter_pred1_uniq //; first by rewrite big_seq1.
solve [by rewrite /index_enum -?enumT ?enum_uniq
|exact: index_enum_uniq]. Qed.

Lemma big_pred1 (I : finType) i (P : pred I) (F : I X) :
P =1 pred1 i \big[*%M/1]_(j | P j) F j F i.
Proof. move/(eq_bigl _ _)->; apply: big_pred1_eq. Qed.

Lemma eqv_map (I1 I2 : finType) (r1 : seq I1) (P1 : pred I1) (P2 : pred I2)
(f : I1 I2) (F1 : I1 X) (F2 : I2 X) :
( x, P1 x = P2 (f x)) ( i : I1, P1 i F1 i F2 (f i))
\big[*%M/1]_(i <- r1 | P1 i) F1 i \big[*%M/1]_(i <- map f r1 | P2 i) F2 i.
Proof.
moveHP HF. elim r1 ⇒ [|k r2 IH]; first by rewrite !big_nil.
rewrite /= !big_cons -HP. case: (boolP (P1 k)) ⇒ [Pk|_]; by rewrite -?HF ?IH.
Qed.

End MonoidTheory.

Section ComMonoidTheory.
Context {X_comMonoid : comMonoidLaws mon0 mon2}.

Local Notation "1" := mon0.
Local Notation "*%M" := mon2 (at level 0).
Notation "x ⊗ y" := (mon2 x y) (left associativity, at level 25).

Lemma big_split I r (P : pred I) (F1 F2 : I X) :
\big[*%M/1]_(i <- r | P i) (F1 i F2 i)
(\big[*%M/1]_(i <- r | P i) F1 i) \big[*%M/1]_(i <- r | P i) F2 i.
Proof.
elim/big_rec3 : _ ⇒ [|i x y z Pi ->]; rewrite ?monU //.
rewrite -!monA. apply: mon_eqv ⇒ //. by rewrite monA [_ y]monC monA.
Qed.

Lemma perm_big (I : eqType) r1 r2 (P : pred I) (F : I X) :
perm_eq r1 r2
\big[*%M/1]_(i <- r1 | P i) F i \big[*%M/1]_(i <- r2 | P i) F i.
Proof.
move/permP; rewrite !(big_mkcond _ P).
elim: r1 r2 ⇒ [|i r1 IHr1] r2 eq_r12.
by case: r2 eq_r12 ⇒ // i r2; move/(_ (pred1 i)); rewrite /= eqxx.
have r2i: i \in r2 by rewrite -has_pred1 has_count -eq_r12 /= eqxx.
case/splitPr: r2 / r2i ⇒ [r3 r4] in eq_r12 ×. rewrite big_cat /= !big_cons.
rewrite monA [_ if _ then _ else _]monC -monA. rewrite -big_cat.
rewrite (IHr1 (r3 ++ r4)) //. movea. move/(_ a) : eq_r12.
Qed.

Lemma bigID (I:eqType) r (a P : pred I) (F : I X) :
\big[*%M/1]_(i <- r | P i) F i
(\big[*%M/1]_(i <- r | P i && a i) F i) \big[*%M/1]_(i <- r | P i && ~~ a i) F i.
Proof.
rewrite !(@big_mkcond _ I r _ F) -big_split.
apply: eqv_bigri; case: (a i); by rewrite /= ?andbT ?andbF ?monU ?monUl.
Qed.
Arguments bigID [I r] a P F.

Lemma bigD1 (I : finType) j (P : pred I) (F : I X) :
P j \big[*%M/1]_(i | P i) F i F j \big[*%M/1]_(i | P i && (i != j)) F i.
Proof.
movePj; rewrite (bigID (pred1 j)); apply mon_eqv ⇒ //.
apply: big_pred1i /=. by rewrite /= andbC; case: eqP ⇒ // →.
Qed.
Arguments bigD1 [I] j [P F].

Lemma reindex_onto (I J : finType) (h : J I) h' (P : pred I) (F : I X) :
( i, P i h (h' i) = i)
\big[*%M/1]_(i | P i) F i
\big[*%M/1]_(j | P (h j) && (h' (h j) == j)) F (h j).
Proof.
moveh'K; elim: {P}_.+1 {-3}P h'K (ltnSn #|P|) ⇒ //= n IHn P h'K.
case: (pickP P) ⇒ [i Pi | P0 _]; last first.
by rewrite !big_pred0 // ⇒ j; rewrite P0.
rewrite ltnS (cardD1x Pi); move/IHn {n IHn} ⇒ IH.
rewrite (bigD1 i Pi) (bigD1 (h' i)) h'K ?Pi ?eq_refl //=. apply: mon_eqv ⇒ //.
rewrite {}IH ⇒ [|j]; [apply: eqv_biglj | by case/andP; auto].
rewrite andbC -andbA (andbCA (P _)); case: eqP ⇒ //= hK; congr (_ && ~~ _).
by apply/eqP/eqP⇒ [<-|->] //; rewrite h'K.
Qed.
Arguments reindex_onto [I J] h h' [P F].

Lemma reindex (I J : finType) (h : J I) (P : pred I) (F : I X) :
{on [pred i | P i], bijective h}
\big[*%M/1]_(i | P i) F i \big[*%M/1]_(j | P (h j)) F (h j).
Proof.
caseh' hK h'K; rewrite (reindex_onto h h' h'K).
by apply eqv_biglj; rewrite !inE; case Pi: (P _); rewrite //= hK ?eqxx.
Qed.
Arguments reindex [I J] h P F.

Lemma partition_big (I J : finType) (P : pred I) p (Q : pred J) (F : I X) :
( i, P i Q (p i))
\big[*%M/1]_(i | P i) F i
\big[*%M/1]_(j | Q j) \big[*%M/1]_(i | P i && (p i == j)) F i.
Proof.
moveQp; transitivity (\big[*%M/1]_(i | P i && Q (p i)) F i).
by apply: eqv_bigli; case Pi: (P i); rewrite // Qp.
elim: {Q Qp}_.+1 {-2}Q (ltnSn #|Q|) ⇒ // n IHn Q.
case: (pickP Q) ⇒ [j Qj | Q0 _]; last first.
by rewrite !big_pred0 // ⇒ i; rewrite Q0 andbF.
rewrite ltnS (cardD1x Qj) (bigD1 j) //; move/IHn⇒ {n IHn} <-.
rewrite (bigID (fun ip i == j)) ⇒ /=. apply: mon_eqv; apply: eqv_bigli.
case: eqP ⇒ [-> | _] ; by rewrite ?(Qj) ?andbT ?andbF.
by rewrite andbA.
Qed.

Lemma big_sumType (I1 I2 : finType) (P : pred (I1 + I2)) (F : (I1 + I2) X) :
\big[*%M/1]_(x | P x) F x
(\big[*%M/1]_(x | P (inl x)) F (inl x)) (\big[*%M/1]_(x | P (inr x)) F (inr x)).
Proof. by rewrite ![index_enum _]unlock [@Finite.enum in X in X _]unlock big_cat !big_map. Qed.
Arguments big_sumType [I1 I2] P F.

Lemma big_unitType (P : pred unit) (F : unit X) :
\big[*%M/1]_(x | P x) F x if P tt then F tt else 1.
Proof. by rewrite ![index_enum _]unlock [@Finite.enum]unlock big_mkcond big_seq1. Qed.

in conjunction with bij_perm_enum
Lemma eqv_big_bij (I1 I2 : finType) (f : I1 I2)
(r1 : seq I1) (r2 : seq I2) (P1 : pred I1) (P2 : pred I2) (F1 : I1 X) (F2 : I2 X) :
perm_eq r2 (map f r1) ( x, P1 x = P2 (f x)) ( i : I1, P1 i F1 i F2 (f i))
\big[*%M/1]_(i <- r1 | P1 i) F1 i \big[*%M/1]_(i <- r2 | P2 i) F2 i.
Proof. movepr HP HF. rewrite (perm_big _ _ pr). exact: eqv_map. Qed.

Lemma big_inj2_eq (I1 I2 : finType) (F : I1 X) (f : I1 I2) (y : I1) :
injective f \big[*%M/mon0]_(x | f x == f y) F x F y.
Proof. moveinj_f; rewrite (@big_pred1 _ _ y) //= ⇒ x; exact: inj_eq. Qed.

End ComMonoidTheory.
End SetoidTheory.

Arguments reindex_onto [X mon0 mon2 _ I J] h h' [P F].
Arguments reindex [X mon0 mon2 _ I J] h [P F].
Arguments bigD1 [X mon0 mon2 _ I] j [P F].
Arguments partition_big [X mon0 mon2 _ I J P] p Q [F].
Arguments big_pred1 [X mon0 mon2 _ I] i P F.