Library mathcomp.ssreflect.bigop

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)
From HB Require Import structures.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path.
From mathcomp Require Import div fintype tuple finfun.

This file provides a generic definition for iterating an operator over a set of indices (bigop); this big operator is parameterized 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 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 (semirings). 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.

Declare Scope big_scope.

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


#[export]
HB.structure Definition Law T := {op of isLaw T op}.
Definition law := Law.type.


#[export]
HB.structure Definition ComLaw T := {op of Law T op & isCommutativeLaw T op}.
Definition com_law := ComLaw.type.





Module Import Exports. End Exports.

Module Theory.

Section Theory.
Variables (T : Type).

Section Plain.
Variable mul : law T.
Lemma mulmA : associative mul.
End Plain.

Section Commutative.
Variable mul : com_law T.
Lemma mulmC : commutative mul.
Lemma mulmCA : left_commutative mul.
Lemma mulmAC : right_commutative mul.
Lemma mulmACA : interchange mul mul.
End Commutative.

End Theory.

End Theory.

Include Theory.

End SemiGroup.
Export SemiGroup.Exports.

Module Monoid.

Export SemiGroup.


#[export]
HB.structure Definition Law T idm :=
  {op of SemiGroup.Law T op & isMonoidLaw T idm op}.
Definition law := Law.type.





#[export]
HB.structure Definition ComLaw T idm :=
  {op of Law T idm op & isCommutativeLaw T op}.
Definition com_law := ComLaw.type.



Lemma opm1 : right_id idm op.




#[export]
HB.structure Definition MulLaw T zero := {mul of isMulLaw T zero mul}.
Definition mul_law := MulLaw.type.


#[export]
HB.structure Definition AddLaw T zero mul :=
  {add of ComLaw T zero add & isAddLaw T mul add}.
Definition add_law := AddLaw.type.

Module Import Exports. End Exports.

Section CommutativeAxioms.

