Reflection in Lean4

Stream: lean4

[Chris Hughes]

I've noticed that reflection is better in Lean4 and not just the natural number improvements. For example the following expression in Lean3 takes much longer to reduce the more xs I add

#reduce
  let x : ℕ := (list.range 10000).nth_le 0 sorry in
  (x, x, x, x, x, x, x)

But the version in Lean4 takes more or less the same time no matter how many xs there are

#reduce
  let x : ℕ := (List.range 10000).get 0 sorry
  (x, x, x, x, x, x, x)

Presumably Lean4 is evaluating x before reducing the let, but Lean3 reduces the let first and has to evaluate x seven times. Lean4 is also smart enough to not evaluate x at all in the following example

#reduce
  let x : ℕ := (List.range 10000).get 0 sorry
  1

I was thinking of writing the abel tactic in Lean4 using reflection a bit like the ring2 tactic in mathlib in Lean 3. Is it sensible to use reflection a lot more in Lean 4? I can think of ways in which reducing things in the wrong order makes reduction take a lot longer. Has there been a deliberate effort to make reduction a lot faster in Lean 4 and is proof by reflection something we could do a lot more in Lean4 without having to worry some huge blow-up in the time it takes to reduce because the kernel is not unfolding things in the best order like the example in Lean3 above?

[Yakov Pechersky]

(deleted)

[Daniel Selsam]

Chris Hughes said:

I've noticed that reflection is better in Lean4 and not just the natural number improvements. For example the following expression in Lean3 takes much longer to reduce the more xs I add

#reduce
  let x : ℕ := (list.range 10000).nth_le 0 sorry in
  (x, x, x, x, x, x, x)

But the version in Lean4 takes more or less the same time no matter how many xs there are

#reduce
  let x : ℕ := (List.range 10000).get 0 sorry
  (x, x, x, x, x, x, x)

Presumably Lean4 is evaluating x before reducing the let, but Lean3 reduces the let first and has to evaluate x seven times. Lean4 is also smart enough to not evaluate x at all in the following example

#reduce
  let x : ℕ := (List.range 10000).get 0 sorry
  1

I was thinking of writing the abel tactic in Lean4 using reflection a bit like the ring2 tactic in mathlib in Lean 3. Is it sensible to use reflection a lot more in Lean 4? I can think of ways in which reducing things in the wrong order makes reduction take a lot longer. Has there been a deliberate effort to make reduction a lot faster in Lean 4 and is proof by reflection something we could do a lot more in Lean4 without having to worry some huge blow-up in the time it takes to reduce because the kernel is not unfolding things in the best order like the example in Lean3 above?

Not exactly answering your question, but FYI Lean4 has support for using the interpreter/compiler for (not as trustworthy) proofs by reflection: https://github.com/leanprover/lean4/blob/master/src/Init/Core.lean#L1012-L1031 I was assuming that Mathlib would not want to use this feature though.

[Mario Carneiro]

FYI Lean4 has support for using the interpreter/compiler for (not as trustworthy) proofs by reflection: ... I was assuming that Mathlib would not want to use this feature though.

This is a decision that we will have to consider once mathlib4 is up and running. It's best to deal with this in the context of a particular proof that benefits greatly from it. But I would guess that this is treated the same as axiom usage reduction: it's okay to use and it's also okay to eliminate the use