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?)
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 with0
- succ
{n : Q(ℕ)}
(n' : Q(ℕ))
(pf : «$n» =Q «$n'».succ)
: UnifyZeroOrSuccResult n
n
unifies withsucc n'
for this specificn'
Instances For
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 subsets'
.
Instances For
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
Instances For
If s = t
and we can get the result for t
, then we can get the result for s
.
Equations
Instances For
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.
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 subsets'
.
Instances For
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
Instances For
If s = t
and we can get the result for t
, then we can get the result for s
.
Equations
Instances For
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
Instances For
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 subsets'
.
Instances For
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
Instances For
If s = t
and we can get the result for t
, then we can get the result for s
.
Equations
Instances For
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.
If a = b
and we can evaluate b
, then we can evaluate a
.
Equations
Instances For
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
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
.