Tactic basics

Stream: lean4

[Marcus Rossel]

I wrote a function that generates an escape path for the mazes in lean4-maze.
Now I would like to write a tactic that automatically proves that a maze is escapable (if possible), but have no idea how to transform my escape path into a sequence of tactics.

For context, a maze looks something like this:

def maze1 := ┌──────┐
             │▓▓▓▓▓▓│
             │▓░░@░▓│
             │▓░░░░▓│
             │▓░░░░▓│
             │▓▓▓▓░▓│
             └──────┘

We can prove that we can escape it, by using the east, west, south and north tactics:

example : can_escape maze1 := by
  east
  south
  west
  ...

My function takes a maze (GameState) and generates a list of Moves that form an escape route (if possible):

inductive Move
  | east | west | north | south

partial def escapePath (g : GameState) : Option (List Move) := ...

I would like to write a tactic that takes a maze, generates the list of required moves and turns those into applications of the corresponding tactics.
I'm guessing the structure would be like this, but I don't know how to fill it:

macro "escape" m:term : tactic => `( ??? )

Where do I start?

[Sebastian Reichelt]

I'm far from an expert, so take this with a grain of salt.

TBH, what you are doing looks a little backwards to me. If escapePath already returns a list of moves, then couldn't you easily change it to return an instance of can_escape directly, eliminating the need to invoke a tactic?

Normally, I would expect the tactic to produce the list of moves. But then you probably don't want to write a macro but an elab, and implement the algorithm as monadic code.

If you really want to write a macro the way you wrote it, what you will need to do (I think) is to essentially run #eval on escapePath applied to m (not sure how to do it, but it's certainly possible) and recursively convert the resulting syntax tree.

[Mac]

Sebastian Reichelt said:

Normally, I would expect the tactic to produce the list of moves. But then you probably don't want to write a macro but an elab, and implement the algorithm as monadic code.

I second this. If you want to have the tactic interactive with current game state you need a elaborate not a macro. Macros are essentially purely syntactic transformations, you cannot retrieve information about the state of the proof from within them.

Sebastian Reichelt said:

If you really want to write a macro the way you wrote it, what you will need to do (I think) is to essentially run #eval on escapePath applied to m (not sure how to do it, but it's certainly possible) and recursively convert the resulting syntax tree.

I don't think this is actually possible with a macro. #eval is a command and I don't think there is way to invoke such a command with the built-in tactics (and thus no way to use it in a tactic macro).

[Marcus Rossel]

I ended up going for the approach below. Note that I've removed the explicit m parameter for the tactic, and instead extract it from the goal state.

syntax (name := escape) "escape" : tactic

open Lean Elab.Tactic in
@[tactic escape] partial def evalEscape : Tactic
  | `(tactic|escape) => do
    match (← getMainTarget) with
    | Expr.app (Expr.const `can_escape ..) m _ =>
      let g ← extractGameState m -- extractGameState : Lean.Expr → Lean.MetaM GameState
      match g.escape_path with
      | none => throwError "Maze is not escapable."
      | some p =>
        for move in p do
          match move with
          | Move.east => -- run the `east` tactic
          | Move.west => -- run the `west` tactic
          | Move.north => -- run the `north` tactic
          | Move.south => -- run the `south` tactic
    | _ => throwError "Cannot solve goal of this type."
  | _ => throwError "Unreachable code has been reached in 'escape' tactic."

Unfortunately I'm still stuck at actually running the tactics that correspond to the moves (in the match-expression).
How would I run a tactic here?

[Marcus Rossel]

Sebastian Reichelt said:

TBH, what you are doing looks a little backwards to me. If escapePath already returns a list of moves, then couldn't you easily change it to return an instance of can_escape directly, eliminating the need to invoke a tactic?
...

This is just a practice example for me to learn some tactic/meta stuff in Lean.
So if the approach is weird, that probably has to do with that.

[Mac]

Marcus Rossel said:

  | _ => throwError "Unreachable code has been reached in 'escape' tactic."

Just FYI, that code is actually not unreachable. That match case just implies that the tactic in question is ill-formed (i.e., someone typo'd in attempt to construct the Syntax of the tactic). Thus, a better message would be, for example, "Ill-formed escape tactic."

[Sebastian Reichelt]

Ah, the way you are using escape_path is a bit different than I thought. It's a bit unusual, but that doesn't make it wrong of course. Basically, you are using object-level code at the meta level as well. In particular, what extractGameState really does is a sort of reflection, converting an object-level expression of type GameState into a meta-level instance of GameState. That way, escape_path actually becomes part of the tactic, which makes some of what I have written above moot.

(This actually creates an interesting ambiguity regarding what "running the tactics that correspond to the moves" actually means, because you now have a choice between running the tactic at the object level (as you normally would) or at the meta level (and then convert the resulting escape path back in the reverse direction of extractGameState). I assume you mean the former.)

I haven't tried running tactics from tactics, but I think the function you are looking for is evalTacticAt. You'd start with mvarId being the result of getMainGoal, and then each invocation of evalTacticAt should give you either 0 or 1 new goals, depending on whether that move escaped the maze. (It's probably easiest to write it as a recursive function rather than a loop; not sure about the implications of either style in Lean.)