Stream: general

Topic: Backtracking

Jason Rute (Apr 21 2020 at 00:15):

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 (Apr 21 2020 at 00:18):

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 (Apr 21 2020 at 00:21):

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 (Apr 21 2020 at 00:23):

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 (Apr 21 2020 at 00:24):

Sure, it's no problem.

Scott Morrison (Apr 21 2020 at 00:24):

Backtracking is free.

Jason Rute (Apr 21 2020 at 00:24):

How does one do it?

Scott Morrison (Apr 21 2020 at 00:24):

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

Scott Morrison (Apr 21 2020 at 00:25):

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

Scott Morrison (Apr 21 2020 at 00:25):

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

Jason Rute (Apr 21 2020 at 00:26):

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

Scott Morrison (Apr 21 2020 at 00:27):

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

Scott Morrison (Apr 21 2020 at 00:27):

and get_state / set_state

Scott Morrison (Apr 21 2020 at 00:27):

should allow you to do anything you like

Scott Morrison (Apr 21 2020 at 00:27):

without any re-running tactics.

Scott Morrison (Apr 21 2020 at 00:27):

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

Jason Rute (Apr 21 2020 at 00:29):

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

no

Scott Morrison (Apr 21 2020 at 00:30):

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

Mario Carneiro (Apr 21 2020 at 00:31):

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

Mario Carneiro (Apr 21 2020 at 00:31):

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

Scott Morrison (Apr 21 2020 at 00:31):

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

Scott Morrison (Apr 21 2020 at 00:32):

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 (Apr 21 2020 at 00:32):

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

Scott Morrison (Apr 21 2020 at 00:33):

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

Jason Rute (Apr 21 2020 at 00:34):

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 (Apr 21 2020 at 00:34):

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

Jason Rute (Apr 21 2020 at 00:36):

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

Mario Carneiro (Apr 21 2020 at 00:36):

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

Mario Carneiro (Apr 21 2020 at 00:37):

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 (Apr 21 2020 at 00:38):

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 (Apr 21 2020 at 00:38):

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

Jason Rute (Apr 21 2020 at 00:39):

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 (Apr 21 2020 at 00:59):

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 (Apr 21 2020 at 01:08):

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

Jason Rute (Apr 21 2020 at 01:23):

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

Last updated: May 08 2021 at 18:17 UTC