advice on a tactic for decomposing inequalities

Stream: metaprogramming / tactics

[Gihan Marasingha]

For help in teaching proof by induction on natural numbers with a different base case, I've written a tactic (indeed, my first tactic) for decomposing an inequality n ≤ m for natural numbers n and m into m + 1 cases (these being n = 0, n = 0.succ, n=1.succ, ...). It works but the cases look a bit messy, with hypotheses of the form n = k.succ.

I'd be grateful if someone more experienced could look at my code an indicate if there's a better way to write it.

import tactic

open tactic expr

meta def foo_aux : expr → tactic unit
| h :=
(do
    try_le_zero ← mk_app `nat.eq_zero_of_le_zero [h],
    note h.local_pp_name none try_le_zero,
    clear h,
    skip) <|>
    do
      pf ← mk_app `nat.of_le_succ [h],
      clear h,
      [(_,[y]), _] ← cases pf [h.local_pp_name, h.local_pp_name],
      try (foo_aux y)

namespace tactic.interactive

setup_tactic_parser

meta def foo (h : parse parser.pexpr) : tactic unit :=
do  h ← to_expr h,
    foo_aux h

end tactic.interactive

example (n : ℕ) (ha : n ≤ 2) : true :=
begin
  foo ha,
  all_goals {trivial},
end

[Yaël Dillies]

Do you know about tactic#interval_cases? That should be good inspiration.

[Gihan Marasingha]

Thanks!