Tactic for range analysis over the Naturals

Stream: new members

[Elizaveta Pertseva]

Hello! Is there a tactic that performs range analysis over the naturals? For example is there a tactic that could automatically deduce the following lemma?

lemma bound {x y : ℕ} (hx : x <= 1) (hy : y <= 1) :
  (1 - x) * y + x * (1 - y) ≤ 1 := by

linarith fails. Thank you so much for your help!

[Kenny Lau]

import Mathlib

lemma bound {x y : ℕ} (hx : x ≤ 1) (hy : y ≤ 1) :
    (1 - x) * y + x * (1 - y) ≤ 1 := by
  interval_cases x <;> interval_cases y <;> decide

lemma bound' {x y : ℕ} (hx : x ≤ 1) (hy : y ≤ 1) :
    (1 - x) * y + x * (1 - y) ≤ 1 := by
  revert x; revert y; decide

[Elizaveta Pertseva]

Thank you! interval_cases really helps, but I am likely to have more complex expressions with a lot of variables so I was hoping there was a tactic that did this under the hood.

[Kenny Lau]

if x is not a variable then you would need to generalize it first