Re-synthesize weakened binders

def GeneralizationLinter.getNthTargetedBinder (fvars : Array Lean.Expr) (n : Nat) : Lean.MetaM (Option (Nat × Lean.Expr))

Among an array fvars of .fvar expressions, find the nth entry that corresponds to a TargetedBinder. This checks the local context to see how each fvar in fvars was declared, and returns some i binder if the nth targeted binder is the fvar binder, and binder = fvars[i]. It returns none if there is no nth targeted binder in fvars.

Equations

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

def GeneralizationLinter.replacementsRedundant (type : Lean.Expr) (binderIdx : Nat) (repls : Array Vertex) : Lean.MetaM Bool

Returns true iff every repl[i]'s class is already synthesizable from the other binders (the ones not being replaced).

Equations

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

def GeneralizationLinter.verifyWeakening (ciType val : Lean.Expr) (n : Nat) (repls : Array Vertex) : Lean.MetaM Bool

Verify that, if we replace the nth targeted binder in ciType with binders for repls, the value (usually a proof term) val can be re-synthesized in the weakened context. If so, returns true; otherwise, returns false.

---

Implementation notes

verifyWeakening … does not imply (recompiledAgainst? …).isSome, nor the other way around:

verifyW…	recompiledA…	% of cands	WeakeningGrade
true	true	≈?%	WeakeningGrade.proofIntact
true	false	≈?%	WeakeningGrade.needsModification
false	true	≈0%	WeakeningGrade.proofIntact
false	false	≈?%	N/A; weakening is not valid

For example, the weakening candidate [Group G] ↝ [MulOneClass M] demonstrates each possible case through the four theorems below (note that, for theorem ff, the candidate wouldn't have been generated in the first place):

variable {G : Type} [inst : Group G] (a : G)
theorem tt : a * 1 = a := mul_one a
theorem tf : a * 1 = a := @mul_one G inst.toDivInvMonoid.toMonoid.toMulOneClass a
theorem ft : a * 1 = a := by first | exact tt | exact mul_one a

class A (α : Type) where
class B (α : Type) where n : Nat
instance A.toB {α : Type} [A α] : B α := ⟨42⟩
theorem ff {α : Type} [A α] : B.n α = 42 := rfl

Equations

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

def GeneralizationLinter.weakenedStatementType (const : Lean.ConstantInfo) (ws : Array (Nat × Array Vertex)) : Lean.MetaM (Option Lean.Expr)

Given a statement with constant info const, returns the type of said statement after weakening, for each (n, repls) in ws, the nth targeted binder of the statement with binders for repls.

Equations

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