Another simp mystery

Stream: lean4

[Patrick Massot]

Since Leo is currently working on the simplifier, I'm resuming my work to detect differences between Lean 3 and Lean 4 simp. I think the following is not directly something I've already discussed here. Compare Lean 3 code:

import analysis.special_functions.exp
import analysis.special_functions.log.basic

open real

example (x : ℕ) (hx : (0 : ℝ) < x) : exp (log x) = x := by
  simp [exp_log, hx]

and Lean 4 version

import Mathlib.Analysis.SpecialFunctions.Exp
import Mathlib.Analysis.SpecialFunctions.Log.Basic

open Real

example (x : ℕ) (hx : (0 : ℝ) < x) : exp (log x) = x := by
  simp [exp_log, hx] -- fails
  -- simp [exp_log hx] would work

[Patrick Massot]

Of course in the example the version that works is one character shorter than the failing one, but this isn't always true.

[Patrick Massot]

I tried making an mathlib-free example but failed to do it quickly and ran out of time for now.

[Kevin Buzzard]

The Lean 3 hx is presumably a statement about nats, so the examples aren't exactly the same?

[Patrick Massot]

Sorry, that was a copy-paste issue on Zulip.

[Patrick Massot]

The two examples are absolutely identical except it works in Lean 3 but not in Lean 4.

[Patrick Massot]

Minimizing is tricky. Consider the following:

import Mathlib.Analysis.SpecialFunctions.Exp
import Mathlib.Analysis.SpecialFunctions.Log.Basic

open Real

set_option trace.Meta.Tactic.simp true

example (x : ℕ) (hx : 0 < Nat.cast x) : exp (log $ Nat.cast x) = Nat.cast x := by
  simp [exp_log, hx] --fails

/-- Fake real numbers. -/
axiom R : Type
@[instance] axiom Rcast : NatCast R
axiom Rexp : R → R
axiom Rlog : R → R
@[instance] axiom Rlt : LT R
@[instance] axiom Rzero : Zero R

axiom Rexp_Rlog {x : R} (hx : 0 < x) : Rexp (Rlog x) = x

example (x : ℕ) (hx : (0 : R) < Nat.cast x) : Rexp (Rlog x) = x := by
  simp [Rexp_Rlog, hx] --works!

[Patrick Massot]

and using @[instance] axiom Rzero : OfNat R 0 instead of @[instance] axiom Rzero : Zero R makes not difference.