AutoGeneralization

AutoGeneralization finds weaker, kernel-checked type class assumptions for Lean theorems.

Install

Add the package to your project's lakefile.toml:

[[require]]
name = "AutoGeneralization"
git = "https://github.com/pelicanhere/AutoGeneralization"
rev = "master"

Then run:

lake update AutoGeneralization

Use

import AutoGeneralization

#autogeneralize theoremName
#autogeneralize! theoremName
#lint only generalizeTypeClass

#autogeneralize proposes one-step generalizations, while #autogeneralize! repeats until the signature stops changing. Apply a command's code action to insert the generated theorem.

To analyze an imported theorem, use import all Module.Name.

Examples

Registered instance conversions can expose weaker assumptions:

import Mathlib.RingTheory.Coprime.Basic
import AutoGeneralization

theorem coprimeIffOverField {R : Type*} [Field R] {m n : R} :
    IsCoprime m n ↔ m ≠ 0 ∨ n ≠ 0 :=
  Semifield.isCoprime_iff

#autogeneralize coprimeIffOverField
-- [Field R] → [Semifield R]

Evidence stored by a retained class is re-synthesized after generalization:

import Mathlib.Algebra.Star.SelfAdjoint
import AutoGeneralization

theorem selfAdjointDivOverField {R : Type*} [Field R] [StarRing R] {x y : R}
    (hx : IsSelfAdjoint x) (hy : IsSelfAdjoint y) : IsSelfAdjoint (x / y) :=
  IsSelfAdjoint.div hx hy

#autogeneralize selfAdjointDivOverField
-- [Field R] → [Semifield R], retaining [StarRing R]

One class can split into several independent capabilities:

import Mathlib.Data.Prod.Lex
import AutoGeneralization

open Prod

theorem lexicographicSelf {α : Type} [Preorder α] {x y : α × α} :
    toLex x ≤ toLex y ↔ x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 ≤ y.2 :=
  Prod.Lex.toLex_le_toLex

#autogeneralize lexicographicSelf
-- [Preorder α] → [LT α] [LE α]

#autogeneralize! applies every available step:

import Mathlib.Topology.Algebra.Group.Basic
import AutoGeneralization

open Set Topology

theorem topologicalInvComponent {G : Type} [TopologicalSpace G] [Group G]
    [IsTopologicalGroup G] {g : G} (hg : g ∈ connectedComponent (1 : G)) :
    g⁻¹ ∈ connectedComponent (1 : G) :=
  inv_mem_connectedComponent_one hg

#autogeneralize! topologicalInvComponent
-- [IsTopologicalGroup G] → [ContinuousInv G]
-- [Group G] → [DivisionMonoid G]

See AutoGeneralizationTest/Examples.lean for checked examples and docs/ALGORITHM.md for the algorithm.

Development

lake test