Commit 2023-07-11 08:31 cefb050f

View on Github →

feat: basic big operator plugin for norm_num (#4350) I wrote a basic implementation for a norm_num plugin evaluating Finset.sum and Finset.prod. It does not yet support as many Finset expressions as the Mathlib 3 implementation, and it cannot deal with variables appearing in the sum. I believe it's valuable to have this implementation since we do use this plugin in various parts of mathlib.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Tactic.lean

Created Mathlib/Tactic/NormNum/BigOperators.lean

added def Mathlib.Meta.Finset.ProveEmptyOrConsResult.eq_trans

added def Mathlib.Meta.Finset.ProveEmptyOrConsResult.uncheckedCast

added inductive Mathlib.Meta.Finset.ProveEmptyOrConsResult

added theorem Mathlib.Meta.Finset.insert_eq_cons

added theorem Mathlib.Meta.Finset.range_succ'

added theorem Mathlib.Meta.Finset.range_zero'

added theorem Mathlib.Meta.Finset.univ_eq_elems

added def Mathlib.Meta.List.ProveNilOrConsResult.eq_trans

added def Mathlib.Meta.List.ProveNilOrConsResult.uncheckedCast

added inductive Mathlib.Meta.List.ProveNilOrConsResult

added theorem Mathlib.Meta.List.range_succ_eq_map'

added theorem Mathlib.Meta.List.range_zero'

added def Mathlib.Meta.Multiset.ProveZeroOrConsResult.eq_trans

added def Mathlib.Meta.Multiset.ProveZeroOrConsResult.uncheckedCast

added inductive Mathlib.Meta.Multiset.ProveZeroOrConsResult

added theorem Mathlib.Meta.Multiset.insert_eq_cons

added theorem Mathlib.Meta.Multiset.range_succ'

added theorem Mathlib.Meta.Multiset.range_zero'

added inductive Mathlib.Meta.Nat.UnifyZeroOrSuccResult

added def Mathlib.Meta.Nat.unifyZeroOrSucc

added def Mathlib.Meta.NormNum.Result.eq_trans

Modified test/norm_num_ext.lean