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].

Instances For
    @[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
      Instances For

        Adds an edge to the graph.

        Equations
          Instances For

            Constructs a directed Graph using facts.

            Equations
              Instances For

                State for the DFS algorithm.

                • visited : Array Bool

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

                Instances For

                  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
                    Instances For