linarith with discharger

Stream: mathlib4

[Heather Macbeth]

I'm hoping to get some help using linarith with a custom discharger, cc @Scott Morrison @Mario Carneiro. Here is an example in which linarith works, and a custom tactic works for the goal which (AFAICT) the discharger would be run on, but linarith does not work with that discharger.

import Mathlib.Tactic.Abel
import Mathlib.Tactic.Linarith

open Lean Elab Tactic

/- This works, and according to `set_option trace.linarith true`, the contradiction found is:
[linarith] The expression
      OfNat.ofNat 4 * -1 + -(t - (4 - s * t)) + (t + s * t)
    should be both 0 and negative
-/
example {s t : ℚ} (h1 : t = 4 - s * t) (h2 : t + s * t ≤ 0) : False := by linarith

def foo : TacticM Unit := do
  evalTactic (←`(tactic| (abel_nf ; push_cast [zsmul_eq_mul] ; norm_num1)))

elab "foo" : tactic => foo

-- the ad hoc tactic `foo` proves the appropriate expression is 0
example (s t : ℚ) : 4 * -1 + (t + s * t) + -(t - (4 - s * t)) = 0 := by foo

-- but `linarith` fails with `foo` set as the discharger
example {s t : ℚ} (h1 : t = 4 - s * t) (h2 : t + s * t ≤ 0) : False := by
  linarith (config := { discharger := foo})

[Mario Carneiro]

@Heather Macbeth The OfNat.ofNat 4 in the trace message seems to be a bad sign, that is a double ofNat expression which should not happen. This is coupled with the fact that foo does not end in ; done and it does not close all goals, which apparently causes linarith to drop those goals.

[Mario Carneiro]

if you put a ; trace_state at the end of foo you will see there is a remaining subgoal after norm_num1:

st: ℚ
h1: t = 4 - s * t
h2: t + s * t ≤ 0
⊢ OfNat.ofNat 4 * -1 + 4 = 0

[Thomas Murrills]

Is something up with norm_num if it’s leaving a goal like that?

[Thomas Murrills]

Or is this about what’s being fed to norm_num?

[Mario Carneiro]

It's not norm_num doing the ofNat here, it is a function in linarith

[Mario Carneiro]

mathlib4#1771

[Heather Macbeth]

Thank you, Mario!