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.

structure Mathlib.Tactic.Order.Edge : Type

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

• src : ℕ

  Source of the edge.

• dst : ℕ

  Destination of the edge.

• proof : Lean.Expr

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

@[implicit_reducible]

instance Mathlib.Tactic.Order.instToStringEdge : ToString Edge

@[reducible, inline]

abbrev Mathlib.Tactic.Order.Graph : Type

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

def Mathlib.Tactic.Order.Graph.addEdge (g : Graph) (edge : Edge) : Graph

Adds an edge to the graph.

def Mathlib.Tactic.Order.Graph.constructLeGraph (facts : Array AtomicFact) : Lean.MetaM Graph

Constructs a directed Graph using ≤ facts. It ignores all other facts.

structure Mathlib.Tactic.Order.Graph.DFSState : Type

State for the DFS algorithm.

• visited : Std.HashSet ℕ

  visited.contains v if and only if the algorithm has already entered vertex v.

partial def Mathlib.Tactic.Order.Graph.buildTransitiveLeProofDFS (g : Graph) (v t : ℕ) (tExpr : Lean.Expr) : StateT DFSState Lean.MetaM (Option Lean.Expr)

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

def Mathlib.Tactic.Order.Graph.buildTransitiveLeProof (g : Graph) (s t : ℕ) : AtomM (Option Lean.Expr)

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