Reflection tactics and unwanted reduction

Stream: lean4

[Mario Carneiro]

BTW, this issue was also reported a while ago as #7729, although I am not sure why it's in the mathlib repo

[Mario Carneiro]

there are some more bits of information there about exactly why this is slow

[Mario Carneiro]

I believe the short version is that this has nothing to do with the thing being binary or unary and more to do with the fact that it is unfolding way more than it should be doing and seeing huge terms (but also doing it in unary)

[Joachim Breitner]

Hmm, that seems related but not quite the question here: There it looks we need better control over the reduction strategy - the question here is really just about whether using lists and indexing is ever a real bottleneck.

[Joachim Breitner]

Maybe you are saying that there are far bigger fish to fry :-D

[Mario Carneiro]

yes, that is what I am saying

[Mario Carneiro]

the indexing strategy certainly matters but for 2^8 it should be approximately zero and it's embarrassing that it's not

[Mario Carneiro]

Have you tried doing this as proof producing instead and measuring the performance of that?

[Mario Carneiro]

my gut feeling is that kernel reduction in lean is really bad performance-wise and I haven't really seen anything to suggest otherwise

[Mario Carneiro]

that's why I always tell people to write proof producing tactics instead

[Joachim Breitner]

For #7729, I wonder if we can instead of letting the kernel solve

List.length as + …  =?= Nat.Linear.Expr.denote [List.length as, Array.size bs] { eq := true; lhs := (Nat.Linear.Expr.var 0)…

that we can prove the goal

∀ x y, x + …  =?= Nat.Linear.Expr.denote [x, y] { eq := true; lhs := (Nat.Linear.Expr.var 0)…

and then,in a separate step, apply that to List.length as. That should avoid any reduction in the atoms, shouldn’t it?

[Joachim Breitner]

my gut feeling is that kernel reduction in lean is really bad performance-wise and I haven't really seen anything to suggest otherwise

Oh, absolutely! But it’s also sometimes convenient. And the roadmap does mention faster reduction :-)

[Mario Carneiro]

I'm not really convinced by that either, writing proof producing tactics is about as easy, especially if you have Qq on your side

[Joachim Breitner]

We don't have a small reproducer for the bug in #7729? Maybe I can cook one up, using a well-founded definition that you better not reduce in the kernel.

[Mario Carneiro]

Maybe it will be good someday but that's like waiting for an implementation of communism that doesn't suck

[Mario Carneiro]

you have to be extremely careful with kernel reduction to guard everything in sight so that unwanted things are not reduced

[Joachim Breitner]

What about large proof certificates like LRAT proofs – isn't it desirable to have a compact encoding of them in the proof term, that's checked by reflection, rather than exploding them into an inductive proof?

[Mario Carneiro]

when I plot the performance cost of kernel typechecking on everything in lean the declarations that top the list are all the ones using these methods

[Notification Bot]

18 messages were moved here from #lean4 > Faster Nat-indexed data structure for kernel reduction by Joachim Breitner.

[Joachim Breitner]

I took the liberty of splitting this from the narrow question of a kernel-friendly Nat-indexed map

[Joachim Breitner]

Mario Carneiro said:

when I plot the performance cost of kernel typechecking on everything in lean the declarations that top the list are all the ones using these methods

But is that because they have expensive proofs and would be even slower if the kernel would have to look at many small explicit steps? Or because we just do reflection badly.

[Mario Carneiro]

We do reflection badly

[Joachim Breitner]

And if we wouldn’t do it badly, shouldn’t it always be faster to evaluate a small function that does the steps, rather than checking a large inductive proof?

[Mario Carneiro]

it is actually faster to look at explicit steps

[Mario Carneiro]

because there is less unfolding

[Mario Carneiro]

everything matches syntactically after instantiation

[Joachim Breitner]

That’s sad, but sounds like something that can be fixed.

[Mario Carneiro]

:shrug:

[Mario Carneiro]

Coq has good kernel reduction, and it completely changes the way people write tactics

[Mario Carneiro]

but keep in mind that we're talking multiple years of work on writing advanced compilers inside the kernel, bytecode evaluation and jit compiling and such

[Mario Carneiro]

and it's all in the TCB

[Joachim Breitner]

Well, we do have by native_decide. So at least for the part of proofs by reflection that checks ground terms, we are not far off, aren't we?

[Joachim Breitner]

At least for those who accept that in the TCB (which seems comparable to what Coq has to offer, with jit and stuff in the TCB?)

[Mario Carneiro]

yes. But coq's bytecode evaluator works on open terms

[Mario Carneiro]

and the jit compiling is beyond what lean can do

[Mario Carneiro]

we don't have a fast evaluator for open terms

[Mario Carneiro]

I also know people in MetaCoq crazy enough to prove the correctness of the bytecode evaluator, so the TCB story is not really the same

[Joachim Breitner]

Reproducer for #7729:

def bad (n : Nat) : Nat :=
  if h : n = 0 then 0 else bad (n / 2)
termination_by n

set_option trace.profiler true in
theorem bar (n : Nat) : 2 * n = n + n := by simp_arith

set_option trace.profiler true in
theorem foo : 2 * bad 100 = bad 100 + bad 100 := by simp_arith

I’ll open a lean4 issue, so that it’s recorded.

[Joachim Breitner]

For open term reduction I wonder how fast they have to be. Of course it shouldn’t be stupidly slow (as in #7729), but maybe the bottle neck is usually going to be the closed evaluation part in roofs by reflection?