Re-synthesize weakened binders

def GeneralizationLinter.replaceBinderType? (oldType : Lean.Expr) (replacement : Vertex) : Lean.MetaM (Option Lean.Expr)

Wrapper around mkClassApp? / reifyKey? that adds support for parametric class binders.

---

Examples

-- M = ⟨`MulOneClass, #[#0], .polymorphic⟩
replaceBinderType? ‹Group G› M = some ‹MulOneClass G›
replaceBinderType? ‹∀ i : ι, Group (f i)› M = some ‹∀ i : ι, MulOneClass (f i)›
replaceBinderType? ‹Group G› ⟨`Pow, #[#0, #1], .polymorphic⟩ = none

Equations

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

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 (0-indexed) 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.

---

Examples

-- theorem tt {G : Type} [inst : Group G] (a : G) : a * 1 = a
getNthTargetedBinder? #[‹G›, ‹inst›, ‹a›] 0 = some (1, ‹inst›)
getNthTargetedBinder? #[‹G›, ‹inst›, ‹a›] 1 = none

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 repls[i]'s class is already synthesizable from the other binders (the ones not being replaced).

---

Examples

-- type = ‹∀ {G : Type} [Group G] [Semigroup G], True›, S = ⟨`Semigroup, #[#0], .polymorphic⟩
replacementsRedundant type 1 #[S] = true
replacementsRedundant type 0 #[⟨`Monoid, #[#0], .polymorphic⟩] = false
replacementsRedundant type 1 #[] = true
replacementsRedundant type 2 #[S] = false

Equations

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

def GeneralizationLinter.weakeningResynthesizable (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

weakeningResynthesizable … does not imply (recompiledAgainst? …).isSome, nor the other way around: For example, the weakening candidate [Group G] ↝ [MulOneClass G] demonstrates three of the possible cases through the three theorems below:

variable {G : Type} [inst : Group G] (a : G)
-- `weakeningResynthesizable` returns `true`, `(recompiledAgainst? …).isSome` returns `true`
theorem tt : a * 1 = a := mul_one a
-- `weakeningResynthesizable` returns `true`, `(recompiledAgainst? …).isSome` returns `false`
theorem tf : a * 1 = a := @mul_one G inst.toDivInvMonoid.toMonoid.toMulOneClass a
-- `weakeningResynthesizable` returns `false`, `(recompiledAgainst? …).isSome` returns `true`
theorem ft : a * 1 = a := by first | exact tt a | exact mul_one a

The remaining case is demonstrated by the following example:

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

-- `weakeningResynthesizable` returns `false`, `(recompiledAgainst? …).isSome` returns `false`
theorem ff {α : Type} [A α] : B.n α = 42 := rfl

Note: We only actually call weakeningResynthesizable in the following two cases:

• redundancyGuard := true (its default) and reshapeRedundantToDrops wants to verify whether dropping a seemingly redundant binder is safe.
• recompiledAgainst? returned none and no candidate has been accepted yet (since weakeningResynthesizable replaces only one binder, and two binder weakenings individually being resynthesizable does not guarantee that they'd be resynthesizable jointly. In principle, nothing would prevent us from implementing a joint resynthesizability check, but we'd be adding complexity for very small gains).

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.

---

Examples

-- theorem tt {G : Type} [inst : Group G] (a : G) : a * 1 = a; below, `tt` is its `ConstantInfo`
-- M = ⟨`MulOneClass, #[#0], .polymorphic⟩, S = ⟨`Semigroup, #[#0], .polymorphic⟩
weakenedStatementType? tt #[(0, #[M])] = some ‹∀ {G} [inst : MulOneClass G] (a : G), a * 1 = a›
weakenedStatementType? tt #[] = some ‹∀ {G} [inst : Group G] (a : G), a * 1 = a›
weakenedStatementType? tt #[(0, #[S])] = none

Equations

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