- -

Library mathcomp.ssreflect.bigop

- -

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

- -

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

-Variant 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 : core.
- -
-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 foldrE r : foldr op idx r = \big [op /idx ]_(x <- r ) x.
- -
-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.
- -
-Lemma big_map_id J (h : J → R) r (P : pred R) :
-  \big [op /idx ]_(i <- map h r | P i ) i
-     = \big [op /idx ]_(j <- r | P (h j)) h j.
- -
-

- -

- 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.
- -
-Lemma big_image_cond I (J : finType) (h : J → I) (A : pred J) (P : pred I) F :
-  \big [op /idx ]_(i <- [seq h j | j in A ] | P i ) F i
-     = \big [op /idx ]_(j in A | P (h j)) F (h j).
- -
-Lemma big_image I (J : finType) (h : J → I) (A : pred J) F :
-  \big [op /idx ]_(i <- [seq h j | j in A ]) F i = \big [op /idx ]_(j in A ) F (h j).
- -
-Lemma big_image_cond_id (J : finType) (h : J → R) (A : pred J) (P : pred R) :
-  \big [op /idx ]_(i <- [seq h j | j in A ] | P i ) i
-     = \big [op /idx ]_(j in A | P (h j)) h j.
- -
-Lemma big_image_id (J : finType) (h : J → R) (A : pred J) :
-  \big [op /idx ]_(i <- [seq h j | j in A ]) i = \big [op /idx ]_(j in A ) h j.
- -
-End Extensionality.
- -
-Section MonoidProperties.
- -
-Import Monoid.Theory.
- -
-Variable R : Type.
- -
-Variable idx : R.
- -
-Section Plain.
- -
-Variable op : Monoid.law 1.
- -
- -
-Lemma foldlE x r : foldl *%M x r = \big [*%M /1]_(y <- x :: r ) y.
- -
-Lemma foldl_idx r : foldl *%M 1 r = \big [*%M /1]_(x <- r ) x.
- -
-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_dep I1 (I2 : I1 → Type) J (h : ∀ i1, I2 i1 → J)
-    (r1 : seq I1) (r2 : ∀ i1, seq (I2 i1)) (F : J → R) :
-  \big [*%M /1]_(i <- [seq h i1 i2 | i1 <- r1 , i2 <- r2 i1 ]) F i =
-    \big [*%M /1]_(i1 <- r1 ) \big [*%M /1]_(i2 <- r2 i1 ) F (h i1 i2).
- -
-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 perm_big (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 sumnE r : sumn r = \sum_(i <- r ) i.
- -
-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.
- -
-Notation "@ 'eq_big_perm'" :=
-  (deprecate eq_big_perm perm_big) (at level 10, only parsing).
- -
-Notation eq_big_perm :=
-  ((fun R idx op I r1 P F r2 ⇒ @eq_big_perm R idx op I r1 r2 P F)
-        _ _ _ _ _ _ _) (only parsing).
-