when does norm_num work?

Stream: maths

[Johan Commelin]

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]

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]

Does norm_num look at simp attributes?

[Mario Carneiro]

norm_num is actually repeat {norm_num1, simp}

[Johan Commelin]

Unfortunately, it doesn't work

[Mario Carneiro]

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

[Johan Commelin]

I see, I'll try that

[Mario Carneiro]

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]

@[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]

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]

You could generate those lemmas with a tactic

[Johan Commelin]

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

[Johan Commelin]

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

[Gabriel Ebner]

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

[Mario Carneiro]

stupid simp...

[Johan Commelin]

Ok, we could put them in a separate set

[Mario Carneiro]

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

[Johan Commelin]

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]

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]

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

[Johan Commelin]

Potentially, yes.

[Johan Commelin]

Why?

[Patrick Massot]

Because it would be nice to have this stuff in;

[Johan Commelin]

Has anyone done anything in the direction of Taylor series?

[Sebastien Gouezel]

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]

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

[Johan Commelin]

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

[Bryan Gin-ge Chen]

(deleted)

[Bryan Gin-ge Chen]

(deleted)