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

TODO

• 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

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

• zero {n : Q(ℕ)} (pf : «$n» =Q 0) : UnifyZeroOrSuccResult n

  n unifies with 0

• succ {n : Q(ℕ)} (n' : Q(ℕ)) (pf : «$n» =Q «$n'».succ) : UnifyZeroOrSuccResult n

  n unifies with succ n' for this specific n'

def Mathlib.Meta.Nat.unifyZeroOrSucc (n : Q(ℕ)) : Lean.MetaM (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.

inductive Mathlib.Meta.List.ProveNilOrConsResult {u : Lean.Level} {α : Q(Type u)} (s : Q(List «$α»)) : Type

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 «$α»)} (pf : Q(«$s» = [])) : ProveNilOrConsResult s

  The set is Nil.

• cons {u : Lean.Level} {α : Q(Type u)} {s : Q(List «$α»)} (a : Q(«$α»)) (s' : Q(List «$α»)) (pf : Q(«$s» = «$a» :: «$s'»)) : ProveNilOrConsResult s

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

def Mathlib.Meta.List.ProveNilOrConsResult.uncheckedCast {u v : Lean.Level} {α : Q(Type u)} {β : Q(Type v)} (s : Q(List «$α»)) (t : Q(List «$β»)) : ProveNilOrConsResult s → ProveNilOrConsResult t

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.

def Mathlib.Meta.List.ProveNilOrConsResult.eq_trans {u : Lean.Level} {α : Q(Type u)} {s t : Q(List «$α»)} (eq : Q(«$s» = «$t»)) : ProveNilOrConsResult t → ProveNilOrConsResult s

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

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

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

partial def Mathlib.Meta.List.proveNilOrCons {u : Lean.Level} {α : Q(Type u)} (s : Q(List «$α»)) : Lean.MetaM (ProveNilOrConsResult s)

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 «$α»)) : Type

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 «$α»)} (pf : Q(«$s» = 0)) : ProveZeroOrConsResult s

  The set is zero.

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

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

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

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.

def Mathlib.Meta.Multiset.ProveZeroOrConsResult.eq_trans {u : Lean.Level} {α : Q(Type u)} {s t : Q(Multiset «$α»)} (eq : Q(«$s» = «$t»)) : ProveZeroOrConsResult t → ProveZeroOrConsResult s

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

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

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

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

def Mathlib.Meta.Multiset.proveZeroOrCons {u : Lean.Level} {α : Q(Type u)} (s : Q(Multiset «$α»)) : Lean.MetaM (ProveZeroOrConsResult s)

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.

inductive Mathlib.Meta.Finset.ProveEmptyOrConsResult {u : Lean.Level} {α : Q(Type u)} (s : Q(Finset «$α»)) : Type

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 «$α»)} (pf : Q(«$s» = ∅)) : ProveEmptyOrConsResult s

  The set is empty.

• cons {u : Lean.Level} {α : Q(Type u)} {s : Q(Finset «$α»)} (a : Q(«$α»)) (s' : Q(Finset «$α»)) (h : Q(«$a» ∉ «$s'»)) (pf : Q(«$s» = Finset.cons «$a» «$s'» «$h»)) : ProveEmptyOrConsResult s

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

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

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.

def Mathlib.Meta.Finset.ProveEmptyOrConsResult.eq_trans {u : Lean.Level} {α : Q(Type u)} {s t : Q(Finset «$α»)} (eq : Q(«$s» = «$t»)) : ProveEmptyOrConsResult t → ProveEmptyOrConsResult s

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

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 : NormNum.IsNat n 0) : Finset.range n = ∅

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

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

partial def Mathlib.Meta.Finset.proveEmptyOrCons {u : Lean.Level} {α : Q(Type u)} (s : Q(Finset «$α»)) : Lean.MetaM (ProveEmptyOrConsResult s)

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 b : Q(«$α»)} (eq : Q(«$a» = «$b»)) : Result b → Result a

If a = b and we can evaluate b, then we can evaluate a.

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

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

partial def Mathlib.Meta.NormNum.evalFinsetBigop {u v : Lean.Level} {α : Q(Type u)} {β : Q(Type v)} (op : Q(Finset «$α» → («$α» → «$β») → «$β»)) (f : Q(«$α» → «$β»)) (res_empty : Result q(«$op» Finset.empty «$f»)) (res_cons : {a : Q(«$α»)} → {s' : Q(Finset «$α»)} → {h : Q(«$a» ∉ «$s'»)} → Result q(«$f» «$a») → Result q(«$op» «$s'» «$f») → Lean.MetaM (Result q(«$op» (Finset.cons «$a» «$s'» «$h») «$f»))) (s : Q(Finset «$α»)) : Lean.MetaM (Result q(«$op» «$s» «$f»))

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

def Mathlib.Meta.NormNum.evalFinsetProd : 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.

def Mathlib.Meta.NormNum.evalFinsetSum : 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.