# Zulip Chat Archive

## Stream: lean4

### Topic: mathport:sunfold

#### Daniel Selsam (Mar 20 2021 at 17:56):

Here is a weird issue: the following theorem typechecks in the kernel but cannot be elaborated:

```
import Lean3Lib.init.data.nat.lemmas
theorem Mathlib.nat.sub_one_alt (n : ℕ) : n - 1 = nat.pred n := rfl
```

The issue is that `nat.pred._sunfold`

is generated in lean3 and auto-ported, and the smart-unfolding in lean4 finds it. In lean4, non-recursive functions don't generate `_sunfold`

definitions, and smart-unfolding seems to work differently though I did not investigate the differences yet. Note: this example works if smart-unfolding is disabled.

I think this is a pretty sketchy proof anyway. It would be better to do induction on `n`

than to rely on two non-simplifying recursor applications being equal. So, I am tempted to ignore the issue.

#### Mario Carneiro (Mar 20 2021 at 19:23):

I don't find this definition to be odd at all. `nat.sub`

is defined as:

```
protected def sub : ℕ → ℕ → ℕ
| a 0 := a
| a (b+1) := pred (sub a b)
```

This is a definition by recursion on the second argument (I would have left `a`

out of the recursion entirely, as in

```
protected def sub (a : ℕ) : ℕ → ℕ
| 0 := a
| (b+1) := pred (sub b)
```

but at least in this case it should come out the same either way), so if you insert `1`

for `b`

then this reduces to `pred (sub a 0) = pred a`

. The first argument is never cased on so it is very reasonable to expect this defeq.

#### Mario Carneiro (Mar 20 2021 at 19:25):

I actually haven't heard of `foo._sunfold`

before. It's not directly referenced by `nat.pred`

or any theorems, so I'm not sure what its role is. It appears to be a copy of `nat.pred._main`

.

#### Daniel Selsam (Mar 20 2021 at 19:43):

It is related to "smart-unfolding", which is a trick to avoid incomprehensible messes when unfolding recursive definitions. Here is an example in lean3: https://github.com/leanprover-community/lean/blob/master/src/library/type_context.h#L443-L457

Note: it is only used as a heuristic by the unifier, and does not appear in any actual theorems/proofs.

#### Daniel Selsam (Mar 20 2021 at 19:44):

One issue here is that lean3 produces these `_sunfold`

even for non-recursive functions, whereas lean4 assumes it will only exist for recursive functions, and so doesn't fall back on regular unfolding when the `_sunfold`

exists and the major premise is not a constructor.

#### Mario Carneiro (Mar 20 2021 at 20:06):

I don't see why this would cause a unification error though. It sounds like this should only affect unfolding in the middle of a proof; anything it comes up with should be defeq to the real thing, so a proof by `rfl`

shouldn't cause any problems because there's only one thing to do

#### Daniel Selsam (Mar 20 2021 at 20:09):

in lean4, when smart-unfolding with an `_sunfold`

, it *does not unfold at all* unless whnf-ing would return an `idRhs`

application. so here it tries smart-unfolding, gets something besides an `idRhs`

application (since the major premise is a local constant) and rolls back.

#### Mario Carneiro (Mar 20 2021 at 20:09):

the major premise should not be a local constant though

#### Mario Carneiro (Mar 20 2021 at 20:09):

the major premise here is `1`

#### Mario Carneiro (Mar 20 2021 at 20:13):

Oh wait, `nat.pred._sunfold`

? We shouldn't be unfolding `nat.pred`

in this proof at all

#### Mario Carneiro (Mar 20 2021 at 20:14):

We do need `nat.sub._sunfold`

but that's a recursive function so according to you that should work in lean 4

#### Daniel Selsam (Mar 20 2021 at 20:15):

Wow there are so many layers to this issue. We are aligning `nat.sub`

-> `Nat.sub`

, but not `nat.pred`

-> `Nat.pred`

. The latter two are def-eq, which is why we can align the `sub`

s. But now we try to unify `nat.pred n =?= Nat.pred (Nat.sub n 0)`

and `nat.pred`

