Canonicalization

This module is responsible for converting class applications of any kind into Vertexs or Keys, which is the process we refer to as canonicalization, and back, which we refer to as reification.

Main definitions:

• keySlots tries to figure out what parameter "slots" of a class are recoverable from the others, which are slots that we don't want to index our class graph with. For instance, for Module R M inst₁ inst₂, the key slots are the first two parameter slots (corresponding to R and M).
• canonArg canonicalizes a single argument. For example, for Module R M, this means R and M become bvar 0 and bvar 1. For Pow α ℕ, this means α becomes bvar 0 and ℕ remains ℕ.
• toKey canonicalizes a class application into a Key that we query the class graph with.
• reifyClass takes a class name and some frame arguments, and reifies them into a proper class application.
• elabEntry

Given an n-ary class C, keySlots `C returns #[b₁, …, bₙ], where bᵢ : Bool is false if

finds a which "slots" (parameters) are required

Head Helpers

def GeneralizationLinter.isTypeConstructor (env : Lean.Environment) (e : Lean.Expr) : Bool

isTypeConstructor e is true iff e is a (possibly nullary) type constructor constant.

---

Examples

isTypeConstructor returns true on the following:

• Nullary type constructors: Nat, etc.
• Unary type constructors: Group, List, etc.
• Binary type constructors: Prod, And, etc.
• etc.

isTypeConstructor returns false on the following:

• Constants that are not type constructors: And.intro, Nat.succ, etc.
• Things that are not constants: 3, #[3], {}, [], etc.

Equations

• GeneralizationLinter.isTypeConstructor env (Lean.Expr.const c us) = Option.any (fun (x : Lean.ConstantInfo) => x.type.getForallBody.isSort) (env.find? c)
• GeneralizationLinter.isTypeConstructor env e = false

def GeneralizationLinter.isSynonymFormer (h : Lean.Name) : Lean.MetaM Bool

Is h a "type-synonym former", i.e., a former that unfolds to one of its own arguments.

---

Examples

isSynonymFormer `Monoid     -- `false`
isSynonymFormer `OrderDual  -- `true`

Equations

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

What to keep

def GeneralizationLinter.eraseHeadLevels : Lean.Expr → Lean.Expr

Used to strip the universe-level arguments off the heads of type formers used within a key slot. We delegate all handling of universe levels to Vertex.levels.

Equations

• GeneralizationLinter.eraseHeadLevels (Lean.Expr.const c us) = Lean.Expr.const c []
• GeneralizationLinter.eraseHeadLevels x✝ = x✝

def GeneralizationLinter.natLitOf? : Lean.Expr → Option Nat

Retrieves the value of a Nat-valued argument.

---

Examples

• .lit (.natVal n) → n
• @OfNat.ofNat ℕ n _ → n

Anti-Unification

@[reducible, inline]

abbrev GeneralizationLinter.CanonVarsM (α : Type) : Type

As we walk an Expr (generally, a telescope), this monad helps us keep track of two things:

• HashMap FVarId Nat: For each fvar id (where id is some FVarId) we encounter in the expression we're parsing, we add an entry id → k to this map to note to which canonical bvar k we've mapped fvar id.
• Array Expr: This keeps track of the specific carriers we've collected thus far, ordered by their de Bruijn indices.

Invariant: The size of the Array is always greater than or equal to the size of the HashMap.

Equations

• GeneralizationLinter.CanonVarsM = StateT (Std.HashMap Lean.FVarId Nat × Array Lean.Expr) Lean.MetaM

partial def GeneralizationLinter.canonArg (e : Lean.Expr) : CanonVarsM Lean.Expr

Canonicalize a single binder/argument.

---

Examples

• ℕ → ℕ
• 3 → 3
• Applied over the arguments of Group G → Group #0
• Applied over the arguments of Module R R → Module #0 #0
• Applied over the arguments of Pow α ℕ → Pow #0 ℕ
• Applied over the arguments of OfNat α 1 → OfNat #0 1

def GeneralizationLinter.universeLevelsOf (lvls : List Lean.Level) : UniverseLevels

Canonicalized universe arguments for a head with universe arguments lvls.

• concrete: when there are no universe parameters or metavariables; in other words, when the class application is not universe-polymorphic. In this case, we track the specific universe levels of the class application.
• polymorphic: when the class application is universe-polymorphic. In this case, we don't track the universe levels, so we "erase" that information.

---

Examples

universeLevelsOf [0, 1] = concrete #[0, 1]
universeLevelsOf [u]    = polymorphic      -- `u` is a universe variable
universeLevelsOf []     = concrete #[]     -- monomorphic class, e.g., `Std.Refl`

Equations

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

def GeneralizationLinter.toKey (e : Lean.Expr) : Lean.MetaM Key

Given an Expr of a class application, canonicalize it into a Key.

---

Implementation notes

• The head name (which sets Vertex.name) and canonicalized arguments (which set Vertex.pattern) are taken from the whnfR form of the expression, so for example IsNoetherianRing R, which reduces to IsNoetherian R R, would have Vertex.name := ``IsNoetherian and Vertex.pattern := #[#0, #0].

• For a family class binder like ∀ prefix, C args, the body (C args) determines the Vertex fields, while the prefix is used to abstract the

  #TODO: finish this docstring

---

Examples

-- class Module (R M : Type*) [Semiring R] [AddCommMonoid M]
toKey ‹@Module R M inst₁ inst₂› = {
  -- `Vertex` fields
  name := `Module,
  levels := .polymorphic
  pattern := #[.bvar 0, .bvar 1],
  -- `Key` fields
  subst := #[R, M],
  familyArity := 0,
}

