type mismatch error

Stream: lean4

[Chris B]

Trying to feel out some simple things in Lean 4, I'm not able to get this Lean 3 theorem to work, but I'm not sure why. Is there an easy way to get more information out of the ?m.166?

-- Lean 3 version
structure Point := (x : ℤ)

theorem PointExt_lean3 (p : Point) : forall (q : Point) (h1 : Point.x p = Point.x q), p = q :=
Point.rec_on p $
fun z1 q, Point.rec_on q $
fun z2 (hA : Point.x (Point.mk z1) = Point.x (Point.mk z2)), congr_arg Point.mk hA

theorem PointExt_lean4 (p : Point) : forall (q : Point) (h1 : Point.x p = Point.x q), p = q :=
Point.recOn p $
fun z1 q => Point.recOn q $
fun z2 (hA : Point.x (Point.mk z1) = Point.x (Point.mk z2)) => congrArg Point.mk hA

/-
type mismatch
  Point.recOn p
    fun (z1 : Int) (q : Point) =>
      Point.recOn q fun (z2 : Int) (hA : { x := z1 }.x = { x := z2 }.x) => congrArg Point.mk hA
has type
  ?m.166 p p
but is expected to have type
  (q : Point) → p.x = q.x → p = q
-/

[Mario Carneiro]

I think this is because the elab_as_eliminator elaboration strategy doesn't exist anymore

[Mario Carneiro]

which means that using recOn directly is always going to be painful

[Mario Carneiro]

The alternative is to use induction using

[Mario Carneiro]

Here's a version using match:

structure Point := (x : Int)

theorem PointExt_lean4 (p : Point) : (q : Point) → p.x = q.x → p = q :=
match p with
| ⟨z1⟩ => fun
  | ⟨z2⟩ => fun (hA : Point.x (Point.mk z1) = Point.x (Point.mk z2)) => congrArg Point.mk hA

[Chris B]

Thanks, I wasn't aware of how much work elab_as_eliminator was doing in the garden-variety case. The lean 4 version does work if I specify the motive.

theorem PointExt_lean4 (p : Point) : forall (q : Point) (h1 : Point.x p = Point.x q), p = q :=
Point.recOn (motive := fun hp => forall hq (hh : Point.x hp = Point.x hq), hp = hq) p $
fun z1 q => Point.recOn (motive := fun (_x : Point) => (Point.x $ Point.mk z1) = (Point.x _x) -> (Point.mk z1) = (_x)) q $
fun z2 (hA : Point.x (Point.mk z1) = Point.x (Point.mk z2)) => congrArg Point.mk hA

[Leonardo de Moura]

We will not support elab_as_eliminator. Users should use match ... with ... or tactics such as induction and cases.
If match ... with ... is not applicable, and you want to keep working in term mode, you can write a macro that "switches" to tactic mode and back into term mode.

[Chris B]

Thanks to both of you. That match example is nice. I'll take a closer look at the new version induction.

[Mario Carneiro]

Is there a way to use match and/or induction such that we can be sure that recOn is getting called (as opposed to some more complicated below compilation or such)?

[Leonardo de Moura]

@Chris B Note that writing : forall (q : Point) ... is a trick to make Lean3 elam_as_eliminator + recOn work. You don't need this kind of trick when using match.

structure Point := (x : Int)

theorem PointExt_lean4 (p : Point) (q : Point) (h1 : Point.x p = Point.x q) : p = q :=
  match p, q, h1 with
  | ⟨_⟩, ⟨_⟩, h1 => congrArg Point.mk h1

theorem PointExt_lean4' (p : Point) (q : Point) (h1 : Point.x p = Point.x q) : p = q := by
  cases p
  cases q
  exact congrArg Point.mk h1

[Mario Carneiro]

Here's a proof using induction using, which I think should get the term right:

structure Point := (x : Int)

theorem PointExt_lean4 (p : Point) : (q : Point) → p.x = q.x → p = q :=
by induction p using Point.recOn with
| mk z1 => intro q; induction q using Point.recOn with
  | mk z2 => exact fun (hA : Point.x (Point.mk z1) = Point.x (Point.mk z2)) => congrArg Point.mk hA

[Mario Carneiro]

(of course there are much easier ways to write this expression, like Leo's version)

[Chris B]

Wow, Lean Zulip really coming through on this one

[Leonardo de Moura]

Mario Carneiro said:

Is there a way to use match and/or induction such that we can be sure that recOn is getting called (as opposed to some more complicated below compilation or such)?

The induction tactic by default uses rec. recOn is just a simple wrapper on top of rec that puts the major premise before minor premises.

[Mario Carneiro]

rec works too. I'm just thinking about those examples where lean 3's compilation strategy either results in a term that is slow to kernel-compute or doesn't support something like small eliminating inductive predicates

[Mario Carneiro]

I would usually either use rec/rec_on or induction to construct the term in those cases

[Mario Carneiro]

here's the golf version

theorem PointExt_lean4 : (p : Point) → (q : Point) → p.x = q.x → p = q
  | ⟨z⟩, ⟨_⟩, rfl => rfl

[Kevin Buzzard]

Nice to see that the rfl trick still works :-)

