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.

See also

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

inductive Mathlib.Meta.Nat.UnifyZeroOrSuccResult (n : Q(ℕ)) : Type

• zero: {n : Q(ℕ)} → «$n» =Q 0 → Mathlib.Meta.Nat.UnifyZeroOrSuccResult n

  n unifies with 0

• succ: {n : Q(ℕ)} → (n' : Q(ℕ)) → «$n» =Q Nat.succ «$n'» → Mathlib.Meta.Nat.UnifyZeroOrSuccResult 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.

def Mathlib.Meta.Nat.unifyZeroOrSucc (n : Q(ℕ)) : Lean.MetaM (Mathlib.Meta.Nat.UnifyZeroOrSuccResult n)

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.

theorem Mathlib.Meta.List.range_zero' {n : ℕ} (pn : Mathlib.Meta.NormNum.IsNat n 0) : List.range n = []

theorem Mathlib.Meta.List.range_succ_eq_map' {n : ℕ} {nn : ℕ} {n' : ℕ} (pn : Mathlib.Meta.NormNum.IsNat n nn) (pn' : nn = Nat.succ n') : List.range n = 0 :: List.map Nat.succ (List.range n')

theorem Mathlib.Meta.Multiset.insert_eq_cons {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) : insert a s = a ::ₘ s

theorem Mathlib.Meta.Multiset.range_zero' {n : ℕ} (pn : Mathlib.Meta.NormNum.IsNat n 0) : Multiset.range n = 0

theorem Mathlib.Meta.Multiset.range_succ' {n : ℕ} {nn : ℕ} {n' : ℕ} (pn : Mathlib.Meta.NormNum.IsNat n nn) (pn' : nn = Nat.succ n') : Multiset.range n = n' ::ₘ Multiset.range n'

theorem Mathlib.Meta.Finset.insert_eq_cons {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) (h : ¬a ∈ s) : insert a s = Finset.cons a s h

theorem Mathlib.Meta.Finset.range_zero' {n : ℕ} (pn : Mathlib.Meta.NormNum.IsNat n 0) : Finset.range n = ∅

theorem Mathlib.Meta.Finset.range_succ' {n : ℕ} {nn : ℕ} {n' : ℕ} (pn : Mathlib.Meta.NormNum.IsNat n nn) (pn' : nn = Nat.succ n') : Finset.range n = Finset.cons n' (Finset.range n') (_ : ¬n' ∈ Finset.range n')

theorem Mathlib.Meta.Finset.univ_eq_elems {α : Type u_1} [Fintype α] (elems : Finset α) (complete : ∀ (x : α), x ∈ elems) : Finset.univ = elems

theorem Mathlib.Meta.NormNum.Finset.sum_empty {β : Type u_1} {α : Type u_2} [CommSemiring β] (f : α → β) : Mathlib.Meta.NormNum.IsNat (Finset.sum ∅ f) 0

theorem Mathlib.Meta.NormNum.Finset.prod_empty {β : Type u_1} {α : Type u_2} [CommSemiring β] (f : α → β) : Mathlib.Meta.NormNum.IsNat (Finset.prod ∅ f) 1

def Mathlib.Meta.NormNum.evalFinsetProd : Mathlib.Meta.NormNum.NormNumExt

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.

def Mathlib.Meta.NormNum.evalFinsetSum : Mathlib.Meta.NormNum.NormNumExt

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.