+ +

Library mathcomp.ssreflect.bigop

+ +

+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
+ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+

+ +

+ This file provides a generic definition for iterating an operator over a + set of indices (bigop); this big operator is parametrized by the return + type (R), the type of indices (I), the operator (op), the default value on + empty lists (idx), the range of indices (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 + and which support a natural use of big operators. + To improve performance of the Coq typechecker on large expressions, the + bigop constant is OPAQUE. It can however be unlocked to reveal the + transparent constant reducebig, to let Coq expand summation on an explicit + sequence with an explicit test. + The lemmas can be classified according to the operator being iterated: + 1. Results independent of the operator: extensionality with respect to + the range of indices, to the filtering predicate or to the expression + being iterated; reindexing, widening or narrowing of the range of + indices; we provide lemmas for the special cases where indices are + natural numbers or bounded natural numbers ("ordinals"). We supply + several "functional" induction principles that can be used with the + ssreflect 1.3 "elim" tactic to do induction over the index range for + up to 3 bigops simultaneously. + 2. Results depending on the properties of the operator: + We distinguish: monoid laws (op is associative, idx is an identity + element), abelian monoid laws (op is also commutative), and laws with + a distributive operation (semi-rings). Examples of such results are + splitting, permuting, and exchanging bigops. + 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). + +
<general_term> can be any expression. + +
<range> binds an index variable in <general_term>; <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 | <condition>) limits the range to the i for which <condition> + holds. <condition> can be any expression that coerces to + bool, and may mention the bound index i. All six kinds of + ranges above can have a <condition> part. + +
One can use the "\big[op/idx]" notations for any operator. + +
BIG_F and BIG_P are pattern abbreviations for the <general_term> and + <condition> part of a \big ... expression; for (i in A) and (i in A | C) + ranges the term matched by BIG_P will include the i \in A condition. + +
The (locked) head constant of a \big notation is bigop. + +
The "\sum", "\prod" and "\max" notations in the %N scope are used for + natural numbers with addition, multiplication and maximum (and their + corresponding neutral elements), respectively. + +
The "\sum" and "\prod" reserved notations are overloaded in ssralg in + the %R scope; in mxalgebra, vector & falgebra in the %MS and %VS scopes; + "\prod" is also overloaded in fingroup, in the %g and %G scopes. + +
We reserve "\bigcup" and "\bigcap" notations for iterated union and + intersection (of sets, groups, vector spaces, etc). +

+ +

+ + 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 + instances are declared. +

+ + Interfaces for operator properties are packaged in the Monoid submodule: + Monoid.law idx == interface (keyed on the operator) for associative + operators with identity element idx. + Monoid.com_law idx == extension (telescope) of Monoid.law for operators + that are also commutative. + Monoid.mul_law abz == interface for operators with absorbing (zero) + element abz. + Monoid.add_law idx mop == extension of Monoid.com_law for operators over + which operation mop distributes (mop will often also + have a Monoid.mul_law idx structure). + [law of op], [com_law of op], [mul_law of op], [add_law mop of op] == + syntax for cloning Monoid structures. + Monoid.Theory == submodule containing basic generic algebra lemmas + for operators satisfying the Monoid interfaces. + Monoid.simpm == generic monoid simplification rewrite multirule. + Monoid structures are predeclared for many basic operators: (_ && _)%B, + (_ || _)%B, (_ (+) _)%B (exclusive or) , (_ + _)%N, (_ * _)%N, maxn, + gcdn, lcmn and (_ ++ _)%SEQ (list concatenation). +

+ + 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 +

