# Zulip Chat Archive

## Stream: maths

### Topic: when does norm_num work?

#### Johan Commelin (Jan 31 2020 at 12:50):

I've written the definition of the Bernoulli numbers, and wanted to test my implementation. `#eval`

computes the first 16 numbers in a breeze. But if I want a verified computation `by norm_num`

fails (because simplify, or something). What is the correct way to write a test for my definition?

import data.stream.basic section bernoulli def bernoulli_fun (n : ℕ) (l : list (ℕ × ℚ)) : ℚ := 1 - (list.sum $ l.map $ λ ⟨k,B⟩, (n.choose k) * B / (n + 1 - k)) def bernoulli_aux : stream ((ℕ × ℚ) × list (ℕ × ℚ)) := stream.iterate (λ ⟨⟨n, B⟩, l⟩, ((n+1, bernoulli_fun (n+1) ((n, B) :: l)), ((n, B) :: l))) ((0, 1), []) def bernoulli (n : ℕ) : ℚ := (bernoulli_aux n).fst.snd #eval bernoulli_aux 16 -- ((16, -3617/510), [(15, 0), (14, 7/6), (13, 0), (12, -691/2730), (11, 0), (10, 5/66), (9, 0), (8, -1/30), (7, 0), (6, 1/42), (5, 0), (4, -1/30), (3, 0), (2, 1/6), (1, 1/2), (0, 1)]) := lemma bernoulli_zero : bernoulli 0 = 1 := rfl lemma bernoulli_one : bernoulli 1 = 1/2 := rfl lemma bernoulli_two : bernoulli 2 = 1/6 := rfl lemma bernoulli_three : bernoulli 3 = 0 := by norm_num -- fails end bernoulli

#### Mario Carneiro (Jan 31 2020 at 12:55):

`norm_num`

doesn't know anything about "your" functions. You have to use `norm_num [bernoulli]`

to have any chance of this working. With luck, that's all that is necessary, as long as all the necessary `list.sum`

simp lemmas are available

#### Johan Commelin (Jan 31 2020 at 12:57):

Does `norm_num`

look at `simp`

attributes?

#### Mario Carneiro (Jan 31 2020 at 12:57):

`norm_num`

is actually `repeat {norm_num1, simp}`

#### Johan Commelin (Jan 31 2020 at 12:58):

Unfortunately, it doesn't work

#### Mario Carneiro (Jan 31 2020 at 12:58):

do the usual thing: look at how it got stuck, identify the next simp lemma to get it unstuck

#### Johan Commelin (Jan 31 2020 at 12:59):

I see, I'll try that

#### Mario Carneiro (Jan 31 2020 at 13:00):

I've mentioned this before, but the "right" solution here is a `cbv`

tactic like coq's that will perform actual reduction, similar to what the VM does but with proofs

#### Johan Commelin (Jan 31 2020 at 19:57):

@[simp] lemma bernoulli_four : bernoulli 4 = -1/30 := begin rw [bernoulli_def], repeat { try { rw [finset.sum_range_succ] }, try { rw [nat.choose_succ_succ] }, simp, norm_num1, }, end

This runs fine now, although it isn't instant.

#### Johan Commelin (Jan 31 2020 at 19:58):

Does it make sense to cache certain small computations in mathlib as simp-lemmas?

For example, do we want `n.choose k = foo`

for all `n,k <= 10`

?

#### Mario Carneiro (Jan 31 2020 at 20:04):

You could generate those lemmas with a tactic

#### Johan Commelin (Jan 31 2020 at 20:05):

Ooh, in this case I'm not too worried about manual duplication (-;

#### Johan Commelin (Jan 31 2020 at 20:05):

But do we want to spend 20 seconds on verifying those simp-lemmas every build?

#### Gabriel Ebner (Jan 31 2020 at 20:06):

The more important issue that the simplifier tries to apply those 11*11 simp-lemmas every time it sees `choose`

.

#### Mario Carneiro (Jan 31 2020 at 20:07):

stupid simp...

#### Johan Commelin (Jan 31 2020 at 20:07):

Ok, we could put them in a separate set

#### Mario Carneiro (Jan 31 2020 at 20:09):

This should be a norm_num extension, but I never properly set that up

#### Johan Commelin (Jan 31 2020 at 20:11):

Here's what I have now: https://github.com/leanprover-community/mathlib/blob/a99538789fff693c88be290fd45a89b199ecc800/src/data/generating_function.lean#L152L179

A nice definition of `bernoulli`

required a new version of `nat.strong_rec_on`

#### Johan Commelin (Jan 31 2020 at 20:12):

I was very surprised to see that it was a definition that completely happened in tactic mode. Also, I couldn't prove anything about it.

#### Patrick Massot (Feb 01 2020 at 10:31):

Is this generating function stuff meant to be PRed to mathlib?

#### Johan Commelin (Feb 01 2020 at 10:31):

Potentially, yes.

#### Johan Commelin (Feb 01 2020 at 10:31):

Why?

#### Patrick Massot (Feb 01 2020 at 10:32):

Because it would be nice to have this stuff in;

#### Johan Commelin (Feb 01 2020 at 10:46):

Has anyone done anything in the direction of Taylor series?

#### Sebastien Gouezel (Feb 01 2020 at 10:53):

Not that I know. But I have in the works a refactor of the iterated derivative (now seen as a continuous multilinear map) and a definition of the n-th derivative of a one-dimensional function, that would be a prerequisite for this. The first step in this direction is #1921, awaiting review (hint, hint :)

#### Johan Commelin (Feb 01 2020 at 12:52):

@Sebastien Gouezel I'll make an attempt at reviewing the PR

#### Johan Commelin (Feb 01 2020 at 20:03):

@Sebastien Gouezel I took a first bite at reviewing this PR. 3 tiny comments so far...

#### Bryan Gin-ge Chen (Feb 01 2020 at 20:13):

(deleted)

#### Bryan Gin-ge Chen (Feb 01 2020 at 20:15):

(deleted)

Last updated: May 12 2021 at 07:17 UTC