Zulip Chat Archive

Stream: new members

Topic: unfold in own tactic


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

view this post on Zulip Johan Commelin (Dec 28 2020 at 16:18):

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

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

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

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

view this post on Zulip Patrick Massot (Dec 28 2020 at 16:34):

Angela, we need a #mwe.

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

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

view this post on Zulip Angela Li (Dec 28 2020 at 16:37):

Oh wait I would write unfold valid_move by hand

view this post on Zulip Rob Lewis (Dec 28 2020 at 16:43):

Where valid_move is some declaration you've defined?

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

view this post on Zulip Rob Lewis (Dec 28 2020 at 16:43):

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

view this post on Zulip Rob Lewis (Dec 28 2020 at 16:44):

In that example, dunfold_target [`cat]

view this post on Zulip Angela Li (Dec 28 2020 at 16:44):

ohh wait then what is tactic.interactive.unfold

view this post on Zulip Angela Li (Dec 28 2020 at 16:44):

thank you!

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

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

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

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

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

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

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

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

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

view this post on Zulip Angela Li (Dec 28 2020 at 18:04):

yes that is correct i forgot to change that

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

view this post on Zulip Eric Wieser (Dec 28 2020 at 18:06):

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

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

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

view this post on Zulip Patrick Massot (Dec 28 2020 at 18:18):

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

view this post on Zulip Angela Li (Dec 28 2020 at 18:29):

Ohh okay I see. Thanks!


Last updated: May 09 2021 at 18:17 UTC