isDefEq thing I dont understand

Stream: lean4

[Henrik Böving]

Someone gave me the following code:

import Lean
open Lean Elab Meta
elab "#isDefEq " t₁:term "===" t₂:term : command => do
  Command.liftTermElabM do
    let e₁ <- Lean.Elab.Term.elabTerm t₁ none
    let e₂ <- Lean.Elab.Term.elabTerm t₂ none
    let isEq <- Lean.Meta.isDefEq e₁ e₂
    logInfo s!"{isEq}"

set_option trace.Meta.isDefEq true in
#isDefEq 0 + 0 === 0

and to my surprise it prints false? However when I run it like this:

import Lean
open Lean Elab Meta
elab "#isDefEq " t₁:term "===" t₂:term : command => do
  Command.liftTermElabM do
    let e₁ <- Lean.Elab.Term.elabTerm t₁ none
    let e₂ <- Lean.Elab.Term.elabTerm t₂ none
    let isEq <- Lean.Meta.isDefEq e₁ e₂
    logInfo s!"{isEq}"

set_option trace.Meta.isDefEq true in
#isDefEq 0 + (0 : Nat) === (0 : Nat)

I get true? Why is the Nat annotation relevant here? In my understanding it should pick the OfNat Nat default instance and just know that it is natural numbers getting thrown around here and the behavior should not change if I add these annotations? So what am I misunderstanding?

[Gabriel Ebner]

I think you're missing a synthesizeSyntheticMVarsUsingDefault here.

[Gabriel Ebner]

In the first example, Lean hasn't decided yet that 0 is a natural number.

[Gabriel Ebner]

It could be a type with weird ops where 0 + 0 = 1 (and 0 ≠ 1).

[Kyle Miller]

open Lean Elab Meta
elab "#isDefEq " t₁:term "===" t₂:term : command => do
  Command.liftTermElabM do
    let e₁ <- Lean.Elab.Term.elabTerm t₁ none
    let e₂ <- Lean.Elab.Term.elabTerm t₂ none
    Term.synthesizeSyntheticMVarsUsingDefault
    let isEq <- Lean.Meta.isDefEq e₁ e₂
    logInfo s!"{isEq}"

#isDefEq 0 + 0 === 0
-- true
#isDefEq 1 === 1 + 0
-- true