Zulip Chat Archive

Stream: new members

Topic: use in tactic


view this post on Zulip Angela Li (Dec 31 2020 at 05:17):

Hello! I'm trying to make Fifteen. Here is hopefully a MWE leanproject get SnobbyDragon/leanfifteen && code leanfifteen (https://github.com/SnobbyDragon/leanfifteen)

In the fifteentactics.lean file, my slide_tile tactic is failing when I try to use the use tactic. I think it's parallel to this problem:

import tactic

meta def solve (n : ) : tactic unit :=
do `[use n] <|> tactic.fail ":("

example :  n : , n + 1 = 2 :=
begin
  solve 1,
end

This fails but works if I do `[use 1]. Is there a way to fix this?
Thanks!

view this post on Zulip Mario Carneiro (Dec 31 2020 at 05:24):

what is Fifteen?

view this post on Zulip Mario Carneiro (Dec 31 2020 at 05:25):

oh this is the 4x4 sliding puzzle?

view this post on Zulip Angela Li (Dec 31 2020 at 05:25):

yeet

view this post on Zulip Johan Commelin (Dec 31 2020 at 05:25):

I guess so

view this post on Zulip Mario Carneiro (Dec 31 2020 at 05:26):

You are passing the literal n to the use tactic there

view this post on Zulip Angela Li (Dec 31 2020 at 05:28):

uhhh I think I don't know what that means

view this post on Zulip Mario Carneiro (Dec 31 2020 at 05:29):

import tactic

namespace tactic
namespace interactive
setup_tactic_parser
meta def solve (n : parse texpr) : tactic unit :=
do use [n] <|> tactic.fail ":("
end interactive
end tactic

example :  n : , n + 1 = 2 :=
begin
  solve 1,
end

view this post on Zulip Mario Carneiro (Dec 31 2020 at 05:30):

the previous version was doing basically solve 1 = use n and it would complain that n doesn't exist at the point of use

view this post on Zulip Mario Carneiro (Dec 31 2020 at 05:30):

and the n : nat was unused

view this post on Zulip Angela Li (Dec 31 2020 at 05:30):

Ohhhh okay that makes sense. Ahhhh parsing I haven't done that yet. time to learn something new. thanks!

view this post on Zulip Mario Carneiro (Dec 31 2020 at 05:31):

alternatively, without the fancy parser, closer to your original version:

import tactic

meta def solve (n : ) : tactic unit :=
do tactic.interactive.use [pexpr.of_expr (reflect n)] <|> tactic.fail ":("

example :  n : , n + 1 = 2 :=
begin
  solve 1,
end

view this post on Zulip Mario Carneiro (Dec 31 2020 at 05:33):

we have to turn n : nat back into a pexpr because that's what use takes as input

view this post on Zulip Angela Li (Dec 31 2020 at 05:33):

Okay thanks! I will try this on tiles now :)

view this post on Zulip Mario Carneiro (Dec 31 2020 at 05:34):

remember that tactics deal in exprs, not the actual types that you see at the user level. This allows them to do some things that would otherwise be impossible, but requires you to get your head around all the parsing and quoting and antiquoting stuff


Last updated: May 14 2021 at 21:11 UTC