mathport:sunfold

Stream: lean4

[Daniel Selsam]

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]

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]

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]

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]

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]

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]

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]

the major premise should not be a local constant though

[Mario Carneiro]

the major premise here is 1

[Mario Carneiro]

Oh wait, nat.pred._sunfold? We shouldn't be unfolding nat.pred in this proof at all

[Mario Carneiro]

We do need nat.sub._sunfold but that's a recursive function so according to you that should work in lean 4

[Daniel Selsam]

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 subs. 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]

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]

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]

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]

Are they really giant behemoths for non-recursive functions?

[Mario Carneiro]

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]

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]

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]

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]

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]

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

[Daniel Selsam]

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]

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]

Which is exactly what you've proposed.