Class Graph

Builds the class graph from the environment.

---

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.

Edges

structure GeneralizationLinter.ClassEdge : Type

An edge of the class graph.

• src : Vertex

  Source vertex of the edge. This is the stronger class, the one we're weakening from.

• tgt : Vertex

  Target vertex of the edge. This is the weaker class, the one we're weakening to.

Extraction

def GeneralizationLinter.statableFrom (sArgs : Array Lean.Expr) (isClosed : Lean.Expr → Lean.MetaM Bool) (e : Lean.Expr) : Lean.MetaM Bool

Returns true iff e is "statable" from sArgs.

We define statability inductively as follows: e is statable from sArgs if

1. whnfR e is syntactically equal to whnfR sArgs[i] for some i,
2. whnfR e is an fvar occurring in whnfR sArgs[i] for some i,
3. whnfR e is "closed" according to isClosed (intuitively, this means it contains no fvars), or
4. whnfR e is an application of a "non-synonym" type former whose key arguments (see keyArgs) are all statable from sArgs, or
5. whnfR e is a projection whose projected term is statable from sArgs.

By synonym type former we mean any type former which unfolds to one of its own arguments. By "non-synonym" type formers we mean any other type former. For example, OrderDual is a synonym type former, while Monoid is a "non-synonym" type former. See also isSynonymFormer.

---

Implementation notes

