solve_by_elim discharge parameter

Stream: new members

[Luigi Massacci]

Hello! Modulo that I might have misunderstood what it's for, I would like to pass nlinarith as a discharger for solve_by_elim, but if I try this:

import Mathlib

example : 1 ≤ 5 := by
  solve_by_elim (config := {discharge := nlinarith})

I get:

  nlinarith
has type
  Lean.ParserDescr : Type
but is expected to have type
  Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId)) : Type

which is beyond my current comprehension I'm afraid. What can I do?

[Shreyas Srinivas]

you probably need to find the MetaM function that nlinarith uses and you probably need to pass the goal that remains as a metavariable

[Shreyas Srinivas]

what you are instead passing is this

[Shreyas Srinivas]

For example this works: (although it uses linarith the example can be extended):

import Mathlib

def use_linarith (goal : Lean.MVarId) : Lean.MetaM (Option (List Lean.MVarId)) := do
  Linarith.linarith false [] {} goal
  return none

example : 1 ≤ 5 := by
  solve_by_elim (config := {discharge := use_linarith})

[Luigi Massacci]

thank you!

[Shreyas Srinivas]

fwiw, I think solve_by_elim solves this goal without nlinarith. So I am not really sure that example is a good test.

[Shreyas Srinivas]

See:

import Mathlib
example : 1 ≤ 5 := by
  show_term solve_by_elim

[Luigi Massacci]

oh yeah, I mean the example could have been just example : True, it was just to put something in the goal, since it was clearly unrelated to the error I was getting anyway

[Shreyas Srinivas]

To be honest I find this way of doing things suboptimal. Ideally the discharger should accept a tactic name, insert the metavariable as a goal and automatically try to solve it. Alternatively there should be a top level MetaM function for each tactic whose name is identical to the tactic name so that the end user doesn't have to hunt down the correct function. For example, I read the nlinarith code and found Linarith.linarith that way. But I didn't find any function called nlinarith

[Shreyas Srinivas]

And for all I know, there is a shortcut to invoke the tactic and have it find the goals to discharge automatically.

[Shreyas Srinivas]

Luigi Massacci said:

oh yeah, I mean the example could have been just example : True, it was just to put something in the goal, since it was clearly unrelated to the error I was getting anyway

Got a chance to put this to a small test. It doesn't quite do what one would expect. I think the following macro would work :

macro "solve_by_elim_nlin" : tactic => `(tactic|(
  try solve_by_elim <;> nlinarith
))

[Luigi Massacci]

Isn’t solve_by_elim a finishing tactic? Does it work to do <;> with those?

[Shreyas Srinivas]

yeah but try makes is non-finishing in some sense

[Shreyas Srinivas]

It backtracks

[Shreyas Srinivas]

What I meant was it works better in some cases than setting linarith as a discharger because in the function I wrote above, to be useful you need to fill in the hypotheses you want linarith to use