buildTransitiveLeProofDFS — Mathlib

Lean4

/-- DFS algorithm for constructing a proof that `x ≤ y` by finding a path from `x` to `y` in the
`≤`-graph. -/
partial def buildTransitiveLeProofDFS (g : Graph) (v t : Nat) (tExpr : Expr) : StateT DFSState MetaM (Option Expr) := do
  modify fun s => { s with visited := s.visited.set! v true }
  if v == t then
    return ← mkAppM ``le_refl #[tExpr]
  for edge in g[v]!do
    let u := edge.dst
    if !(← get).visited[u]! then
      match ← buildTransitiveLeProofDFS g u t tExpr with
      | some pf =>
        return some <| ← mkAppM ``le_trans #[edge.proof, pf]
      | none =>
        continue
  return none

Похожие утверждения