## 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.

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.

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...

(deleted)

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

(deleted)

Last updated: May 12 2021 at 07:17 UTC