won't unfold because of the `_sunfold`

issue.

#### Mario Carneiro (Mar 20 2021 at 20:17):

I see. I think this means that definitions by the equation compiler have to be aligned if they are to be treated as defeq, because unapplied equation compiler definitions are effectively constants

#### Daniel Selsam (Mar 20 2021 at 20:21):

This specific issue will go away now that I added `nat.pred -> Nat.pred`

to the align list. We might preempt many others by having lean3 no longer produce these `_sunfold`

lemmas for non-recursive functions. Also, it might be a good idea to do a more careful pass accumulating other things to align.

#### Mario Carneiro (Mar 20 2021 at 20:39):

Even if we removed the `_sunfold`

lemmas, it still seems like good practice to not try unifying distinct equation compiler definitions anyway, they are giant behemoths and anything that relies on such unfolding will be slow and brittle wrt changes in the actual compilation strategy

#### Daniel Selsam (Mar 20 2021 at 20:41):

Are they really giant behemoths for non-recursive functions?

#### Mario Carneiro (Mar 20 2021 at 20:45):

They can be, if there are lots of nested matches or a match on `n+5`

or something; but my main point is that we want to isolate the equation compiler's output from the user-level equations as much as possible in order to allow for more flexibility in compilation

#### Mario Carneiro (Mar 20 2021 at 20:46):

For example, if you pattern match on two `option A`

's and give four equations for the cases it shouldn't be observable which one was matched first

#### Daniel Selsam (Mar 23 2021 at 02:52):

Mario Carneiro said:

I see. I think this means that definitions by the equation compiler have to be aligned if they are to be treated as defeq, because unapplied equation compiler definitions are effectively constants

Lean4's equation compiler does not produce the same definitions. Here is Lean3:

```
def temp.pred : nat → nat
| 0 := 0
| (n+1) := n
#print temp.pred
/-
def temp.pred : ℕ → ℕ :=
temp.pred._main
-/
```

and here is Lean4:

```
def Temp.pred : Nat → Nat
| 0 => 0
| n+1 => n
#print Temp.pred
/-
def Temp.pred : Nat → Nat :=
fun (x : Nat) =>
match x with
| 0 => 0
| Nat.succ n => n
-/
```

If we align `temp.pred`

-> `Temp.pred`

, the old definition `temp.pred._main`

should be orphaned, which is fine.

#### Gabriel Ebner (Mar 23 2021 at 10:20):

The definition produced by the Lean 4 elaborator is actually very similar to the Lean 3 one (except for the extra main redirection). It's just that the new pretty-printer is much better at hiding the ugly details:

```
set_option pp.all true in #print Temp.pred
/-
def Temp.pred : Nat → Nat :=
fun x => Temp.pred.match_1.{1} (fun x => Nat) x (fun _ => @OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) fun n => n
-/
```

#### Daniel Selsam (Mar 23 2021 at 16:42):

Thanks, I forgot that the matches were sugar for aux definitions. But still, if we align `foo3`

-> `foo4`

, `foo3._main`

should be orphaned and so there is no need to align it to anything.

#### Gabriel Ebner (Mar 23 2021 at 16:51):

It's possible that foo3._main occurs in a proof.

#### Daniel Selsam (Mar 23 2021 at 17:25):

Yes, what I wrote about is not quite right, since I forgot that the lean3 equation lemmas are defined to be the `_main`

equation lemmas. This is why I already had to map e.g. `nat.add._main`

-> `Nat.add`

. Do you see any reason why that wouldn't work in general? Specifically, if `foo3`

-> `foo4`

and `foo3._main`

exists, then `foo3._main`

-> `foo4`

(rather than aligning the `_main`

to a aux match decl inside `foo4`

).

#### Gabriel Ebner (Mar 23 2021 at 17:33):

For non-mutual definitions, `foo3`

and `foo3._main`

should be interchangeable. So I'd try to map both `foo3`

and `foo3._main`

to `foo4`

.

#### Gabriel Ebner (Mar 23 2021 at 17:34):

Which is exactly what you've proposed.

Last updated: May 07 2021 at 13:21 UTC