# 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?)

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

• zero: {n : Q()} → «$n» =Q 0 n unifies with 0 • succ: {n : Q()} → (n' : Q()) → «$n» =Q «$n'».succ n unifies with succ n' for this specific n' 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. Equations • One or more equations did not get rendered due to their size. Instances For inductive Mathlib.Meta.List.ProveNilOrConsResult {u : Lean.Level} {α : Q(Type u)} (s : Q(List «$α»)) :

This represents the result of trying to determine whether the given expression s : Q(List $α) is either empty or consists of an element inserted into a strict subset. • nil: {u : Lean.Level} → {α : Q(Type u)} → {s : Q(List «$α»)} → Q(«$s» = []) The set is Nil. • cons: {u : Lean.Level} → {α : Q(Type u)} → {s : Q(List «$α»)} → (a : Q(«$α»)) → (s' : Q(List «$α»)) → Q(«$s» = «$a» :: «$s'») The set equals a inserted into the strict subset s'. Instances For def Mathlib.Meta.List.ProveNilOrConsResult.uncheckedCast {u : Lean.Level} {v : Lean.Level} {α : Q(Type u)} {β : Q(Type v)} (s : Q(List «$α»)) (t : Q(List «$β»)) : If s unifies with t, convert a result for s to a result for t. If s does not unify with t, this results in a type-incorrect proof. Equations • One or more equations did not get rendered due to their size. Instances For def Mathlib.Meta.List.ProveNilOrConsResult.eq_trans {u : Lean.Level} {α : Q(Type u)} {s : Q(List «$α»)} {t : Q(List «$α»)} (eq : Q(«$s» = «$t»)) : If s = t and we can get the result for t, then we can get the result for s. Equations • One or more equations did not get rendered due to their size. Instances For theorem Mathlib.Meta.List.range_zero' {n : } (pn : ) : = [] theorem Mathlib.Meta.List.range_succ_eq_map' {n : } {nn : } {n' : } (pn : ) (pn' : nn = n'.succ) : = 0 :: partial def Mathlib.Meta.List.proveNilOrCons {u : Lean.Level} {α : Q(Type u)} (s : Q(List «$α»)) :

Either show the expression s : Q(List α) is Nil, or remove one element from it.

Fails if we cannot determine which of the alternatives apply to the expression.

inductive Mathlib.Meta.Multiset.ProveZeroOrConsResult {u : Lean.Level} {α : Q(Type u)} (s : Q(Multiset «$α»)) : This represents the result of trying to determine whether the given expression s : Q(Multiset$α) is either empty or consists of an element inserted into a strict subset.

• zero: {u : Lean.Level} → {α : Q(Type u)} → {s : Q(Multiset «$α»)} → Q(«$s» = 0)

The set is zero.

• cons: {u : Lean.Level} → {α : Q(Type u)} → {s : Q(Multiset «$α»)} → (a : Q(«$α»)) → (s' : Q(Multiset «$α»)) → Q(«$s» = «$a» ::ₘ «$s'»)

The set equals a inserted into the strict subset s'.

Instances For
def Mathlib.Meta.Multiset.ProveZeroOrConsResult.uncheckedCast {u : Lean.Level} {v : Lean.Level} {α : Q(Type u)} {β : Q(Type v)} (s : Q(Multiset «$α»)) (t : Q(Multiset «$β»)) :

If s unifies with t, convert a result for s to a result for t.

If s does not unify with t, this results in a type-incorrect proof.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Mathlib.Meta.Multiset.ProveZeroOrConsResult.eq_trans {u : Lean.Level} {α : Q(Type u)} {s : Q(Multiset «$α»)} {t : Q(Multiset «$α»)} (eq : Q(«$s» = «$t»)) :

If s = t and we can get the result for t, then we can get the result for s.

