certificates for calculations

Stream: general

[Scott Morrison]

Could someone help me prove

def s (p : ℕ) : ℕ → ℕ
| 0 := 4
| (i+1) := ((s i)^2 - 2) % (2^p - 1)

lemma s15 : s 17 15 = 0 := sorry

I can't get anywhere close: here are my attempts so far.

import tactic.norm_num

def s (p : ℕ) : ℕ → ℕ
| 0 := 4
| (i+1) := ((s i)^2 - 2) % (2^p - 1)

lemma s0 : s 17 0 = 4 := rfl
lemma s1 : s 17 1 = 14 := rfl
lemma s2 : s 17 2 = 194 := rfl

-- deep recursion:
-- lemma s3_a : s 17 3 = 37634 :=

-- timeout:
-- lemma s3_b : s 17 3 = 37634 := rfl
-- by { dsimp [s] {single_pass:=tt}, rw s2, norm_num, }

-- timeout:
-- lemma s3_c : s 17 3 = 37634 :=
-- begin
--   dsimp [s] {single_pass:=tt}, transitivity,
--   apply congr_fun, apply congr_arg, apply congr_fun,
--   apply congr_arg, apply congr_fun, apply congr_arg,
--   exact s2, norm_num,
-- end

[Scott Morrison]

(A student here may have a go at the Lucas-Lehmer primality test, but I'd like to know that we can run it, before she writes the proof that it works...)

[Johan Commelin]

I guess it helps a lot to use optimizations for these computations in base 2

[Johan Commelin]

Nevertheless, you would hope that at some point Lean can cope on its own with numbers of size 2^17.

[Johan Commelin]

@Scott Morrison I guess the tricky bit is % (2^p - 1).

[Scott Morrison]

There are certainly tricks, like using that $k = (k mod 2^n) + \floor{k/2^n} mod 2^{n-1}$, but yeah, I'd like to know how to do this without such tricks (which should only be deployed later).

[Johan Commelin]

But how is Lean going to calculate foo % (2^17 - 1)?

[Johan Commelin]

That's going to take an insane amount of time, right?

[Mario Carneiro]

I have a tactic that gets the answer right, but I think the elaborator is getting in the way and causing the timeout

[Johan Commelin]

I would think you rw immediately into base 2 numbers, and then compute using the tricks.

[Mario Carneiro]

import tactic.norm_num

def s (p : ℕ) : ℕ → ℕ
| 0 := 4
| (i+1) := ((s i)^2 - 2) % (2^p - 1)

lemma s0 : s 17 0 = 4 := rfl

lemma s_suc {p a i b c}
  (h1 : 2^p - 1 = a)
  (h2 : s p i = b)
  (h3 : (b * b - 2) % a = c) :
  s p (i+1) = c :=
by rw [s, h1, h2, nat.pow_two, h3]

meta def prove_s (p ea ha : expr) (a : ℕ) : ℕ → tactic (ℕ × expr × expr)
| 0 := return (4, `(4), `(s0))
| (i+1) := do
  (b, eb, pb) ← prove_s i,
  let c := (b * b - 2) % a,
  let ec := reflect c,
  (ec', pc) ← norm_num.derive `((%%eb * %%eb - 2) % %%ea),
  return (c, ec, `(@s_suc %%p %%ea %%(reflect i) %%eb %%ec %%ha %%pb %%pc))

open tactic
meta def norm_num_s : tactic unit :=
do `(s %%p %%ei = %%e2) ← target,
  i ← eval_expr ℕ ei,
  (ea, pa) ← norm_num.derive `(2 ^ (%%p : ℕ) - 1),
  a ← eval_expr ℕ ea,
  (_, ec, pc) ← prove_s p ea pa a i,
  tactic.refine ``(eq.trans %%pc _)

lemma s15 : s 17 15 = 0 := by norm_num_s

[Mario Carneiro]

Honestly, norm_num is designed to be extensible and prove_s should properly be an extension (it can be one of the alternatives in the norm_num.derive), but right now you have to modify the tactic.norm_num file to do that

[Scott Morrison]

Hmm, replacing the last line with lemma s15 : s 17 15 = 0 := by { norm_num_s, refl } still times out.

[Mario Carneiro]

right, that's what I mean

[Mario Carneiro]

if you try to close the goal, the elaborator or something takes over and takes too long in doing so

[Scott Morrison]

Hmm, okay, I'd got that far.

[Mario Carneiro]

hm, I think it might be the kernel... this fails too

meta def add_s_thm (p i : ℕ) : tactic unit := do
  let ep := reflect p,
  (ea, pa) ← norm_num.derive `(2 ^ (%%ep : ℕ) - 1),
  a ← eval_expr ℕ ea,
  (_, ec, pc) ← prove_s ep ea pa a i,
  add_decl $ declaration.thm `foo [] `(s %%ep %%(reflect i) = %%ec) (return pc)

run_cmd add_s_thm 17 1

[Mario Carneiro]

in which case there is a bug somewhere, because there shouldn't be any significant kernel normalization

[Scott Morrison]

oh!

[Mario Carneiro]

unfortunately the kernel is absolutely terrible at reporting wtf is happening

[Scott Morrison]

:-(

[Mario Carneiro]

I do not have words to express my frustration with lean being so slow at basic verified math. It would be great if I could just turn off definition unfolding, which isn't supposed to happen in this proof

[Mario Carneiro]

It is very easy to get the impression that this is a result of the fact that we have to check a big proof. It's not. This is easy, lean is being stupid

[Scott Morrison]

I wonder if we can minimise an example here that shows clearly the problem.

[Scott Morrison]

It would be nice to pass some good examples up the chain...

[Mario Carneiro]

I'm not sure an example will help, in the sense that the problem is almost certainly fixable on the norm_num side. There is some bad application or something, and it's not on the happy path so lean totally falls to pieces

[Mario Carneiro]

the problem is that lean doesn't help very much to say what the problem is

[Mario Carneiro]

and since norm_num deals with a bunch of constants that have definitions, lean goes unfold-happy at the slightest misuse of anything and performance goes down to the level of "2 ^ 4 exhausts memory"

[Johan Commelin]

So if the "constants that have definitions" get replaced by atoms, does the problem go away?

[Mario Carneiro]

probably lean will give a hard error somewhere instead of crashing

[Mario Carneiro]

but that's a bit hard to implement easily

[Mario Carneiro]

because we're talking about things like + on nat; it's not acceptable to say that norm_num doesn't accept goals containing these symbols anymore

[Mario Carneiro]

hey, this works:

lemma foo : 2 ^ 17 - 1 = 131071 := by norm_num

lemma s_suc {p a i b c}
  (h1 : 2^p - 1 = a)
  (h2 : s p i = b)
  (h3 : (b * b - 2) % a = c) :
  s p (i+1) = c :=
by rw [s, h1, h2, nat.pow_two, h3]

example : s 17 15 = 0 :=
begin
  have := s0,
  iterate 15 {have := s_suc foo this (by norm_num; refl)},
  exact this
end

I fixed a bug in norm_num which may be related, but it should only affect the proof of foo, not the main proof

[Scott Morrison]

I better sleep, but I'll have a look in the morning.

[Kevin Buzzard]

It would be nice to pass some good examples up the chain...

coughgoingtovisitLeotomorrowcough

[Scott Morrison]

It seems the bug fix in norm_num fixed my other attempts to prove s 17 15 = 0, so perhaps we can put this down to the norm_num bug, rather than a kernel problem?

[Mario Carneiro]

the kernel problem is bad error reporting

[Mario Carneiro]

It's kind of difficult to test if norm_num is working if lean doesn't say when it's wrong

[Mario Carneiro]

keep in mind that norm_num is trying to prove things that are already true by rfl in principle

[Scott Morrison]

@Mario Carneiro, could I have some new help on this. I revisited this, and decided I needed to switch from nat to int. Unfortunately then your strategy using norm_num to handle each step is running into an error:

deep recursion was detected at 'replace' (potential solution: increase stack space in your system)

Here is the #mwe:

import tactic.norm_num

def s (p : ℕ) : ℕ → ℤ
| 0 := 4 % (2^p - 1)
| (i+1) := ((s i)^2 - 2) % (2^p - 1)

lemma s_succ {p a i b c}
  (h1 : (2^p - 1 : ℤ) = a)
  (h2 : s p i = b)
  (h3 : (b * b - 2) % a = c) :
  s p (i+1) = c :=
by { dsimp [s], rw [h1, h2, pow_two, h3] }

example : s 7 5 = 0 :=
begin
  have w : (2^7 - 1 : ℤ) = 127 := by norm_num,
  have h : s 7 0 = 4 := rfl,
  replace h := s_succ w h (by { norm_num, refl }),
  replace h := s_succ w h (by { norm_num, refl }),
  replace h := s_succ w h (by { norm_num, refl }),
  replace h := s_succ w h (by { norm_num, refl }),
  replace h := s_succ w h (by { norm_num, refl }),
  exact h,
end

This runs fine up to the exact h, and then takes a few seconds before giving the error message.

[Kenny Lau]

maybe you need to increase stack space in your system

[Scott Morrison]

Very unlikely, @Kenny Lau. The calculation is trivial, and changing int back to nat makes this work fine.

[Mario Carneiro]

Here is a more minimized version:

example : ((111 * 111 - 2) % 127 : ℤ) = 0 := by norm_num

this is the last subgoal

[Mario Carneiro]

I think norm_num has likely produced a bad proof, and rather than failing lean is trying to unfold everything to find out if it is actually a good proof

[Mario Carneiro]

example : (12321 - 2 : ℤ) = 12319 := by norm_num

[Mario Carneiro]

Oh dear...

example : int.has_sub = add_group_has_sub := rfl

example :
  (@has_sub.sub ℤ int.has_sub 12321 2 : ℤ) =
  (@has_sub.sub ℤ add_group_has_sub 12321 2) := rfl -- deep recursion

[Mario Carneiro]

This may have been a consequence of the move to get algebra out of core

[Mario Carneiro]

I think the issue is actually in the kernel check; the elaborator seems to have no problem with typechecking this

[Mario Carneiro]

#2804