Documentation

Mathlib.Tactic.Order.Graph.Basic

Graphs for the order tactic #

This module defines the Graph structure and basic operations on it. The order tactic uses -graphs, where the vertices represent atoms, and an edge (x, y) exists if x ≤ y.

An edge in a graph. In the order tactic, the proof field stores the of atomToIdx[src] ≤ atomToIdx[dst].

  • src :

    Source of the edge.

  • dst :

    Destination of the edge.

  • proof : Lean.Expr

    Proof of atomToIdx[src] ≤ atomToIdx[dst].

@[reducible, inline]

If g is a Graph, then for a vertex with index v, g[v] is an array containing the edges starting from this vertex.

Equations

Adds an edge to the graph.

Equations

Constructs a directed Graph using facts.

Equations
  • One or more equations did not get rendered due to their size.

State for the DFS algorithm.

  • visited : Array Bool

    visited[v] = true if and only if the algorithm has already entered vertex v.

DFS algorithm for constructing a proof that x ≤ y by finding a path from x to y in the -graph.

Given a -graph g, finds a proof of s ≤ t using transitivity.

Equations