The graph algorithm part of rewrite search #

search.lean contains the logic to do a graph search. The search algorithm starts with an equation to prove, treats the left hand side and right hand side as two vertices in a graph, and uses rewrite rules to find a path that connects the two sides.

source

meta structure tactic.rewrite_search.edge :

Type

from_id : ℕ
to_id : ℕ
proof : tactic expr
how : tactic.rewrite_search.how

An edge represents a proof that can get from one expression to another. It represents the fact that, starting from the vertex fr, the expression in proof can prove the vertex to. how contains information that the explainer will use to generate Lean code for the proof.

Instances for tactic.rewrite_search.edge

tactic.rewrite_search.edge.has_to_format

source

meta def tactic.rewrite_search.edge.to_string :

tactic.rewrite_search.edge → format

Converting an edge to a human-readable string.

source

@[protected, instance]

meta def tactic.rewrite_search.edge.has_to_format :

has_to_format tactic.rewrite_search.edge

source

meta structure tactic.rewrite_search.vertex :

Type

id : ℕ
exp : expr
pp : string
side : tactic.rewrite_search.side
parent : option tactic.rewrite_search.edge

A vertex represents an expression that is equivalent to either the left or right side of our initial equation.

id is a numerical id used to refer to this vertex in the context of a single graph.
exp is the expression this vertex represents.
pp is the string format of the expression; we store this in the vertex to avoid recalculating it.
side is whether this vertex descends from the left or right side of the equation.
parent is the edge that originally added this vertex to the graph.

source

meta structure tactic.rewrite_search.graph :

Type

conf : tactic.rewrite_search.config
rules : list (expr × bool)
vertices : buffer tactic.rewrite_search.vertex
vmap : native.rb_map string (list ℕ)
solving_edge : option tactic.rewrite_search.edge
lhs : expr
rhs : expr

The graph represents two trees, one descending from each of the left and right sides of our initial equation.

conf and rules determine what rewrites are used to generate new graph vertices. Here, the format of a rewrite rule is an expression for rewriting, plus a flag for the direction to apply it in.
vertices maps vertex.id to vertex.
vmap maps vertex.pp to a list of vertex.id with that pp, so we can quickly find collisions.
solving_edge represents a solution that will prove our target equation. It is an edge that would connect the two trees, so solving_edge.fr and solving_edge.to are vertices in different trees.
lhs and rhs are the left and right expressions we are trying to prove are equal.

source

meta def tactic.rewrite_search.mk_graph (conf : tactic.rewrite_search.config) (rules : list (expr × bool)) (eq : expr) :

tactic tactic.rewrite_search.graph

Construct a graph to search for a proof of a given equation.

This graph initially contains only two disconnected vertices corresponding to the two sides of the equation. When find_proof is called, we will run a search and add new vertices and edges.

source

meta def tactic.rewrite_search.graph.find_proof (g : tactic.rewrite_search.graph) :

tactic (tactic.rewrite_search.graph × expr × list tactic.rewrite_search.proof_unit)

Run the search to find a proof for the provided graph. Normally, this is the only external method needed to run the graph search.