Zulip Chat Archive

Stream: new members

Topic: use in tactic

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!

Mario Carneiro (Dec 31 2020 at 05:24):

what is Fifteen?

Mario Carneiro (Dec 31 2020 at 05:25):

oh this is the 4x4 sliding puzzle?

Angela Li (Dec 31 2020 at 05:25):

yeet

Johan Commelin (Dec 31 2020 at 05:25):

I guess so

Mario Carneiro (Dec 31 2020 at 05:26):

You are passing the literal n to the use tactic there

Angela Li (Dec 31 2020 at 05:28):

uhhh I think I don't know what that means

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

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

Mario Carneiro (Dec 31 2020 at 05:30):

and the n : nat was unused

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!

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

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

Angela Li (Dec 31 2020 at 05:33):

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

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: Dec 20 2023 at 11:08 UTC