unfold in own tactic

Stream: new members

[Angela Li]

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]

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

[Johan Commelin]

(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]

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]

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

[Patrick Massot]

Angela, we need a #mwe.

[Rob Lewis]

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]

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]

Oh wait I would write unfold valid_move by hand

[Rob Lewis]

Where valid_move is some declaration you've defined?

[Angela Li]

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]

Then you probably want to do dunfold_target [`valid_move].

[Rob Lewis]

In that example, dunfold_target [`cat]

[Angela Li]

ohh wait then what is tactic.interactive.unfold

[Angela Li]

thank you!

[Rob Lewis]

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

[Rob Lewis]

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

[Angela Li]

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

[Patrick Massot]

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]

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]

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]

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]

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]

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]

yes that is correct i forgot to change that

[Eric Wieser]

@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]

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

[Angela Li]

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

[Patrick Massot]

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]

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

[Angela Li]

Ohh okay I see. Thanks!