-- class Small (α : Type*)
-- structure Subtype {α : Sort u} (p : α → Prop)
toKey ‹@Small (@Subtype α p)› = {
  -- `Vertex` fields
  name := `Small,
  levels := .polymorphic
  pattern := #[Subtype (.bvar 0)],
  -- `Key` fields
  subst := #[p],
  familyArity := 0,
}

-- class IsWellFounded (α : Type*) (r : α → α → Prop)
-- structure Submodule (R M : Type*) [Semiring R] [AddCommMonoid M] [Module R M]
toKey ‹@IsWellFounded (@Submodule α α inst₁ inst₂ inst₃) β› = {
  -- `Vertex` fields
  name := `IsWellFounded,
  levels := .polymorphic
  pattern := #[Submodule (.bvar 0) (.bvar 0), .bvar 1],
  -- `Key` fields
  subst := #[α, β]
  familyArity := 0,
}

Note how the class applications Small (Subtype p) and IsWellFounded (Submodule α α) β get indexed in the class graph in accordance with what keySlots returns for the type formers Subtype and Submodule, which are themselves not classes.

Equations

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

Reification

def GeneralizationLinter.reifyClass (name : Lean.Name) (vals : Array Lean.Expr) (useKeySlots : Bool := false) : Lean.MetaM (Option Lean.Expr)

Reifies a class name at the frame arguments frame into a valid Expr, wrapped as an Option (if name is not a constant defined in the environment, or if something else went wrong, then none is returned).

---

Example

Suppose the linter encountered the following declaration, and that Algebra could be weakened to Module within this declaration.

theorem thm.{w} {S : Type 0} {A : Type w} [CommSemiring S] [Semiring A] [Algebra S A] (x : A) : … := …

To know what exactly it'd be suggesting (e.g., so that it can verify said suggestion candidate), the linter needs to construct Module S A somehow — the weakened binder's type. To do this, it calls ReSynth.replBinderTypeFamilyAware with Algebra S A as an Expr and the Name `Module. This in turn then computes the frame #[S, A] of Algebra S A using frameArgs, and then calls reifyClass `Module #[S, A], which will output the Expr corresponding to Module S A (wrapped as an Option; if `Module were not a constant defined in the environment, or if something else went wrong, then reifyClass would return none).

Note that, in constructing its output, reifyClass may perform instance synthesis: in the `Module example, it's actually constructing @Module S A ?i₁ ?i₂, and finds ?i₁ and ?i₂ (instance metavariables spawned by reifyClassGo) via instance synthesis.

Equations

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

partial def GeneralizationLinter.elabPatternEntry (e : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Elaborate a pattern entry e.

Pattern entries can be applications, in which case subst won't tell us what the pattern entry is, but rather what its key arguments are.

def GeneralizationLinter.reify (name : Lean.Name) (pattern subst : Array Lean.Expr) : Lean.MetaM (Option Lean.Expr)

The inverse of toKey for non-family class binders. Reifies the class name by instantiating the pattern of its key with the concrete values provided by subst, each elaborated #TODO, and then inferring the non-key-slots of name. Returns none if pattern needs more values than subst provides, or if elaboration or inference failed at any point.

Equations

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

def GeneralizationLinter.withGenericKey {α : Type} (name : Lean.Name) (k : Lean.Expr → Lean.MetaM (Option α)) : Lean.MetaM (Option α)

Run the continuation k on the "generic" application name.{…} a₁ … aₙ of n-ary class name on fresh local hypotheses a₁, …, aₙ.

For motivation, see isSubsingletonClass.

Equations

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