Library RelationAlgebra.sums


sums: finite sums, a la ssreflect

this tiny module extends sups to the setting of monoids (it is a separate module just to avoid sups to depend on monoid)

Require Import monoid.
Require Export sups.

in the setting of monoids, we prefer the "sum" notation

Notation "\sum_ ( i \in l ) f" := (@sup (mor _ _) _ (fun if) l)
  (at level 41, f at level 41, i, l at level 50,
    format "'[' \sum_ ( i \in l ) '/ ' f ']'"): ra_terms.

Notation "\sum_ ( i < n ) f" := (\sum_(i \in seq n) f)
  (at level 41, f at level 41, i, n at level 50,
    format "'[' \sum_ ( i < n ) '/ ' f ']'"): ra_terms.

dot distributes over sums
Lemma dotxsum `{laws} `{BSL<<l} I J n m p (f: I X m n) (x: X p m):
  x × (\sum_(i\in J) f i) == \sum_(i\in J) (x × f i).
Proof. apply f_sup_weq. apply dotx0. intros; apply dotxpls. Qed.

Lemma dotsumx `{laws} `{BSL<<l} I J n m p (f: I X n m) (x: X m p):
  (\sum_(i\in J) f i) × x == \sum_(i\in J) (f i × x).
Proof. dual @dotxsum. Qed.

converse commutes with sums
Lemma cnvsum `{laws} `{BSL+CNV<<l} I J n m (f: I X n m):
  (\sum_(i\in J) f i)` == \sum_(i\in J) (f i`).
Proof. apply f_sup_weq. apply cnv0. apply cnvpls. Qed.