Function not equal to itself

Stream: new members

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

I am once again confused by definitional equality. The following function is not equal to its own definition by Eq.refl. What is going on? This is with Lean v4.14.0-rc1.

@[reducible] def g : Nat → Nat
  | 0 => 0
  | n+1 => g n

set_option pp.explicit true in
#print g

example :
    g =
    -- output of #print above
    (fun x ↦
      @Nat.brecOn (fun x ↦ Nat) x fun x f ↦
        g.match_1 (fun x ↦ @Nat.below (fun x ↦ Nat) x → Nat) x (fun a x ↦ @OfNat.ofNat Nat 0 (instOfNatNat 0))
          (fun n x ↦ x.1) f) :=
  Eq.refl _ -- type mismatch

[Kyle Miller]

Hmm, using delta to unfold g with its definition works:

example :
    g =
    -- output of #print above
    (fun x ↦
      @Nat.brecOn (fun x ↦ Nat) x fun x f ↦
        g.match_1 (fun x ↦ @Nat.below (fun x ↦ Nat) x → Nat) x (fun a x ↦ @OfNat.ofNat Nat 0 (instOfNatNat 0))
          (fun n x ↦ x.1) f) := by
  delta g
  rfl

[Kyle Miller]

It seems that smart unfolding is getting in the way. This works:

set_option smartUnfolding false
example :
    g =
    -- output of #print above
    (fun x ↦
      @Nat.brecOn (fun x ↦ Nat) x fun x f ↦
        g.match_1 (fun x ↦ @Nat.below (fun x ↦ Nat) x → Nat) x (fun a x ↦ @OfNat.ofNat Nat 0 (instOfNatNat 0))
          (fun n x ↦ x.1) f) :=
  rfl

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Oh, I thought if I write := Eq.refl _ that would get sent straight to the C++ kernel rather than the user-space typechecker. smartUnfolding does not affect the C++ kernel, right?

[Kyle Miller]

That still gets checked by the elaborator first. To skip, that, you'd have to write some term elaborator that doesn't do any checking.

[Kyle Miller]

Here's skipping the elaborator's type checking:

open Lean Meta
elab "rfl!" : term <= expectedType => do
  let some (_, lhs, _) := (← instantiateMVars expectedType).eq? | throwError "not eq"
  let pf ← Lean.Meta.mkEqRefl lhs
  mkExpectedTypeHint pf expectedType

example :
    g =
    (fun x ↦
      @Nat.brecOn (fun x ↦ Nat) x fun x f ↦
        g.match_1 (fun x ↦ @Nat.below (fun x ↦ Nat) x → Nat) x (fun a x ↦ @OfNat.ofNat Nat 0 (instOfNatNat 0))
          (fun n x ↦ x.1) f) :=
  rfl!

[Kyle Miller]

Apparently there's a rfl' tactic for doing rfl with smart unfolding turned off and allowing everything to be reduced

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Thanks! I know that cases where the elaborator-typechecker accepts something that the kernel rejects are considered bugs. Is the converse also?

[Sebastian Ullrich]

No, this is as intended