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.
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
can prove the vertex
how contains information that the explainer will use to generate Lean code for the
- 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.
idis a numerical id used to refer to this vertex in the context of a single graph.
expis the expression this vertex represents.
ppis the string format of the expression; we store this in the vertex to avoid recalculating it.
sideis whether this vertex descends from the left or right side of the equation.
parentis the edge that originally added this vertex to the graph.
- 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.
rulesdetermine 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.
verticesmaps vertex.id to vertex.
vmapmaps vertex.pp to a list of vertex.id with that pp, so we can quickly find collisions.
solving_edgerepresents a solution that will prove our target equation. It is an edge that would connect the two trees, so
solving_edge.toare vertices in different trees.
rhsare the left and right expressions we are trying to prove are equal.
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.