mathlib3 documentation

algebra.big_operators.norm_num

norm_num plugin for big operators #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This norm_num plugin provides support for computing sums and products of lists, multisets and finsets.

Example goals this plugin can solve:

Implementation notes #

The tactic works by first converting the expression denoting the collection (list, multiset, finset) to a list of expressions denoting each element. For finsets, this involves erasing duplicate elements (the tactic fails if equality or disequality cannot be determined).

After rewriting the big operator to a product/sum of lists, we evaluate this using norm_num itself to handle multiplication/addition.

Finally, we package up the result using some congruence lemmas.

Use norm_num to decide equality between two expressions.

If the decision procedure succeeds, the bool value indicates whether the expressions are equal, and the expr is a proof of (dis)equality. This procedure is partial: it will fail in cases where norm_num can't reduce either side to a rational numeral.

theorem tactic.norm_num.list.not_mem_cons {α : Type u_1} {x y : α} {ys : list α} (h₁ : x y) (h₂ : x ys) :
x y :: ys

Use a decision procedure for the equality of list elements to decide list membership.

If the decision procedure succeeds, the bool value indicates whether the expressions are equal, and the expr is a proof of (dis)equality. This procedure is partial iff its parameter decide_eq is partial.

theorem tactic.norm_num.list.map_cons_congr {α : Type u_1} {β : Type u_2} (f : α β) {x : α} {xs : list α} {fx : β} {fxs : list β} (h₁ : f x = fx) (h₂ : list.map f xs = fxs) :
list.map f (x :: xs) = fx :: fxs

Apply ef : α → β to all elements of the list, constructing an equality proof.

theorem tactic.norm_num.list.cons_congr {α : Type u_1} (x : α) {xs xs' : list α} (xs_eq : xs' = xs) :
x :: xs' = x :: xs
theorem tactic.norm_num.list.map_congr {α : Type u_1} {β : Type u_2} (f : α β) {xs xs' : list α} {ys : list β} (xs_eq : xs = xs') (ys_eq : list.map f xs' = ys) :
list.map f xs = ys

Convert an expression denoting a list to a list of elements.

theorem tactic.norm_num.multiset.cons_congr {α : Type u_1} (x : α) {xs : multiset α} {xs' : list α} (xs_eq : xs' = xs) :
(x :: xs') = x ::ₘ xs
theorem tactic.norm_num.multiset.map_congr {α : Type u_1} {β : Type u_2} (f : α β) {xs : multiset α} {xs' : list α} {ys : list β} (xs_eq : xs = xs') (ys_eq : list.map f xs' = ys) :

Convert an expression denoting a multiset to a list of elements.

We return a list rather than a finset, so we can more easily iterate over it (without having to prove that our tactics are independent of the order of iteration, which is in general not true).

theorem tactic.norm_num.finset.mk_congr {α : Type u_1} {xs xs' : multiset α} (h : xs = xs') (nd : xs.nodup) (nd' : xs'.nodup) :
{val := xs, nodup := nd} = {val := xs', nodup := nd'}
theorem tactic.norm_num.finset.insert_eq_coe_list_of_mem {α : Type u_1} [decidable_eq α] (x : α) (xs : finset α) {xs' : list α} (h : x xs') (nd_xs : xs'.nodup) (hxs' : xs = {val := xs', nodup := _}) :
has_insert.insert x xs = {val := xs', nodup := _}
theorem tactic.norm_num.finset.insert_eq_coe_list_cons {α : Type u_1} [decidable_eq α] (x : α) (xs : finset α) {xs' : list α} (h : x xs') (nd_xs : xs'.nodup) (nd_xxs : (x :: xs').nodup) (hxs' : xs = {val := xs', nodup := _}) :
has_insert.insert x xs = {val := (x :: xs'), nodup := _}

For now this only works on types that are contiguous subsets of the integers

Convert an expression denoting a finset to a list of elements, a proof that this list is equal to the original finset, and a proof that the list contains no duplicates.

We return a list rather than a finset, so we can more easily iterate over it (without having to prove that our tactics are independent of the order of iteration, which is in general not true).

decide_eq is a (partial) decision procedure for determining whether two elements of the finset are equal, for example to parse {2, 1, 2} into [2, 1].

theorem tactic.norm_num.list.sum_cons_congr {α : Type u_1} [add_monoid α] (xs : list α) (x y z : α) (his : xs.sum = y) (hi : x + y = z) :
(x :: xs).sum = z
theorem tactic.norm_num.list.prod_cons_congr {α : Type u_1} [monoid α] (xs : list α) (x y z : α) (his : xs.prod = y) (hi : x * y = z) :
(x :: xs).prod = z

Evaluate list.prod %%xs, producing the evaluated expression and an equality proof.

Evaluate list.sum %%xs, sumucing the evaluated expression and an equality proof.

theorem tactic.norm_num.list.prod_congr {α : Type u_1} [monoid α] {xs xs' : list α} {z : α} (h₁ : xs = xs') (h₂ : xs'.prod = z) :
xs.prod = z
theorem tactic.norm_num.list.sum_congr {α : Type u_1} [add_monoid α] {xs xs' : list α} {z : α} (h₁ : xs = xs') (h₂ : xs'.sum = z) :
xs.sum = z
theorem tactic.norm_num.multiset.sum_congr {α : Type u_1} [add_comm_monoid α] {xs : multiset α} {xs' : list α} {z : α} (h₁ : xs = xs') (h₂ : xs'.sum = z) :
xs.sum = z
theorem tactic.norm_num.multiset.prod_congr {α : Type u_1} [comm_monoid α] {xs : multiset α} {xs' : list α} {z : α} (h₁ : xs = xs') (h₂ : xs'.prod = z) :
xs.prod = z

Evaluate (%%xs.map (%%ef : %%α → %%β)).prod, producing the evaluated expression and an equality proof.

Evaluate (%%xs.map (%%ef : %%α → %%β)).sum, producing the evaluated expression and an equality proof.

theorem tactic.norm_num.finset.eval_prod_of_list {β : Type u_1} {α : Type u_2} [comm_monoid β] (s : finset α) (f : α β) {is : list α} (his : is.nodup) (hs : {val := is, nodup := _} = s) {x : β} (hx : (list.map f is).prod = x) :
s.prod f = x
theorem tactic.norm_num.finset.eval_sum_of_list {β : Type u_1} {α : Type u_2} [add_comm_monoid β] (s : finset α) (f : α β) {is : list α} (his : is.nodup) (hs : {val := is, nodup := _} = s) {x : β} (hx : (list.map f is).sum = x) :
s.sum f = x