Variable (T : Type) (zero one : T) (mul add : T → 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.

Export SemiGroup.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 iteropE n x : iterop n mul x idm = iter n (mul x) idm.
End Plain.

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 mulmDl : left_distributive mul add.
Lemma mulmDr : right_distributive mul add.
End Add.

Definition simpm := (mulm1, mulm0, mul1m, mul0m, mulmA).

End Theory.

End Theory.
Include SemiGroup.Theory.
Include Theory.

End Monoid.
Export Monoid.Exports.

Section PervasiveMonoids.

Import Monoid.








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.

Canonical bigop_unlock := Unlockable bigop.unlock.

Definition index_iota m n := iota m (n - m).

Lemma mem_index_iota m n i : i \in index_iota m n = (m ≤ i < n).

Legacy mathcomp scripts have been relying on the fact that enum A and filter A (index_enum T) are convertible. This is likely to change in the next mathcomp release when enum, pick, subset and card are generalised to predicates with finite support in a choiceType - in fact the two will only be equal up to permutation in this new theory. It is therefore advisable to stop relying on this, and use the new facilities provided in this library: lemmas big_enumP, big_enum, big_image and such. Users wishing to test compliance should change the Defined in index_enum_key to Qed, and comment out the filter_index_enum compatibility definition below (or Import Deprecation.Reject).
Fact index_enum_key : unit. (* Qed. *)
Definition index_enum (T : finType) :=
  locked_with index_enum_key (Finite.enum T).

Lemma deprecated_filter_index_enum T P : filter P (index_enum T) = enum P.

Lemma mem_index_enum T i : i \in index_enum T.
#[global] Hint Resolve mem_index_enum : core.

Lemma index_enum_uniq T : uniq (index_enum T).

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

Arguments big_load [R] K [K'] idx op [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.

Arguments big_rec3 [R1 R2 R3] K [id1 op1 id2 op2 id3 op3] _ [I r P F1 F2 F3].
Arguments big_ind3 [R1 R2 R3] K [id1 op1 id2 op2 id3 op3] _ _ [I r P F1 F2 F3].

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.

Arguments big_rec2 [R1 R2] K [id1 op1 id2 op2] _ [I r P F1 F2].
Arguments big_ind2 [R1 R2] K [id1 op1 id2 op2] _ _ [I r P F1 F2].
Arguments big_morph [R1 R2] f [id1 op1 id2 op2] _ _ [I].

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.

Arguments big_rec [R] K [idx op] _ [I r P F].
Arguments big_ind [R] K [idx op] _ _ [I r P F].
Arguments eq_big_op [R] K [idx op] op' _ _ _ [I].
Arguments big_endo [R] f [idx op] _ _ [I].

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.

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_mask_tuple I n m (t : n.-tuple I) (P : pred I) F :
  \big[op/idx]_(i <- mask m t | P i) F i
    = \big[op/idx]_(i < n | nth false m i && P (tnth t i)) F (tnth t i).

Lemma big_mask I r m (P : pred I) (F : I → R) (r_ := tnth (in_tuple r)) :
  \big[op/idx]_(i <- mask m r | P i) F i
    = \big[op/idx]_(i < size r | nth false m i && P (r_ i)) F (r_ i).

Lemma big_tnth I r (P : pred I) F (r_ := tnth (in_tuple r)) :
  \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_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.

Variant big_enum_spec (I : finType) (P : pred I) : seq I → Type :=
  BigEnumSpec e of
    ∀ R idx op (F : I → R),
      \big[op/idx]_(i <- e) F i = \big[op/idx]_(i | P i) F i
  & uniq e ∧ (∀ i, i \in e = P i)
  & (let cP := [pred i | P i] in perm_eq e (enum cP) ∧ size e = #|cP|)
  : big_enum_spec P e.

This lemma can be used to introduce an enumeration into a non-abelian bigop, in one of three ways: have [e big_e [Ue mem_e] [e_enum size_e] ] := big_enumP P. gives a permutation e of enum P alongside a equation big_e for converting between bigops iterating on (i <- e) and ones on (i | P i). Usually not all properties of e are needed, but see below the big_distr_big_dep proof where most are. rewrite -big_filter; have [e ... ] := big_enumP. uses big_filter to do this conversion first, and then abstracts the resulting filter P (index_enum T) enumeration as an e with the same properties (see big_enum_cond below for an example of this usage). Finally rewrite -big_filter; case def_e: _ / big_enumP => [e ... ] does the same while remembering the definition of e.

Lemma big_enumP I P : big_enum_spec P (filter P (index_enum I)).

Section BigConst.

Variables (R : Type) (idx : R) (op : R → R → R).

Lemma big_const_seq I r (P : pred I) x :
  \big[op/idx]_(i <- r | P i) x = iter (count P r) (op x) idx.

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.

End BigConst.

Section Plain.

Variable R : Type.
Variable op : R → R → R.
Variable x : R.

Lemma big_seq1_id I (i : I) (F : I → R) :
  \big[op/x]_(j <- [:: i]) F j = op (F i) x.

Lemma big_nat1_id n F : \big[op/x]_(n ≤ i < n.+1) F i = op (F n) x.

Lemma big_pred1_eq_id (I : finType) (i : I) F :
  \big[op/x]_(j | j == i) F j = op (F i) x.

Lemma big_pred1_id (I : finType) i (P : pred I) F :
  P =1 pred1 i → \big[op/x]_(j | P j) F j = op (F i) x.

End Plain.

Section SemiGroupProperties.

Variable R : Type.

#[local] Notation opA := SemiGroup.opA.
#[local] Notation opC := SemiGroup.opC.

Section Id.

Variable op : SemiGroup.law R.

Variable x : R.
Hypothesis opxx : op x x = x.

Lemma big_const_idem I (r : seq I) P : \big[op/x]_(i <- r | P i) x = x.

Lemma big1_idem I r (P : pred I) F :
  (∀ i, P i → F i = x) → \big[op/x]_(i <- r | P i) F i = x.

Lemma big_id_idem I (r : seq I) P F :
  op (\big[op/x]_(i <- r | P i) F i) x = \big[op/x]_(i <- r | P i) F i.

End Id.

Section Abelian.

Variable op : SemiGroup.com_law R.

Let opCA : left_commutative op.

Variable x : R.

Lemma big_rem_AC (I : eqType) (r : seq I) z (P : pred I) F : z \in r →
  \big[op/x]_(y <- r | P y) F y
    = if P z then op (F z) (\big[op/x]_(y <- rem z r | P y) F y)
      else \big[op/x]_(y <- rem z r | P y) F y.

Lemma big_undup (I : eqType) (r : seq I) (P : pred I) F :
    idempotent op →
  \big[op/x]_(i <- undup r | P i) F i = \big[op/x]_(i <- r | P i) F i.

Lemma perm_big (I : eqType) r1 r2 (P : pred I) F :
    perm_eq r1 r2 →
  \big[op/x]_(i <- r1 | P i) F i = \big[op/x]_(i <- r2 | P i) F i.

Lemma big_enum_cond (I : finType) (A : {pred I}) (P : pred I) F :
  \big[op/x]_(i <- enum A | P i) F i = \big[op/x]_(i in A | P i) F i.

Lemma big_enum (I : finType) (A : {pred I}) F :
  \big[op/x]_(i <- enum A) F i = \big[op/x]_(i in A) F i.

Lemma big_uniq (I : finType) (r : seq I) F :
  uniq r → \big[op/x]_(i <- r) F i = \big[op/x]_(i in r) F i.

Lemma bigD1 (I : finType) j (P : pred I) F :
  P j → \big[op/x]_(i | P i) F i
    = op (F j) (\big[op/x]_(i | P i && (i != j)) F i).
Arguments bigD1 [I] j [P F].

Lemma bigD1_seq (I : eqType) (r : seq I) j F :
    j \in r → uniq r →
  \big[op/x]_(i <- r) F i = op (F j) (\big[op/x]_(i <- r | i != j) F i).

Lemma big_image_cond I (J : finType) (h : J → I) (A : pred J) (P : pred I) F :
  \big[op/x]_(i <- [seq h j | j in A] | P i) F i
     = \big[op/x]_(j in A | P (h j)) F (h j).

Lemma big_image I (J : finType) (h : J → I) (A : pred J) F :
  \big[op/x]_(i <- [seq h j | j in A]) F i = \big[op/x]_(j in A) F (h j).

Lemma cardD1x (I : finType) (A : pred I) j :
  A j → #|SimplPred A| = 1 + #|[pred i | A i & i != j]|.
Arguments cardD1x [I A].

Lemma reindex_omap (I J : finType) (h : J → I) h' (P : pred I) F :
    (∀ i, P i → omap h (h' i) = some i) →
  \big[op/x]_(i | P i) F i =
    \big[op/x]_(j | P (h j) && (h' (h j) == some j)) F (h j).
Arguments reindex_omap [I J] h h' [P F].

Lemma reindex_onto (I J : finType) (h : J → I) h' (P : pred I) F :
    (∀ i, P i → h (h' i) = i) →
  \big[op/x]_(i | P i) F i =
    \big[op/x]_(j | P (h j) && (h' (h j) == j)) F (h j).
Arguments reindex_onto [I J] h h' [P F].

Lemma reindex (I J : finType) (h : J → I) (P : pred I) F :
    {on [pred i | P i], bijective h} →
  \big[op/x]_(i | P i) F i = \big[op/x]_(j | P (h j)) F (h j).
Arguments reindex [I J] h [P F].

Lemma reindex_inj (I : finType) (h : I → I) (P : pred I) F :
  injective h → \big[op/x]_(i | P i) F i = \big[op/x]_(j | P (h j)) F (h j).
Arguments reindex_inj [I h P F].

Lemma bigD1_ord n j (P : pred 'I_n) F :
  P j → \big[op/x]_(i < n | P i) F i
    = op (F j) (\big[op/x]_(i < n.-1 | P (lift j i)) F (lift j i)).

Lemma big_enum_val_cond (I : finType) (A : pred I) (P : pred I) F :
  \big[op/x]_(x in A | P x) F x =
  \big[op/x]_(i < #|A| | P (enum_val i)) F (enum_val i).
Arguments big_enum_val_cond [I A] P F.

Lemma big_enum_rank_cond (I : finType) (A : pred I) z (zA : z \in A) P F
  (h := enum_rank_in zA) :
  \big[op/x]_(i < #|A| | P i) F i = \big[op/x]_(s in A | P (h s)) F (h s).
Arguments big_enum_rank_cond [I A z] zA P F.

Lemma big_nat_rev m n P F :
  \big[op/x]_(m ≤ i < n | P i) F i
     = \big[op/x]_(m ≤ i < n | P (m + n - i.+1)) F (m + n - i.+1).

Lemma big_rev_mkord m n P F :
 \big[op/x]_(m ≤ k < n | P k) F k
    = \big[op/x]_(k < n - m | P (n - k.+1)) F (n - k.+1).

Section Id.

Hypothesis opxx : op x x = x.

Lemma big_mkcond_idem I r (P : pred I) F :
  \big[op/x]_(i <- r | P i) F i = \big[op/x]_(i <- r) (if P i then F i else x).

Lemma big_mkcondr_idem I r (P Q : pred I) F :
  \big[op/x]_(i <- r | P i && Q i) F i =
    \big[op/x]_(i <- r | P i) (if Q i then F i else x).

Lemma big_mkcondl_idem I r (P Q : pred I) F :
  \big[op/x]_(i <- r | P i && Q i) F i =
    \big[op/x]_(i <- r | Q i) (if P i then F i else x).

Lemma big_rmcond_idem I (r : seq I) (P : pred I) F :
  (∀ i, ~~ P i → F i = x) →
  \big[op/x]_(i <- r | P i) F i = \big[op/x]_(i <- r) F i.

Lemma big_rmcond_in_idem (I : eqType) (r : seq I) (P : pred I) F :
  (∀ i, i \in r → ~~ P i → F i = x) →
  \big[op/x]_(i <- r | P i) F i = \big[op/x]_(i <- r) F i.

Lemma big_cat_idem I r1 r2 (P : pred I) F :
  \big[op/x]_(i <- r1 ++ r2 | P i) F i =
    op (\big[op/x]_(i <- r1 | P i) F i) (\big[op/x]_(i <- r2 | P i) F i).

Lemma big_allpairs_dep_idem I1 (I2 : I1 → Type) J (h : ∀ i1, I2 i1 → J)
    (r1 : seq I1) (r2 : ∀ i1, seq (I2 i1)) (F : J → R) :
  \big[op/x]_(i <- [seq h i1 i2 | i1 <- r1, i2 <- r2 i1]) F i =
    \big[op/x]_(i1 <- r1) \big[op/x]_(i2 <- r2 i1) F (h i1 i2).

Lemma big_allpairs_idem I1 I2 (r1 : seq I1) (r2 : seq I2) F :
  \big[op/x]_(i <- [seq (i1, i2) | i1 <- r1, i2 <- r2]) F i =
    \big[op/x]_(i1 <- r1) \big[op/x]_(i2 <- r2) F (i1, i2).

Lemma big_cat_nat_idem n m p (P : pred nat) F : m ≤ n → n ≤ p →
  \big[op/x]_(m ≤ i < p | P i) F i =
    op (\big[op/x]_(m ≤ i < n | P i) F i) (\big[op/x]_(n ≤ i < p | P i) F i).

Lemma big_split_idem I r (P : pred I) F1 F2 :
  \big[op/x]_(i <- r | P i) op (F1 i) (F2 i) =
    op (\big[op/x]_(i <- r | P i) F1 i) (\big[op/x]_(i <- r | P i) F2 i).

Lemma big_id_idem_AC I (r : seq I) P F :
  \big[op/x]_(i <- r | P i) op (F i) x = \big[op/x]_(i <- r | P i) F i.

Lemma bigID_idem I r (a P : pred I) F :
  \big[op/x]_(i <- r | P i) F i =
    op (\big[op/x]_(i <- r | P i && a i) F i)
       (\big[op/x]_(i <- r | P i && ~~ a i) F i).
Arguments bigID_idem [I r].

Lemma bigU_idem (I : finType) (A B : pred I) F :
    [disjoint A & B] →
  \big[op/x]_(i in [predU A & B]) F i =
    op (\big[op/x]_(i in A) F i) (\big[op/x]_(i in B) F i).

Lemma partition_big_idem I (s : seq I)
      (J : finType) (P : pred I) (p : I → J) (Q : pred J) F :
  (∀ i, P i → Q (p i)) →
  \big[op/x]_(i <- s | P i) F i =
  \big[op/x]_(j : J | Q j) \big[op/x]_(i <- s | (P i) && (p i == j)) F i.

Arguments partition_big_idem [I s J P] p Q [F].

Lemma sig_big_dep_idem (I : finType) (J : I → finType)
    (P : pred I) (Q : ∀ {i}, pred (J i)) (F : ∀ {i}, J i → R) :
  \big[op/x]_(i | P i) \big[op/x]_(j : J i | Q j) F j =
  \big[op/x]_(p : {i : I & J i} | P (tag p) && Q (tagged p)) F (tagged p).

Lemma pair_big_dep_idem (I J : finType) (P : pred I) (Q : I → pred J) F :
  \big[op/x]_(i | P i) \big[op/x]_(j | Q i j) F i j =
    \big[op/x]_(p | P p.1 && Q p.1 p.2) F p.1 p.2.

Lemma pair_big_idem (I J : finType) (P : pred I) (Q : pred J) F :
  \big[op/x]_(i | P i) \big[op/x]_(j | Q j) F i j =
    \big[op/x]_(p | P p.1 && Q p.2) F p.1 p.2.

Lemma pair_bigA_idem (I J : finType) (F : I → J → R) :
  \big[op/x]_i \big[op/x]_j F i j = \big[op/x]_p F p.1 p.2.

Lemma exchange_big_dep_idem 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[op/x]_(i <- rI | P i) \big[op/x]_(j <- rJ | Q i j) F i j =
    \big[op/x]_(j <- rJ | xQ j) \big[op/x]_(i <- rI | P i && Q i j) F i j.
Arguments exchange_big_dep_idem [I J rI rJ P Q] xQ [F].

Lemma exchange_big_idem I J rI rJ (P : pred I) (Q : pred J) F :
  \big[op/x]_(i <- rI | P i) \big[op/x]_(j <- rJ | Q j) F i j =
    \big[op/x]_(j <- rJ | Q j) \big[op/x]_(i <- rI | P i) F i j.

Lemma exchange_big_dep_nat_idem 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[op/x]_(m1 ≤ i < n1 | P i) \big[op/x]_(m2 ≤ j < n2 | Q i j) F i j =
    \big[op/x]_(m2 ≤ j < n2 | xQ j)
       \big[op/x]_(m1 ≤ i < n1 | P i && Q i j) F i j.
Arguments exchange_big_dep_nat_idem [m1 n1 m2 n2 P Q] xQ [F].

Lemma exchange_big_nat_idem m1 n1 m2 n2 (P Q : pred nat) F :
  \big[op/x]_(m1 ≤ i < n1 | P i) \big[op/x]_(m2 ≤ j < n2 | Q j) F i j =
    \big[op/x]_(m2 ≤ j < n2 | Q j) \big[op/x]_(m1 ≤ i < n1 | P i) F i j.

End Id.

End Abelian.

End SemiGroupProperties.
Arguments big_undup [R op x I].
Arguments perm_big [R op x I r1 r2].
Arguments bigD1 [R op x I] j [P F].
Arguments reindex_omap [R op x I J] h h' [P F].
Arguments reindex_onto [R op x I J] h h' [P F].
Arguments reindex [R op x I J] h [P F].
Arguments reindex_inj [R op x I h P F].
Arguments big_enum_val_cond [R op x I A] P F.
Arguments big_enum_rank_cond [R op x I A z] zA P F.

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_rmcond I (r : seq I) (P : pred I) F :
  (∀ i, ~~ P i → F i = 1) →
  \big[*%M/1]_(i <- r | P i) F i = \big[*%M/1]_(i <- r) F i.

Lemma big_rmcond_in (I : eqType) (r : seq I) (P : pred I) F :
  (∀ i, i \in r → ~~ P i → F i = 1) →
  \big[*%M/1]_(i <- r | P i) F i = \big[*%M/1]_(i <- r) F i.

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_ord1_eq (F : nat → R) i n :
  \big[op/idx]_(j < n | j == i :> nat) F j = if i < n then F i else idx.

Lemma big_ord1_cond_eq (F : nat → R) (P : pred nat) i n :
  \big[op/idx]_(j < n | P j && (j == i :> nat)) F j =
    if (i < n) && P i then F i else idx.

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_nat_widenl (m1 m2 n : nat) (P : pred nat) F :
  m2 ≤ m1 →
  \big[op/idx]_(m1 ≤ i < n | P i) F i =
  \big[op/idx]_(m2 ≤ i < n | P i && (m1 ≤ i)) F i.

Lemma big_geq_mkord (m n : nat) (P : pred nat) F :
  \big[op/idx]_(m ≤ i < n | P i) F i =
  \big[op/idx]_(i < n | P i && (m ≤ i)) F i.

Lemma big_nat1_eq (F : nat → R) i m n :
  \big[op/idx]_(m ≤ j < n | j == i) F j = if m ≤ i < n then F i else idx.

Lemma big_nat1_cond_eq (F : nat → R) (P : pred nat) i m n :
  \big[op/idx]_(m ≤ j < n | P j && (j == i)) F j =
    if (m ≤ i < n) && P i then F i else idx.

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_nat_mul n k F :
  \big[*%M/1]_(0 ≤ i < n × k) F i =
  \big[*%M/1]_(0 ≤ i < n) \big[*%M/1]_(i × k ≤ j < i.+1 × k) F j.

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.

Lemma big_pmap J I (h : J → option I) (r : seq J) F :
  \big[op/idx]_(i <- pmap h r) F i = \big[op/idx]_(j <- r) oapp F idx (h j).

Lemma telescope_big (f : nat → nat → R) (n m : nat) :
  (∀ k, n < k < m → op (f n k) (f k k.+1) = f n k.+1) →
  \big[op/idx]_(n ≤ i < m) f i i.+1 = if n < m then f n m else idx.

End Plain.

Section Abelian.

Variable op : Monoid.com_law 1.


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 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.
Arguments bigID [I r].

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 partition_big I (s : seq I)
      (J : finType) (P : pred I) (p : I → J) (Q : pred J) F :
  (∀ i, P i → Q (p i)) →
  \big[*%M/1]_(i <- s | P i) F i =
  \big[*%M/1]_(j : J | Q j) \big[*%M/1]_(i <- s | (P i) && (p i == j)) F i.

Arguments partition_big [I s J P] p Q [F].

Lemma big_enum_val (I : finType) (A : pred I) F :
  \big[op/idx]_(x in A) F x = \big[op/idx]_(i < #|A|) F (enum_val i).
Arguments big_enum_val [I A] F.

Lemma big_enum_rank (I : finType) (A : pred I) x (xA : x \in A) F
  (h := enum_rank_in xA) :
  \big[op/idx]_(i < #|A|) F i = \big[op/idx]_(s in A) F (h s).
Arguments big_enum_rank [I A x] xA F.

Lemma sig_big_dep (I : finType) (J : I → finType)
    (P : pred I) (Q : ∀ {i}, pred (J i)) (F : ∀ {i}, J i → R) :
  \big[op/idx]_(i | P i) \big[op/idx]_(j : J i | Q j) F j =
  \big[op/idx]_(p : {i : I & J i} | P (tag p) && Q (tagged p)) F (tagged p).

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.
Arguments exchange_big_dep [I J rI rJ P Q] xQ [F].

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.
Arguments exchange_big_dep_nat [m1 n1 m2 n2 P Q] xQ [F].

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.

Arguments big_filter [R idx op I].
Arguments big_filter_cond [R idx op I].
Arguments congr_big [R idx op I r1] r2 [P1] P2 [F1] F2.
Arguments eq_big [R idx op I r P1] P2 [F1] F2.
Arguments eq_bigl [R idx op I r P1] P2.
Arguments eq_bigr [R idx op I r P F1] F2.
Arguments eq_big_idx [R idx op idx' I] i0 [P F].
Arguments big_seq_cond [R idx op I r].
Arguments eq_big_seq [R idx op I r F1] F2.
Arguments congr_big_nat [R idx op m1 n1] m2 n2 [P1] P2 [F1] F2.
Arguments big_map [R idx op I J] h [r].
Arguments big_nth [R idx op I] x0 [r].
Arguments big_catl [R idx op I r1 r2 P F].
Arguments big_catr [R idx op I r1 r2 P F].
Arguments big_geq [R idx op m n P F].
Arguments big_ltn_cond [R idx op m n P F].
Arguments big_ltn [R idx op m n F].
Arguments big_addn [R idx op].
Arguments big_mkord [R idx op n].
Arguments big_nat_widen [R idx op].
Arguments big_nat_widenl [R idx op].
Arguments big_geq_mkord [R idx op].
Arguments big_ord_widen_cond [R idx op n1].
Arguments big_ord_widen [R idx op n1].
Arguments big_ord_widen_leq [R idx op n1].
Arguments big_ord_narrow_cond [R idx op n1 n2 P F].
Arguments big_ord_narrow_cond_leq [R idx op n1 n2 P F].
Arguments big_ord_narrow [R idx op n1 n2 F].
Arguments big_ord_narrow_leq [R idx op n1 n2 F].
Arguments big_mkcond [R idx op I r].
Arguments big1_eq [R idx op I].
Arguments big1_seq [R idx op I].
Arguments big1 [R idx op I].
Arguments big_pred1 [R idx op I] i [P F].
Arguments perm_big [R op x I r1] r2 [P F].
Arguments big_uniq [R op x I] r [F].
Arguments big_rem [R idx op I r] x [P F].
Arguments bigID [R idx op I r].
Arguments bigU [R idx op I].
Arguments bigD1 [R op x I] j [P F].
Arguments bigD1_seq [R op x I r] j [F].
Arguments bigD1_ord [R op x n] j [P F].
Arguments partition_big [R idx op I s J P] p Q [F].
Arguments reindex_omap [R op x I J] h h' [P F].
Arguments reindex_onto [R op x I J] h h' [P F].
Arguments reindex [R op x I J] h [P F].
Arguments reindex_inj [R op x I h P F].
Arguments big_enum_val_cond [R op x I A] P F.
Arguments big_enum_rank_cond [R op x I A z] zA P F.
Arguments big_enum_val [R idx op I A] F.
Arguments big_enum_rank [R idx op I A x] xA F.
Arguments sig_big_dep [R idx op I J].
Arguments pair_big_dep [R idx op I J].
Arguments pair_big [R idx op I J].
Arguments big_allpairs_dep {R idx op I1 I2 J h r1 r2 F}.
Arguments big_allpairs {R idx op I1 I2 r1 r2 F}.
Arguments exchange_big_dep [R idx op I J rI rJ P Q] xQ [F].
Arguments exchange_big_dep_nat [R idx op m1 n1 m2 n2 P Q] xQ [F].
Arguments big_ord_recl [R idx op].
Arguments big_ord_recr [R idx op].
Arguments big_nat_recl [R idx op].
Arguments big_nat_recr [R idx op].
Arguments big_pmap [R idx op J I] h [r].
Arguments telescope_big [R idx op] f [n m].

Section EqSupport.

Variables (R : eqType) (idx : R).

Section MonoidSupport.

Variables (op : Monoid.law idx) (I : Type).

Lemma eq_bigl_supp (r : seq I) (P1 : pred I) (P2 : pred I) (F : I → R) :
  {in [pred x | F x != idx], P1 =1 P2} →
  \big[op/idx]_(i <- r | P1 i) F i = \big[op/idx]_(i <- r | P2 i) F i.

End MonoidSupport.

Section ComoidSupport.

Variables (op : Monoid.com_law idx) (I : eqType).

Lemma perm_big_supp_cond [r s : seq I] [P : pred I] (F : I → R) :
  perm_eq
    [seq i <- r | P i && (F i != idx)]
    [seq i <- s | P i && (F i != idx)] →
  \big[op/idx]_(i <- r | P i) F i = \big[op/idx]_(i <- s | P i) F i.

Lemma perm_big_supp [r s : seq I] [P : pred I] (F : I → R) :
  perm_eq [seq i <- r | F i != idx] [seq i <- s | F i != idx] →
  \big[op/idx]_(i <- r | P i) F i = \big[op/idx]_(i <- s | P i) F i.

End ComoidSupport.

End EqSupport.

Arguments eq_bigl_supp [R idx op I r P1].
Arguments perm_big_supp_cond [R idx op I r s P].
Arguments perm_big_supp [R idx op I r s P].

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.

Arguments big_distrl [R zero times plus I r].
Arguments big_distrr [R zero times plus I r].
Arguments big_distr_big_dep [R zero one times plus I J].
Arguments big_distr_big [R zero one times plus I J].
Arguments bigA_distr_big_dep [R zero one times plus I J].
Arguments bigA_distr_big [R zero one times plus I J].
Arguments bigA_distr_bigA [R zero one times plus I J].

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.

Lemma big_bool R (idx : R) (op : Monoid.com_law idx) (F : bool → R):
  \big[op/idx]_(i : bool) F i = op (F true) (F false).

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 telescope_sumn_in n m f : n ≤ m →
  {in [pred i | n ≤ i ≤ m], {homo f : x y / x ≤ y}} →
  \sum_(n ≤ k < m) (f k.+1 - f k) = f m - f n.

Lemma telescope_sumn n m f : {homo f : x y / x ≤ y} →
  \sum_(n ≤ k < m) (f k.+1 - f k) = f m - f n.

Lemma sumnE r : sumn r = \sum_(i <- r) i.

Lemma card_bseq n (T : finType) : #|{bseq n of T}| = \sum_(i < n.+1) #|T| ^ 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 sumnB I r (P : pred I) (E1 E2 : I → nat) :
     (∀ i, P i → E1 i ≤ E2 i) →
  \sum_(i <- r | P i) (E2 i - E1 i) =
  \sum_(i <- r | P i) E2 i - \sum_(i <- r | P i) E1 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 leq_prod I r (P : pred I) (E1 E2 : I → nat) :
    (∀ i, P i → E1 i ≤ E2 i) →
  \prod_(i <- r | P i) E1 i ≤ \prod_(i <- r | P i) E2 i.

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_seq (I : eqType) r (P : pred I) F i0 :
  i0 \in r → P i0 → F i0 ≤ \max_(i <- r | P i) F i.
Arguments leq_bigmax_seq [I r P F].

Lemma leq_bigmax_cond (I : finType) (P : pred I) F i0 :
  P i0 → F i0 ≤ \max_(i | P i) F i.
Arguments leq_bigmax_cond [I P F].

Lemma leq_bigmax (I : finType) F (i0 : I) : F i0 ≤ \max_i F i.
Arguments leq_bigmax [I F].

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_leqP_seq (I : eqType) r (P : pred I) m F :
  reflect (∀ i, i \in r → P i → F i ≤ m) (\max_(i <- r | 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.
Arguments bigmax_sup [I] i0 [P m F].

Lemma bigmax_sup_seq (I : eqType) r i0 (P : pred I) m F :
  i0 \in r → P i0 → m ≤ F i0 → m ≤ \max_(i <- r | P i) F i.
Arguments bigmax_sup_seq [I r] i0 [P m F].

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].
Arguments bigmax_eq_arg [I] i0 [P F].

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.
Arguments biglcmn_sup [I] i0 [P F m].

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.
Arguments biggcdn_inf [I] i0 [P F m].

#[deprecated(since="mathcomp 1.13.0", note="Use big_rmcond instead.")]
Notation big_uncond := big_rmcond (only parsing).