# Zulip Chat Archive

## Stream: metaprogramming / tactics

### Topic: tactic.induction does not keep case names

#### Henning Dieterichs (Jan 05 2021 at 15:52):

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 (Jan 05 2021 at 15:59):

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 (Jan 05 2021 at 19:15):

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 (Jan 05 2021 at 19:21):

`all_goals`

is not what is dismissing the tags, `unfold`

is. You can wrap it in `propagate_tags`

#### Henning Dieterichs (Jan 05 2021 at 19:25):

~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 (Jan 05 2021 at 19:33):

Why do you need ` `[ ... ]`

?

#### Henning Dieterichs (Jan 05 2021 at 19:35):

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 (Jan 05 2021 at 19:35):

But

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

finally does it.

Last updated: May 09 2021 at 21:10 UTC