# Zulip Chat Archive

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

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

I will add.

#### 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