Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: tactic.induction does not keep case names


view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip 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,

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip Simon Hudon (Jan 05 2021 at 19:33):

Why do you need `[ ... ]?

view this post on Zulip 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.

view this post on Zulip 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