Equations
• One or more equations did not get rendered due to their size.
Instances For
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 = n'.succ) :
= n' ::ₘ
def Mathlib.Meta.Multiset.proveZeroOrCons {u : Lean.Level} {α : Q(Type u)} (s : Q(Multiset «$α»)) : Either show the expression s : Q(Multiset α) is Zero, or remove one element from it. Fails if we cannot determine which of the alternatives apply to the expression. Equations • One or more equations did not get rendered due to their size. Instances For inductive Mathlib.Meta.Finset.ProveEmptyOrConsResult {u : Lean.Level} {α : Q(Type u)} (s : Q(Finset «$α»)) :

This represents the result of trying to determine whether the given expression s : Q(Finset $α) is either empty or consists of an element inserted into a strict subset. • empty: {u : Lean.Level} → {α : Q(Type u)} → {s : Q(Finset «$α»)} → Q(«$s» = ) The set is empty. • cons: {u : Lean.Level} → {α : Q(Type u)} → {s : Q(Finset «$α»)} → (a : Q(«$α»)) → (s' : Q(Finset «$α»)) → (h : Q(«$a»«$s'»)) → Q(«$s» = Finset.cons «$a» «$s'» «$h»)

The set equals a inserted into the strict subset s'.

Instances For
def Mathlib.Meta.Finset.ProveEmptyOrConsResult.uncheckedCast {u : Lean.Level} {v : Lean.Level} {α : Q(Type u)} {β : Q(Type v)} (s : Q(Finset «$α»)) (t : Q(Finset «$β»)) :

If s unifies with t, convert a result for s to a result for t.

If s does not unify with t, this results in a type-incorrect proof.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Mathlib.Meta.Finset.ProveEmptyOrConsResult.eq_trans {u : Lean.Level} {α : Q(Type u)} {s : Q(Finset «$α»)} {t : Q(Finset «$α»)} (eq : Q(«$s» = «$t»)) :

If s = t and we can get the result for t, then we can get the result for s.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Mathlib.Meta.Finset.insert_eq_cons {α : Type u_1} [] (a : α) (s : ) (h : as) :
insert a s = Finset.cons a s h
theorem Mathlib.Meta.Finset.range_succ' {n : } {nn : } {n' : } (pn : ) (pn' : nn = n'.succ) :
= Finset.cons n' ()
theorem Mathlib.Meta.Finset.univ_eq_elems {α : Type u_1} [] (elems : ) (complete : ∀ (x : α), x elems) :
Finset.univ = elems
partial def Mathlib.Meta.Finset.proveEmptyOrCons {u : Lean.Level} {α : Q(Type u)} (s : Q(Finset «$α»)) : Either show the expression s : Q(Finset α) is empty, or remove one element from it. Fails if we cannot determine which of the alternatives apply to the expression. def Mathlib.Meta.NormNum.Result.eq_trans {u : Lean.Level} {α : Q(Type u)} {a : Q(«$α»)} {b : Q(«$α»)} (eq : Q(«$a» = «$b»)) : If a = b and we can evaluate b, then we can evaluate a. Equations • One or more equations did not get rendered due to their size. Instances For 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 : αβ) : partial def Mathlib.Meta.NormNum.evalFinsetBigop {u : Lean.Level} {v : Lean.Level} {α : Q(Type u)} {β : Q(Type v)} (op : Q(Finset «$α»(«$α»«$β»)«$β»)) (f : Q(«$α»«$β»)) (res_empty : Mathlib.Meta.NormNum.Result q(«$op» Finset.empty «$f»)) (res_cons : {a : Q(«$α»)} → {s' : Q(Finset «$α»)} → {h : Q(«$a»«$s'»)} → Mathlib.Meta.NormNum.Result q(«$f» «$a»)Mathlib.Meta.NormNum.Result q(«$op» «$s'» «$f»)Lean.MetaM (Mathlib.Meta.NormNum.Result q(«$op» (Finset.cons «$a» «$s'» «$h») «$f»))) (s : Q(Finset «$α»)) :
Lean.MetaM (Mathlib.Meta.NormNum.Result q(«$op» «$s» «\$f»))

Evaluate a big operator applied to a finset by repeating proveEmptyOrCons until we exhaust all elements of the set.

norm_num plugin for evaluating products of finsets.

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

Equations
• One or more equations did not get rendered due to their size.
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.

Equations
• One or more equations did not get rendered due to their size.
Instances For