positivity discharger

Stream: metaprogramming / tactics

[Casavaca]

set_option trace.Tactic.positivity true in
example {x : ℝ} (h1 : 0 < x) (h2 : x ≤ 4) : (4 - x) / x ≥ 0 := by
  positivity

[Tactic.positivity] trying to prove positivity of (4 - x) / x
[Tactic.positivity] trying to prove positivity of 4 - x
[Tactic.positivity] 4 - x => none
[Tactic.positivity] (4 - x) / x => none

How can I do something like "run positivity but try linarith when you can't make it"?

[Sam Ezeh]

Are you looking for the first combinator?

set_option trace.Tactic.positivity true in
example {x : ℝ} (h1 : 0 < x) (h2 : x ≤ 4) : (4 - x) / x ≥ 0 := by
  first | positivity | linarith

[Casavaca]

No. you totally missed the point.

[Casavaca]

Wish list: add option to posivitity, so that something like positivity (??? := linarith) is possible?

[Yaël Dillies]

This is not currently possible

[Yaël Dillies]

Do you have more complicated statements than this that you would like to solve with a discharger?

[Yaël Dillies]

If not, there is thinking happening behind the scenes between @Geoffrey Irving and I to make your examples work out of the box

[Yaël Dillies]

cc @Casavaca

[Casavaca]

Not necessarily. I remembered that in my case, it has more terms, but can be solved by linarith only [h] where h is in the context. Anyway, even if we can make positivity a little bit smarter, it would help.