[Leonardo de Moura]

@Mario Carneiro

I'm just thinking about those examples where lean 3's compilation strategy either results in a term that is slow to kernel-compute

I'm not concerned about this case. We don't rely on kernel-compute that much. Have you measured the overhead of brecOn vs rec in real examples?

doesn't support something like small eliminating inductive predicates

Yes, this one is a real problem. I have seen many examples where using equations would be much nicer.
Right now, the best option is to switch to the tactic mode and use induction. In Lean 4, this is not as bad as in Lean 3 since the induction tactic notation is nicer.

I know you have been asking for this feature for ages, but it will not come anytime soon. The "equation compiler" decouples dependent pattern matching from termination checking. The code is more modular, the dependent pattern matching uses the casesOn recursor, and structural termination checker uses brecOn. Moreover, we can add new termination strategies (e.g., well-founded recursion) without even touching the dependent pattern matching modulo. To support rec/recOn, we would have to implement yet another strategy that does a bit of both: patter matching and termination checking. It will be implemented one day, but don't hold your breath :)

[Mario Carneiro]

I'm not concerned about this case. We don't rely on kernel-compute that much. Have you measured the overhead of brecOn vs rec in real examples?

These are lean 3 concerns. I'm sure that the calculus in lean 4 is completely different, but that's just an example of why I would want to do something as masochistic as using recursors directly instead of the many bits of sugar on top.

[Leonardo de Moura]

These are lean 3 concerns. I'm sure that the calculus in lean 4 is completely different, but that's just an example of why I would want to do something as masochistic as using recursors directly instead of the many bits of sugar on top.

Do you have examples where you had to use rec manually because of a performance problem in Lean 3? How much faster was it when you switched from brec_on to rec/rec_on?

[Mario Carneiro]

Is decTrivial still a thing in lean 4? That's the main place where kernel compute comes up in mathlib, although I think it also shows up in code with a different style in third party lean 3 projects

[Mario Carneiro]

Profiling kernel computation in lean 3 is very difficult, it doesn't show up with set_option profiler true, so my judgment on these matters is a little coarse-grained

[Mario Carneiro]

Right now, the best option is to switch to the tactic mode and use induction. In Lean 4, this is not as bad as in Lean 3 since the induction tactic notation is nicer.

I think this is fine, I have enough experience doing just this in lean 3

[Leonardo de Moura]

Mario Carneiro said:

Is decTrivial still a thing in lean 4? That's the main place where kernel compute comes up in mathlib, although I think it also shows up in code with a different style in third party lean 3 projects

Yes, it is. We have a macro called decide!.

[Mario Carneiro]

A similar example where the kernel term is more or less unwritable in lean 3 is eq.rec, where it's worth it to use tactic mode just to use rw even if nothing else is in tactic mode

[Leonardo de Moura]

Mario Carneiro said:

A similar example where the kernel term is more or less unwritable in lean 3 is eq.rec, where it's worth it to use tactic mode just to use rw even if nothing else is in tactic mode

We have a custom elaborator for generating Eq.rec applications in term mode.
The notation is also available in Lean 3 h ▸ e. However, the Lean 4 elaborator for this notation is supposed to be better.

[Mario Carneiro]

But supposing the user wanted to have a syntax like applying a term, I guess it wouldn't be too bad to add a macro like elim!(Foo.rec_on) x ... which either calls induction internals or just reimplements the elab_as_eliminator magic itself

[Mario Carneiro]

(that should be implementable outside the core, I think?)

[Mario Carneiro]

Yeah, h ▸ e does show up in mathlib occasionally, but it fails in a lot of situations where by rw h; exact e works - I think the main reason is metavariables in the expected type

[Leonardo de Moura]

Yes, if one wants to add support to elab_as_eliminator. I think the one to go is to add a macro such as elim! ....

(that should be implementable outside the core, I think?)

Yes, and if I had to do it, I would do it on top of the induction tactic.

[Mario Carneiro]

Do we still need recOn at all in lean 4? As I understand it the main reason is to make it easier to write these term proofs, since it's more natural to put the scrutinee first, but if users can't really write it anymore then it doesn't seem necessary to have it at all

[Leonardo de Moura]

@Mario Carneiro Returning to brecOn vs rec, it would be very useful if you could get numbers for dec_trivial in mathlib with rec and brecOn. We have been assuming the difference is not big. If it is big, then we have a problem because the generated code for definitions using rec sucks. That is, one may speed up kernel reduction using rec, but they are also slowing down the generated C code.

