## Stream: lean4

### Topic: type mismatch error

#### Chris B (Feb 04 2021 at 21:33):

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 (Feb 04 2021 at 21:41):

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

#### Mario Carneiro (Feb 04 2021 at 21:42):

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

#### Mario Carneiro (Feb 04 2021 at 21:43):

The alternative is to use induction using

#### Mario Carneiro (Feb 04 2021 at 21:51):

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 (Feb 04 2021 at 21:51):

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 (Feb 04 2021 at 21:51):

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 (Feb 04 2021 at 21:53):

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

#### Mario Carneiro (Feb 04 2021 at 21:53):

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 (Feb 04 2021 at 21:56):

@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 (Feb 04 2021 at 21:56):

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 (Feb 04 2021 at 21:57):

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

#### Chris B (Feb 04 2021 at 21:57):

Wow, Lean Zulip really coming through on this one

#### Leonardo de Moura (Feb 04 2021 at 21:59):

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 (Feb 04 2021 at 22:00):

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 (Feb 04 2021 at 22:01):

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

#### Mario Carneiro (Feb 04 2021 at 22:04):

here's the golf version

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


#### Kevin Buzzard (Feb 04 2021 at 22:16):

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

#### Leonardo de Moura (Feb 04 2021 at 22:18):

@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 (Feb 04 2021 at 22:21):

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 (Feb 04 2021 at 22:22):

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 (Feb 04 2021 at 22:23):

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 (Feb 04 2021 at 22:24):

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 (Feb 04 2021 at 22:27):

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 (Feb 04 2021 at 22:27):

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 (Feb 04 2021 at 22:28):

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 (Feb 04 2021 at 22:30):

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 (Feb 04 2021 at 22:31):

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 (Feb 04 2021 at 22:32):

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

#### Mario Carneiro (Feb 04 2021 at 22:33):

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 (Feb 04 2021 at 22:33):

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 (Feb 04 2021 at 22:37):

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 (Feb 04 2021 at 22:41):

@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 (Feb 04 2021 at 22:43):

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 (Feb 04 2021 at 22:43):

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 (Feb 04 2021 at 22:44):

I will see if I can come up with an example

#### Leonardo de Moura (Feb 04 2021 at 22:51):

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 (Feb 04 2021 at 23:00):

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 (Feb 04 2021 at 23:09):

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

#### Daniel Selsam (Feb 04 2021 at 23:17):

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

#### Daniel Selsam (Feb 04 2021 at 23:19):

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

#### Leonardo de Moura (Feb 04 2021 at 23:24):

@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.

#### Mario Carneiro (Feb 04 2021 at 23:51):

@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 (Feb 04 2021 at 23:59):

@Mario Carneiro Thanks for testing it.

Last updated: May 07 2021 at 12:15 UTC