zify! tactic

[BoltonBailey]

The zify tactic is considered the default way to deal with goals that use tsub natural subtraction. One of the more tedious aspects of using this tactic is manually inputting all of the inequalities that allow zify to determine if a - b cast to ints should be (a : Z) - (b : Z) or zero. Very often the answer is that it is always the former.

I would like a zify! tactic that automates some of this away. I could see two ways:

1. Assume all the subtractions are not truncated for the purposes of the cast, and then spinning these off as additional goals.
2. Recursively splitting into cases for each subgoal, and then letting the user deal with all the subcases (perhaps applying linarith or ring to each subcase to catch the trivial ones).

[timotree3]

Here is an example proof that could be produced by option 2 above. In principle this approach generates 2^n cases (where n = # tsubs), but in this example, using the heuristic of starting with the nested substraction m - n resulted in only 6 cases.

import Mathlib

example (m n k : ℕ) : (m - n) - k = m - (n + k) := by
  -- zify!
  -- . linarith
  -- . linarith
  -- . linarith
  -- . ring
  cases Nat.lt_or_ge m n with
  | inl h1 =>
    simp only [zero_le, tsub_eq_zero_of_le, h1.le]
    cases Nat.lt_or_ge m (n + k) with
    | inl h2 =>
      simp only [zero_le, tsub_eq_zero_of_le, h2.le]
      -- case solved by simp
    | inr h2 =>
      zify [h2]
      -- all tsubs gone. hand over to user
      linarith
  | inr h1 =>
    cases Nat.lt_or_ge m (n + k) with
    | inl h2 =>
      simp only [zero_le, tsub_eq_zero_of_le, h2.le]
      cases Nat.lt_or_ge (m - n) k with
      | inl h3 =>
        simp only [zero_le, tsub_eq_zero_of_le, h3.le]
        -- case solved by simp
      | inr h3 =>
        zify [h1, h3]
        zify [h1] at h3 -- note: removing tsubs in hypotheses as well
        -- all tsubs gone
        linarith
    | inr h2 =>
      cases Nat.lt_or_ge (m - n) k with
      | inl h3 =>
        simp only [zero_le, tsub_eq_zero_of_le, h3.le]
        zify [h1, h2]
        zify [h1] at h3
        -- all tsubs gone
        linarith
      | inr h3 =>
        zify [h1, h2, h3]
        zify [h1] at h3
        -- all tsubs gone
        ring