Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: advice on a tactic for decomposing inequalities


Gihan Marasingha (Sep 18 2022 at 14:56):

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 (Sep 18 2022 at 15:06):

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

Gihan Marasingha (Sep 18 2022 at 16:09):

Thanks!


Last updated: Dec 20 2023 at 11:08 UTC