Backtracking

Stream: general

[Jason Rute]

Let's say I have a finite list of tactics (with no arguments) that I'd like to try on a state. I'd like to do a breath first search with this list of tactics. Two questions:

1. Is this theoretically possible? Can one "back track" or go to a previously visited state using tactics?
2. Is there any caching or will I have to incur the cost of executing that tactic again every time I go back to a previously explored branch.

(I'm not actually interested in this exact application per say, but I'm trying to understand how flexible tree searching is in Lean tactics.)

[Jason Rute]

Actually, I realize the answer to (1) is true, but the algorithm I have in mind isn't pretty. The top tactic enumerates all the finite partial paths through the tree in BFS order and then repeatedly tries to execute the sub tactics in that order. However, it is algorithms like this which make me ask the second question. Is there anything more efficient?

[Jason Rute]

Maybe after applying a string of tactics, e.g. A, B, A, C if it succeeds one can record the partial term proof so far and store it in a map object. Whenever a path extending that path comes up again, one can just execute the term instead of the tactics, but I don't know if this is entirely possible.

[Jason Rute]

Another possibility is that it is possible to save all the expressions in a goal stack and manually set that goal stack. (This might only partially work, since I assume changing the goals isn't sound, so if a tactic does it, the final proof won't work.)

[Scott Morrison]

Sure, it's no problem.

[Scott Morrison]

Backtracking is free.

[Jason Rute]

How does one do it?

[Scott Morrison]

You can use get_state and set_state, and pass the tactic_state terms around however you please.

[Scott Morrison]

I'm not sure from what you say if you already know about s <|> t

[Scott Morrison]

which runs s, and if that fails restores the previous state, then runs t.

[Jason Rute]

I do know about s <|> t. I don't just want to backtrack on fails.

[Scott Morrison]

try_core t, which returns an none if t fails, and some a if t returns a

[Scott Morrison]

and get_state / set_state

[Scott Morrison]

should allow you to do anything you like

[Scott Morrison]

without any re-running tactics.

[Scott Morrison]

We have lots of "time-travelling" tactics in tactic.core.

[Jason Rute]

Follow up question: Can you use get_state's output as a key in a rbmap or rbset?

[Mario Carneiro]

no

[Scott Morrison]

Is "no" addressed to the last comment? If so, I agree, tactic.core doesn't have much of this.

[Mario Carneiro]

I think there is a tactic for checking if the goal has changed

[Mario Carneiro]

but you can't hash the entire state (from lean)

[Scott Morrison]

tactic.suggest does a certain amount of manipulation of tactic_state.

[Scott Morrison]

Oh -- I don't know if @Jason Rute is actually talking about detecting multiple paths in the graph of tactic_states and state transitions.

[Scott Morrison]

My reading of his question was that he was happy to treat it as a tree.

[Scott Morrison]

And the point of the question is about breadth first, rather than depth first, search.

[Jason Rute]

My thoughts are many level's deep. I've moved from tree to graph. With a tree, I can key each node by the path if needed. As a graph, I could record all the expressions in the goals (including the local context and target) if I really want to.

[Mario Carneiro]

I don't actually know why you need to compare tactic_state objects for your original use case

[Jason Rute]

I probably don't, but I was just curious.

[Mario Carneiro]

Even if you could, the relation would probably be too fine for your needs

[Mario Carneiro]

If you want to deduplicate nodes in the tree, you should focus on the important things that future tactics will be looking at: the goal statement and the hypotheses. I don't know if you are treating multiple goals differently

[Scott Morrison]

I would avoid comparing tactic_state for now, and make sure you know how to do a BFS search of the tree resulting from tactic applications.

[Scott Morrison]

I can write something if you'd like some hints; it's probably only a few lines long.

[Jason Rute]

Thanks. This was very informative. I think I know where to start, but if you every feel inclined, I'd be happy to see some code. :slight_smile:

[Scott Morrison]

I haven't attempted to polish this at all, or test anything beyond the example, but:

import tactic.core

open tactic

meta def run_for_state {α : Type} (t : tactic α) : tactic (option (tactic_state × α)) :=
do a ← try_core t,
   s ← get_state,
   return $ a.map (prod.mk s)

meta def which_succeed (tactics : list (tactic unit)) (state : tactic_state) : tactic (list (ℕ × tactic_state)) :=
do os ←
  tactics.enum.mmap (λ p : ℕ × tactic unit, do
    set_state state,
    r ← run_for_state p.2,
    return $ r.map (λ ⟨s', _⟩, (p.1, s'))),
  return $ (os.map (option.to_list)).join

meta def bfs (tactics : list (tactic unit)) : tactic (list (list ℕ)) :=
(done >> return [[]]) <|>
(do
  s ← get_state,
  rs ← which_succeed tactics s,
  ns ← rs.mmap (λ r, do set_state r.2, ns ← bfs, return $ ns.map (λ n, r.1 :: n)),
  return ns.join)

example : ℕ × ℕ :=
begin
  bfs [`[exact 0], `[exact 1], `[split]] >>= trace,
end

[Jason Rute]

Thanks! Let me play with the code a little, so I understand everything.

[Jason Rute]

First, think I need to upgrade from 3.4.2. I wonder what I've been missing out...