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:

∑ i in finset.range 10, (i^2 : ℕ) = 285
Π i in {1, 4, 9, 16}, nat.sqrt i = 24
([1, 2, 1, 3]).sum = 7

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.

meta def tactic.norm_num.decide_eq (l r : expr) :

tactic (bool × expr)

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

meta def tactic.norm_num.list.decide_mem (decide_eq : expr → expr → tactic (bool × expr)) :

expr → list expr → tactic (bool × expr)

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

meta def tactic.norm_num.eval_list_map (ef : expr) :

list expr → tactic (list expr × expr)

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

meta def tactic.norm_num.eval_list :

expr → tactic (list expr × expr)

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) :

multiset.map f xs = ↑ys

meta def tactic.norm_num.eval_multiset :

expr → tactic (list expr × expr)

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 := _}

meta def tactic.norm_num.eval_finset_interval :

expr → tactic (option (list expr × expr × expr))

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

meta def tactic.norm_num.eval_finset (decide_eq : expr → expr → tactic (bool × expr)) :

expr → tactic (list expr × expr × expr)

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

meta def tactic.norm_num.list.prove_prod (α : expr) :

list expr → tactic (expr × expr)

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

meta def tactic.norm_num.list.prove_sum (α : expr) :

list expr → tactic (expr × expr)

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

meta def tactic.norm_num.list.prove_prod_map (β ef : expr) (xs : list expr) :

tactic (expr × expr)

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

meta def tactic.norm_num.list.prove_sum_map (β ef : expr) (xs : list expr) :

tactic (expr × expr)

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

meta def tactic.norm_num.eval_big_operators :

expr → tactic (expr × expr)

norm_num plugin for evaluating big operators: