Class Graph

Builds the class graph from the environment.

---

Main definitions

• isWeakeningEdge: helper for extractEdge? that determines whether an edge should be considered a weakening edge.
• extractEdge?: convert an instance into a ClassEdge, if appropriate.
• ofEnv: build the class graph from the environment.

---

References

• [A. J. Best. 2023. Automatically Generalizing Theorems Using Typeclasses.][best2023automaticallyGeneralizingTheorems]

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.isSortTyped (a : Lean.Expr) : Lean.MetaM Bool

Returns true iff a's type is or reduces to Sort.

Equations

• GeneralizationLinter.isSortTyped a = do let __do_lift ← Lean.Meta.inferType a let __do_lift ← Lean.Meta.whnfR __do_lift pure __do_lift.isSort

def GeneralizationLinter.frameArgs (classAppE : Lean.Expr) : Lean.MetaM (Array Lean.Expr)

The non-instance-implicit arguments of a class application. These are the arguments that are used by reifyClass to reify a suggestion candidate. We call these arguments the frame arguments or frame of a class application.

There can be some overlap between frame arguments and targeted binders, which is fine, because we're not using frame arguments to index entries of the class graph, but rather just to reify suggestion candidates.

---

Examples

-- class IsPreorder (α : Sort*) (r : α → α → Prop) : Prop
frameArgs (@IsPreorder α r) = #[α, r]
-- class CharP (R : Type*) [AddMonoidWithOne R] (p : outParam ℕ) : Prop
frameArgs (@CharP R _ p) = #[R, p]
-- class Module (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] : Type (max u v)
frameArgs (@Module R M _ _) = #[R, M]

Equations

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

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 to arguments that are 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 α β) : Magma β (let's pretend that it makes sense) would be extracted into an (unsound) edge from Monoid α to Magma β 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 cases 2 and 4:

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

Non-examples:

• α is not statable from #[] or #[β].
• Monoid α is not statable from #[] or #[β].
• α is not statable from #[Monoid α].
• OrderDual α is not statable from #[α].

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 frame 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, wee 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, frame arguments and class-typed arguments comprise all arguments 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 frame args	C1
IsTopologicalGroup.toContinuousInv	G, inst₁, inst₂, self	G	✓
Semiring.toNatAlgebra	R, inst	ℕ, R	✓
ULift.addLeftCancelMonoid	α, inst	ULift α	✓
Lex.instIsRightCancelAdd	α, inst₁, inst₂	Lex α	✗
Matrix.isScalarTower	R, S, α, inst₁, inst₃, inst₂	R, S, Matrix m n α	✗
IsNoetherianRing.wfDvdMonoid	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)	@ULift α	✓
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

• Single-premise instance declaration. Forgetful instance automatically generated by class Monoid (M : Type u) extends Semigroup M:

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

• Multi-premise instance declaration yielding. 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 result in an edge:

  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 iff the vertex's class's codomain is Prop or if all applications of the vertex's class are subsingletons.

• 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 class and instance declarations), collecting weakening edges and taking note of subsingleton classes as it goes.

---

Implementation notes

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

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.

def GeneralizationLinter.ClassGraph.ofEnv : Lean.MetaM ClassGraph

Scans the environment's instances into a ClassGraph.

Equations

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