Directed Graphs

Small directed graph module providing the core graph-theoretic mechanisms used by the generalization linter.

---

Main definitions

• Digraph: Implemented as an adjacency list.
• Condensation: Condensation of digraph into DAG of SCCs.
• minCommonAncestors: Find the minimal common ancestors.

---

References

• Alex J. Best. 2023. Automatically Generalizing Theorems Using Typeclasses. In Fifth Workshop on Formal Mathematics for Mathematicians. CEUR Workshop Proceedings. Retrieved from https://ceur-ws.org/Vol-3377/fmm12.pdf.
• David J. King and John Launchbury. 1995. Structuring depth-first search algorithms in Haskell. In Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL ’95, 1995. ACM Press, San Francisco, California, United States, 344–354. https://doi.org/10.1145/199448.199530

structure GeneralizationLinter.Digraph (V : Type u) [BEq V] [Hashable V] : Type u

Directed graph with vertices of type V, implemented through an adjacency list adj.

• adj : Std.HashMap V (Array V)

  Adjacency list of the directed graph.

  Given a vertex a, adj[a] is the array of immediate successors of a.

  Default: {}

  ---

  Example

  1 → 2 ─┐
  ↓   ↑  │    5
  3   4 ←┘
  

  For the graph shown above (where the 5 is an isolated vertex), we'd have:

  • adj[1] = #[2, 3]
  • adj[2] = #[4]
  • adj[3] = #[]
  • adj[4] = #[2]
  • adj[5] = #[]

  ---

  Implementation Notes

  Storing the successors as an Array instead of a List is more efficient for our purposes. Conceptually, either one would work.

@[implicit_reducible]

instance GeneralizationLinter.instInhabitedDigraph {a✝ : Type u_1} {a✝¹ : BEq a✝} {a✝² : Hashable a✝} : Inhabited (Digraph a✝)

Equations

• GeneralizationLinter.instInhabitedDigraph = { default := GeneralizationLinter.instInhabitedDigraph.default }

def GeneralizationLinter.Digraph.vertices {V : Type u} [BEq V] [Hashable V] (G : Digraph V) : Array V

Returns an array of the vertices of G in some order.

Equations

• G.vertices = G.adj.keysArray

def GeneralizationLinter.Digraph.contains {V : Type u} [BEq V] [Hashable V] (G : Digraph V) (v : V) : Bool

Returns true iff G contains the vertex v.

Equations

• G.contains v = G.adj.contains v

def GeneralizationLinter.Digraph.succs {V : Type u} [BEq V] [Hashable V] (G : Digraph V) (v : V) : Array V

Returns the immediate successors of v in G.

Warning: If v is not in G, this will silently return the empty array.

Equations

• G.succs v = G.adj.getD v #[]

def GeneralizationLinter.Digraph.insertVertex {V : Type u} [BEq V] [Hashable V] (G : Digraph V) (v : V) : Digraph V

Inserts vertex v into G, and returns updated G.

Equations