[Leonardo de Moura]

Mario Carneiro said:

Do we still need recOn at all in lean 4? As I understand it the main reason is to make it easier to write these term proofs, since it's more natural to put the scrutinee first, but if users can't really write it anymore then it doesn't seem necessary to have it at all

We needed it while transitioning from the old to the new frontend, but it is now a "leftover". We may still have code that depends on it though. It is also useful to keep it for Daniel's porting tool. Otherwise, he will have to add support for converting rec_on applications into rec.

[Mario Carneiro]

I don't think the difference is big, but it is one of the things on my list of "how to optimize code for kernel computation". The fact that optimizing for kernel computation vs VM computation is often in opposition is a long standing problem that I hope lean 4's implementedBy will solve

[Mario Carneiro]

I will see if I can come up with an example

[Leonardo de Moura]

I hope lean 4's implementedBy will solve

Unfortunately, it doesn't solve this problem since it only requires the two definitions to have the same type.
When we use @[implementedBy f] def g ..., we are telling the code generator: "trust me, it is safe to replace g with f".
For solving the issue you raised, we can use another feature we are planning to add: simp lemmas for the compiler. The user provers an equation lemma and tells the compiler to use it as a rewriting rule to optimize code. Haskell has a similar feature, but the rewriting rules come without proof.

[Daniel Selsam]

It is also useful to keep it for Daniel's porting tool. Otherwise, he will have to add support for converting rec_on applications into rec.

FYI I am not currently aligning rec_on to recOn.

[Leonardo de Moura]

@Daniel Selsam What about noConfusion, casesOn, and brecOn?

[Daniel Selsam]

@Leonardo de Moura I am not currently aligning any of them.

[Daniel Selsam]

I haven't even checked which ones are identical. For a pair that is identical, it is very easy to align.

[Leonardo de Moura]

@Daniel Selsam We need them. Otherwise, we will not be able to pattern match, use tactics such as cases and injection, use recursive equations, etc. If aligning is problematic, another option is to invoke the generators for noConfusion, casesOn, and brecOn from the porting tool.

[Daniel Selsam]

I will add.

[Mario Carneiro]

@Leonardo de Moura I just did a test using the primality test in data.num.prime, which has been optimized for kernel computation.

import data.num.prime
example : num.min_fac 104729 = 104729 := rfl

I tested replacements for three of the core functions in this computation:

protected def add : pos_num → pos_num → pos_num :=
λ a, pos_num.rec_on a succ
  (λ a IH b, pos_num.cases_on b (bit0 (succ a)) (λ b, bit0 (succ (IH b))) (λ b, bit1 (IH b)))
  (λ a IH b, pos_num.cases_on b (bit1 a) (λ b, bit1 (IH b)) (λ b, bit0 (IH b)))

protected def mul (a : pos_num) : pos_num → pos_num :=
λ b, pos_num.rec_on b a
  (λ b IH, pos_num.add (bit0 IH) a)
  (λ b IH, bit0 IH)

def min_fac_aux (n : pos_num) : ℕ → pos_num → pos_num :=
λ k, nat.rec (λ _, n) (λ fuel IH k,
  if n < k.bit1 * k.bit1 then n else
  if k.bit1 ∣ n then k.bit1 else
  IH k.succ) k

vs

protected def add : pos_num → pos_num → pos_num
| 1        b        := succ b
| a        1        := succ a
| (bit0 a) (bit0 b) := bit0 (add a b)
| (bit1 a) (bit1 b) := bit0 (succ (add a b))
| (bit0 a) (bit1 b) := bit1 (add a b)
| (bit1 a) (bit0 b) := bit1 (add a b)

protected def mul (a : pos_num) : pos_num → pos_num
| 1        := a
| (bit0 b) := bit0 (mul b)
| (bit1 b) := bit0 (mul b) + a

def min_fac_aux (n : pos_num) : ℕ → pos_num → pos_num
| 0 _ := n
| (fuel+1) k :=
  if h : n < k.bit1 * k.bit1 then n else
  if k.bit1 ∣ n then k.bit1 else
  min_fac_aux fuel k.succ

Since the built in profiler doesn't work, I used rm test.olean; /usr/bin/time -f %U lean --make test.lean to test, so the data is a bit noisy. For the equation compiler definition:

13.89, 13.82, 14.02, 13.64, 13.71

For the rec definition:

10.76, 10.59, 10.66, 10.51, 10.60

This suggests that the difference, while not large, is measurable, especially in hot functions like add and mul in this example, which should be called ~3,000,000 times in this test

[Leonardo de Moura]

@Mario Carneiro Thanks for testing it.