tactic.induction does not keep case names

Stream: metaprogramming / tactics

[Henning Dieterichs]

I'm very new to tactic programming. I want to apply induction, however, when I use tactic.induction inside my tactic, it loses the goal names:

import tactic
import data.finset

inductive Tree (α: Type)
| leaf (a: α): Tree
| branch (tr1 tr2: Tree) : Tree

variables { α: Type } [decidable_eq α]

def Tree.leaves_list: Tree α → list α
| (Tree.leaf a) := { a }
| (Tree.branch tr1 tr2) := tr1.leaves_list ++ tr2.leaves_list

def Tree.leaves (a: Tree α): finset α := a.leaves_list.to_finset

def Tree.disjoint : Tree α → Prop
| (Tree.leaf leaf) := true
| (Tree.branch tr1 tr2) := tr1.disjoint ∧ tr2.disjoint ∧ disjoint tr1.leaves tr2.leaves


open tactic expr

namespace tactic
namespace interactive
setup_tactic_parser

meta def disjoint_induction (n: parse parser.pexpr) : tactic unit :=
do
    e ← to_expr n,
    tactic.induction e,
    skip

end interactive
end tactic

lemma Tree.leaves_list.nodup { t: Tree α } (tree_disjoint: t.disjoint):
    t.leaves_list.nodup :=
begin
  disjoint_induction t,
end

This is the goal:

2 goals
α : Type,
_inst_1 : decidable_eq α,
t : α,
tree_disjoint : (Tree.leaf t).disjoint
⊢ (Tree.leaf t).leaves_list.nodup

α : Type,
_inst_1 : decidable_eq α,
t_tr1 t_tr2 : Tree α,
t_ih_tr1 : t_tr1.disjoint → t_tr1.leaves_list.nodup,
t_ih_tr2 : t_tr2.disjoint → t_tr2.leaves_list.nodup,
tree_disjoint : (t_tr1.branch t_tr2).disjoint
⊢ (t_tr1.branch t_tr2).leaves_list.nodup

This is what I would like to get:

2 goals
case Tree.leaf
α : Type,
_inst_1 : decidable_eq α,
t : α,
tree_disjoint : (Tree.leaf t).disjoint
⊢ (Tree.leaf t).leaves_list.nodup

case Tree.branch
α : Type,
_inst_1 : decidable_eq α,
t_tr1 t_tr2 : Tree α,
t_ih_tr1 : t_tr1.disjoint → t_tr1.leaves_list.nodup,
t_ih_tr2 : t_tr2.disjoint → t_tr2.leaves_list.nodup,
tree_disjoint : (t_tr1.branch t_tr2).disjoint
⊢ (t_tr1.branch t_tr2).leaves_list.nodup

What do I do wrong?

[Jannis Limperg]

The goal names are called 'case tags' and they are set by tactic.interactive.induction, which wraps tactic.induction. Look at the private function set_cases_tags in init/meta/tactic/interactive.lean (above the definition of tactic.interactive.induction).

[Henning Dieterichs]

Thanks, that hint helped me! I'm just calling interactive.induction now. Now I want to preprocess some cases. However, if I do this with '[all_goals { ... }] I lose all the tags again...

meta def ant_disjoint_induction (hp : parse cases_arg_p) (h : parse (tk "have" *> ident)) (rec_name : parse using_ident) (ids : parse with_ident_list)
  (revert : parse $ (tk "generalizing" *> ident*)?) : tactic unit :=
do
    induction hp rec_name ids revert,
    `[
        all_goals {
            unfold Tree.disjoint at tree_disjoint,
        }
    ],
    skip,

[Simon Hudon]

all_goals is not what is dismissing the tags, unfold is. You can wrap it in propagate_tags

[Henning Dieterichs]

~ohh awesome! But how can I wrap it within '[ ... ]?~
This does it:

do
    induction hp rec_name ids revert,
    propagate_tags `[
        all_goals {
            unfold Tree.disjoint at tree_disjoint,
        }
    ],
    skip

thank you!

[Simon Hudon]

Why do you need `[ ... ]?

[Henning Dieterichs]

I don't know much about tactics programming yet. ` [ ...] seemed to be the easiest way to transform a repetitive pattern into a reusable tactic.

[Henning Dieterichs]

But

    all_goals $ propagate_tags `[
        unfold Tree.disjoint at tree_disjoint
    ],

finally does it.