apply_rules with discharger

Stream: mathlib4

[Heather Macbeth]

@Scott Morrison In your streamlining of backtracking in solve_by_elim, is there a new mechanism for non-backtracking with a discharger? Here is how I used to write this -- should it be different now?

import Mathlib.Tactic.Positivity
import Mathlib.Tactic.SolveByElim

open Lean Mathlib

def PositivityDischarge (g : MVarId) : MetaM (Option (List MVarId)) :=
do Meta.Positivity.positivity g; pure (some []) <|> pure none

-- works
example (x : ℤ) : 0 ≤ x ^ 2 := by
  solve_by_elim (config := { discharge := PositivityDischarge })

-- fails
example (x : ℤ) : 0 ≤ x ^ 2 := by
  solve_by_elim (config := { discharge := PositivityDischarge, backtracking := false })

-- fails
example (x : ℤ) : 0 ≤ x ^ 2 := by
  apply_rules (config := { discharge := PositivityDischarge })

[Notification Bot]

This topic was moved here from #lean4 > apply_rules with discharger by Heather Macbeth.

[Heather Macbeth]

@Scott Morrison Shall I open an issue for this? No hurry, just wanted to check before filing that this wasn't a misunderstanding.

[Scott Morrison]

Ah, sorry, forgot about this one. I think I have broken your use case, unfortunately, and will need to change some things to make this possible again.

[Scott Morrison]

I've not been contributing much to the #queue4 the last few days, and was hoping to do less metaprogramming today. :-) What are your time constraints for a fix?

[Heather Macbeth]

None in particular, I plan to keep my course on my current (pre- !4#3480) mathlib4 commit for the rest of the semester (which is nearly done).

[Heather Macbeth]

I'll open an issue and it can be fixed at leisure.

[Heather Macbeth]

!4#3844