## Stream: new members

### Topic: unfold in own tactic

#### Angela Li (Dec 28 2020 at 15:57):

Hi everyone. I'm trying to write my own tactic and I'd like it to unfold a goal at some point. How would I go about using unfold in my tactic? Would I have to do some parsing? Thanks and sorry this is vague

#### Johan Commelin (Dec 28 2020 at 16:18):

Can you share some of the code that you have already written?

#### Johan Commelin (Dec 28 2020 at 16:18):

(I'm not a tactic writer, but I'm sure that sharing a bit of code will make it easier for others to help you.)

#### Angela Li (Dec 28 2020 at 16:31):

meta def fmove (s d : tower) : tactic unit :=
do { (can_get_to' %%t₁ %%t₂) ← tactic.target,
tactic.apply (@fmove' %%t₁ %%t₂ %%(reflect s) %%(reflect d)),
tactic.applyc and.intro,
-- need to check if valid, then simplify move
[vm, cgt] ← get_goals,
tactic.interactive.unfold vm,
tactic.skip }
<|> tactic.trace "failed to move :("


tactic.interactive.unfold vm This part is definitely wrong because it's complaining. I guess I'm just not sure what to pass in...

#### Angela Li (Dec 28 2020 at 16:32):

I think the docs wanted a parse ident* type but I'm not sure how to get that.

#### Patrick Massot (Dec 28 2020 at 16:34):

Angela, we need a #mwe.

#### Rob Lewis (Dec 28 2020 at 16:35):

I'm not sure what you mean by "unfold a goal." What would you write if you were using the unfold tactic by hand? You can unfold certain definitions in the goal but there's no concept of unfolding an entire goal.

#### Shing Tak Lam (Dec 28 2020 at 16:36):

I think I remember what this is from, but posting mwe with imports, the current tactic code that you have, as well as an example which you expect the tactic to make progress would be helpful.

#### Angela Li (Dec 28 2020 at 16:37):

Oh wait I would write unfold valid_move by hand

#### Rob Lewis (Dec 28 2020 at 16:43):

Where valid_move is some declaration you've defined?

#### Angela Li (Dec 28 2020 at 16:43):

Hmm wait I think I can post an smaller example...

def cat := 1 + 1

meta def unfold_cat : tactic unit :=
do {
sorry
}

example : cat = 2 := sorry


I guess like if I wanted to just unfold cat. I think refl works for this example but not for the stuff I was doing. I kinda just have no idea what to put in unfold_cat

#### Rob Lewis (Dec 28 2020 at 16:43):

Then you probably want to do dunfold_target [valid_move].

#### Rob Lewis (Dec 28 2020 at 16:44):

In that example, dunfold_target [cat]

#### Angela Li (Dec 28 2020 at 16:44):

ohh wait then what is tactic.interactive.unfold

thank you!

#### Rob Lewis (Dec 28 2020 at 16:46):

It's an interactive tactic. It's doing something similar but it's for use inside begin...end blocks.

#### Rob Lewis (Dec 28 2020 at 16:46):

The details about interactive/non-interactive mode are covered in the tactic writing tutorials, have you had a look at those?

#### Angela Li (Dec 28 2020 at 16:48):

Yes I looked at those. I got super lost at parsing though... Think I will look at them again. Thanks!

#### Patrick Massot (Dec 28 2020 at 16:58):

Are you doing this as a tactic writing exercise or do you really want this tactic to help you? If this is not a tactic writing exercise then you almost certainly have a #xy issue. You should tell more about the context.

#### Angela Li (Dec 28 2020 at 17:40):

I do want to use this hopefully... I think it's working okay right now. I just want to use it as a macro to move a disk from one tower to another in hanoi. There was a lot of list simplifying / clean up things I wanted to put in one tactic. I'm hoping to somehow connect this to a widget now.

#### Patrick Massot (Dec 28 2020 at 17:41):

I'm pretty sure you would learn a lot by posting more code (or a link to a repository), but it's up to you.

#### Angela Li (Dec 28 2020 at 17:52):

I think so too. Thanks. https://github.com/SnobbyDragon/leanhanoi This is really quite a mess. I have not started making the widget yet so... but I will be trying to figure that out

#### Patrick Massot (Dec 28 2020 at 18:02):

For the record, let me first point out that, while the basic first step is always to ask specific questions about well designed #mwe, sharing a well-formed Lean project is as simple as telling people "You can type leanproject get SnobbyDragon/leanhanoi && code leanhanoi. This immediately (well, after maybe 20 seconds depending on bandwidth) gives everyone access to you work, without compiling anything.

#### Patrick Massot (Dec 28 2020 at 18:03):

Now, testGames.lean doesn't appear to be working. Do I guess correctly that the import lines should be:

import hanoi
import hanoitactics


#### Angela Li (Dec 28 2020 at 18:04):

yes that is correct i forgot to change that

#### Eric Wieser (Dec 28 2020 at 18:06):

@Edward Ayers demoed building an interactive widget for the tower of hanoi in the Xena Discord the a week or two ago, in case you're interested.

#### Eric Wieser (Dec 28 2020 at 18:06):

(unrelated to your question, but perhaps still of interest)

#### Angela Li (Dec 28 2020 at 18:08):

Oh yes that would be super cool! I think I asked on Discord but I think people are here more :sweat_smile:

#### Patrick Massot (Dec 28 2020 at 18:18):

You can simplify your tactic file a bit to:

import hanoi

open hanoi

namespace tactic.interactive
setup_tactic_parser
open tactic

-- moves curr tower to a new position if valid, otherwise fails
meta def move_disk (s d : tower) : tactic unit :=
do { (can_get_to' %%t₁ %%t₂) ← tactic.target,
tactic.apply (@fmove' %%t₁ %%t₂ %%(reflect s) %%(reflect d)),
tactic.applyc and.intro,
[simp only [valid_move, list.range', false_or, eq_self_iff_true, not_true, ne.def, not_false_iff, and_self, false_and]],
[dsimp [move]]} <|> tactic.trace "failed to move disk :("

meta def startgame : tactic unit :=
do { (game' %%d) ← tactic.target,
dunfold_target [game']
} <|> tactic.trace "not a game"

-- if two towers are the same then we win
meta def endgame : tactic unit :=
tactic.applyc hanoi.can_get_to'.can_get_to_self'

end tactic.interactive


#### Patrick Massot (Dec 28 2020 at 18:18):

Note that your tactic.trace error messages should really be tactic.fail

#### Angela Li (Dec 28 2020 at 18:29):

Ohh okay I see. Thanks!

Last updated: May 09 2021 at 18:17 UTC