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 atomToIdx[src] ≤ atomToIdx[dst].

• src : ℕ

  Source of the edge.

• dst : ℕ

  Destination of the edge.

• proof : Lean.Expr

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

instance Mathlib.Tactic.Order.instToStringEdge : ToString Edge

Equations

• Mathlib.Tactic.Order.instToStringEdge = { toString := fun (e : Mathlib.Tactic.Order.Edge) => toString "" ++ toString e.src ++ toString " ⟶ " ++ toString e.dst ++ toString "" }

@[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.

Equations

• Mathlib.Tactic.Order.Graph = Array (Array Mathlib.Tactic.Order.Edge)

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

Adds an edge to the graph.

Equations

• g.addEdge edge = Array.modify g edge.src fun (edges : Array Mathlib.Tactic.Order.Edge) => edges.push edge

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

Constructs a directed Graph using ≤ facts.

Equations

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

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

State for the DFS algorithm.

• visited : Array Bool

  visited[v] = true 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) (idxToAtom : Std.HashMap ℕ Lean.Expr) (s t : ℕ) : Lean.MetaM (Option Lean.Expr)

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

Equations

• g.buildTransitiveLeProof idxToAtom s t = (g.buildTransitiveLeProofDFS s t (idxToAtom.get! t)).run' { visited := mkArray (Array.size g) false }