One could argue that condition 2 should be weakened to whnfR e being an fvar that occurs in sArgs[i] instead of whnfR sArgs[i]. For example, if sArgs[i] is FirstOf α β, where FirstOf α β := α, and whnfR e is β, the weakened version would claim that β is statable from FirstOf α β, while the original condition 2 claims that it is not. However, condition 2, as stated, is better-suited for our purposes. This is because canonArg also uses whnfR, meaning that an application like Monoid (FirstOf α β) would be canonicalized into Monoid α. Hence, an instance like instance [Monoid (FirstOf α β)] : Mul β (let's pretend that it makes sense) would be extracted into an (unsound) edge from Monoid α to Mul β under the weakened condition 2, and rejected under the original condition 2.

---

Examples

According to our definition of "statable", we have the following (where α and β are fvars):

Definition case 1:

• α is statable from #[α].
• Monoid α is statable from #[Monoid α].
• OrderDual α is statable from #[OrderDual α].

Definition case 2:

• α is statable from #[Monoid α].
• α is statable from #[OrderDual α].

Definition case 3:

• ℕ is statable from #[].
• Monoid ℕ is statable from #[].

Definition case 4:

• Monoid α is statable from #[α].

Definition case 5: Suppose x : Nat × Nat. Then:

• x.1 is statable from #[x].
• x.1 is statable from #[x.1].
• x is statable from #[x.1].

Definition cases 2 and 4:

• Monoid α is statable from #[Group α].

Non-examples:

• α is not statable from #[] or #[β].
• Monoid α is not statable from #[] or #[β].
• OrderDual α is not statable from #[α].
• If x y : Nat × Nat then x.1 is not statable from #[y] or #[y.1].

Note: The reason we claim that OrderDual α is not statable from #[α], while at the same time claiming that α is statable from #[OrderDual α], is that we don't want to introduce synonyms, but are okay with removing them.

Equations

• GeneralizationLinter.statableFrom sArgs isClosed e = do let __do_lift ← Array.mapM Lean.Meta.whnfR sArgs GeneralizationLinter.statableFrom.go✝ isClosed __do_lift e

def GeneralizationLinter.isWeakeningEdge (s t : Lean.Expr) (otherPrems : Array Lean.Expr) : Lean.MetaM Bool

Helper for extractEdge? which, given some information about the instance declaration that extractEdge? is processing, indicates whether the edge is a weakening edge, which is the case iff all of the following conditions are satisfied:

1. Every key argument of the target is statable from the source's arguments (see also statableFrom).

   Why? Our graph's edges are ordered pairs of vertices, each vertex representing a specific kind of class application. For the graph to be sound, we need each edge to guarantee that, given the source vertex, we can reach the target vertex. If the target is not statable from the source's arguments, then this cannot be the case.

2. Every class-typed argument of the declaration other than the source is contained in the source's type as a direct argument.

   Why? The rationale is essentially the same as for condition 1, this is just the analog for class-typed args. Together, non-instance-implicit and class-typed arguments comprise all of an instance (unless there's a non-class-typed instance-implicit parameter, which is almost never the case; Mathlib has only one such declaration, CategoryTheory.Bundled.of, and even there the intended usage is that the instance-implicit parameter should be a typeclass). They may also overlap; for example, there's plenty of class-typed implicit arguments in Mathlib (see e.g. IsTopologicalGroup.toContinuousInv in the examples section below).

For a brief discussion on this topic, see the thread general > When are instance mappings projections on the Lean Zulip.

---

Examples

(Note: In the examples below, "source" refers to the last argument of the instance, which is looser than the sense in which the term is used for sourceArg?.)

Instance	Source's args	Target's key args	C1
IsTopologicalGroup.toContinuousInv	G, inst₁, inst₂	G	✓
Semiring.toNatAlgebra	R	ℕ, R	✓
ULift.addLeftCancelMonoid	α	ULift α	✓
Lex.instIsRightCancelAdd	α, inst₁	Lex α	✗
Matrix.isScalarTower	R, S, α, inst₁, inst₃, inst₂	R, S, Matrix m n α	✗
IsNoetherianRing.wfDvdMonoid	R, @CommSemiring.toSemiring R inst₁	R	✓

Instance	Class-typed args…¹	Source's type	C2
IsTopologicalGroup.toContinuousInv	inst₁, inst₂	@IsTopologicalGroup G inst₁ inst₂	✓
Semiring.toNatAlgebra	(none)	@Semiring R	✓
ULift.addLeftCancelMonoid	(none)	@AddLeftCancelMonoid α	✓
Lex.instIsRightCancelAdd	inst₁	@IsRightCancelAdd α inst₁	✓
Matrix.isScalarTower	inst₁, inst₂, inst₃	@IsScalarTower R S α inst₁ inst₃ inst₂	✓
IsNoetherianRing.wfDvdMonoid	inst₁, inst₂	@IsNoetherianRing R (CommSemiring.toSemiring R inst₁)	✗

¹Class-typed args of the declaration other than the source.

instance IsTopologicalGroup.toContinuousInv {G : Type*} {inst₁ : TopologicalSpace G}
  {inst₂ : Group G} [self : @IsTopologicalGroup G inst₁ inst₂] : ContinuousInv G
instance Semiring.toNatAlgebra {R : Type*} [inst : @Semiring R] : Algebra ℕ R
instance ULift.addLeftCancelMonoid {α : Type*}
  [inst : @AddLeftCancelMonoid α] : AddLeftCancelMonoid (ULift α)
instance Lex.instIsRightCancelAdd {α : Type*} [inst₁ : Add α]
  [inst₂ : @IsRightCancelAdd α inst₁] : IsRightCancelAdd (Lex α)
instance Matrix.isScalarTower {m n R S α : Type*}
  [inst₁ : SMul R S] [inst₂ : SMul R α] [inst₃ : SMul S α]
  [inst₄ : @IsScalarTower R S α inst₁ inst₃ inst₂] : IsScalarTower R S (Matrix m n α)
instance IsNoetherianRing.wfDvdMonoid {R : Type u_1} [inst₁ : CommSemiring R]
  [inst₂ : @IsDomain R (@CommSemiring.toSemiring R inst₁)]
  [inst₃ : @IsNoetherianRing R (@CommSemiring.toSemiring R inst₁)] : WfDvdMonoid R

Equations

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

def GeneralizationLinter.extractEdge? (name : Lean.Name) : Lean.MetaM (Option ClassEdge)

Processes a declaration into an edge for the class graph, if appropriate.

---

Examples (each edge below abbreviates its src/tgt Vertex to that vertex's class name)

• Single-premise instance declaration. One of the forgetful instances automatically generated by class Monoid (M : Type u) extends Semigroup M, MulOneClass M, NPow M:

  -- instance Monoid.toSemigroup {α} [Monoid α] : Semigroup α
  extractEdge? `Monoid.toSemigroup =
    some { src := `Monoid, tgt := `Semigroup }
  

• Multi-premise instance declaration yielding an edge. Suppose we call extractEdge? on the following instance declaration:

  instance Algebra.toModule {R A} {_ : CommSemiring R} {_ : Semiring A} [Algebra R A] : Module R A
  

  Despite having multiple premises, this would lead to an edge being extracted:

  extractEdge? `Algebra.toModule = some { src := `Algebra, tgt := `Module }
  

  The reason for this is that the class Algebra R A requires that instances [CommSemiring R] and [Semiring A] be provided. In fact, Algebra R A is hiding these instance implicit arguments; the fully explicit version would be @Algebra R A instCommSemiringR instSemiringA. This is established in the class's declaration:

  class Algebra (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] extends SMul R A where
  

  Accordingly, whenever we encounter a class hypothesis [Algebra R A] in a theorem, we're actually seeing @Algebra R A instCommSemiringR instSemiringA, meaning that the {_ : CommSemiring R} and {_ : Semiring A} premises of Algebra.toModule are satisfied.

• Instance declaration not yielding any edge because the carrier changes.

  -- instance Prod.instMonoid [Monoid M] [Monoid N] : Monoid (M × N)
  extractEdge? `Prod.instMonoid = none -- conclusion is over a new carrier
  

Equations

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

Build

structure GeneralizationLinter.ClassGraph : Type

The class graph.

• edges : Array ClassEdge

  Array of edges. This is what defines the class graph.

• isSubsingleton : Vertex → Bool

  true only if all applications of the vertex's class are subsingletons; in particular, true for every Prop-valued class in the graph. ClassGraph.assemble decides this per class, and only attempts synthesis for classes in subHeads, so false is not a negative verdict.

• condensation : Digraph.Condensation Vertex

  Condensation of the class graph.

def GeneralizationLinter.ClassGraph.scanInstances (names : Array Lean.Name) : Lean.MetaM (Array ClassEdge × Std.HashSet Lean.Name)

Scans every name in names (which is expected to be a list of instance declarations), collecting weakening edges and taking note of classes that may be subsingletons as it goes.

---

Implementation notes

This is quite expensive, taking several seconds, and so we try to run it as seldomly as possible.

---

Examples (edges abbreviated as in extractEdge?)

-- instance Monoid.toSemigroup {α} [Monoid α] : Semigroup α
-- instance Fintype.subsingleton (α : Type*) : Subsingleton (Fintype α)
-- instance Prod.instMonoid [Monoid M] [Monoid N] : Monoid (M × N)
ClassGraph.scanInstances #[`Monoid.toSemigroup, `Fintype.subsingleton, `Prod.instMonoid] =
  (#[{ src := `Monoid, tgt := `Semigroup }], {`Fintype})
ClassGraph.scanInstances #[] = (#[], {})

Equations

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

def GeneralizationLinter.ClassGraph.assemble (edges : Array ClassEdge) (subHeads : Std.HashSet Lean.Name) : Lean.MetaM ClassGraph

Assembles weakening edges and heads of subsingleton classes into a ClassGraph.

---

Implementation notes

This function is relatively fast compared to ClassGraph.scanInstances, so we re-run it on local rebuilds.

Equations

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