rfl fails to prove that defintiional equal functions are =

Stream: general

[Frederick Pu]

import Lean
import Qq

open Lean Meta Elab Tactic Qq

def const_equivalent (xn yn : Name) : MetaM Bool := do
  isDefEq (← getConstInfo xn).value! (← getConstInfo yn).value!

-- Example usage
inductive Nat1
| zero
| succ (n : Nat1)

def Nat1.add : Nat1 → Nat1 → Nat1
| .zero, y => y
| .succ x, y => .succ (add x y)

def Nat1.add' : Nat1 → Nat1 → Nat1
| .zero, y => y
| .succ x, y => .succ (add' x y)

example : Nat1.add = Nat1.add' := by
  run_tac do
    let mvarId ← getMainGoal
    let womp ← mvarId.getType

    -- -- Cast to Q(Prop) instead of Sort u
    let this : Q(Prop) ← (← getMainGoal).getType

    match this with
    | ~q(@Eq $α $x $y) =>
      logInfo m!"{← isDefEq x y}"
      match x.constName?, y.constName? with
      | some xn, some yn =>
        logInfo m!"Found equality {xn} {yn}"
        evalTactic (← `(tactic| ext x))
        logInfo m!"{(← getConstInfo xn).value!}\n\n{(← getConstInfo yn).value!}"
        logInfo m!"are strucutrually identitical: {← const_equivalent xn yn}"
      | _, _ => logInfo "not equality between function symbols"
    | _ =>
      logInfo m!"Not an equality"
  -- are strucutrually identitical: true
  rfl -- however rfl fails

[Chris Bailey]

You can use rfl' (with a "prime" tick) which is more aggressive in reduction. I think this is a consequence of the "smart unfolding" used by rfl but not rfl'.

[Jovan Gerbscheid]

I would do a proof by induction:

example : Nat1.add = Nat1.add' := by
  ext
  fun_induction Nat1.add <;> grind [Nat1.add']

[Yury G. Kudryashov]

When you define a function using pattern matching, the elaborator does a lot under the hood (I'm not sure about the details). You shouldn't assume that 2 pattern-matching definitions that look the same are rfl.

[Frederick Pu]

they're definitionally equal underisDefEqtho

[Jakub Nowak]

isDefEq printed false.

[Jakub Nowak]

This works:

inductive Nat1
| zero
| succ (n : Nat1)

def Nat1.add : Nat1 → Nat1 → Nat1
| .zero, y => y
| .succ x, y => .succ (add x y)

def Nat1.add' : Nat1 → Nat1 → Nat1
| .zero, y => y
| .succ x, y => .succ (add' x y)

example : Nat1.add = Nat1.add' := by
  delta Nat1.add
  delta Nat1.add'
  rfl

[Jakub Nowak]

Basically, rfl can't really prove equality of recursive definitions. You would have to do induction for this.
delta (which is equivalent to (← getConstInfo xn).value! you did), makes the definition non-recursive, by using Nat1.brenOn directly. Unlike unfolding which "unfolds" one level of recursion. I don't know, but suspect, that rfl uses this smart unfolding instead of direct delta-expansion. And rfl' works, because it uses delta-expansion directly.

[Aaron Liu]

I suspect if you turn off smart unfolding then rfl works

[Jakub Nowak]

Indeed, this works:

set_option smartUnfolding false in
example : Nat1.add = Nat1.add' := by
  rfl

But I think this case is one of the reason why rfl' exists. It disables smart unfolding.

[Frederick Pu]

what is smart unfolding? does it guard against certain definitional expansions?

[Yury G. Kudryashov]

When Lean tests 2 expressions for defeq, it has to unfold some definitions. There are 2 algorithms, the newer one is called "smart".

[Yury G. Kudryashov]

(AFAIK)

[Jovan Gerbscheid]

The difference between normal unfolding and smart unfolding is that smart unfolding will unfold the definition and the match in one go. So it will unfold Nat1.add if it is applied to either 0 or Nat1.succ _. It couldn't do this in your example, hency why it didn't work.

[Jakub Nowak]

Jovan Gerbscheid said:

So it will unfold Nat1.add if it is applied to either 0 or Nat1.succ _. It couldn't do this in your example, hency why it didn't work.

I don't think you're right. This works:

inductive Nat1
| zero
| succ (n : Nat1)

def Nat1.add : Nat1 → Nat1 → Nat1
| .zero, y => y
| .succ x, y => x
y
def Nat1.add' : Nat1 → Nat1 → Nat1
| .zero, y => y
| .succ x, y => x

example : Nat1.add = Nat1.add' := by
  rfl

[Jakub Nowak]

Description for option smartUnfolding says "when computing weak head normal form, use auxiliary definition created for functions defined by structural recursion". So I think the main point of smart unfolding is the way recursive definitions are handled.

[Jakub Nowak]

Ah, no, I think you're right. "smart unfolding" is about reducing match expressions.

[Jakub Nowak]

Hm, reading the code it looks like turning off smartUnfolding makes rfl use deltaBetaDefinition which I suspect is similar to what delta tactic does. And with smartUnfolding on it rewrites definition to Nat1.add._sunfold, which is similar to what unfold does plus the behaviour of "shortcutting" match expressions.

Because of this I think that turning smartUnfolding off does more than it should? It not only turns off smartUnfolding but also turns off the unfolding behaviour.

Should we report this as a bug? I'm not sure if it's a bug, because I'm not sure whether smartUnfolding refers only to the behaviour of "shortcutting" match expressions, or more generally to unfolding via .eq_def?

[Joachim Breitner]

As Jovan says, smart unfolding will unfold the definition and matches in one step, if it can, and not at all otherwise. The point is that if it could unfold the definition, but not that match, for a structurally recursive function, you'd end up seeing some gory mess involving .brecOn, which as a user you usually don't want to.

In your case it seems that by exposing the .brecOn implementation on both sides, the equality can be shown.

Note that for structurally recursive functions, the .eq_def is not a definitional equality, but the rewrites that then also reduce the matche are.

[Jakub Nowak]

Maybe I don't understand what smart unfolding is supposed to do exactly? My understanding is that rewriting Nat1.add .zero y with (match .zero, y with | Nat1.zero, y => y | x.succ, y => (x.add y).succ) is normal unfolding.
And smart unfolding is rewriting Nat1.add .zero y with y.

[Joachim Breitner]

Right, but the former equality is not an definitional equality, so not usable by rfl

[Joachim Breitner]

You can delta Nat1 to see what it would really unfold to without smart unfolding