• G.insertVertex v = if G.contains v = true then G else { adj := G.adj.insert v #[] }

def GeneralizationLinter.Digraph.insertEdge {V : Type u} [BEq V] [Hashable V] (G : Digraph V) (s t : V) : Digraph V

Inserts edge s → t into G, and returns updated G. (s stands for "source vertex" and t stands for "target vertex" of the edge to be inserted.)

---

Examples

-- `G := ({} : Digraph Nat).insertEdge 1 2`
G.vertices = #[1, 2]
G.succs 1 = #[2]
(G.insertEdge 1 2).succs 1 = #[2]

Equations

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

Reachability

partial def GeneralizationLinter.Digraph.dfs {V : Type u} [BEq V] [Hashable V] (G : Digraph V) (v : V) (acc : Array V) (vis : Std.HashSet V) : Array V × Std.HashSet V

Depth-first search to compute transitive closure of v under G.

• acc is an accumulator: the returned array is acc with the vertices newly visited by this search pushed onto it, in DFS postorder (so, if G is acyclic, in reverse topological order). The newly visited vertices are those reachable from v along a path that avoids vis (anything lying only behind an already-visited vertex is skipped). (sccs relies on exactly this, threading vis across its calls so that each call returns one strongly-connected component.)
• vis is the set of visited vertices. The returned set is vis together with the same newly visited vertices that were pushed onto acc.

---

Examples

/-
Suppose `G` has edges `1 → 2`, `1 → 3`, `2 → 4`, `4 → 2`, and an isolated vertex `5`:

1 → 2 ─┐
↓   ↑  │    5
3   4 ←┘
-/
G.dfs 1 #[] {} = (#[4, 2, 3, 1], {1, 2, 3, 4})
G.dfs 1 #[] {2} = (#[3, 1], {1, 2, 3})
G.dfs 1 #[] {1} = (#[], {1})
G.dfs 3 #[0] {} = (#[0, 3], {3})
G.dfs 9 #[] {} = (#[9], {9})

def GeneralizationLinter.Digraph.downSet {V : Type u} [BEq V] [Hashable V] (G : Digraph V) (v : V) : Std.HashSet V

Returns the set of vertices of G reachable from v, including v.

Warning: If v is not a vertex of G, this returns the singleton set {v} rather than {}.

Equations

• G.downSet v = (G.dfs v #[] ∅).snd

def GeneralizationLinter.Digraph.downSets {V : Type u} [BEq V] [Hashable V] (G : Digraph V) : Std.HashMap V (Std.HashSet V)

Returns map from vertices to the set of vertices that each can reach.

Equations

• G.downSets = Std.HashMap.fold (fun (sets : Std.HashMap V (Std.HashSet V)) (v : V) (x : Array V) => sets.insert v (G.downSet v)) ∅ G.adj

def GeneralizationLinter.Digraph.postorder {V : Type u} [BEq V] [Hashable V] (G : Digraph V) : Array V

Returns all vertices of G, in the postorder of a depth-first search that starts a new tree at each vertex of G in turn. If G is acyclic, this is a reverse topological order.

Equations

• G.postorder = (Array.foldl (fun (x : Array V × Std.HashSet V) (v : V) => match x with | (acc, vis) => G.dfs v acc vis) (#[], ∅) G.vertices).fst

def GeneralizationLinter.Digraph.transpose {V : Type u} [BEq V] [Hashable V] (G : Digraph V) : Digraph V

Returns transpose of G.

Equations

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

Condensation

def GeneralizationLinter.Digraph.sccs {V : Type u} [BEq V] [Hashable V] (G : Digraph V) : Array (Array V)

Strongly-connected components of G, computed with Kosaraju–Sharir's algorithm.

---

Examples

/-
Suppose `G` has edges `1 → 2`, `1 → 3`, `2 → 4`, `4 → 2`, and an isolated vertex `5`:

1 → 2 ─┐
↓   ↑  │    5
3   4 ←┘
-/
G.sccs = #[#[5], #[1], #[3], #[4, 2]]
-- Suppose `H` has edges `1 → 2` and `2 → 1`.
H.sccs = #[#[2, 1]]

Equations

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

structure GeneralizationLinter.Digraph.Condensation (V : Type u) [BEq V] [Hashable V] : Type u

• graph : Digraph Nat

  Digraph of indices. Guaranteed to be a DAG.

• members : Std.HashMap Nat (Array V)

  Maps an index to the array of vertices contained in the SCC corresponding to the index.

• componentsMap : Std.HashMap V Nat

  Maps a vertex to the index of the SCC which contains it.

• downSetsByIndex : Std.HashMap Nat (Std.HashSet Nat)

  Maps an index to its corresponding down-set.

• vertices : Array Nat

  graph.vertices, cached inside condense.

def GeneralizationLinter.Digraph.condense {V : Type u} [BEq V] [Hashable V] (G : Digraph V) : Condensation V

Condense digraph G into DAG of SCCs of G and return the result as a Condensation structure.

Equations

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

def GeneralizationLinter.Digraph.Condensation.indicesOf {V : Type u} [BEq V] [Hashable V] (c : Condensation V) (vs : Std.HashSet V) : Std.HashSet Nat

Returns indices of SCCs containing the vertices vs.

---

Examples

-- Suppose `H` has edges `1 → 2` and `2 → 1`, so that `H.condense` has a single SCC, at index `0`.
H.condense.indicesOf {1, 2} = {0}
H.condense.indicesOf {2, 9} = {0}
H.condense.indicesOf {9} = {}

Equations

• c.indicesOf vs = Std.HashSet.fold (fun (indices : Std.HashSet Nat) (v : V) => match c.componentsMap[v]? with | some idx => indices.insert idx | none => indices) ∅ vs

Minimal Common Ancestors

inductive GeneralizationLinter.Digraph.Condensation.AbsencePolicy : Type

Establishes how minCommonAncestors should handle witness sets where none of the witnesses corresponds to a vertex of the condensation.

• failClosed : AbsencePolicy

  If any witness set has none of its witnesses corresponding to a vertex of the condensation, then minCommonAncestors abandons the whole query and returns #[]. (Default.)

• failOpenGuarded : AbsencePolicy

  Witness sets where none of the witnesses corresponds to a vertex of the condensation are discarded, leading to minCommonAncestors not taking them into account and hence returning ancestors which will not have any of these witness sets' witnesses as a descendant.

@[implicit_reducible]

instance GeneralizationLinter.Digraph.Condensation.instBEqAbsencePolicy : BEq AbsencePolicy

Equations

• GeneralizationLinter.Digraph.Condensation.instBEqAbsencePolicy = { beq := GeneralizationLinter.Digraph.Condensation.instBEqAbsencePolicy.beq }

def GeneralizationLinter.Digraph.Condensation.instBEqAbsencePolicy.beq : AbsencePolicy → AbsencePolicy → Bool

Equations

• GeneralizationLinter.Digraph.Condensation.instBEqAbsencePolicy.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def GeneralizationLinter.Digraph.Condensation.instReprAbsencePolicy.repr : AbsencePolicy → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance GeneralizationLinter.Digraph.Condensation.instReprAbsencePolicy : Repr AbsencePolicy

Equations

• GeneralizationLinter.Digraph.Condensation.instReprAbsencePolicy = { reprPrec := GeneralizationLinter.Digraph.Condensation.instReprAbsencePolicy.repr }

def GeneralizationLinter.Digraph.Condensation.minCommonAncestors {V : Type u} [BEq V] [Hashable V] (cond : Condensation V) (witnessSets : Array (Std.HashSet V)) (ap : AbsencePolicy := AbsencePolicy.failClosed) : Array (Array V)

Idea: Given the set of classes that a theorem uses, find the minimal common ancestor of that set in the class DAG, i.e., the weakest common ancestor of the elements of the set (i.e., their join), if a unique one exists. The class DAG is not a lattice, however, so the join is not guaranteed to exist. In those cases, an antichain of incomparable answers is returned.

---

Implementation notes

The set of used classes is given as an array (witnessSets) of sets.

The idea is that the array of sets communicates the requirements as a general AND of ORs. Let's call each set a set of witnesses. The question then becomes:

Find a class that is a common ancestor to at least one witness of each requirement (i.e., a common ancestor of at least one transversal of the sets of witnesses).

The answer is returned as an array of arrays. Any element of any of the inner arrays is a class which satisfies, on its own, all the given requirements. The structure within which the classes are given encodes the relationships between all of these classes:

• All classes within each inner array are mutually equipotent. Each inner array therefore represents a single SCC of the class graph pre-condensation (or, equivalently, a single vertex in the class DAG, i.e., in the condensation of the class graph).
• The SCCs listed in the outer array are pairwise unreachable in the class graph. Alternatively, roughly speaking, the outer array represents the antichain of vertices of the class DAG which satisfy the requirements. More precisely, each of these vertices is a bona-fide minimal common ancestor; it's just that minimality doesn't generally imply uniqueness in our case, since the class DAG is not a lattice.

---

Examples (as of Mathlib v4.32.1)

• Unique minimal common ancestor: Sometimes, there is exactly one minimal common ancestor.

  minCommonAncestors #[{Monoid #0}, {CommSemigroup #0}] = #[#[CommMonoid #0]]
  

• No common ancestors: Quite often, there may not exist any class which satisfies all the given requirements.

  minCommonAncestors #[{Inv #0}, {SDiff #0}] = #[]
  

• Minimal common ancestors of single classes: Within an SCC of the class graph (pre-condensation), all classes are pairwise equipotent. This means that any element of the SCC is a minimal common ancestor of any other element or subset of the SCC. Note that the vast majority of the SCCs of the class graph (pre-condensation) are singletons.

  minCommonAncestors #[{One #0}] = #[#[OfNat #0 1, One #0]]
  minCommonAncestors #[{Monoid #0}] = #[#[Monoid #0]]
  

• Multiple non-equipotent minimal common ancestors: Rarely, requirements may have multiple non-equipotent minimal common ancestors.

  minCommonAncestors #[{Add #0}, {Mul #0}] = #[
    #[Lean.Grind.Semiring #0],
    #[Distrib #0],
  ]
  

Equations

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

def GeneralizationLinter.Digraph.Condensation.reaches {V : Type u} [BEq V] [Hashable V] (c : Condensation V) (s t : V) : Bool

Given the condensation of a graph and two vertices s and t of the graph (pre-condensation), returns whether s reaches t in the graph (pre-condensation).

---

Examples

/-
Suppose `G` has edges `1 → 2`, `1 → 3`, `2 → 4`, `4 → 2`, and an isolated vertex `5`:

1 → 2 ─┐
↓   ↑  │    5
3   4 ←┘
-/
G.condense.reaches 1 4 = true
G.condense.reaches 4 2 = true
G.condense.reaches 4 1 = false
G.condense.reaches 5 5 = true
G.condense.reaches 9 9 = false

Equations

• c.reaches s t = match c.componentsMap[s]?, c.componentsMap[t]? with | some s_idx, some t_idx => (c.downSetsByIndex.getD s_idx ∅).contains t_idx | x, x_1 => false

def GeneralizationLinter.Digraph.Condensation.coalesceWith {α : Type u_1} [Inhabited α] (fuse : α → α → α) (connected : α → α → Bool) (xs : Array α) : Array α

Given an array xs and methods

• fuse to merge two elements of the array and
• connected to query whether two elements of the array should be merged,

returns an array in which no two elements should be merged anymore.

We require the following preconditions:

• connected must be a symmetric relation.
• For any a b c : α, connected a c or connected b c implies connected (fuse a b) c.

---

Examples

coalesceWith (·.append ·) (fun x y : List Nat => x.any y.contains)
  #[[1], [1, 2], [3], [2, 4], [5, 6]] = #[[1, 1, 2, 2, 4], [3], [5, 6]]
coalesceWith (·.union ·) (fun x y : HashSet Nat => !(x.inter y).isEmpty)
  #[{1}, {1, 2}, {3}, {2, 4}, {5, 6}] = #[{1, 2, 4}, {3}, {5, 6}]

Equations

• GeneralizationLinter.Digraph.Condensation.coalesceWith fuse connected xs = GeneralizationLinter.Digraph.Condensation.coalesceWith.loop✝ fuse connected xs (xs.size * xs.size + 1)

def GeneralizationLinter.Digraph.Condensation.partitionByDesc {V : Type u} [BEq V] [Hashable V] (used : Std.HashSet V) (conn : V → V → Bool) : Array (Std.HashSet V)

Partitions used into subsets whose down-sets are disconnected according to conn.

---

Example

Roughly speaking, in our use-case, if partitionByDesc was called on {Semigroup #0, MulOneClass #0, IsPreorder #0}, it would return #[{Semigroup #0, MulOneClass #0}, {IsPreorder #0}]. See MCAContext.sharesDataDesc for more information.

Equations

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