mathlib documentation

tactic.rewrite_search.search

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.

meta structure tactic.rewrite_search.edge  :
Type

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.

Converting an edge to a human-readable string.

meta structure tactic.rewrite_search.vertex  :
Type

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.
meta structure tactic.rewrite_search.graph  :
Type

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.

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.

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