has_to_pexpr and has_reflect for a function

Stream: new members

[Angela Li]

Hello! For Fifteen, I'm trying to write a tactic to close the goal when you reach the goal position. Here is the project leanproject get SnobbyDragon/leanfifteen.
My tactic (called finish_game in the file fifteentactics.lean) is supposed to be a macro for the easy_cheesy example in the file play.lean

meta def finish_game : tactic unit :=
do { p ← get_position,
     «have» `H ``(%%p.map = goal_position.map) ``(by dec_trivial), --this line doesn't work
     tactic.skip
} <|> tactic.fail "we are not done !"

example : game easy_cheesy :=
begin
  slide_tile dd, --excluding this line
  have H : (slide dd dc easy_cheesy).map = goal_position.map := by exact dec_trivial,
  have H' : (slide dd dc easy_cheesy) = goal_position := by tauto,
  rw H',
  apply can_slide_to.self goal_position,
end

I'm not too sure how to do have since it's complaining about has_to_pexpr, so I tried reflecting, but it didn't like @[derive has_reflect] for a function. This would fail (in file fifteen.lean):

@[derive [decidable_eq, has_reflect]]
structure position :=
(map : tile → fin 16)
-- (bij : function.bijective map)

Is there a way I can make it has_reflect? Or is there a better way to approach this?
Any insight/feedback is appreciated!
Thanks!

[Mario Carneiro]

what does get_position return? What does the tactic state look like just before finish_game?

[Mario Carneiro]

You probably don't want to be reflecting anything

[Angela Li]

get_position returns tactic position

[Mario Carneiro]

See why do you need that? You should keep the positions out of the tactic, and then you don't need reflect to turn it back into an expr. It should be a tactic expr

[Mario Carneiro]

how is it implemented

[Angela Li]

oh wait that makes more sense.

meta def get_position : tactic position :=
do { `(can_slide_to %%p₁ %%p₂) ← tactic.target,
     p ← (eval_expr position) p₁,
     return p
} <|> get_start_position

I think i was just using it for other things

[Angela Li]

but I'll just not use this in what im trying to do

[Mario Carneiro]

don't do eval_expr

[Mario Carneiro]

just return p1

[Mario Carneiro]

I downloaded your project but you are using begin [fifteen_tactic'] end and it complains that the fifteen_tactic' tactic class doesn't exist, which is true

[Angela Li]

oh wait i forgot to push a file sorry ill do that now

[Angela Li]

okay pushed!

[Mario Carneiro]

yeehaw indeed

[Mario Carneiro]

So without using finish_game, just using the underlying tactics manually, what would a completed game look like?

[Mario Carneiro]

I tried

example : game easy_cheesy :=
begin
  slide_tile dd,
  exact dec_trivial,
end

but that doesn't work

[Angela Li]

example : game easy_cheesy :=
begin
  slide_tile dd,
  have H : (slide dd dc easy_cheesy).map = goal_position.map := by exact dec_trivial,
  have H' : (slide dd dc easy_cheesy) = goal_position := by tauto,
  rw H',
  apply can_slide_to.self goal_position,
end

I think this should end it. I'm not sure why it's so complicated

[Angela Li]

Probably with how I defined the structure position ? It only has a function in it bc I commented out the bijective part since it made things hard

[Mario Carneiro]

it looks like derive decidable_eq is not making a good instance. Try this instead:

@[ext] structure position :=
(map : tile → fin 16)

instance : decidable_eq position :=
λ a b, decidable_of_iff' _ (position.ext_iff _ _)

[Angela Li]

Cool thanks!

[Mario Carneiro]

then you can reduce the original proof to

lemma can_slide_to.of_eq : ∀ {p₁ p₂ : position} (h : p₁ = p₂), can_slide_to p₁ p₂
| p _ rfl := can_slide_to.self p

example : game easy_cheesy :=
begin
  slide_tile dd,
  exact can_slide_to.of_eq dec_trivial,
end

[Mario Carneiro]

And then your tactic reduces to:

meta def finish_game : tactic unit :=
do { applyc ``can_slide_to.of_eq,
     tactic.exact_dec_trivial
} <|> tactic.fail "we are not done !"

example : game easy_cheesy :=
begin
  slide_tile dd,
  finish_game
end

[Angela Li]

Is it better to do that than stuff like `[exact can_slide_to.of_eq dec_trivial]

[Mario Carneiro]

It's more flexible, and a bit faster. The tactic quoting syntax is pretty limited as you saw with that have proof

[Mario Carneiro]

In this case you want as much to be done in a theorem as you can, and then just call the dec_trivial tactic to do the part that depends on the actual goal

[Mario Carneiro]

You can also automatically finish every proof in your custom state with this as a "closer":

  meta instance : interactive.executor fifteen_tactic' :=
  { config_type := unit,
    execute_with := λ n tac, tac >> fifteentactics.finish_game
  }

example : game easy_cheesy :=
begin [fifteen_tactic']
  slide_tile dd,
end

[Angela Li]

Ooo that's cool thanks so much!

[Mario Carneiro]

You probably need some special handling with the widget stuff if you want to show the goal in case of errors

[Angela Li]

True... although I haven't managed to make an error through clicking yet (at least since I disabled clicking on tiles not next to the hole) but I wouldn't count on it :eyes: