Library bigops
Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype.
Require Import finfun paths.
Require Import finfun paths.
This file provides a generic definition for iterating an operator over a
set of indexes (reducebig); this big operator is parametrized by the
return type (R), the type of indexes (I), the operator (op), the default
value on empty lists (idx), the range of indexes (r), the filter applied
on this range (P) and the expression we are iterating (F). The definition
is not to be used directly, but via the wide range of notations provided
and which allows a natural use of big operators.
The lemmas can be classified according to the operator being iterated:
1. results independent of the operator: extensionality with respect to
the range of indexes, to the filtering predicate or to the
expression being iterated; reindexing, widening or narrowing of the
range of indexes; we provide lemmas for the special case where
indexes are natural numbers
2. results depending on the properties of the operator:
we distinguish: monoid laws (op is associative, idx is the neutral
element), abelian monoid laws (op is also comutative), the case
where we have 2 operators compatible with a certain property, the
case of 2 operators compatible with a certain relation (e.g. order)
the case of 2 operators that interact through distributivity (e.g.
the addition and multiplication in a ring structure).
A special section is dedicated to big operators on natural numbers.
Notations:
The general form for iterated operators is
<bigop>_<range> <general_term>
- <bigop> is one of \big[op/idx], \sum, \prod, or \max (see below)
- <range> binds an index variable (say, i) in <general_term>, which can
be any expression; <range> is one of
(i <- s) i ranges over the sequence s
(m <= i < n) i ranges over the nat interval m, m.+1, ..., n.-1
(i < n) i ranges over the (finite) type 'I_n (i.e., ordinal n)
(i : T) i ranges over the finite type T
i or (i) i ranges over its (inferred) finite type
(i \in A) i ranges over the elements that satisfy the collective
predicate A (the domain of A must be a finite type)
(i <- s | C) limits the range to those i for which C holds (i is thus
bound in C); works with all six kinds of ranges above.
- the fall-back notation <bigop>_(<- s | predicate) function is used if
the Coq display algorithm fails to recognize any of the above (such
as when <general_term> does not depend on i);
- one can use the "\big[op/idx]" notations for any operator;
- the "\sum", "\prod" and "\max" notations in nat_scope are used for
natural numbers with addition, multiplication and maximum (and their
corresponding neutral elements), respectively;
- the "\sum" and "\prod" reserved notations are re-bounded in ssralg.v
in ring_scope to the addition and multiplication big operators of a
ring, and, in groups.v/group_scope, to iterated group product.
- finset.v defines "\bigcup" and "\bigcap" notations for iterated
union and intersection.
Tips for using lemmas in this file: to apply a lemma for a specific operator: if no special property is required for the operator, simply apply the lemma; if the lemma needs certain properties for the operator, make sure the appropriate Canonical Structures are declared.
Additional documentation for this file:
Y. Bertot, G. Gonthier, S. Ould Biha and I. Pasca.
Canonical Big Operators. In TPHOLs 2008, LNCS vol. 5170, Springer.
Article available at:
http://hal.inria.fr/docs/00/33/11/93/PDF/main.pdf
Examples of use in: poly.v, matrix.v
Import Prenex Implicits.
Reserved Notation "\big [ op / idx ]_ i F"
(at level 36, F at level 36, op, idx at level 10, i at level 0,
right associativity,
format "'[' \big [ op / idx ]_ i '/ ' F ']'").
Reserved Notation "\big [ op / idx ]_ ( <- r | P ) F"
(at level 36, F at level 36, op, idx at level 10, r at level 50,
format "'[' \big [ op / idx ]_ ( <- r | P ) '/ ' F ']'").
Reserved Notation "\big [ op / idx ]_ ( i <- r | P ) F"
(at level 36, F at level 36, op, idx at level 10, i, r at level 50,
format "'[' \big [ op / idx ]_ ( i <- r | P ) '/ ' F ']'").
Reserved Notation "\big [ op / idx ]_ ( i <- r ) F"
(at level 36, F at level 36, op, idx at level 10, i, r at level 50,
format "'[' \big [ op / idx ]_ ( i <- r ) '/ ' F ']'").
Reserved Notation "\big [ op / idx ]_ ( m <= i < n | P ) F"
(at level 36, F at level 36, op, idx at level 10, m, i, n at level 50,
format "'[' \big [ op / idx ]_ ( m <= i < n | P ) F ']'").
Reserved Notation "\big [ op / idx ]_ ( m <= i < n ) F"
(at level 36, F at level 36, op, idx at level 10, i, m, n at level 50,
format "'[' \big [ op / idx ]_ ( m <= i < n ) '/ ' F ']'").
Reserved Notation "\big [ op / idx ]_ ( i | P ) F"
(at level 36, F at level 36, op, idx at level 10, i at level 50,
format "'[' \big [ op / idx ]_ ( i | P ) '/ ' F ']'").
Reserved Notation "\big [ op / idx ]_ ( i : t | P ) F"
(at level 36, F at level 36, op, idx at level 10, i at level 50,
format "'[' \big [ op / idx ]_ ( i : t | P ) '/ ' F ']'").
Reserved Notation "\big [ op / idx ]_ ( i : t ) F"
(at level 36, F at level 36, op, idx at level 10, i at level 50,
format "'[' \big [ op / idx ]_ ( i : t ) '/ ' F ']'").
Reserved Notation "\big [ op / idx ]_ ( i < n | P ) F"
(at level 36, F at level 36, op, idx at level 10, i, n at level 50,
format "'[' \big [ op / idx ]_ ( i < n | P ) '/ ' F ']'").
Reserved Notation "\big [ op / idx ]_ ( i < n ) F"
(at level 36, F at level 36, op, idx at level 10, i, n at level 50,
format "'[' \big [ op / idx ]_ ( i < n ) F ']'").
Reserved Notation "\big [ op / idx ]_ ( i \in A | P ) F"
(at level 36, F at level 36, op, idx at level 10, i, A at level 50,
format "'[' \big [ op / idx ]_ ( i \in A | P ) '/ ' F ']'").
Reserved Notation "\big [ op / idx ]_ ( i \in A ) F"
(at level 36, F at level 36, op, idx at level 10, i, A at level 50,
format "'[' \big [ op / idx ]_ ( i \in A ) '/ ' F ']'").
Reserved Notation "\sum_ i F"
(at level 41, F at level 41, i at level 0,
right associativity,
format "'[' \sum_ i '/ ' F ']'").
Reserved Notation "\sum_ ( <- r | P ) F"
(at level 41, F at level 41, r at level 50,
format "'[' \sum_ ( <- r | P ) '/ ' F ']'").
Reserved Notation "\sum_ ( i <- r | P ) F"
(at level 41, F at level 41, i, r at level 50,
format "'[' \sum_ ( i <- r | P ) '/ ' F ']'").
Reserved Notation "\sum_ ( i <- r ) F"
(at level 41, F at level 41, i, r at level 50,
format "'[' \sum_ ( i <- r ) '/ ' F ']'").
Reserved Notation "\sum_ ( m <= i < n | P ) F"
(at level 41, F at level 41, i, m, n at level 50,
format "'[' \sum_ ( m <= i < n | P ) '/ ' F ']'").
Reserved Notation "\sum_ ( m <= i < n ) F"
(at level 41, F at level 41, i, m, n at level 50,
format "'[' \sum_ ( m <= i < n ) '/ ' F ']'").
Reserved Notation "\sum_ ( i | P ) F"
(at level 41, F at level 41, i at level 50,
format "'[' \sum_ ( i | P ) '/ ' F ']'").
Reserved Notation "\sum_ ( i : t | P ) F"
(at level 41, F at level 41, i at level 50,
only parsing).
Reserved Notation "\sum_ ( i : t ) F"
(at level 41, F at level 41, i at level 50,
only parsing).
Reserved Notation "\sum_ ( i < n | P ) F"
(at level 41, F at level 41, i, n at level 50,
format "'[' \sum_ ( i < n | P ) '/ ' F ']'").
Reserved Notation "\sum_ ( i < n ) F"
(at level 41, F at level 41, i, n at level 50,
format "'[' \sum_ ( i < n ) '/ ' F ']'").
Reserved Notation "\sum_ ( i \in A | P ) F"
(at level 41, F at level 41, i, A at level 50,
format "'[' \sum_ ( i \in A | P ) '/ ' F ']'").
Reserved Notation "\sum_ ( i \in A ) F"
(at level 41, F at level 41, i, A at level 50,
format "'[' \sum_ ( i \in A ) '/ ' F ']'").
Reserved Notation "\max_ i F"
(at level 41, F at level 41, i at level 0,
format "'[' \max_ i '/ ' F ']'").
Reserved Notation "\max_ ( <- r | P ) F"
(at level 41, F at level 41, r at level 50,
format "'[' \max_ ( <- r | P ) '/ ' F ']'").
Reserved Notation "\max_ ( i <- r | P ) F"
(at level 41, F at level 41, i, r at level 50,
format "'[' \max_ ( i <- r | P ) '/ ' F ']'").
Reserved Notation "\max_ ( i <- r ) F"
(at level 41, F at level 41, i, r at level 50,
format "'[' \max_ ( i <- r ) '/ ' F ']'").
Reserved Notation "\max_ ( m <= i < n | P ) F"
(at level 41, F at level 41, i, m, n at level 50,
format "'[' \max_ ( m <= i < n | P ) '/ ' F ']'").
Reserved Notation "\max_ ( m <= i < n ) F"
(at level 41, F at level 41, i, m, n at level 50,
format "'[' \max_ ( m <= i < n ) '/ ' F ']'").
Reserved Notation "\max_ ( i | P ) F"
(at level 41, F at level 41, i at level 50,
format "'[' \max_ ( i | P ) '/ ' F ']'").
Reserved Notation "\max_ ( i : t | P ) F"
(at level 41, F at level 41, i at level 50,
only parsing).
Reserved Notation "\max_ ( i : t ) F"
(at level 41, F at level 41, i at level 50,
only parsing).
Reserved Notation "\max_ ( i < n | P ) F"
(at level 41, F at level 41, i, n at level 50,
format "'[' \max_ ( i < n | P ) '/ ' F ']'").
Reserved Notation "\max_ ( i < n ) F"
(at level 41, F at level 41, i, n at level 50,
format "'[' \max_ ( i < n ) F ']'").
Reserved Notation "\max_ ( i \in A | P ) F"
(at level 41, F at level 41, i, A at level 50,
format "'[' \max_ ( i \in A | P ) '/ ' F ']'").
Reserved Notation "\max_ ( i \in A ) F"
(at level 41, F at level 41, i, A at level 50,
format "'[' \max_ ( i \in A ) '/ ' F ']'").
Reserved Notation "\prod_ i F"
(at level 36, F at level 36, i at level 0,
format "'[' \prod_ i '/ ' F ']'").
Reserved Notation "\prod_ ( <- r | P ) F"
(at level 36, F at level 36, r at level 50,
format "'[' \prod_ ( <- r | P ) '/ ' F ']'").
Reserved Notation "\prod_ ( i <- r | P ) F"
(at level 36, F at level 36, i, r at level 50,
format "'[' \prod_ ( i <- r | P ) '/ ' F ']'").
Reserved Notation "\prod_ ( i <- r ) F"
(at level 36, F at level 36, i, r at level 50,
format "'[' \prod_ ( i <- r ) '/ ' F ']'").
Reserved Notation "\prod_ ( m <= i < n | P ) F"
(at level 36, F at level 36, i, m, n at level 50,
format "'[' \prod_ ( m <= i < n | P ) '/ ' F ']'").
Reserved Notation "\prod_ ( m <= i < n ) F"
(at level 36, F at level 36, i, m, n at level 50,
format "'[' \prod_ ( m <= i < n ) '/ ' F ']'").
Reserved Notation "\prod_ ( i | P ) F"
(at level 36, F at level 36, i at level 50,
format "'[' \prod_ ( i | P ) '/ ' F ']'").
Reserved Notation "\prod_ ( i : t | P ) F"
(at level 36, F at level 36, i at level 50,
only parsing).
Reserved Notation "\prod_ ( i : t ) F"
(at level 36, F at level 36, i at level 50,
only parsing).
Reserved Notation "\prod_ ( i < n | P ) F"
(at level 36, F at level 36, i, n at level 50,
format "'[' \prod_ ( i < n | P ) '/ ' F ']'").
Reserved Notation "\prod_ ( i < n ) F"
(at level 36, F at level 36, i, n at level 50,
format "'[' \prod_ ( i < n ) '/ ' F ']'").
Reserved Notation "\prod_ ( i \in A | P ) F"
(at level 36, F at level 36, i, A at level 50,
format "'[' \prod_ ( i \in A | P ) F ']'").
Reserved Notation "\prod_ ( i \in A ) F"
(at level 36, F at level 36, i, A at level 50,
format "'[' \prod_ ( i \in A ) '/ ' F ']'").
Module Monoid.
Section Definitions.
Variables (T : Type) (idm : T).
Structure law : Type := Law {
operator :> T -> T -> T;
_ : associative operator;
_ : left_id idm operator;
_ : right_id idm operator
}.
Structure com_law : Type := ComLaw {
com_operator :> law;
_ : commutative com_operator
}.
Structure mul_law : Type := MulLaw {
mul_operator :> T -> T -> T;
_ : left_zero idm mul_operator;
_ : right_zero idm mul_operator
}.
Structure add_law (mul : T -> T -> T) : Type := AddLaw {
add_operator :> com_law;
_ : left_distributive mul add_operator;
_ : right_distributive mul add_operator
}.
Let op_id (op1 op2 : T -> T -> T) := phant_id op1 op2.
Definition clone_law op :=
fun (opL : law) & op_id opL op =>
fun opmA op1m opm1 (opL' := @Law op opmA op1m opm1)
& phant_id opL' opL => opL'.
Definition clone_com_law op :=
fun (opL : law) (opC : com_law) & op_id opL op & op_id opC op =>
fun opmC (opC' := @ComLaw opL opmC) & phant_id opC' opC => opC'.
Definition clone_mul_law op :=
fun (opM : mul_law) & op_id opM op =>
fun op0m opm0 (opM' := @MulLaw op op0m opm0) & phant_id opM' opM => opM'.
Definition clone_add_law mop aop :=
fun (opC : com_law) (opA : add_law mop) & op_id opC aop & op_id opA aop =>
fun mopDm mopmD (opA' := @AddLaw mop opC mopDm mopmD)
& phant_id opA' opA => opA'.
End Definitions.
Section CommutativeAxioms.
Variable (T : Type) (zero one : T) (mul add : T -> T -> T) (inv : T -> T).
Hypothesis mulC : commutative mul.
Lemma mulC_id : left_id one mul -> right_id one mul.
Lemma mulC_zero : left_zero zero mul -> right_zero zero mul.
Lemma mulC_dist : left_distributive mul add -> right_distributive mul add.
End CommutativeAxioms.
Module Theory.
Section Theory.
Variables (T : Type) (idm : T).
Section Plain.
Variable mul : law idm.
Lemma mul1m : left_id idm mul.
Lemma mulm1 : right_id idm mul.
Lemma mulmA : associative mul.
Lemma iteropE : forall n x, iterop n mul x idm = iter n (mul x) idm.
End Plain.
Section Commutative.
Variable mul : com_law idm.
Lemma mulmC : commutative mul.
Lemma mulmCA : left_commutative mul.
Lemma mulmAC : right_commutative mul.
End Commutative.
Section Mul.
Variable mul : mul_law idm.
Lemma mul0m : left_zero idm mul.
Lemma mulm0 : right_zero idm mul.
End Mul.
Section Add.
Variables (mul : T -> T -> T) (add : add_law idm mul).
Lemma addmA : associative add.
Lemma addmC : commutative add.
Lemma addmCA : left_commutative add.
Lemma addmAC : right_commutative add.
Lemma add0m : left_id idm add.
Lemma addm0 : right_id idm add.
Lemma mulm_addl : left_distributive mul add.
Lemma mulm_addr : right_distributive mul add.
End Add.
Definition simpm := (mulm1, mulm0, mul1m, mul0m, mulmA).
End Theory.
End Theory.
Include Theory.
End Monoid.
Notation "[ 'law' 'of' f ]" := (@Monoid.clone_law _ _ f _ id _ _ _ id)
(at level 0, format"[ 'law' 'of' f ]") : form_scope.
Notation "[ 'com_law' 'of' f ]" := (@Monoid.clone_com_law _ _ f _ _ id id _ id)
(at level 0, format "[ 'com_law' 'of' f ]") : form_scope.
Notation "[ 'mul_law' 'of' f ]" := (@Monoid.clone_mul_law _ _ f _ id _ _ id)
(at level 0, format"[ 'mul_law' 'of' f ]") : form_scope.
Notation "[ 'add_law' m 'of' a ]" :=
(@Monoid.clone_add_law _ _ m a _ _ id id _ _ id)
(at level 0, format "[ 'add_law' m 'of' a ]") : form_scope.
Section PervasiveMonoids.
Import Monoid.
Canonical Structure andb_monoid := Law andbA andTb andbT.
Canonical Structure andb_comoid := ComLaw andbC.
Canonical Structure andb_muloid := MulLaw andFb andbF.
Canonical Structure orb_monoid := Law orbA orFb orbF.
Canonical Structure orb_comoid := ComLaw orbC.
Canonical Structure orb_muloid := MulLaw orTb orbT.
Canonical Structure addb_monoid := Law addbA addFb addbF.
Canonical Structure addb_comoid := ComLaw addbC.
Canonical Structure orb_addoid := AddLaw andb_orl andb_orr.
Canonical Structure andb_addoid := AddLaw orb_andl orb_andr.
Canonical Structure addb_addoid := AddLaw andb_addl andb_addr.
Canonical Structure addn_monoid := Law addnA add0n addn0.
Canonical Structure addn_comoid := ComLaw addnC.
Canonical Structure muln_monoid := Law mulnA mul1n muln1.
Canonical Structure muln_comoid := ComLaw mulnC.
Canonical Structure muln_muloid := MulLaw mul0n muln0.
Canonical Structure addn_addoid := AddLaw muln_addl muln_addr.
Canonical Structure maxn_monoid := Law maxnA max0n maxn0.
Canonical Structure maxn_comoid := ComLaw maxnC.
Canonical Structure maxn_addoid := AddLaw maxn_mull maxn_mulr.
Canonical Structure gcdn_monoid := Law gcdnA gcd0n gcdn0.
Canonical Structure gcdn_comoid := ComLaw gcdnC.
Canonical Structure gcdn_addoid := AddLaw muln_gcdl muln_gcdr.
Canonical Structure lcmn_monoid := Law lcmnA lcm1n lcmn1.
Canonical Structure lcmn_comoid := ComLaw lcmnC.
Canonical Structure lcmn_addoid := AddLaw muln_lcml muln_lcmr.
Canonical Structure cat_monoid T := Law (@catA T) (@cat0s T) (@cats0 T).
End PervasiveMonoids.
Delimit Scope big_scope with BIG.
Open Scope big_scope.
Definition reducebig R I idx op r (P : pred I) (F : I -> R) : R :=
foldr (fun i x => if P i then op (F i) x else x) idx r.
Module Type ReduceBigSig.
Parameter bigop : forall R I,
R -> (R -> R -> R) -> seq I -> pred I -> (I -> R) -> R.
Axiom bigopE : bigop = reducebig.
End ReduceBigSig.
Module ReduceBig : ReduceBigSig.
Definition bigop := reducebig.
Lemma bigopE : bigop = reducebig.
End ReduceBig.
Notation bigop := ReduceBig.bigop (only parsing).
Canonical Structure reduce_big_unlock := Unlockable ReduceBig.bigopE.
Definition index_iota m n := iota m (n - m).
Definition index_enum (T : finType) := Finite.enum T.
Lemma mem_index_iota : forall m n i, i \in index_iota m n = (m <= i < n).
Lemma filter_index_enum : forall T P, filter P (index_enum T) = enum P.
Notation "\big [ op / idx ]_ ( <- r | P ) F" :=
(bigop idx op r P F) : big_scope.
Notation "\big [ op / idx ]_ ( i <- r | P ) F" :=
(bigop idx op r (fun i => P%B) (fun i => F)) : big_scope.
Notation "\big [ op / idx ]_ ( i <- r ) F" :=
(bigop idx op r (fun _ => true) (fun i => F)) : big_scope.
Notation "\big [ op / idx ]_ ( m <= i < n | P ) F" :=
(bigop idx op (index_iota m n) (fun i : nat => P%B) (fun i : nat => F))
: big_scope.
Notation "\big [ op / idx ]_ ( m <= i < n ) F" :=
(bigop idx op (index_iota m n) (fun _ => true) (fun i : nat => F))
: big_scope.
Notation "\big [ op / idx ]_ ( i | P ) F" :=
(bigop idx op (index_enum _) (fun i => P%B) (fun i => F)) : big_scope.
Notation "\big [ op / idx ]_ i F" :=
(bigop idx op (index_enum _) (fun _ => true) (fun i => F)) : big_scope.
Notation "\big [ op / idx ]_ ( i : t | P ) F" :=
(bigop idx op (index_enum _) (fun i : t => P%B) (fun i : t => F))
(only parsing) : big_scope.
Notation "\big [ op / idx ]_ ( i : t ) F" :=
(bigop idx op (index_enum _) (fun _ => true) (fun i : t => F))
(only parsing) : big_scope.
Notation "\big [ op / idx ]_ ( i < n | P ) F" :=
(\big[op/idx]_(i : ordinal n | P%B) F) : big_scope.
Notation "\big [ op / idx ]_ ( i < n ) F" :=
(\big[op/idx]_(i : ordinal n) F) : big_scope.
Notation "\big [ op / idx ]_ ( i \in A | P ) F" :=
(\big[op/idx]_(i | (i \in A) && P) F) : big_scope.
Notation "\big [ op / idx ]_ ( i \in A ) F" :=
(\big[op/idx]_(i | i \in A) F) : big_scope.
Notation Local "+%N" := addn (at level 0, only parsing).
Notation "\sum_ ( <- r | P ) F" :=
(\big[+%N/0%N]_(<- r | P%B) F%N) : nat_scope.
Notation "\sum_ ( i <- r | P ) F" :=
(\big[+%N/0%N]_(i <- r | P%B) F%N) : nat_scope.
Notation "\sum_ ( i <- r ) F" :=
(\big[+%N/0%N]_(i <- r) F%N) : nat_scope.
Notation "\sum_ ( m <= i < n | P ) F" :=
(\big[+%N/0%N]_(m <= i < n | P%B) F%N) : nat_scope.
Notation "\sum_ ( m <= i < n ) F" :=
(\big[+%N/0%N]_(m <= i < n) F%N) : nat_scope.
Notation "\sum_ ( i | P ) F" :=
(\big[+%N/0%N]_(i | P%B) F%N) : nat_scope.
Notation "\sum_ i F" :=
(\big[+%N/0%N]_i F%N) : nat_scope.
Notation "\sum_ ( i : t | P ) F" :=
(\big[+%N/0%N]_(i : t | P%B) F%N) (only parsing) : nat_scope.
Notation "\sum_ ( i : t ) F" :=
(\big[+%N/0%N]_(i : t) F%N) (only parsing) : nat_scope.
Notation "\sum_ ( i < n | P ) F" :=
(\big[+%N/0%N]_(i < n | P%B) F%N) : nat_scope.
Notation "\sum_ ( i < n ) F" :=
(\big[+%N/0%N]_(i < n) F%N) : nat_scope.
Notation "\sum_ ( i \in A | P ) F" :=
(\big[+%N/0%N]_(i \in A | P%B) F%N) : nat_scope.
Notation "\sum_ ( i \in A ) F" :=
(\big[+%N/0%N]_(i \in A) F%N) : nat_scope.
Notation Local "*%N" := muln (at level 0, only parsing).
Notation "\prod_ ( <- r | P ) F" :=
(\big[*%N/1%N]_(<- r | P%B) F%N) : nat_scope.
Notation "\prod_ ( i <- r | P ) F" :=
(\big[*%N/1%N]_(i <- r | P%B) F%N) : nat_scope.
Notation "\prod_ ( i <- r ) F" :=
(\big[*%N/1%N]_(i <- r) F%N) : nat_scope.
Notation "\prod_ ( m <= i < n | P ) F" :=
(\big[*%N/1%N]_(m <= i < n | P%B) F%N) : nat_scope.
Notation "\prod_ ( m <= i < n ) F" :=
(\big[*%N/1%N]_(m <= i < n) F%N) : nat_scope.
Notation "\prod_ ( i | P ) F" :=
(\big[*%N/1%N]_(i | P%B) F%N) : nat_scope.
Notation "\prod_ i F" :=
(\big[*%N/1%N]_i F%N) : nat_scope.
Notation "\prod_ ( i : t | P ) F" :=
(\big[*%N/1%N]_(i : t | P%B) F%N) (only parsing) : nat_scope.
Notation "\prod_ ( i : t ) F" :=
(\big[*%N/1%N]_(i : t) F%N) (only parsing) : nat_scope.
Notation "\prod_ ( i < n | P ) F" :=
(\big[*%N/1%N]_(i < n | P%B) F%N) : nat_scope.
Notation "\prod_ ( i < n ) F" :=
(\big[*%N/1%N]_(i < n) F%N) : nat_scope.
Notation "\prod_ ( i \in A | P ) F" :=
(\big[*%N/1%N]_(i \in A | P%B) F%N) : nat_scope.
Notation "\prod_ ( i \in A ) F" :=
(\big[*%N/1%N]_(i \in A) F%N) : nat_scope.
Notation "\max_ ( <- r | P ) F" :=
(\big[maxn/0%N]_(<- r | P%B) F%N) : nat_scope.
Notation "\max_ ( i <- r | P ) F" :=
(\big[maxn/0%N]_(i <- r | P%B) F%N) : nat_scope.
Notation "\max_ ( i <- r ) F" :=
(\big[maxn/0%N]_(i <- r) F%N) : nat_scope.
Notation "\max_ ( i | P ) F" :=
(\big[maxn/0%N]_(i | P%B) F%N) : nat_scope.
Notation "\max_ i F" :=
(\big[maxn/0%N]_i F%N) : nat_scope.
Notation "\max_ ( i : I | P ) F" :=
(\big[maxn/0%N]_(i : I | P%B) F%N) (only parsing) : nat_scope.
Notation "\max_ ( i : I ) F" :=
(\big[maxn/0%N]_(i : I) F%N) (only parsing) : nat_scope.
Notation "\max_ ( m <= i < n | P ) F" :=
(\big[maxn/0%N]_(m <= i < n | P%B) F%N) : nat_scope.
Notation "\max_ ( m <= i < n ) F" :=
(\big[maxn/0%N]_(m <= i < n) F%N) : nat_scope.
Notation "\max_ ( i < n | P ) F" :=
(\big[maxn/0%N]_(i < n | P%B) F%N) : nat_scope.
Notation "\max_ ( i < n ) F" :=
(\big[maxn/0%N]_(i < n) F%N) : nat_scope.
Notation "\max_ ( i \in A | P ) F" :=
(\big[maxn/0%N]_(i \in A | P%B) F%N) : nat_scope.
Notation "\max_ ( i \in A ) F" :=
(\big[maxn/0%N]_(i \in A) F%N) : nat_scope.
Redundant, unparseable notation to print some constant sums and products.
Notation "\su 'm_' ( i | P ) e" :=
(\sum_(<- index_enum _ | (fun i => P)) (fun _ => e%N))
(at level 41, e at level 41, format "\su 'm_' ( i | P ) e") : nat_scope.
Notation "\su 'm_' ( i \in A ) e" :=
(\sum_(<- index_enum _ | (fun i => i \in A)) (fun _ => e%N))
(at level 41, e at level 41, format "\su 'm_' ( i \in A ) e") : nat_scope.
Notation "\su 'm_' ( i \in A | P ) e" :=
(\sum_(<- index_enum _ | (fun i => (i \in A) && P)) (fun _ => e%N))
(at level 41, e at level 41, format "\su 'm_' ( i \in A | P ) e")
: nat_scope.
Notation "\pro 'd_' ( i | P ) e" :=
(\prod_(<- index_enum _ | (fun i => P)) (fun _ => e%N))
(at level 36, e at level 36, format "\pro 'd_' ( i | P ) e") : nat_scope.
Section Extensionality.
Variables (R : Type) (idx : R) (op : R -> R -> R).
Section SeqExtension.
Variable I : Type.
Lemma big_filter : forall r (P : pred I) F,
\big[op/idx]_(i <- filter P r) F i = \big[op/idx]_(i <- r | P i) F i.
Lemma big_filter_cond : forall r (P1 P2 : pred I) F,
\big[op/idx]_(i <- filter P1 r | P2 i) F i
= \big[op/idx]_(i <- r | P1 i && P2 i) F i.
Lemma eq_bigl : forall r (P1 P2 : pred I) F, P1 =1 P2 ->
\big[op/idx]_(i <- r | P1 i) F i = \big[op/idx]_(i <- r | P2 i) F i.
Lemma eq_bigr : forall r (P : pred I) F1 F2, (forall i, P i -> F1 i = F2 i) ->
\big[op/idx]_(i <- r | P i) F1 i = \big[op/idx]_(i <- r | P i) F2 i.
Lemma eq_big : forall r (P1 P2 : pred I) F1 F2,
P1 =1 P2 -> (forall i, P1 i -> F1 i = F2 i) ->
\big[op/idx]_(i <- r | P1 i) F1 i = \big[op/idx]_(i <- r | P2 i) F2 i.
Lemma congr_big : forall r1 r2 (P1 P2 : pred I) F1 F2,
r1 = r2 -> P1 =1 P2 -> (forall i, P1 i -> F1 i = F2 i) ->
\big[op/idx]_(i <- r1 | P1 i) F1 i = \big[op/idx]_(i <- r2 | P2 i) F2 i.
Lemma big_nil : forall (P : pred I) F,
\big[op/idx]_(i <- [::] | P i) F i = idx.
Lemma big_cons : forall i r (P : pred I) F,
let x := \big[op/idx]_(j <- r | P j) F j in
\big[op/idx]_(j <- i :: r | P j) F j = if P i then op (F i) x else x.
Lemma big_map : forall (J : eqType) (h : J -> I) r (P : pred I) F,
\big[op/idx]_(i <- map h r | P i) F i
= \big[op/idx]_(j <- r | P (h j)) F (h j).
Lemma big_nth : forall x0 r (P : pred I) F,
\big[op/idx]_(i <- r | P i) F i
= \big[op/idx]_(0 <= i < size r | P (nth x0 r i)) (F (nth x0 r i)).
Lemma big_hasC : forall r (P : pred I) F,
~~ has P r -> \big[op/idx]_(i <- r | P i) F i = idx.
Lemma big_pred0_eq : forall (r : seq I) F,
\big[op/idx]_(i <- r | false) F i = idx.
Lemma big_pred0 : forall r (P : pred I) F, P =1 xpred0 ->
\big[op/idx]_(i <- r | P i) F i = idx.
Lemma big_cat_nested : forall r1 r2 (P : pred I) F,
let x := \big[op/idx]_(i <- r2 | P i) F i in
\big[op/idx]_(i <- r1 ++ r2 | P i) F i = \big[op/x]_(i <- r1 | P i) F i.
Lemma big_catl : forall r1 r2 (P : pred I) F, ~~ has P r2 ->
\big[op/idx]_(i <- r1 ++ r2 | P i) F i = \big[op/idx]_(i <- r1 | P i) F i.
Lemma big_catr : forall r1 r2 (P : pred I) F, ~~ has P r1 ->
\big[op/idx]_(i <- r1 ++ r2 | P i) F i = \big[op/idx]_(i <- r2 | P i) F i.
Lemma big_const_seq : forall r (P : pred I) x,
\big[op/idx]_(i <- r | P i) x = iter (count P r) (op x) idx.
End SeqExtension.
(\sum_(<- index_enum _ | (fun i => P)) (fun _ => e%N))
(at level 41, e at level 41, format "\su 'm_' ( i | P ) e") : nat_scope.
Notation "\su 'm_' ( i \in A ) e" :=
(\sum_(<- index_enum _ | (fun i => i \in A)) (fun _ => e%N))
(at level 41, e at level 41, format "\su 'm_' ( i \in A ) e") : nat_scope.
Notation "\su 'm_' ( i \in A | P ) e" :=
(\sum_(<- index_enum _ | (fun i => (i \in A) && P)) (fun _ => e%N))
(at level 41, e at level 41, format "\su 'm_' ( i \in A | P ) e")
: nat_scope.
Notation "\pro 'd_' ( i | P ) e" :=
(\prod_(<- index_enum _ | (fun i => P)) (fun _ => e%N))
(at level 36, e at level 36, format "\pro 'd_' ( i | P ) e") : nat_scope.
Section Extensionality.
Variables (R : Type) (idx : R) (op : R -> R -> R).
Section SeqExtension.
Variable I : Type.
Lemma big_filter : forall r (P : pred I) F,
\big[op/idx]_(i <- filter P r) F i = \big[op/idx]_(i <- r | P i) F i.
Lemma big_filter_cond : forall r (P1 P2 : pred I) F,
\big[op/idx]_(i <- filter P1 r | P2 i) F i
= \big[op/idx]_(i <- r | P1 i && P2 i) F i.
Lemma eq_bigl : forall r (P1 P2 : pred I) F, P1 =1 P2 ->
\big[op/idx]_(i <- r | P1 i) F i = \big[op/idx]_(i <- r | P2 i) F i.
Lemma eq_bigr : forall r (P : pred I) F1 F2, (forall i, P i -> F1 i = F2 i) ->
\big[op/idx]_(i <- r | P i) F1 i = \big[op/idx]_(i <- r | P i) F2 i.
Lemma eq_big : forall r (P1 P2 : pred I) F1 F2,
P1 =1 P2 -> (forall i, P1 i -> F1 i = F2 i) ->
\big[op/idx]_(i <- r | P1 i) F1 i = \big[op/idx]_(i <- r | P2 i) F2 i.
Lemma congr_big : forall r1 r2 (P1 P2 : pred I) F1 F2,
r1 = r2 -> P1 =1 P2 -> (forall i, P1 i -> F1 i = F2 i) ->
\big[op/idx]_(i <- r1 | P1 i) F1 i = \big[op/idx]_(i <- r2 | P2 i) F2 i.
Lemma big_nil : forall (P : pred I) F,
\big[op/idx]_(i <- [::] | P i) F i = idx.
Lemma big_cons : forall i r (P : pred I) F,
let x := \big[op/idx]_(j <- r | P j) F j in
\big[op/idx]_(j <- i :: r | P j) F j = if P i then op (F i) x else x.
Lemma big_map : forall (J : eqType) (h : J -> I) r (P : pred I) F,
\big[op/idx]_(i <- map h r | P i) F i
= \big[op/idx]_(j <- r | P (h j)) F (h j).
Lemma big_nth : forall x0 r (P : pred I) F,
\big[op/idx]_(i <- r | P i) F i
= \big[op/idx]_(0 <= i < size r | P (nth x0 r i)) (F (nth x0 r i)).
Lemma big_hasC : forall r (P : pred I) F,
~~ has P r -> \big[op/idx]_(i <- r | P i) F i = idx.
Lemma big_pred0_eq : forall (r : seq I) F,
\big[op/idx]_(i <- r | false) F i = idx.
Lemma big_pred0 : forall r (P : pred I) F, P =1 xpred0 ->
\big[op/idx]_(i <- r | P i) F i = idx.
Lemma big_cat_nested : forall r1 r2 (P : pred I) F,
let x := \big[op/idx]_(i <- r2 | P i) F i in
\big[op/idx]_(i <- r1 ++ r2 | P i) F i = \big[op/x]_(i <- r1 | P i) F i.
Lemma big_catl : forall r1 r2 (P : pred I) F, ~~ has P r2 ->
\big[op/idx]_(i <- r1 ++ r2 | P i) F i = \big[op/idx]_(i <- r1 | P i) F i.
Lemma big_catr : forall r1 r2 (P : pred I) F, ~~ has P r1 ->
\big[op/idx]_(i <- r1 ++ r2 | P i) F i = \big[op/idx]_(i <- r2 | P i) F i.
Lemma big_const_seq : forall r (P : pred I) x,
\big[op/idx]_(i <- r | P i) x = iter (count P r) (op x) idx.
End SeqExtension.
The following lemma can be used to localise extensionality to the specific index sequence. This is done by ssreflect rewriting, before applying congruence or induction lemmas. This is important for the latter, because ssreflect 1.1 still relies on primitive Coq matching unification for second-order application (e.g., for elim), and the latter can't handle the eqType constraint on I, as it doesn't recognize canonical projections.
Lemma big_cond_seq : forall (I : eqType) r (P : pred I) F,
\big[op/idx]_(i <- r | P i) F i
= \big[op/idx]_(i <- r | P i && (i \in r)) F i.
Lemma congr_big_nat : forall m1 n1 m2 n2 P1 P2 F1 F2,
m1 = m2 -> n1 = n2 ->
(forall i, m1 <= i < n2 -> P1 i = P2 i) ->
(forall i, P1 i && (m1 <= i < n2) -> F1 i = F2 i) ->
\big[op/idx]_(m1 <= i < n1 | P1 i) F1 i
= \big[op/idx]_(m2 <= i < n2 | P2 i) F2 i.
Lemma big_geq : forall m n (P : pred nat) F, m >= n ->
\big[op/idx]_(m <= i < n | P i) F i = idx.
Lemma big_ltn_cond : forall m n (P : pred nat) F, m < n ->
let x := \big[op/idx]_(m.+1 <= i < n | P i) F i in
\big[op/idx]_(m <= i < n | P i) F i = if P m then op (F m) x else x.
Lemma big_ltn : forall m n F, m < n ->
\big[op/idx]_(m <= i < n) F i = op (F m) (\big[op/idx]_(m.+1 <= i < n) F i).
Lemma big_addn : forall m n a (P : pred nat) F,
\big[op/idx]_(m + a <= i < n | P i) F i =
\big[op/idx]_(m <= i < n - a | P (i + a)) F (i + a).
Lemma big_add1 : forall m n (P : pred nat) F,
\big[op/idx]_(m.+1 <= i < n | P i) F i =
\big[op/idx]_(m <= i < n.-1 | P (i.+1)) F (i.+1).
Lemma big_nat_recl : forall n F,
\big[op/idx]_(0 <= i < n.+1) F i =
op (F 0) (\big[op/idx]_(0 <= i < n) F i.+1).
Lemma big_mkord : forall n (P : pred nat) F,
\big[op/idx]_(0 <= i < n | P i) F i = \big[op/idx]_(i < n | P i) F i.
Lemma big_nat_widen : forall m n1 n2 (P : pred nat) F, n1 <= n2 ->
\big[op/idx]_(m <= i < n1 | P i) F i
= \big[op/idx]_(m <= i < n2 | P i && (i < n1)) F i.
Lemma big_ord_widen_cond : forall n1 n2 (P : pred nat) (F : nat -> R),
n1 <= n2 ->
\big[op/idx]_(i < n1 | P i) F i
= \big[op/idx]_(i < n2 | P i && (i < n1)) F i.
Lemma big_ord_widen : forall n1 n2 (F : nat -> R),
n1 <= n2 ->
\big[op/idx]_(i < n1) F i = \big[op/idx]_(i < n2 | i < n1) F i.
Lemma big_ord_widen_leq : forall n1 n2 (P : pred 'I_(n1.+1)) F,
n1 < n2 ->
\big[op/idx]_(i < n1.+1 | P i) F i
= \big[op/idx]_(i < n2 | P (inord i) && (i <= n1)) F (inord i).
Lemma big_ord_narrow_cond : forall n1 n2 (P : pred 'I_n2) F,
forall le_n1_n2 : n1 <= n2,
let w := widen_ord le_n1_n2 in
\big[op/idx]_(i < n2 | P i && (i < n1)) F i
= \big[op/idx]_(i < n1 | P (w i)) F (w i).
Lemma big_ord_narrow_cond_leq : forall n1 n2 (P : pred 'I_(n2.+1)) F,
forall le_n1_n2 : n1 <= n2,
let w := @widen_ord n1.+1 n2.+1 le_n1_n2 in
\big[op/idx]_(i < n2.+1 | P i && (i <= n1)) F i
= \big[op/idx]_(i < n1.+1 | P (w i)) F (w i).
Lemma big_ord_narrow : forall n1 n2 F,
forall le_n1_n2 : n1 <= n2,
let w := widen_ord le_n1_n2 in
\big[op/idx]_(i < n2 | i < n1) F i = \big[op/idx]_(i < n1) F (w i).
Lemma big_ord_narrow_leq : forall n1 n2 F,
forall le_n1_n2 : n1 <= n2,
let w := @widen_ord n1.+1 n2.+1 le_n1_n2 in
\big[op/idx]_(i < n2.+1 | i <= n1) F i = \big[op/idx]_(i < n1.+1) F (w i).
Lemma big_ord0 : forall P F, \big[op/idx]_(i < 0 | P i) F i = idx.
Lemma big_ord_recl : forall n F,
\big[op/idx]_(i < n.+1) F i =
op (F ord0) (\big[op/idx]_(i < n) F (@lift n.+1 ord0 i)).
Lemma big_const : forall (I : finType) (A : pred I) x,
\big[op/idx]_(i \in A) x = iter #|A| (op x) idx.
Lemma big_const_nat : forall m n x,
\big[op/idx]_(m <= i < n) x = iter (n - m) (op x) idx.
Lemma big_const_ord : forall n x,
\big[op/idx]_(i < n) x = iter n (op x) idx.
End Extensionality.
Section MonoidProperties.
Import Monoid.Theory.
Variable R : Type.
Variable idx : R.
Notation Local "1" := idx.
Section Plain.
Variable op : Monoid.law 1.
Notation Local "*%M" := op (at level 0).
Notation Local "x * y" := (op x y).
Lemma eq_big_idx_seq : forall idx' I r (P : pred I) F,
right_id idx' *%M -> has P r ->
\big[*%M/idx']_(i <- r | P i) F i =\big[*%M/1]_(i <- r | P i) F i.
Lemma eq_big_idx : forall idx' (I : finType) i0 (P : pred I) F,
P i0 -> right_id idx' *%M ->
\big[*%M/idx']_(i | P i) F i =\big[*%M/1]_(i | P i) F i.
Lemma big1_eq : forall I r (P : pred I), \big[*%M/1]_(i <- r | P i) 1 = 1.
Lemma big1 : forall (I : finType) (P : pred I) F,
(forall i, P i -> F i = 1) -> \big[*%M/1]_(i | P i) F i = 1.
Lemma big1_seq : forall (I : eqType) r (P : pred I) F,
(forall i, P i && (i \in r) -> F i = 1)
-> \big[*%M/1]_(i <- r | P i) F i = 1.
Lemma big_seq1 : forall I (i : I) F, \big[*%M/1]_(j <- [:: i]) F j = F i.
Lemma big_mkcond : forall I r (P : pred I) F,
\big[*%M/1]_(i <- r | P i) F i =
\big[*%M/1]_(i <- r) (if P i then F i else 1).
Lemma big_cat : forall I r1 r2 (P : pred I) F,
\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.
Lemma big_pred1_eq : forall (I : finType) (i : I) F,
\big[*%M/1]_(j | j == i) F j = F i.
Lemma big_pred1 : forall (I : finType) i (P : pred I) F,
P =1 pred1 i -> \big[*%M/1]_(j | P j) F j = F i.
Lemma big_cat_nat : forall n m p (P : pred nat) F, m <= n -> n <= p ->
\big[*%M/1]_(m <= i < p | P i) F i =
(\big[*%M/1]_(m <= i < n | P i) F i) * (\big[*%M/1]_(n <= i < p | P i) F i).
Lemma big_nat1 : forall n F, \big[*%M/1]_(n <= i < n.+1) F i = F n.
Lemma big_nat_recr : forall n F,
\big[*%M/1]_(0 <= i < n.+1) F i = (\big[*%M/1]_(0 <= i < n) F i) * F n.
Lemma big_ord_recr : forall n F,
\big[*%M/1]_(i < n.+1) F i =
(\big[*%M/1]_(i < n) F (widen_ord (leqnSn n) i)) * F ord_max.
Lemma big_sumType : forall (I1 I2 : finType) (P : pred (I1 + I2)) F,
\big[*%M/1]_(i | P i) F i =
(\big[*%M/1]_(i | P (inl _ i)) F (inl _ i))
* (\big[*%M/1]_(i | P (inr _ i)) F (inr _ i)).
Lemma big_split_ord : forall m n (P : pred 'I_(m + n)) F,
\big[*%M/1]_(i | P i) F i =
(\big[*%M/1]_(i | P (lshift n i)) F (lshift n i))
* (\big[*%M/1]_(i | P (rshift m i)) F (rshift m i)).
End Plain.
Section Abelian.
Variable op : Monoid.com_law 1.
Notation Local "'*%M'" := op (at level 0).
Notation Local "x * y" := (op x y).
Lemma eq_big_perm : forall (I : eqType) r1 r2 (P : pred I) F,
perm_eq r1 r2 ->
\big[*%M/1]_(i <- r1 | P i) F i = \big[*%M/1]_(i <- r2 | P i) F i.
Lemma big_uniq : forall (I : finType) (r : seq I) F,
uniq r -> \big[*%M/1]_(i <- r) F i = \big[*%M/1]_(i | i \in r) F i.
Lemma big_split : forall I r (P : pred I) F1 F2,
\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.
Lemma bigID : forall I r (a P : pred I) F,
\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.
Implicit Arguments bigID [I r].
Lemma bigU : forall (I : finType) (A B : pred I) F,
[disjoint A & B] ->
\big[*%M/1]_(i \in [predU A & B]) F i =
(\big[*%M/1]_(i \in A) F i) * (\big[*%M/1]_(i \in B) F i).
Lemma bigD1 : forall (I : finType) j (P : pred I) F,
P j -> \big[*%M/1]_(i | P i) F i
= F j * \big[*%M/1]_(i | P i && (i != j)) F i.
Implicit Arguments bigD1 [I P F].
Lemma cardD1x : forall (I : finType) (A : pred I) j,
A j -> #|SimplPred A| = 1 + #|[pred i | A i && (i != j)]|.
Implicit Arguments cardD1x [I A].
Lemma partition_big : forall (I J : finType) (P : pred I) p (Q : pred J) F,
(forall 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.
Implicit Arguments partition_big [I J P F].
Lemma reindex_onto : forall (I J : finType) (h : J -> I) h' (P : pred I) F,
(forall 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).
Implicit Arguments reindex_onto [I J P F].
Lemma reindex : forall (I J : finType) (h : J -> I) (P : pred I) F,
{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).
Implicit Arguments reindex [I J P F].
Lemma reindex_inj : forall (I : finType) (h : I -> I) (P : pred I) F,
injective h -> \big[*%M/1]_(i | P i) F i = \big[*%M/1]_(j | P (h j)) F (h j).
Implicit Arguments reindex_inj [I h P F].
Lemma big_nat_rev : forall m n P F,
\big[*%M/1]_(m <= i < n | P i) F i
= \big[*%M/1]_(m <= i < n | P (m + n - i.+1)) F (m + n - i.+1).
Lemma pair_big_dep : forall (I J : finType) (P : pred I) (Q : I -> pred J) F,
\big[*%M/1]_(i | P i) \big[*%M/1]_(j | Q i j) F i j =
\big[*%M/1]_(p | P p.1 && Q p.1 p.2) F p.1 p.2.
Lemma pair_big : forall (I J : finType) (P : pred I) (Q : pred J) F,
\big[*%M/1]_(i | P i) \big[*%M/1]_(j | Q j) F i j =
\big[*%M/1]_(p | P p.1 && Q p.2) F p.1 p.2.
Lemma pair_bigA : forall (I J : finType) (F : I -> J -> R),
\big[*%M/1]_i \big[*%M/1]_j F i j = \big[*%M/1]_p F p.1 p.2.
Lemma exchange_big_dep :
forall (I J : finType) (P : pred I) (Q : I -> pred J) (xQ : pred J) F,
(forall i j, P i -> Q i j -> xQ j) ->
\big[*%M/1]_(i | P i) \big[*%M/1]_(j | Q i j) F i j =
\big[*%M/1]_(j | xQ j) \big[*%M/1]_(i | P i && Q i j) F i j.
Implicit Arguments exchange_big_dep [I J P Q F].
Lemma exchange_big : forall (I J : finType) (P : pred I) (Q : pred J) F,
\big[*%M/1]_(i | P i) \big[*%M/1]_(j | Q j) F i j =
\big[*%M/1]_(j | Q j) \big[*%M/1]_(i | P i) F i j.
Lemma exchange_big_dep_nat :
forall m1 n1 m2 n2 (P : pred nat) (Q : rel nat) (xQ : pred nat) F,
(forall i j, m1 <= i < n1 -> m2 <= j < n2 -> P i -> Q i j -> xQ j) ->
\big[*%M/1]_(m1 <= i < n1 | P i) \big[*%M/1]_(m2 <= j < n2 | Q i j) F i j =
\big[*%M/1]_(m2 <= j < n2 | xQ j)
\big[*%M/1]_(m1 <= i < n1 | P i && Q i j) F i j.
Implicit Arguments exchange_big_dep_nat [m1 n1 m2 n2 P Q F].
Lemma exchange_big_nat : forall m1 n1 m2 n2 (P Q : pred nat) F,
\big[*%M/1]_(m1 <= i < n1 | P i) \big[*%M/1]_(m2 <= j < n2 | Q j) F i j =
\big[*%M/1]_(m2 <= j < n2 | Q j) \big[*%M/1]_(m1 <= i < n1 | P i) F i j.
End Abelian.
End MonoidProperties.
Implicit Arguments big_filter [R op idx I].
Implicit Arguments big_filter_cond [R op idx I].
Implicit Arguments congr_big [R op idx I r1 P1 F1].
Implicit Arguments eq_big [R op idx I r P1 F1].
Implicit Arguments eq_bigl [R op idx I r P1].
Implicit Arguments eq_bigr [R op idx I r P F1].
Implicit Arguments eq_big_idx [R op idx idx' I P F].
Implicit Arguments big_cond_seq [R op idx I r].
Implicit Arguments congr_big_nat [R op idx m1 n1 P1 F1].
Implicit Arguments big_map [R op idx I J r].
Implicit Arguments big_nth [R op idx I r].
Implicit Arguments big_catl [R op idx I r1 r2 P F].
Implicit Arguments big_catr [R op idx I r1 r2 P F].
Implicit Arguments big_geq [R op idx m n P F].
Implicit Arguments big_ltn_cond [R op idx m n P F].
Implicit Arguments big_ltn [R op idx m n F].
Implicit Arguments big_addn [R op idx].
Implicit Arguments big_mkord [R op idx n].
Implicit Arguments big_nat_widen [R op idx] .
Implicit Arguments big_ord_widen_cond [R op idx n1].
Implicit Arguments big_ord_widen [R op idx n1].
Implicit Arguments big_ord_widen_leq [R op idx n1].
Implicit Arguments big_ord_narrow_cond [R op idx n1 n2 P F].
Implicit Arguments big_ord_narrow_cond_leq [R op idx n1 n2 P F].
Implicit Arguments big_ord_narrow [R op idx n1 n2 F].
Implicit Arguments big_ord_narrow_leq [R op idx n1 n2 F].
Implicit Arguments big_mkcond [R op idx I r].
Implicit Arguments big1_eq [R op idx I].
Implicit Arguments big1_seq [R op idx I].
Implicit Arguments big1 [R op idx I].
Implicit Arguments big_pred1 [R op idx I P F].
Implicit Arguments eq_big_perm [R op idx I r1 P F].
Implicit Arguments big_uniq [R op idx I F].
Implicit Arguments bigID [R op idx I r].
Implicit Arguments bigU [R op idx I].
Implicit Arguments bigD1 [R op idx I P F].
Implicit Arguments partition_big [R op idx I J P F].
Implicit Arguments reindex_onto [R op idx I J P F].
Implicit Arguments reindex [R op idx I J P F].
Implicit Arguments reindex_inj [R op idx I h P F].
Implicit Arguments pair_big_dep [R op idx I J].
Implicit Arguments pair_big [R op idx I J].
Implicit Arguments exchange_big_dep [R op idx I J P Q F].
Implicit Arguments exchange_big_dep_nat [R op idx m1 n1 m2 n2 P Q F].
Implicit Arguments big_ord_recl [R op idx].
Implicit Arguments big_ord_recr [R op idx].
Implicit Arguments big_nat_recl [R op idx].
Implicit Arguments big_nat_recr [R op idx].
Section BigProp.
Variables (R : Type) (Pb : R -> Type).
Variables (idx : R) (op1 op2 : R -> R -> R).
Hypothesis (Pb_idx : Pb idx)
(Pb_op1 : forall x y, Pb x -> Pb y -> Pb (op1 x y))
(Pb_eq_op : forall x y, Pb x -> Pb y -> op1 x y = op2 x y).
Lemma big_prop : forall I r (P : pred I) F,
(forall i, P i -> Pb (F i)) -> Pb (\big[op1/idx]_(i <- r | P i) F i).
\big[op/idx]_(i <- r | P i) F i
= \big[op/idx]_(i <- r | P i && (i \in r)) F i.
Lemma congr_big_nat : forall m1 n1 m2 n2 P1 P2 F1 F2,
m1 = m2 -> n1 = n2 ->
(forall i, m1 <= i < n2 -> P1 i = P2 i) ->
(forall i, P1 i && (m1 <= i < n2) -> F1 i = F2 i) ->
\big[op/idx]_(m1 <= i < n1 | P1 i) F1 i
= \big[op/idx]_(m2 <= i < n2 | P2 i) F2 i.
Lemma big_geq : forall m n (P : pred nat) F, m >= n ->
\big[op/idx]_(m <= i < n | P i) F i = idx.
Lemma big_ltn_cond : forall m n (P : pred nat) F, m < n ->
let x := \big[op/idx]_(m.+1 <= i < n | P i) F i in
\big[op/idx]_(m <= i < n | P i) F i = if P m then op (F m) x else x.
Lemma big_ltn : forall m n F, m < n ->
\big[op/idx]_(m <= i < n) F i = op (F m) (\big[op/idx]_(m.+1 <= i < n) F i).
Lemma big_addn : forall m n a (P : pred nat) F,
\big[op/idx]_(m + a <= i < n | P i) F i =
\big[op/idx]_(m <= i < n - a | P (i + a)) F (i + a).
Lemma big_add1 : forall m n (P : pred nat) F,
\big[op/idx]_(m.+1 <= i < n | P i) F i =
\big[op/idx]_(m <= i < n.-1 | P (i.+1)) F (i.+1).
Lemma big_nat_recl : forall n F,
\big[op/idx]_(0 <= i < n.+1) F i =
op (F 0) (\big[op/idx]_(0 <= i < n) F i.+1).
Lemma big_mkord : forall n (P : pred nat) F,
\big[op/idx]_(0 <= i < n | P i) F i = \big[op/idx]_(i < n | P i) F i.
Lemma big_nat_widen : forall m n1 n2 (P : pred nat) F, n1 <= n2 ->
\big[op/idx]_(m <= i < n1 | P i) F i
= \big[op/idx]_(m <= i < n2 | P i && (i < n1)) F i.
Lemma big_ord_widen_cond : forall n1 n2 (P : pred nat) (F : nat -> R),
n1 <= n2 ->
\big[op/idx]_(i < n1 | P i) F i
= \big[op/idx]_(i < n2 | P i && (i < n1)) F i.
Lemma big_ord_widen : forall n1 n2 (F : nat -> R),
n1 <= n2 ->
\big[op/idx]_(i < n1) F i = \big[op/idx]_(i < n2 | i < n1) F i.
Lemma big_ord_widen_leq : forall n1 n2 (P : pred 'I_(n1.+1)) F,
n1 < n2 ->
\big[op/idx]_(i < n1.+1 | P i) F i
= \big[op/idx]_(i < n2 | P (inord i) && (i <= n1)) F (inord i).
Lemma big_ord_narrow_cond : forall n1 n2 (P : pred 'I_n2) F,
forall le_n1_n2 : n1 <= n2,
let w := widen_ord le_n1_n2 in
\big[op/idx]_(i < n2 | P i && (i < n1)) F i
= \big[op/idx]_(i < n1 | P (w i)) F (w i).
Lemma big_ord_narrow_cond_leq : forall n1 n2 (P : pred 'I_(n2.+1)) F,
forall le_n1_n2 : n1 <= n2,
let w := @widen_ord n1.+1 n2.+1 le_n1_n2 in
\big[op/idx]_(i < n2.+1 | P i && (i <= n1)) F i
= \big[op/idx]_(i < n1.+1 | P (w i)) F (w i).
Lemma big_ord_narrow : forall n1 n2 F,
forall le_n1_n2 : n1 <= n2,
let w := widen_ord le_n1_n2 in
\big[op/idx]_(i < n2 | i < n1) F i = \big[op/idx]_(i < n1) F (w i).
Lemma big_ord_narrow_leq : forall n1 n2 F,
forall le_n1_n2 : n1 <= n2,
let w := @widen_ord n1.+1 n2.+1 le_n1_n2 in
\big[op/idx]_(i < n2.+1 | i <= n1) F i = \big[op/idx]_(i < n1.+1) F (w i).
Lemma big_ord0 : forall P F, \big[op/idx]_(i < 0 | P i) F i = idx.
Lemma big_ord_recl : forall n F,
\big[op/idx]_(i < n.+1) F i =
op (F ord0) (\big[op/idx]_(i < n) F (@lift n.+1 ord0 i)).
Lemma big_const : forall (I : finType) (A : pred I) x,
\big[op/idx]_(i \in A) x = iter #|A| (op x) idx.
Lemma big_const_nat : forall m n x,
\big[op/idx]_(m <= i < n) x = iter (n - m) (op x) idx.
Lemma big_const_ord : forall n x,
\big[op/idx]_(i < n) x = iter n (op x) idx.
End Extensionality.
Section MonoidProperties.
Import Monoid.Theory.
Variable R : Type.
Variable idx : R.
Notation Local "1" := idx.
Section Plain.
Variable op : Monoid.law 1.
Notation Local "*%M" := op (at level 0).
Notation Local "x * y" := (op x y).
Lemma eq_big_idx_seq : forall idx' I r (P : pred I) F,
right_id idx' *%M -> has P r ->
\big[*%M/idx']_(i <- r | P i) F i =\big[*%M/1]_(i <- r | P i) F i.
Lemma eq_big_idx : forall idx' (I : finType) i0 (P : pred I) F,
P i0 -> right_id idx' *%M ->
\big[*%M/idx']_(i | P i) F i =\big[*%M/1]_(i | P i) F i.
Lemma big1_eq : forall I r (P : pred I), \big[*%M/1]_(i <- r | P i) 1 = 1.
Lemma big1 : forall (I : finType) (P : pred I) F,
(forall i, P i -> F i = 1) -> \big[*%M/1]_(i | P i) F i = 1.
Lemma big1_seq : forall (I : eqType) r (P : pred I) F,
(forall i, P i && (i \in r) -> F i = 1)
-> \big[*%M/1]_(i <- r | P i) F i = 1.
Lemma big_seq1 : forall I (i : I) F, \big[*%M/1]_(j <- [:: i]) F j = F i.
Lemma big_mkcond : forall I r (P : pred I) F,
\big[*%M/1]_(i <- r | P i) F i =
\big[*%M/1]_(i <- r) (if P i then F i else 1).
Lemma big_cat : forall I r1 r2 (P : pred I) F,
\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.
Lemma big_pred1_eq : forall (I : finType) (i : I) F,
\big[*%M/1]_(j | j == i) F j = F i.
Lemma big_pred1 : forall (I : finType) i (P : pred I) F,
P =1 pred1 i -> \big[*%M/1]_(j | P j) F j = F i.
Lemma big_cat_nat : forall n m p (P : pred nat) F, m <= n -> n <= p ->
\big[*%M/1]_(m <= i < p | P i) F i =
(\big[*%M/1]_(m <= i < n | P i) F i) * (\big[*%M/1]_(n <= i < p | P i) F i).
Lemma big_nat1 : forall n F, \big[*%M/1]_(n <= i < n.+1) F i = F n.
Lemma big_nat_recr : forall n F,
\big[*%M/1]_(0 <= i < n.+1) F i = (\big[*%M/1]_(0 <= i < n) F i) * F n.
Lemma big_ord_recr : forall n F,
\big[*%M/1]_(i < n.+1) F i =
(\big[*%M/1]_(i < n) F (widen_ord (leqnSn n) i)) * F ord_max.
Lemma big_sumType : forall (I1 I2 : finType) (P : pred (I1 + I2)) F,
\big[*%M/1]_(i | P i) F i =
(\big[*%M/1]_(i | P (inl _ i)) F (inl _ i))
* (\big[*%M/1]_(i | P (inr _ i)) F (inr _ i)).
Lemma big_split_ord : forall m n (P : pred 'I_(m + n)) F,
\big[*%M/1]_(i | P i) F i =
(\big[*%M/1]_(i | P (lshift n i)) F (lshift n i))
* (\big[*%M/1]_(i | P (rshift m i)) F (rshift m i)).
End Plain.
Section Abelian.
Variable op : Monoid.com_law 1.
Notation Local "'*%M'" := op (at level 0).
Notation Local "x * y" := (op x y).
Lemma eq_big_perm : forall (I : eqType) r1 r2 (P : pred I) F,
perm_eq r1 r2 ->
\big[*%M/1]_(i <- r1 | P i) F i = \big[*%M/1]_(i <- r2 | P i) F i.
Lemma big_uniq : forall (I : finType) (r : seq I) F,
uniq r -> \big[*%M/1]_(i <- r) F i = \big[*%M/1]_(i | i \in r) F i.
Lemma big_split : forall I r (P : pred I) F1 F2,
\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.
Lemma bigID : forall I r (a P : pred I) F,
\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.
Implicit Arguments bigID [I r].
Lemma bigU : forall (I : finType) (A B : pred I) F,
[disjoint A & B] ->
\big[*%M/1]_(i \in [predU A & B]) F i =
(\big[*%M/1]_(i \in A) F i) * (\big[*%M/1]_(i \in B) F i).
Lemma bigD1 : forall (I : finType) j (P : pred I) F,
P j -> \big[*%M/1]_(i | P i) F i
= F j * \big[*%M/1]_(i | P i && (i != j)) F i.
Implicit Arguments bigD1 [I P F].
Lemma cardD1x : forall (I : finType) (A : pred I) j,
A j -> #|SimplPred A| = 1 + #|[pred i | A i && (i != j)]|.
Implicit Arguments cardD1x [I A].
Lemma partition_big : forall (I J : finType) (P : pred I) p (Q : pred J) F,
(forall 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.
Implicit Arguments partition_big [I J P F].
Lemma reindex_onto : forall (I J : finType) (h : J -> I) h' (P : pred I) F,
(forall 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).
Implicit Arguments reindex_onto [I J P F].
Lemma reindex : forall (I J : finType) (h : J -> I) (P : pred I) F,
{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).
Implicit Arguments reindex [I J P F].
Lemma reindex_inj : forall (I : finType) (h : I -> I) (P : pred I) F,
injective h -> \big[*%M/1]_(i | P i) F i = \big[*%M/1]_(j | P (h j)) F (h j).
Implicit Arguments reindex_inj [I h P F].
Lemma big_nat_rev : forall m n P F,
\big[*%M/1]_(m <= i < n | P i) F i
= \big[*%M/1]_(m <= i < n | P (m + n - i.+1)) F (m + n - i.+1).
Lemma pair_big_dep : forall (I J : finType) (P : pred I) (Q : I -> pred J) F,
\big[*%M/1]_(i | P i) \big[*%M/1]_(j | Q i j) F i j =
\big[*%M/1]_(p | P p.1 && Q p.1 p.2) F p.1 p.2.
Lemma pair_big : forall (I J : finType) (P : pred I) (Q : pred J) F,
\big[*%M/1]_(i | P i) \big[*%M/1]_(j | Q j) F i j =
\big[*%M/1]_(p | P p.1 && Q p.2) F p.1 p.2.
Lemma pair_bigA : forall (I J : finType) (F : I -> J -> R),
\big[*%M/1]_i \big[*%M/1]_j F i j = \big[*%M/1]_p F p.1 p.2.
Lemma exchange_big_dep :
forall (I J : finType) (P : pred I) (Q : I -> pred J) (xQ : pred J) F,
(forall i j, P i -> Q i j -> xQ j) ->
\big[*%M/1]_(i | P i) \big[*%M/1]_(j | Q i j) F i j =
\big[*%M/1]_(j | xQ j) \big[*%M/1]_(i | P i && Q i j) F i j.
Implicit Arguments exchange_big_dep [I J P Q F].
Lemma exchange_big : forall (I J : finType) (P : pred I) (Q : pred J) F,
\big[*%M/1]_(i | P i) \big[*%M/1]_(j | Q j) F i j =
\big[*%M/1]_(j | Q j) \big[*%M/1]_(i | P i) F i j.
Lemma exchange_big_dep_nat :
forall m1 n1 m2 n2 (P : pred nat) (Q : rel nat) (xQ : pred nat) F,
(forall i j, m1 <= i < n1 -> m2 <= j < n2 -> P i -> Q i j -> xQ j) ->
\big[*%M/1]_(m1 <= i < n1 | P i) \big[*%M/1]_(m2 <= j < n2 | Q i j) F i j =
\big[*%M/1]_(m2 <= j < n2 | xQ j)
\big[*%M/1]_(m1 <= i < n1 | P i && Q i j) F i j.
Implicit Arguments exchange_big_dep_nat [m1 n1 m2 n2 P Q F].
Lemma exchange_big_nat : forall m1 n1 m2 n2 (P Q : pred nat) F,
\big[*%M/1]_(m1 <= i < n1 | P i) \big[*%M/1]_(m2 <= j < n2 | Q j) F i j =
\big[*%M/1]_(m2 <= j < n2 | Q j) \big[*%M/1]_(m1 <= i < n1 | P i) F i j.
End Abelian.
End MonoidProperties.
Implicit Arguments big_filter [R op idx I].
Implicit Arguments big_filter_cond [R op idx I].
Implicit Arguments congr_big [R op idx I r1 P1 F1].
Implicit Arguments eq_big [R op idx I r P1 F1].
Implicit Arguments eq_bigl [R op idx I r P1].
Implicit Arguments eq_bigr [R op idx I r P F1].
Implicit Arguments eq_big_idx [R op idx idx' I P F].
Implicit Arguments big_cond_seq [R op idx I r].
Implicit Arguments congr_big_nat [R op idx m1 n1 P1 F1].
Implicit Arguments big_map [R op idx I J r].
Implicit Arguments big_nth [R op idx I r].
Implicit Arguments big_catl [R op idx I r1 r2 P F].
Implicit Arguments big_catr [R op idx I r1 r2 P F].
Implicit Arguments big_geq [R op idx m n P F].
Implicit Arguments big_ltn_cond [R op idx m n P F].
Implicit Arguments big_ltn [R op idx m n F].
Implicit Arguments big_addn [R op idx].
Implicit Arguments big_mkord [R op idx n].
Implicit Arguments big_nat_widen [R op idx] .
Implicit Arguments big_ord_widen_cond [R op idx n1].
Implicit Arguments big_ord_widen [R op idx n1].
Implicit Arguments big_ord_widen_leq [R op idx n1].
Implicit Arguments big_ord_narrow_cond [R op idx n1 n2 P F].
Implicit Arguments big_ord_narrow_cond_leq [R op idx n1 n2 P F].
Implicit Arguments big_ord_narrow [R op idx n1 n2 F].
Implicit Arguments big_ord_narrow_leq [R op idx n1 n2 F].
Implicit Arguments big_mkcond [R op idx I r].
Implicit Arguments big1_eq [R op idx I].
Implicit Arguments big1_seq [R op idx I].
Implicit Arguments big1 [R op idx I].
Implicit Arguments big_pred1 [R op idx I P F].
Implicit Arguments eq_big_perm [R op idx I r1 P F].
Implicit Arguments big_uniq [R op idx I F].
Implicit Arguments bigID [R op idx I r].
Implicit Arguments bigU [R op idx I].
Implicit Arguments bigD1 [R op idx I P F].
Implicit Arguments partition_big [R op idx I J P F].
Implicit Arguments reindex_onto [R op idx I J P F].
Implicit Arguments reindex [R op idx I J P F].
Implicit Arguments reindex_inj [R op idx I h P F].
Implicit Arguments pair_big_dep [R op idx I J].
Implicit Arguments pair_big [R op idx I J].
Implicit Arguments exchange_big_dep [R op idx I J P Q F].
Implicit Arguments exchange_big_dep_nat [R op idx m1 n1 m2 n2 P Q F].
Implicit Arguments big_ord_recl [R op idx].
Implicit Arguments big_ord_recr [R op idx].
Implicit Arguments big_nat_recl [R op idx].
Implicit Arguments big_nat_recr [R op idx].
Section BigProp.
Variables (R : Type) (Pb : R -> Type).
Variables (idx : R) (op1 op2 : R -> R -> R).
Hypothesis (Pb_idx : Pb idx)
(Pb_op1 : forall x y, Pb x -> Pb y -> Pb (op1 x y))
(Pb_eq_op : forall x y, Pb x -> Pb y -> op1 x y = op2 x y).
Lemma big_prop : forall I r (P : pred I) F,
(forall i, P i -> Pb (F i)) -> Pb (\big[op1/idx]_(i <- r | P i) F i).
Pb must be given explicitly for the lemma below, because Coq second-order unification will not handle the eqType constraint on I.
Lemma big_prop_seq : forall (I : eqType) (r : seq I) (P : pred I) F,
(forall i, P i && (i \in r) -> Pb (F i)) ->
Pb (\big[op1/idx]_(i <- r | P i) F i).
(forall i, P i && (i \in r) -> Pb (F i)) ->
Pb (\big[op1/idx]_(i <- r | P i) F i).
Change operation
Lemma eq_big_op : forall I r (P : pred I) F,
(forall i, P i -> Pb (F i)) ->
\big[op1/idx]_(i <- r | P i) F i = \big[op2/idx]_(i <- r | P i) F i.
Lemma eq_big_op_seq : forall (I : eqType) r (P : pred I) F,
(forall i, P i && (i \in r) -> Pb (F i)) ->
\big[op1/idx]_(i <- r | P i) F i = \big[op2/idx]_(i <- r | P i) F i.
End BigProp.
(forall i, P i -> Pb (F i)) ->
\big[op1/idx]_(i <- r | P i) F i = \big[op2/idx]_(i <- r | P i) F i.
Lemma eq_big_op_seq : forall (I : eqType) r (P : pred I) F,
(forall i, P i && (i \in r) -> Pb (F i)) ->
\big[op1/idx]_(i <- r | P i) F i = \big[op2/idx]_(i <- r | P i) F i.
End BigProp.
The implicit arguments expect an explicit Pb
Implicit Arguments eq_big_op_seq [R idx op1 I r P F].
Implicit Arguments eq_big_op [R idx op1 I P F].
Section BigRel.
Variables (R1 R2 : Type) (Pr : R1 -> R2 -> Type).
Variables (idx1 : R1) (op1 : R1 -> R1 -> R1).
Variables (idx2 : R2) (op2 : R2 -> R2 -> R2).
Hypothesis Pr_idx : Pr idx1 idx2.
Hypothesis Pr_rel : forall x1 x2 y1 y2,
Pr x1 x2 -> Pr y1 y2 -> Pr (op1 x1 y1) (op2 x2 y2).
Implicit Arguments eq_big_op [R idx op1 I P F].
Section BigRel.
Variables (R1 R2 : Type) (Pr : R1 -> R2 -> Type).
Variables (idx1 : R1) (op1 : R1 -> R1 -> R1).
Variables (idx2 : R2) (op2 : R2 -> R2 -> R2).
Hypothesis Pr_idx : Pr idx1 idx2.
Hypothesis Pr_rel : forall x1 x2 y1 y2,
Pr x1 x2 -> Pr y1 y2 -> Pr (op1 x1 y1) (op2 x2 y2).
Pr must be given explicitly
Lemma big_rel : forall I r (P : pred I) F1 F2,
(forall i, (P i) -> Pr (F1 i) (F2 i)) ->
Pr (\big[op1/idx1]_(i <- r | P i) F1 i) (\big[op2/idx2]_(i <- r | P i) F2 i).
Lemma big_rel_seq : forall (I : eqType) (r : seq I) (P : pred I) F1 F2,
(forall i, P i && (i \in r) -> Pr (F1 i) (F2 i)) ->
Pr (\big[op1/idx1]_(i <- r | P i) F1 i) (\big[op2/idx2]_(i <- r | P i) F2 i).
End BigRel.
Implicit Arguments big_rel_seq [R1 R2 idx1 op1 idx2 op2 I r P F1 F2].
Implicit Arguments big_rel [R1 R2 idx1 op1 idx2 op2 I P F1 F2].
Section Morphism.
Variables R1 R2 : Type.
Variables (idx1 : R1) (idx2 : R2).
Variables (op1 : R1 -> R1 -> R1) (op2 : R2 -> R2 -> R2).
Variable phi : R1 -> R2.
Hypothesis phiM : {morph phi : x y / op1 x y >-> op2 x y}.
Hypothesis phi_id : phi idx1 = idx2.
Lemma big_morph : forall I r (P : pred I) F,
phi (\big[op1/idx1]_(i <- r | P i) F i) =
\big[op2/idx2]_(i <- r | P i) phi (F i).
End Morphism.
(forall i, (P i) -> Pr (F1 i) (F2 i)) ->
Pr (\big[op1/idx1]_(i <- r | P i) F1 i) (\big[op2/idx2]_(i <- r | P i) F2 i).
Lemma big_rel_seq : forall (I : eqType) (r : seq I) (P : pred I) F1 F2,
(forall i, P i && (i \in r) -> Pr (F1 i) (F2 i)) ->
Pr (\big[op1/idx1]_(i <- r | P i) F1 i) (\big[op2/idx2]_(i <- r | P i) F2 i).
End BigRel.
Implicit Arguments big_rel_seq [R1 R2 idx1 op1 idx2 op2 I r P F1 F2].
Implicit Arguments big_rel [R1 R2 idx1 op1 idx2 op2 I P F1 F2].
Section Morphism.
Variables R1 R2 : Type.
Variables (idx1 : R1) (idx2 : R2).
Variables (op1 : R1 -> R1 -> R1) (op2 : R2 -> R2 -> R2).
Variable phi : R1 -> R2.
Hypothesis phiM : {morph phi : x y / op1 x y >-> op2 x y}.
Hypothesis phi_id : phi idx1 = idx2.
Lemma big_morph : forall I r (P : pred I) F,
phi (\big[op1/idx1]_(i <- r | P i) F i) =
\big[op2/idx2]_(i <- r | P i) phi (F i).
End Morphism.
Allows apply: (big_morph phi).
Implicit Arguments big_morph [R1 R2 idx1 idx2 op1 op2].
Section Distributivity.
Import Monoid.Theory.
Variable R : Type.
Variables zero one : R.
Notation Local "0" := zero.
Notation Local "1" := one.
Variable times : Monoid.mul_law 0.
Notation Local "*%M" := times (at level 0).
Notation Local "x * y" := (times x y).
Variable plus : Monoid.add_law 0 *%M.
Notation Local "+%M" := plus (at level 0).
Notation Local "x + y" := (plus x y).
Lemma big_distrl : forall I r a (P : pred I) F,
\big[+%M/0]_(i <- r | P i) F i * a = \big[+%M/0]_(i <- r | P i) (F i * a).
Lemma big_distrr : forall I r a (P : pred I) F,
a * \big[+%M/0]_(i <- r | P i) F i = \big[+%M/0]_(i <- r | P i) (a * F i).
Lemma big_distr_big_dep :
forall (I J : finType) j0 (P : pred I) (Q : I -> pred J) F,
\big[*%M/1]_(i | P i) \big[+%M/0]_(j | Q i j) F i j =
\big[+%M/0]_(f | pfamily j0 P Q f) \big[*%M/1]_(i | P i) F i (f i).
Lemma big_distr_big :
forall (I J : finType) j0 (P : pred I) (Q : pred J) F,
\big[*%M/1]_(i | P i) \big[+%M/0]_(j | Q j) F i j =
\big[+%M/0]_(f | pffun_on j0 P Q f) \big[*%M/1]_(i | P i) F i (f i).
Lemma bigA_distr_big_dep :
forall (I J : finType) (Q : I -> pred J) F,
\big[*%M/1]_i \big[+%M/0]_(j | Q i j) F i j
= \big[+%M/0]_(f | family Q f) \big[*%M/1]_i F i (f i).
Lemma bigA_distr_big :
forall (I J : finType) (Q : pred J) (F : I -> J -> R),
\big[*%M/1]_i \big[+%M/0]_(j | Q j) F i j
= \big[+%M/0]_(f | ffun_on Q f) \big[*%M/1]_i F i (f i).
Lemma bigA_distr_bigA :
forall (I J : finType) F,
\big[*%M/1]_(i : I) \big[+%M/0]_(j : J) F i j
= \big[+%M/0]_(f : {ffun I -> J}) \big[*%M/1]_i F i (f i).
End Distributivity.
Implicit Arguments big_distrl [R zero times plus I r].
Implicit Arguments big_distrr [R zero times plus I r].
Implicit Arguments big_distr_big_dep [R zero one times plus I J].
Implicit Arguments big_distr_big [R zero one times plus I J].
Implicit Arguments bigA_distr_big_dep [R zero one times plus I J].
Implicit Arguments bigA_distr_big [R zero one times plus I J].
Implicit Arguments bigA_distr_bigA [R zero one times plus I J].
Section NatConst.
Variables (I : finType) (A : pred I).
Lemma sum_nat_const : forall n, \sum_(i \in A) n = #|A| * n.
Lemma sum1_card : \sum_(i \in A) 1 = #|A|.
Lemma prod_nat_const : forall n, \prod_(i \in A) n = n ^ #|A|.
Lemma sum_nat_const_nat : forall n1 n2 n,
\sum_(n1 <= i < n2) n = (n2 - n1) * n.
Lemma prod_nat_const_nat : forall n1 n2 n,
\prod_(n1 <= i < n2) n = n ^ (n2 - n1).
End NatConst.
Lemma prodn_cond_gt0 : forall I r (P : pred I) F,
(forall i, P i -> 0 < F i) -> 0 < \prod_(i <- r | P i) F i.
Lemma prodn_gt0 : forall I r (P : pred I) F,
(forall i, 0 < F i) -> 0 < \prod_(i <- r | P i) F i.
Lemma leq_bigmax_cond : forall (I : finType) (P : pred I) F i0,
P i0 -> F i0 <= \max_(i | P i) F i.
Implicit Arguments leq_bigmax_cond [I P F].
Lemma leq_bigmax : forall (I : finType) F (i0 : I), F i0 <= \max_i F i.
Implicit Arguments leq_bigmax [I F].
Lemma bigmax_leqP : forall (I : finType) (P : pred I) m F,
reflect (forall i, P i -> F i <= m) (\max_(i | P i) F i <= m).
Lemma bigmax_sup : forall (I : finType) i0 (P : pred I) m F,
P i0 -> m <= F i0 -> m <= \max_(i | P i) F i.
Implicit Arguments bigmax_sup [I P m F].
Lemma bigmax_eq_arg : forall (I : finType) i0 (P : pred I) F,
P i0 -> \max_(i | P i) F i = F [arg max_(i > i0 | P i) F i].
Implicit Arguments bigmax_eq_arg [I P F].
Lemma eq_bigmax_cond : forall (I : finType) (A : pred I) F,
#|A| > 0 -> {i0 | i0 \in A & \max_(i \in A) F i = F i0}.
Lemma eq_bigmax : forall (I : finType) F,
#|I| > 0 -> {i0 : I | \max_i F i = F i0}.
Lemma expn_sum : forall m I r (P : pred I) F,
(m ^ (\sum_(i <- r | P i) F i) = \prod_(i <- r | P i) m ^ F i)%N.
Lemma dvdn_biglcmP : forall (I : finType) (P : pred I) F m,
reflect (forall i, P i -> F i %| m) (\big[lcmn/1%N]_(i | P i) F i %| m).
Lemma biglcmn_sup : forall (I : finType) i0 (P : pred I) F m,
P i0 -> m %| F i0 -> m %| \big[lcmn/1%N]_(i | P i) F i.
Implicit Arguments biglcmn_sup [I P F m].
Lemma dvdn_biggcdP : forall (I : finType) (P : pred I) F m,
reflect (forall i, P i -> m %| F i) (m %| \big[gcdn/0]_(i | P i) F i).
Lemma biggcdn_inf : forall (I : finType) i0 (P : pred I) F m,
P i0 -> F i0 %| m -> \big[gcdn/0]_(i | P i) F i %| m.
Implicit Arguments biggcdn_inf [I P F m].
Section BigBool.
Variables (I : finType) (P : pred I).
Lemma big_orE : forall B,
\big[orb/false]_(i | P i) B i = (existsb i, P i && B i).
Lemma big_andE : forall B,
\big[andb/true]_(i | P i) B i = (forallb i, P i ==> B i).
End BigBool.
Section Distributivity.
Import Monoid.Theory.
Variable R : Type.
Variables zero one : R.
Notation Local "0" := zero.
Notation Local "1" := one.
Variable times : Monoid.mul_law 0.
Notation Local "*%M" := times (at level 0).
Notation Local "x * y" := (times x y).
Variable plus : Monoid.add_law 0 *%M.
Notation Local "+%M" := plus (at level 0).
Notation Local "x + y" := (plus x y).
Lemma big_distrl : forall I r a (P : pred I) F,
\big[+%M/0]_(i <- r | P i) F i * a = \big[+%M/0]_(i <- r | P i) (F i * a).
Lemma big_distrr : forall I r a (P : pred I) F,
a * \big[+%M/0]_(i <- r | P i) F i = \big[+%M/0]_(i <- r | P i) (a * F i).
Lemma big_distr_big_dep :
forall (I J : finType) j0 (P : pred I) (Q : I -> pred J) F,
\big[*%M/1]_(i | P i) \big[+%M/0]_(j | Q i j) F i j =
\big[+%M/0]_(f | pfamily j0 P Q f) \big[*%M/1]_(i | P i) F i (f i).
Lemma big_distr_big :
forall (I J : finType) j0 (P : pred I) (Q : pred J) F,
\big[*%M/1]_(i | P i) \big[+%M/0]_(j | Q j) F i j =
\big[+%M/0]_(f | pffun_on j0 P Q f) \big[*%M/1]_(i | P i) F i (f i).
Lemma bigA_distr_big_dep :
forall (I J : finType) (Q : I -> pred J) F,
\big[*%M/1]_i \big[+%M/0]_(j | Q i j) F i j
= \big[+%M/0]_(f | family Q f) \big[*%M/1]_i F i (f i).
Lemma bigA_distr_big :
forall (I J : finType) (Q : pred J) (F : I -> J -> R),
\big[*%M/1]_i \big[+%M/0]_(j | Q j) F i j
= \big[+%M/0]_(f | ffun_on Q f) \big[*%M/1]_i F i (f i).
Lemma bigA_distr_bigA :
forall (I J : finType) F,
\big[*%M/1]_(i : I) \big[+%M/0]_(j : J) F i j
= \big[+%M/0]_(f : {ffun I -> J}) \big[*%M/1]_i F i (f i).
End Distributivity.
Implicit Arguments big_distrl [R zero times plus I r].
Implicit Arguments big_distrr [R zero times plus I r].
Implicit Arguments big_distr_big_dep [R zero one times plus I J].
Implicit Arguments big_distr_big [R zero one times plus I J].
Implicit Arguments bigA_distr_big_dep [R zero one times plus I J].
Implicit Arguments bigA_distr_big [R zero one times plus I J].
Implicit Arguments bigA_distr_bigA [R zero one times plus I J].
Section NatConst.
Variables (I : finType) (A : pred I).
Lemma sum_nat_const : forall n, \sum_(i \in A) n = #|A| * n.
Lemma sum1_card : \sum_(i \in A) 1 = #|A|.
Lemma prod_nat_const : forall n, \prod_(i \in A) n = n ^ #|A|.
Lemma sum_nat_const_nat : forall n1 n2 n,
\sum_(n1 <= i < n2) n = (n2 - n1) * n.
Lemma prod_nat_const_nat : forall n1 n2 n,
\prod_(n1 <= i < n2) n = n ^ (n2 - n1).
End NatConst.
Lemma prodn_cond_gt0 : forall I r (P : pred I) F,
(forall i, P i -> 0 < F i) -> 0 < \prod_(i <- r | P i) F i.
Lemma prodn_gt0 : forall I r (P : pred I) F,
(forall i, 0 < F i) -> 0 < \prod_(i <- r | P i) F i.
Lemma leq_bigmax_cond : forall (I : finType) (P : pred I) F i0,
P i0 -> F i0 <= \max_(i | P i) F i.
Implicit Arguments leq_bigmax_cond [I P F].
Lemma leq_bigmax : forall (I : finType) F (i0 : I), F i0 <= \max_i F i.
Implicit Arguments leq_bigmax [I F].
Lemma bigmax_leqP : forall (I : finType) (P : pred I) m F,
reflect (forall i, P i -> F i <= m) (\max_(i | P i) F i <= m).
Lemma bigmax_sup : forall (I : finType) i0 (P : pred I) m F,
P i0 -> m <= F i0 -> m <= \max_(i | P i) F i.
Implicit Arguments bigmax_sup [I P m F].
Lemma bigmax_eq_arg : forall (I : finType) i0 (P : pred I) F,
P i0 -> \max_(i | P i) F i = F [arg max_(i > i0 | P i) F i].
Implicit Arguments bigmax_eq_arg [I P F].
Lemma eq_bigmax_cond : forall (I : finType) (A : pred I) F,
#|A| > 0 -> {i0 | i0 \in A & \max_(i \in A) F i = F i0}.
Lemma eq_bigmax : forall (I : finType) F,
#|I| > 0 -> {i0 : I | \max_i F i = F i0}.
Lemma expn_sum : forall m I r (P : pred I) F,
(m ^ (\sum_(i <- r | P i) F i) = \prod_(i <- r | P i) m ^ F i)%N.
Lemma dvdn_biglcmP : forall (I : finType) (P : pred I) F m,
reflect (forall i, P i -> F i %| m) (\big[lcmn/1%N]_(i | P i) F i %| m).
Lemma biglcmn_sup : forall (I : finType) i0 (P : pred I) F m,
P i0 -> m %| F i0 -> m %| \big[lcmn/1%N]_(i | P i) F i.
Implicit Arguments biglcmn_sup [I P F m].
Lemma dvdn_biggcdP : forall (I : finType) (P : pred I) F m,
reflect (forall i, P i -> m %| F i) (m %| \big[gcdn/0]_(i | P i) F i).
Lemma biggcdn_inf : forall (I : finType) i0 (P : pred I) F m,
P i0 -> F i0 %| m -> \big[gcdn/0]_(i | P i) F i %| m.
Implicit Arguments biggcdn_inf [I P F m].
Section BigBool.
Variables (I : finType) (P : pred I).
Lemma big_orE : forall B,
\big[orb/false]_(i | P i) B i = (existsb i, P i && B i).
Lemma big_andE : forall B,
\big[andb/true]_(i | P i) B i = (forallb i, P i ==> B i).
End BigBool.