unwanted reduction when checking simp_arith proof objects

[nomeata]

This was originally reported as #7729 on mathlib4 by @digama0, but is actually a lean bug.

When the kernel checks the proof produced by simp_arith it is prone to start evaluating atoms that it shouldn’t and neend’t evaluate.

-- A function that reduced badly, as a canary for kernel reduction
def bad (n : Nat) : Nat :=
  if h : n = 0 then 0 else bad (n / 2)
termination_by n

-- this is fast:

/-- info: time: 11ms -/
#guard_msgs in
#time
theorem bar (n : Nat) : 2 * n = n + n := by simp_arith

-- this is slow:

/-- info: time: 311ms -/
#guard_msgs in #time
theorem foo : 2 * bad 100 = bad 100 + bad 100 := by simp_arith

-- the profiler tells us that the time is spent in kernel reduction

-- these are the proof terms produced:

/-- info: time: 13ms -/
#guard_msgs in
#time
theorem bar' : ∀ (n : Nat), 2 * n = n + n :=
  fun n =>
  of_eq_true
    (Nat.Linear.ExprCnstr.eq_true_of_isValid [n]
      { eq := true, lhs := Nat.Linear.Expr.mulL 2 (Nat.Linear.Expr.var 0),
        rhs := (Nat.Linear.Expr.var 0).add (Nat.Linear.Expr.var 0) }
      (Eq.refl true))

/-- info: time: 335ms -/
#guard_msgs in
#time
theorem foo' : 2 * bad 100 = bad 100 + bad 100 :=
  of_eq_true
    (Nat.Linear.ExprCnstr.eq_true_of_isValid [bad 100]
      { eq := true, lhs := Nat.Linear.Expr.mulL 2 (Nat.Linear.Expr.var 0),
        rhs := (Nat.Linear.Expr.var 0).add (Nat.Linear.Expr.var 0) }
      (Eq.refl true))

-- A possible fix could be to abstract the proof over the atoms, and use an `id`, 
-- and fingers crossed that the kernel checks the proof in the right way:

/-- info: time: 15ms -/
#guard_msgs in
#time
theorem foo'fix : 2 * bad 100 = bad 100 + bad 100 :=
  @id (∀ (n : Nat), 2 * n = n + n)
    (fun x1 => of_eq_true
    (Nat.Linear.ExprCnstr.eq_true_of_isValid [x1]
      { eq := true, lhs := Nat.Linear.Expr.mulL 2 (Nat.Linear.Expr.var 0),
        rhs := (Nat.Linear.Expr.var 0).add (Nat.Linear.Expr.var 0) }
      (Eq.refl true))) (bad 100)

-- NB: This does not help.

/-- info: time: 313ms -/
#guard_msgs in
#time
theorem baz : 2 * bad 100 = bad 100 + bad 100 := by
  generalize bad 100 = x
  simp_arith

It’s unclear to me how often that happens in practice. It does not seem to affect omega in the same way, so maybe low priority.

Versions

"4.12.0-rc1"

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.