Instance override phenomenon

Stream: lean4

[Yves Jäckle]

So we played around with instances a bit and found:

instance (priority := high)  : Add Nat := ⟨fun x y => Nat.sub x y⟩

--local instance (priority := high) : HAdd Nat Nat Nat := ⟨fun x y => Nat.sub x y⟩

#eval 2 + 3

set_option pp.all true in
theorem testit : True := by
  -- let myAdd : Add Nat := ⟨fun x y => x - y⟩
  have : 2 + 3 = 5 := by
    dsimp
  exact True.intro

The eval returns 0, but in the have below, dsimp reduces addition with actual Nat.add it seems, despite using the above instance for add, according to pp.all. The theorem raises a bizarre error message. This is reproducible on live.lean. Is this an issue ?

[Eric Wieser]

This is arguably a bug in docs#Nat.reduceAdd (dsimp only [Nat.reduceAdd] reproduces it)

[Eric Wieser]

The argument would be that it should be performing defeq matching on the instances, rather than just assuming they are the builtin ones

[Markus Himmel]

This is lean4#7444 / lean4#7557.

[Bhavik Mehta]

I'd argue it's slightly different from those issues, which are specifically about a mismatch in the decidability proof. I'd go further and say that this is actually intended behaviour, see for instance the comment here https://github.com/leanprover/lean4/blob/045d07d2349b9989278991fbcd79a6430032930d/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean#L47, which says exactly that if overriding the instances for arithmetic operators as you've done will cause problems.
(Whether this intended behaviour is the correct one is a different question though; I agree it can be confusing behaviour!)

[Yves Jäckle]

Ok cool :+1: Of course, the above has no real use case, it occurred when I tried to explain to someone how instances work.

[Eric Wieser]

I think this intended behavior might be at odds with the intended behavior of "tactics should fail rather than produce an illegal proof"