# Documentation

Mathlib.Tactic.NormNum.BigOperators

# norm_num plugin for big operators #

This file adds norm_num plugins for Finset.prod and Finset.sum.

The driving part of this plugin is Mathlib.Meta.NormNum.evalFinsetBigop. We repeatedly use Finset.proveEmptyOrCons to try to find a proof that the given set is empty, or that it consists of one element inserted into a strict subset, and evaluate the big operator on that subset until the set is completely exhausted.

• The fin_cases tactic has similar scope: splitting out a finite collection into its elements.

## Porting notes #

This plugin is noticeably less powerful than the equivalent version in Mathlib 3: the design of norm_num means plugins have to return numerals, rather than a generic expression. In particular, we can't use the plugin on sums containing variables. (See also the TODO note "To support variables".)

## TODOs #

• Support intervals: Finset.Ico, Finset.Icc, ...
• To support variables, like in Mathlib 3, turn this into a standalone tactic that unfolds the sum/prod, without computing its numeric value (using the ring tactic to do some normalization?)
• zero: {n : Q()} → «$n» =Q 0 n unifies with 0 • succ: {n : Q()} → (n' : Q()) → «$n» =Q Nat.succ «\$n'»

n unifies with succ n' for this specific n'

This represents the result of trying to determine whether the given expression n : Q(ℕ) is either zero or succ.

Instances For

Determine whether the expression n : Q(ℕ) unifies with 0 or Nat.succ n'.

We do not use norm_num functionality because we want definitional equality, not propositional equality, for use in dependent types.

Fails if neither of the options succeed.

Instances For
theorem Mathlib.Meta.List.range_zero' {n : } (pn : ) :
= []
theorem Mathlib.Meta.List.range_succ_eq_map' {n : } {nn : } {n' : } (pn : ) (pn' : nn = Nat.succ n') :
= 0 ::
theorem Mathlib.Meta.Multiset.insert_eq_cons {α : Type u_1} [] (a : α) (s : ) :
insert a s = a ::ₘ s
theorem Mathlib.Meta.Multiset.range_succ' {n : } {nn : } {n' : } (pn : ) (pn' : nn = Nat.succ n') :
= n' ::ₘ
theorem Mathlib.Meta.Finset.insert_eq_cons {α : Type u_1} [] (a : α) (s : ) (h : ¬a s) :
insert a s = Finset.cons a s h
theorem Mathlib.Meta.Finset.range_succ' {n : } {nn : } {n' : } (pn : ) (pn' : nn = Nat.succ n') :
= Finset.cons n' () (_ : ¬n' )
theorem Mathlib.Meta.Finset.univ_eq_elems {α : Type u_1} [] (elems : ) (complete : ∀ (x : α), x elems) :
Finset.univ = elems
theorem Mathlib.Meta.NormNum.Finset.sum_empty {β : Type u_1} {α : Type u_2} [] (f : αβ) :
theorem Mathlib.Meta.NormNum.Finset.prod_empty {β : Type u_1} {α : Type u_2} [] (f : αβ) :

norm_num plugin for evaluating products of finsets.

If your finset is not supported, you can add it to the match in Finset.proveEmptyOrCons.

Instances For

norm_num plugin for evaluating sums of finsets.

If your finset is not supported, you can add it to the match in Finset.proveEmptyOrCons.

Instances For