Zulip Chat Archive

Stream: maths

Topic: when does norm_num work?


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jan 31 2020 at 12:57):

Does norm_num look at simp attributes?

view this post on Zulip Mario Carneiro (Jan 31 2020 at 12:57):

norm_num is actually repeat {norm_num1, simp}

view this post on Zulip Johan Commelin (Jan 31 2020 at 12:58):

Unfortunately, it doesn't work

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jan 31 2020 at 12:59):

I see, I'll try that

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jan 31 2020 at 20:04):

You could generate those lemmas with a tactic

view this post on Zulip Johan Commelin (Jan 31 2020 at 20:05):

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

view this post on Zulip Johan Commelin (Jan 31 2020 at 20:05):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jan 31 2020 at 20:07):

stupid simp...

view this post on Zulip Johan Commelin (Jan 31 2020 at 20:07):

Ok, we could put them in a separate set

view this post on Zulip Mario Carneiro (Jan 31 2020 at 20:09):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Feb 01 2020 at 10:31):

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

view this post on Zulip Johan Commelin (Feb 01 2020 at 10:31):

Potentially, yes.

view this post on Zulip Johan Commelin (Feb 01 2020 at 10:31):

Why?

view this post on Zulip Patrick Massot (Feb 01 2020 at 10:32):

Because it would be nice to have this stuff in;

view this post on Zulip Johan Commelin (Feb 01 2020 at 10:46):

Has anyone done anything in the direction of Taylor series?

view this post on Zulip 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 :)

view this post on Zulip Johan Commelin (Feb 01 2020 at 12:52):

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

view this post on Zulip Johan Commelin (Feb 01 2020 at 20:03):

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

view this post on Zulip Bryan Gin-ge Chen (Feb 01 2020 at 20:13):

(deleted)

view this post on Zulip Bryan Gin-ge Chen (Feb 01 2020 at 20:15):

(deleted)


Last updated: May 12 2021 at 07:17 UTC