Zulip Chat Archive

Stream: general

Topic: Backtracking


view this post on Zulip 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.)

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip Scott Morrison (Apr 21 2020 at 00:24):

Sure, it's no problem.

view this post on Zulip Scott Morrison (Apr 21 2020 at 00:24):

Backtracking is free.

view this post on Zulip Jason Rute (Apr 21 2020 at 00:24):

How does one do it?

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Apr 21 2020 at 00:25):

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

view this post on Zulip Scott Morrison (Apr 21 2020 at 00:25):

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

view this post on Zulip Jason Rute (Apr 21 2020 at 00:26):

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

view this post on Zulip 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

view this post on Zulip Scott Morrison (Apr 21 2020 at 00:27):

and get_state / set_state

view this post on Zulip Scott Morrison (Apr 21 2020 at 00:27):

should allow you to do anything you like

view this post on Zulip Scott Morrison (Apr 21 2020 at 00:27):

without any re-running tactics.

view this post on Zulip Scott Morrison (Apr 21 2020 at 00:27):

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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Apr 21 2020 at 00:30):

no

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Apr 21 2020 at 00:31):

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

view this post on Zulip Mario Carneiro (Apr 21 2020 at 00:31):

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

view this post on Zulip Scott Morrison (Apr 21 2020 at 00:31):

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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Apr 21 2020 at 00:32):

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

view this post on Zulip Scott Morrison (Apr 21 2020 at 00:33):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Jason Rute (Apr 21 2020 at 00:36):

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

view this post on Zulip Mario Carneiro (Apr 21 2020 at 00:36):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip Jason Rute (Apr 21 2020 at 01:08):

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

view this post on Zulip 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