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

instance Mathlib.Tactic.Order.instToStringEdge : ToString Edge

Equations

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

@[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 = Std.HashMap ℕ (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 = Std.HashMap.alter g edge.src fun (x : Option (Array Mathlib.Tactic.Order.Edge)) => match x with | none => some #[edge] | some edges => some (edges.push edge)

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

Constructs a directed Graph using ≤ facts. It ignores all other 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 : 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.

Equations

• g.buildTransitiveLeProof s t = do let __do_lift ← get liftM ((g.buildTransitiveLeProofDFS s t __do_lift.atoms[t]!).run' { visited := ∅ })