zify!

Stream: mathlib4

[Patrick Massot]

The current zify tactic is nice, but it is not good enough, as illustrated from the following code extracted from Terence Tao's work:

import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Zify

example {n k : ℕ} (h₁ : 8 ≤ n) (h₂ : 2 * k > n) (h₃: k + 1 < n) :
    n - (n - (k + 1)) = k + 1 := by
  have f₁ : k + 1 ≤ n := by linarith
  have f₂ : n - (k + 1) ≤ n := by zify [f₁]; linarith
  zify [f₁, f₂] at *
  linarith

where the full proof should be zify! ; linarith. The algorithm to write the above proof is pretty simple: look for every Nat subtraction a - b in the target expressions (here the goal and all assumptions), create a list of goal a \le b, putting the most deeply nested subtractions first. Try to prove these goals using zify [every nat le around] ; linarith (we could allow other dischargers instead of linarith). Discard those new goals that couldn't be proved, run the original zify call with all successfully proven inequalities (on top of any existing proof terms). Does anyone feels like implementing this?