+ +
+Set Implicit Arguments.
+ +
+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 ]_ ( 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_ ( 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_ ( 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_ ( 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 ']'").
+ +
+Reserved Notation "\bigcup_ i F"
+  (at level 41, F at level 41, i at level 0,
+           format "'[' \bigcup_ i '/ ' F ']'").
+Reserved Notation "\bigcup_ ( i <- r | P ) F"
+  (at level 41, F at level 41, i, r at level 50,
+           format "'[' \bigcup_ ( i <- r | P ) '/ ' F ']'").
+Reserved Notation "\bigcup_ ( i <- r ) F"
+  (at level 41, F at level 41, i, r at level 50,
+           format "'[' \bigcup_ ( i <- r ) '/ ' F ']'").
+Reserved Notation "\bigcup_ ( m <= i < n | P ) F"
+  (at level 41, F at level 41, m, i, n at level 50,
+           format "'[' \bigcup_ ( m <= i < n | P ) '/ ' F ']'").
+Reserved Notation "\bigcup_ ( m <= i < n ) F"
+  (at level 41, F at level 41, i, m, n at level 50,
+           format "'[' \bigcup_ ( m <= i < n ) '/ ' F ']'").
+Reserved Notation "\bigcup_ ( i | P ) F"
+  (at level 41, F at level 41, i at level 50,
+           format "'[' \bigcup_ ( i | P ) '/ ' F ']'").
+Reserved Notation "\bigcup_ ( i : t | P ) F"
+  (at level 41, F at level 41, i at level 50,
+           format "'[' \bigcup_ ( i : t | P ) '/ ' F ']'").
+Reserved Notation "\bigcup_ ( i : t ) F"
+  (at level 41, F at level 41, i at level 50,
+           format "'[' \bigcup_ ( i : t ) '/ ' F ']'").
+Reserved Notation "\bigcup_ ( i < n | P ) F"
+  (at level 41, F at level 41, i, n at level 50,
+           format "'[' \bigcup_ ( i < n | P ) '/ ' F ']'").
+Reserved Notation "\bigcup_ ( i < n ) F"
+  (at level 41, F at level 41, i, n at level 50,
+           format "'[' \bigcup_ ( i < n ) '/ ' F ']'").
+Reserved Notation "\bigcup_ ( i 'in' A | P ) F"
+  (at level 41, F at level 41, i, A at level 50,
+           format "'[' \bigcup_ ( i 'in' A | P ) '/ ' F ']'").
+Reserved Notation "\bigcup_ ( i 'in' A ) F"
+  (at level 41, F at level 41, i, A at level 50,
+           format "'[' \bigcup_ ( i 'in' A ) '/ ' F ']'").
+ +
+Reserved Notation "\bigcap_ i F"
+  (at level 41, F at level 41, i at level 0,
+           format "'[' \bigcap_ i '/ ' F ']'").
+Reserved Notation "\bigcap_ ( i <- r | P ) F"
+  (at level 41, F at level 41, i, r at level 50,
+           format "'[' \bigcap_ ( i <- r | P ) F ']'").
+Reserved Notation "\bigcap_ ( i <- r ) F"
+  (at level 41, F at level 41, i, r at level 50,
+           format "'[' \bigcap_ ( i <- r ) '/ ' F ']'").
+Reserved Notation "\bigcap_ ( m <= i < n | P ) F"
+  (at level 41, F at level 41, m, i, n at level 50,
+           format "'[' \bigcap_ ( m <= i < n | P ) '/ ' F ']'").
+Reserved Notation "\bigcap_ ( m <= i < n ) F"
+  (at level 41, F at level 41, i, m, n at level 50,
+           format "'[' \bigcap_ ( m <= i < n ) '/ ' F ']'").
+Reserved Notation "\bigcap_ ( i | P ) F"
+  (at level 41, F at level 41, i at level 50,
+           format "'[' \bigcap_ ( i | P ) '/ ' F ']'").
+Reserved Notation "\bigcap_ ( i : t | P ) F"
+  (at level 41, F at level 41, i at level 50,
+           format "'[' \bigcap_ ( i : t | P ) '/ ' F ']'").
+Reserved Notation "\bigcap_ ( i : t ) F"
+  (at level 41, F at level 41, i at level 50,
+           format "'[' \bigcap_ ( i : t ) '/ ' F ']'").
+Reserved Notation "\bigcap_ ( i < n | P ) F"
+  (at level 41, F at level 41, i, n at level 50,
+           format "'[' \bigcap_ ( i < n | P ) '/ ' F ']'").
+Reserved Notation "\bigcap_ ( i < n ) F"
+  (at level 41, F at level 41, i, n at level 50,
+           format "'[' \bigcap_ ( i < n ) '/ ' F ']'").
+Reserved Notation "\bigcap_ ( i 'in' A | P ) F"
+  (at level 41, F at level 41, i, A at level 50,
+           format "'[' \bigcap_ ( i 'in' A | P ) '/ ' F ']'").
+Reserved Notation "\bigcap_ ( i 'in' A ) F"
+  (at level 41, F at level 41, i, A at level 50,
+           format "'[' \bigcap_ ( i 'in' A ) '/ ' F ']'").
+ +
+Module Monoid.
+ +
+Section Definitions.
+Variables (T : Type) (idm : T).
+ +
+Structure law := Law {
+  operator : T → T → T;
+  _ : associative operator;
+  _ : left_id idm operator;
+  _ : right_id idm operator
+}.
+ +
+Structure com_law := ComLaw {
+   com_operator : law;
+   _ : commutative com_operator
+}.
+ +
+Structure mul_law := MulLaw {
+  mul_operator : T → T → T;
+  _ : left_zero idm mul_operator;
+  _ : right_zero idm mul_operator
+}.
+ +
+Structure add_law (mul : T → T → T) := 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.
+ +
+Module Import Exports.
+Coercion operator : law >-> Funclass.
+Coercion com_operator : com_law >-> law.
+Coercion mul_operator : mul_law >-> Funclass.
+Coercion add_operator : add_law >-> com_law.
+Notation "[ 'law' 'of' f ]" := (@clone_law _ _ f _ id _ _ _ id)
+  (at level 0, format"[ 'law' 'of' f ]") : form_scope.
+Notation "[ 'com_law' 'of' f ]" := (@clone_com_law _ _ f _ _ id id _ id)
+  (at level 0, format "[ 'com_law' 'of' f ]") : form_scope.
+Notation "[ 'mul_law' 'of' f ]" := (@clone_mul_law _ _ f _ id _ _ id)
+  (at level 0, format"[ 'mul_law' 'of' f ]") : form_scope.
+Notation "[ 'add_law' m 'of' a ]" := (@clone_add_law _ _ m a _ _ id id _ _ id)
+  (at level 0, format "[ 'add_law' m 'of' a ]") : form_scope.
+End Exports.
+ +
+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 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.
+ Lemma mulmACA : interchange mul 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.
+Export Monoid.Exports.
+ +
+Section PervasiveMonoids.
+ +
+Import Monoid.
+ +
+Canonical andb_monoid := Law andbA andTb andbT.
+Canonical andb_comoid := ComLaw andbC.
+ +
+Canonical andb_muloid := MulLaw andFb andbF.
+Canonical orb_monoid := Law orbA orFb orbF.
+Canonical orb_comoid := ComLaw orbC.
+Canonical orb_muloid := MulLaw orTb orbT.
+Canonical addb_monoid := Law addbA addFb addbF.
+Canonical addb_comoid := ComLaw addbC.
+Canonical orb_addoid := AddLaw andb_orl andb_orr.
+Canonical andb_addoid := AddLaw orb_andl orb_andr.
+Canonical addb_addoid := AddLaw andb_addl andb_addr.
+ +
+Canonical addn_monoid := Law addnA add0n addn0.
+Canonical addn_comoid := ComLaw addnC.
+Canonical muln_monoid := Law mulnA mul1n muln1.
+Canonical muln_comoid := ComLaw mulnC.
+Canonical muln_muloid := MulLaw mul0n muln0.
+Canonical addn_addoid := AddLaw mulnDl mulnDr.
+ +
+Canonical maxn_monoid := Law maxnA max0n maxn0.
+Canonical maxn_comoid := ComLaw maxnC.
+Canonical maxn_addoid := AddLaw maxn_mull maxn_mulr.
+ +
+Canonical gcdn_monoid := Law gcdnA gcd0n gcdn0.
+Canonical gcdn_comoid := ComLaw gcdnC.
+Canonical gcdnDoid := AddLaw muln_gcdl muln_gcdr.
+ +
+Canonical lcmn_monoid := Law lcmnA lcm1n lcmn1.
+Canonical lcmn_comoid := ComLaw lcmnC.
+Canonical lcmn_addoid := AddLaw muln_lcml muln_lcmr.
+ +
+Canonical cat_monoid T := Law (@catA T) (@cat0s T) (@cats0 T).
+ +
+End PervasiveMonoids.
+ +
+

+ +

+ Unit test for the [...law of ... ] Notations +Definition myp := addn. Definition mym := muln. +Canonical myp_mon := [law of myp]. +Canonical myp_cmon := [com_law of myp]. +Canonical mym_mul := [mul_law of mym]. +Canonical myp_add := [add_law _ of myp]. +Print myp_add. +Print Canonical Projections. + +

+ +
+Delimit Scope big_scope with BIG.
+Open Scope big_scope.
+ +
+

+ +

+ The bigbody wrapper is a workaround for a quirk of the Coq pretty-printer, + which would fail to redisplay the \big notation when the <general_term> or + <condition> do not depend on the bound index. The BigBody constructor + packages both in in a term in which i occurs; it also depends on the + iterated <op>, as this can give more information on the expected type of + the <general_term>, thus allowing for the insertion of coercions. +

+CoInductive bigbody R I := BigBody of I & (R → R → R) & bool & R.
+ +
+Definition applybig {R I} (body : bigbody R I) x :=
+  let: BigBody _ op b v := body in if b then op v x else x.
+ +
+Definition reducebig R I idx r (body : I → bigbody R I) :=
+  foldr (applybig \o body) idx r.
+ +
+Module Type BigOpSig.
+Parameter bigop : ∀ R I, R → seq I → (I → bigbody R I ) → R.
+Axiom bigopE : bigop = reducebig.
+End BigOpSig.
+ +
+Module BigOp : BigOpSig.
+Definition bigop := reducebig.
+Lemma bigopE : bigop = reducebig.
+End BigOp.
+ +
+Notation bigop := BigOp.bigop (only parsing).
+Canonical bigop_unlock := Unlockable BigOp.bigopE.
+ +
+Definition index_iota m n := iota m (n - m).
+ +
+Definition index_enum (T : finType) := Finite.enum T.
+ +
+Lemma mem_index_iota m n i : i \in index_iota m n = (m ≤ i < n ).
+ +
+Lemma mem_index_enum T i : i \in index_enum T.
+ Hint Resolve mem_index_enum.
+ +
+Lemma filter_index_enum T P : filter P (index_enum T) = enum P.
+ +
+Notation "\big [ op / idx ]_ ( i <- r | P ) F" :=
+  (bigop idx r (fun i ⇒ BigBody i op P%B F)) : big_scope.
+Notation "\big [ op / idx ]_ ( i <- r ) F" :=
+  (bigop idx r (fun i ⇒ BigBody i op true F)) : big_scope.
+Notation "\big [ op / idx ]_ ( m <= i < n | P ) F" :=
+  (bigop idx (index_iota m n) (fun i : nat ⇒ BigBody i op P%B F))
+     : big_scope.
+Notation "\big [ op / idx ]_ ( m <= i < n ) F" :=
+  (bigop idx (index_iota m n) (fun i : nat ⇒ BigBody i op true F))
+     : big_scope.
+Notation "\big [ op / idx ]_ ( i | P ) F" :=
+  (bigop idx (index_enum _) (fun i ⇒ BigBody i op P%B F)) : big_scope.
+Notation "\big [ op / idx ]_ i F" :=
+  (bigop idx (index_enum _) (fun i ⇒ BigBody i op true F)) : big_scope.
+Notation "\big [ op / idx ]_ ( i : t | P ) F" :=
+  (bigop idx (index_enum _) (fun i : t ⇒ BigBody i op P%B F))
+     (only parsing) : big_scope.
+Notation "\big [ op / idx ]_ ( i : t ) F" :=
+  (bigop idx (index_enum _) (fun i : t ⇒ BigBody i op true 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 BIG_F := (F in \big [_/_]_(i <- _ | _) F i )%pattern.
+Notation BIG_P := (P in \big [_/_]_(i <- _ | P i ) _)%pattern.
+ +
+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 "\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_ ( 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.
+ +
+

+ +

+ Induction loading +

+Lemma big_load R (K K' : R → Type) idx op I r (P : pred I) F :
+  K (\big [op /idx ]_(i <- r | P i ) F i) × K' (\big [op /idx ]_(i <- r | P i ) F i)
+  → K' (\big [op /idx ]_(i <- r | P i ) F i).
+ +
+ +
+Section Elim3.
+ +
+Variables (R1 R2 R3 : Type) (K : R1 → R2 → R3 → Type).
+Variables (id1 : R1) (op1 : R1 → R1 → R1).
+Variables (id2 : R2) (op2 : R2 → R2 → R2).
+Variables (id3 : R3) (op3 : R3 → R3 → R3).
+ +
+Hypothesis Kid : K id1 id2 id3.
+ +
+Lemma big_rec3 I r (P : pred I) F1 F2 F3
+    (K_F : ∀ i y1 y2 y3, P i → K y1 y2 y3 →
+       K (op1 (F1 i) y1) (op2 (F2 i) y2) (op3 (F3 i) y3)) :
+  K (\big [op1 /id1 ]_(i <- r | P i ) F1 i)
+    (\big [op2 /id2 ]_(i <- r | P i ) F2 i)
+    (\big [op3 /id3 ]_(i <- r | P i ) F3 i).
+ +
+Hypothesis Kop : ∀ x1 x2 x3 y1 y2 y3,
+  K x1 x2 x3 → K y1 y2 y3 → K (op1 x1 y1) (op2 x2 y2) (op3 x3 y3).
+Lemma big_ind3 I r (P : pred I) F1 F2 F3
+   (K_F : ∀ i, P i → K (F1 i) (F2 i) (F3 i)) :
+  K (\big [op1 /id1 ]_(i <- r | P i ) F1 i)
+    (\big [op2 /id2 ]_(i <- r | P i ) F2 i)
+    (\big [op3 /id3 ]_(i <- r | P i ) F3 i).
+ +
+End Elim3.
+ +
+ +
+Section Elim2.
+ +
+Variables (R1 R2 : Type) (K : R1 → R2 → Type) (f : R2 → R1).
+Variables (id1 : R1) (op1 : R1 → R1 → R1).
+Variables (id2 : R2) (op2 : R2 → R2 → R2).
+ +
+Hypothesis Kid : K id1 id2.
+ +
+Lemma big_rec2 I r (P : pred I) F1 F2
+    (K_F : ∀ i y1 y2, P i → K y1 y2 →
+       K (op1 (F1 i) y1) (op2 (F2 i) y2)) :
+  K (\big [op1 /id1 ]_(i <- r | P i ) F1 i) (\big [op2 /id2 ]_(i <- r | P i ) F2 i).
+ +
+Hypothesis Kop : ∀ x1 x2 y1 y2,
+  K x1 x2 → K y1 y2 → K (op1 x1 y1) (op2 x2 y2).
+Lemma big_ind2 I r (P : pred I) F1 F2 (K_F : ∀ i, P i → K (F1 i) (F2 i)) :
+  K (\big [op1 /id1 ]_(i <- r | P i ) F1 i) (\big [op2 /id2 ]_(i <- r | P i ) F2 i).
+ +
+Hypotheses (f_op : {morph f : x y / op2 x y >-> op1 x y }) (f_id : f id2 = id1).
+Lemma big_morph I r (P : pred I) F :
+  f (\big [op2 /id2 ]_(i <- r | P i ) F i) = \big [op1 /id1 ]_(i <- r | P i ) f (F i).
+ +
+End Elim2.
+ +
+ +
+Section Elim1.
+ +
+Variables (R : Type) (K : R → Type) (f : R → R).
+Variables (idx : R) (op op' : R → R → R).
+ +
+Hypothesis Kid : K idx.
+ +
+Lemma big_rec I r (P : pred I) F
+    (Kop : ∀ i x, P i → K x → K (op (F i) x)) :
+  K (\big [op /idx ]_(i <- r | P i ) F i).
+ +
+Hypothesis Kop : ∀ x y, K x → K y → K (op x y).
+Lemma big_ind I r (P : pred I) F (K_F : ∀ i, P i → K (F i)) :
+  K (\big [op /idx ]_(i <- r | P i ) F i).
+ +
+Hypothesis Kop' : ∀ x y, K x → K y → op x y = op' x y.
+Lemma eq_big_op I r (P : pred I) F (K_F : ∀ i, P i → K (F i)) :
+  \big [op /idx ]_(i <- r | P i ) F i = \big [op'/idx ]_(i <- r | P i ) F i.
+ +
+Hypotheses (fM : {morph f : x y / op x y }) (f_id : f idx = idx).
+Lemma big_endo I r (P : pred I) F :
+  f (\big [op /idx ]_(i <- r | P i ) F i) = \big [op /idx ]_(i <- r | P i ) f (F i).
+ +
+End Elim1.
+ +
+ +
+Section Extensionality.
+ +
+Variables (R : Type) (idx : R) (op : R → R → R).
+ +
+Section SeqExtension.
+ +
+Variable I : Type.
+ +
+Lemma big_filter 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 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 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.
+ +
+

+ +

+ A lemma to permute aggregate conditions. +

+Lemma big_andbC r (P Q : pred I) F :
+  \big [op /idx ]_(i <- r | P i && Q i ) F i
+    = \big [op /idx ]_(i <- r | Q i && P i ) F i.
+ +
+Lemma eq_bigr r (P : pred I) F1 F2 : (∀ 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 r (P1 P2 : pred I) F1 F2 :
+    P1 =1 P2 → (∀ 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 r1 r2 (P1 P2 : pred I) F1 F2 :
+    r1 = r2 → P1 =1 P2 → (∀ 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 (P : pred I) F : \big [op /idx ]_(i <- [::] | P i ) F i = idx.
+ +
+Lemma big_cons 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 J (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 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 r (P : pred I) F :
+  ~~ has P r → \big [op /idx ]_(i <- r | P i ) F i = idx.
+ +
+Lemma big_pred0_eq (r : seq I) F : \big [op /idx ]_(i <- r | false ) F i = idx.
+ +
+Lemma big_pred0 r (P : pred I) F :
+  P =1 xpred0 → \big [op /idx ]_(i <- r | P i ) F i = idx.
+ +
+Lemma big_cat_nested 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 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 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 r (P : pred I) x :
+  \big [op /idx ]_(i <- r | P i ) x = iter (count P r) (op x) idx.
+ +
+End SeqExtension.
+ +
+

+ +

+ The following lemmas can be used to localise extensionality to a specific + index sequence. This is done by ssreflect rewriting, before applying + congruence or induction lemmas. +

+Lemma big_seq_cond (I : eqType) r (P : pred I) F :
+  \big [op /idx ]_(i <- r | P i ) F i
+    = \big [op /idx ]_(i <- r | (i \in r ) && P i ) F i.
+ +
+Lemma big_seq (I : eqType) (r : seq I) F :
+  \big [op /idx ]_(i <- r ) F i = \big [op /idx ]_(i <- r | i \in r ) F i.
+ +
+Lemma eq_big_seq (I : eqType) (r : seq I) F1 F2 :
+  {in r , F1 =1 F2 } → \big [op /idx ]_(i <- r ) F1 i = \big [op /idx ]_(i <- r ) F2 i.
+ +
+

+ +

+ Similar lemmas for exposing integer indexing in the predicate. +

+Lemma big_nat_cond m n (P : pred nat) F :
+  \big [op /idx ]_(m ≤ i < n | P i ) F i
+    = \big [op /idx ]_(m ≤ i < n | (m ≤ i < n ) && P i ) F i.
+ +
+Lemma big_nat m n F :
+  \big [op /idx ]_(m ≤ i < n ) F i = \big [op /idx ]_(m ≤ i < n | m ≤ i < n ) F i.
+ +
+Lemma congr_big_nat m1 n1 m2 n2 P1 P2 F1 F2 :
+    m1 = m2 → n1 = n2 →
+    (∀ i, m1 ≤ i < n2 → P1 i = P2 i ) →
+    (∀ 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 eq_big_nat m n F1 F2 :
+    (∀ i, m ≤ i < n → F1 i = F2 i ) →
+  \big [op /idx ]_(m ≤ i < n ) F1 i = \big [op /idx ]_(m ≤ i < n ) F2 i.
+ +
+Lemma big_geq m n (P : pred nat) F :
+  m ≥ n → \big [op /idx ]_(m ≤ i < n | P i ) F i = idx.
+ +
+Lemma big_ltn_cond 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 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 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 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 n m F : m ≤ n →
+  \big [op /idx ]_(m ≤ i < n .+1 ) F i =
+     op (F m) (\big [op /idx ]_(m ≤ i < n ) F i .+1).
+ +
+Lemma big_mkord 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 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 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 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 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_ord0 P F : \big [op /idx ]_(i < 0 | P i ) F i = idx.
+ +
+Lemma big_tnth I r (P : pred I) F :
+  let r_ := tnth (in_tuple r) in
+  \big [op /idx ]_(i <- r | P i ) F i
+     = \big [op /idx ]_(i < size r | P (r_ i)) (F (r_ i)).
+ +
+Lemma big_index_uniq (I : eqType) (r : seq I) (E : 'I_(size r ) → R) :
+    uniq r →
+  \big [op /idx ]_i E i = \big [op /idx ]_(x <- r ) oapp E idx (insub (index x r)).
+ +
+Lemma big_tuple I n (t : n .-tuple I) (P : pred I) F :
+  \big [op /idx ]_(i <- t | P i ) F i
+     = \big [op /idx ]_(i < n | P (tnth t i)) F (tnth t i).
+ +
+Lemma big_ord_narrow_cond n1 n2 (P : pred 'I_n2) F (le_n12 : n1 ≤ n2) :
+    let w := widen_ord le_n12 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 n1 n2 (P : pred _) F (le_n12 : n1 ≤ n2) :
+    let w := @widen_ord n1 .+1 n2 .+1 le_n12 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 n1 n2 F (le_n12 : n1 ≤ n2) :
+    let w := widen_ord le_n12 in
+  \big [op /idx ]_(i < n2 | i < n1 ) F i = \big [op /idx ]_(i < n1 ) F (w i).
+ +
+Lemma big_ord_narrow_leq n1 n2 F (le_n12 : n1 ≤ n2) :
+    let w := @widen_ord n1 .+1 n2 .+1 le_n12 in
+  \big [op /idx ]_(i < n2 .+1 | i ≤ n1 ) F i = \big [op /idx ]_(i < n1 .+1 ) F (w i).
+ +
+Lemma big_ord_recl 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 (I : finType) (A : pred I) x :
+  \big [op /idx ]_(i in A ) x = iter #|A | (op x) idx.
+ +
+Lemma big_const_nat m n x :
+  \big [op /idx ]_(m ≤ i < n ) x = iter (n - m) (op x) idx.
+ +
+Lemma big_const_ord n x :
+  \big [op /idx ]_(i < n ) x = iter n (op x) idx.
+ +
+Lemma big_nseq_cond I n a (P : pred I) F :
+  \big [op /idx ]_(i <- nseq n a | P i ) F i = if P a then iter n (op (F a)) idx else idx.
+ +
+Lemma big_nseq I n a (F : I → R):
+  \big [op /idx ]_(i <- nseq n a ) F i = iter n (op (F a)) idx.
+ +
+End Extensionality.
+ +
+Section MonoidProperties.
+ +
+Import Monoid.Theory.
+ +
+Variable R : Type.
+ +
+Variable idx : R.
+ +
+Section Plain.
+ +
+Variable op : Monoid.law 1.
+ +
+ +
+Lemma eq_big_idx_seq 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 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 I r (P : pred I) : \big [*%M /1]_(i <- r | P i ) 1 = 1.
+ +
+Lemma big1 I r (P : pred I) F :
+  (∀ i, P i → F i = 1) → \big [*%M /1]_(i <- r | P i ) F i = 1.
+ +
+Lemma big1_seq (I : eqType) r (P : pred I) F :
+    (∀ i, P i && (i \in r ) → F i = 1) →
+  \big [*%M /1]_(i <- r | P i ) F i = 1.
+ +
+Lemma big_seq1 I (i : I) F : \big [*%M /1]_(j <- [:: i ]) F j = F i.
+ +
+Lemma big_mkcond 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_mkcondr I r (P Q : pred I) F :
+  \big [*%M /1]_(i <- r | P i && Q i ) F i =
+     \big [*%M /1]_(i <- r | P i ) (if Q i then F i else 1).
+ +
+Lemma big_mkcondl I r (P Q : pred I) F :
+  \big [*%M /1]_(i <- r | P i && Q i ) F i =
+     \big [*%M /1]_(i <- r | Q i ) (if P i then F i else 1).
+ +
+Lemma big_cat 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_allpairs I1 I2 (r1 : seq I1) (r2 : seq I2) F :
+  \big [*%M /1]_(i <- [seq (i1 , i2 ) | i1 <- r1 , i2 <- r2 ]) F i =
+    \big [*%M /1]_(i1 <- r1 ) \big [op /idx ]_(i2 <- r2 ) F (i1 , i2 ).
+ +
+Lemma big_pred1_eq (I : finType) (i : I) F :
+  \big [*%M /1]_(j | j == i ) F j = F i.
+ +
+Lemma big_pred1 (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 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 n F : \big [*%M /1]_(n ≤ i < n .+1 ) F i = F n.
+ +
+Lemma big_nat_recr n m F : m ≤ n →
+  \big [*%M /1]_(m ≤ i < n .+1 ) F i = (\big [*%M /1]_(m ≤ i < n ) F i ) × F n.
+ +
+Lemma big_ord_recr 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 (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 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)).
+ +
+Lemma big_flatten I rr (P : pred I) F :
+  \big [*%M /1]_(i <- flatten rr | P i ) F i
+    = \big [*%M /1]_(r <- rr ) \big [*%M /1]_(i <- r | P i ) F i.
+ +
+End Plain.
+ +
+Section Abelian.
+ +
+Variable op : Monoid.com_law 1.
+ +
+ +
+Lemma eq_big_perm (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 (I : finType) (r : seq I) F :
+  uniq r → \big [*%M /1]_(i <- r ) F i = \big [*%M /1]_(i in r ) F i.
+ +
+Lemma big_rem (I : eqType) r x (P : pred I) F :
+    x \in r →
+  \big [*%M /1]_(y <- r | P y ) F y
+    = (if P x then F x else 1) × \big [*%M /1]_(y <- rem x r | P y ) F y.
+ +
+Lemma big_undup (I : eqType) (r : seq I) (P : pred I) F :
+    idempotent *%M →
+  \big [*%M /1]_(i <- undup r | P i ) F i = \big [*%M /1]_(i <- r | P i ) F i.
+ +
+Lemma eq_big_idem (I : eqType) (r1 r2 : seq I) (P : pred I) F :
+    idempotent *%M → r1 =i r2 →
+  \big [*%M /1]_(i <- r1 | P i ) F i = \big [*%M /1]_(i <- r2 | P i ) F i.
+ +
+Lemma big_undup_iterop_count (I : eqType) (r : seq I) (P : pred I) F :
+  \big [*%M /1]_(i <- undup r | P i ) iterop (count_mem i r) *%M (F i) 1
+    = \big [*%M /1]_(i <- r | P i ) F i.
+ +
+Lemma big_split 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 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.
+ +
+Lemma bigU (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 (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.
+ +
+Lemma bigD1_seq (I : eqType) (r : seq I) j F :
+    j \in r → uniq r →
+  \big [*%M /1]_(i <- r ) F i = F j × \big [*%M /1]_(i <- r | i != j ) F i.
+ +
+Lemma cardD1x (I : finType) (A : pred I) j :
+  A j → #|SimplPred A | = 1 + #|[pred i | A i & i != j ]|.
+ +
+Lemma partition_big (I J : finType) (P : pred I) p (Q : pred J) F :
+    (∀ 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.
+ +
+ +
+Lemma reindex_onto (I J : finType) (h : J → I) h' (P : pred I) F :
+   (∀ 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).
+ +
+Lemma reindex (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).
+ +
+Lemma reindex_inj (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).
+ +
+Lemma big_nat_rev 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 (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 (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 (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 I J rI rJ (P : pred I) (Q : I → pred J)
+                       (xQ : pred J) F :
+    (∀ i j, P i → Q i j → xQ j ) →
+  \big [*%M /1]_(i <- rI | P i ) \big [*%M /1]_(j <- rJ | Q i j ) F i j =
+    \big [*%M /1]_(j <- rJ | xQ j ) \big [*%M /1]_(i <- rI | P i && Q i j ) F i j.
+ +
+Lemma exchange_big I J rI rJ (P : pred I) (Q : pred J) F :
+  \big [*%M /1]_(i <- rI | P i ) \big [*%M /1]_(j <- rJ | Q j ) F i j =
+    \big [*%M /1]_(j <- rJ | Q j ) \big [*%M /1]_(i <- rI | P i ) F i j.
+ +
+Lemma exchange_big_dep_nat m1 n1 m2 n2 (P : pred nat) (Q : rel nat)
+                           (xQ : pred nat) F :
+    (∀ 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.
+ +
+Lemma exchange_big_nat 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.
+ +
+ +
+Section Distributivity.
+ +
+Import Monoid.Theory.
+ +
+Variable R : Type.
+Variables zero one : R.
+Variable times : Monoid.mul_law 0.
+Variable plus : Monoid.add_law 0 *%M.
+ +
+Lemma big_distrl 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 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_distrlr I J rI rJ (pI : pred I) (pJ : pred J) F G :
+  (\big [+%M /0]_(i <- rI | pI i ) F i ) × (\big [+%M /0]_(j <- rJ | pJ j ) G j )
+   = \big [+%M /0]_(i <- rI | pI i ) \big [+%M /0]_(j <- rJ | pJ j ) (F i × G j ).
+ +
+Lemma big_distr_big_dep (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 in pfamily j0 P Q ) \big [*%M /1]_(i | P i ) F i (f i).
+ +
+Lemma big_distr_big (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 in pffun_on j0 P Q ) \big [*%M /1]_(i | P i ) F i (f i).
+ +
+Lemma bigA_distr_big_dep (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 in family Q ) \big [*%M /1]_i F i (f i).
+ +
+Lemma bigA_distr_big (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 in ffun_on Q ) \big [*%M /1]_i F i (f i).
+ +
+Lemma bigA_distr_bigA (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.
+ +
+ +
+Section BigBool.
+ +
+Section Seq.
+ +
+Variables (I : Type) (r : seq I) (P B : pred I).
+ +
+Lemma big_has : \big [orb /false ]_(i <- r ) B i = has B r.
+ +
+Lemma big_all : \big [andb /true ]_(i <- r ) B i = all B r.
+ +
+Lemma big_has_cond : \big [orb /false ]_(i <- r | P i ) B i = has (predI P B) r.
+ +
+Lemma big_all_cond :
+  \big [andb /true ]_(i <- r | P i ) B i = all [pred i | P i ==> B i ] r.
+ +
+End Seq.
+ +
+Section FinType.
+ +
+Variables (I : finType) (P B : pred I).
+ +
+Lemma big_orE : \big [orb /false ]_(i | P i ) B i = [∃ (i | P i ), B i ].
+ +
+Lemma big_andE : \big [andb /true ]_(i | P i ) B i = [∀ (i | P i ), B i ].
+ +
+End FinType.
+ +
+End BigBool.
+ +
+Section NatConst.
+ +
+Variables (I : finType) (A : pred I).
+ +
+Lemma sum_nat_const n : \sum_(i in A ) n = #|A | × n.
+ +
+Lemma sum1_card : \sum_(i in A ) 1 = #|A |.
+ +
+Lemma sum1_count J (r : seq J) (a : pred J) : \sum_(j <- r | a j ) 1 = count a r.
+ +
+Lemma sum1_size J (r : seq J) : \sum_(j <- r ) 1 = size r.
+ +
+Lemma prod_nat_const n : \prod_(i in A ) n = n ^ #|A |.
+ +
+Lemma sum_nat_const_nat n1 n2 n : \sum_(n1 ≤ i < n2 ) n = (n2 - n1 ) × n.
+ +
+Lemma prod_nat_const_nat n1 n2 n : \prod_(n1 ≤ i < n2 ) n = n ^ (n2 - n1 ).
+ +
+End NatConst.
+ +
+Lemma leqif_sum (I : finType) (P C : pred I) (E1 E2 : I → nat) :
+    (∀ i, P i → E1 i ≤ E2 i ?= iff C i ) →
+  \sum_(i | P i ) E1 i ≤ \sum_(i | P i ) E2 i ?= iff [∀ (i | P i ), C i ].
+ +
+Lemma leq_sum I r (P : pred I) (E1 E2 : I → nat) :
+    (∀ i, P i → E1 i ≤ E2 i ) →
+  \sum_(i <- r | P i ) E1 i ≤ \sum_(i <- r | P i ) E2 i.
+ +
+Lemma sum_nat_eq0 (I : finType) (P : pred I) (E : I → nat) :
+  (\sum_(i | P i ) E i == 0)%N = [∀ (i | P i ), E i == 0%N].
+ +
+Lemma prodn_cond_gt0 I r (P : pred I) F :
+  (∀ i, P i → 0 < F i ) → 0 < \prod_(i <- r | P i ) F i.
+ +
+Lemma prodn_gt0 I r (P : pred I) F :
+  (∀ i, 0 < F i ) → 0 < \prod_(i <- r | P i ) F i.
+ +
+Lemma leq_bigmax_cond (I : finType) (P : pred I) F i0 :
+  P i0 → F i0 ≤ \max_(i | P i ) F i.
+ +
+Lemma leq_bigmax (I : finType) F (i0 : I) : F i0 ≤ \max_i F i.
+ +
+Lemma bigmax_leqP (I : finType) (P : pred I) m F :
+  reflect (∀ i, P i → F i ≤ m) (\max_(i | P i ) F i ≤ m).
+ +
+Lemma bigmax_sup (I : finType) i0 (P : pred I) m F :
+  P i0 → m ≤ F i0 → m ≤ \max_(i | P i ) F i.
+ +
+Lemma bigmax_eq_arg (I : finType) i0 (P : pred I) F :
+  P i0 → \max_(i | P i ) F i = F [arg max_(i > i0 | P i ) F i ].
+ +
+Lemma eq_bigmax_cond (I : finType) (A : pred I) F :
+  #|A | > 0 → {i0 | i0 \in A & \max_(i in A ) F i = F i0 }.
+ +
+Lemma eq_bigmax (I : finType) F : #|I | > 0 → {i0 : I | \max_i F i = F i0 }.
+ +
+Lemma expn_sum 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 (I : finType) (P : pred I) F m :
+  reflect (∀ i, P i → F i %| m) (\big [lcmn /1%N]_(i | P i ) F i %| m).
+ +
+Lemma biglcmn_sup (I : finType) i0 (P : pred I) F m :
+  P i0 → m %| F i0 → m %| \big [lcmn /1%N]_(i | P i ) F i.
+ +
+Lemma dvdn_biggcdP (I : finType) (P : pred I) F m :
+  reflect (∀ i, P i → m %| F i) (m %| \big [gcdn /0]_(i | P i ) F i).
+ +
+Lemma biggcdn_inf (I : finType) i0 (P : pred I) F m :
+  P i0 → F i0 %| m → \big [gcdn /0]_(i | P i ) F i %| m.
+ +
+Unset Implicit Arguments.
+