← All papers
Automatically Generalizing Theorems Using Typeclasses
cs.LO
Aug 1, 2021 · v1
TL;DR
Develops a Lean metaprogram to detect and suggest generalizations of typeclass assumptions in proofs.
Abstract
When typeclass assumptions in formally verified mathematical developments are stronger than necessary, this can be detected from elaborated proof terms. This paper introduces a metaprogram for the Lean theorem prover that finds and informs the user about possible generalizations of theorems by analyzing typeclass usage in proofs.
Problem
Typeclass assumptions in formal mathematical developments are often stronger than necessary, but detecting such over-constraining manually is tedious and error-prone.
Approach
The paper introduces a metaprogram for Lean that analyzes elaborated proof terms to detect when typeclass assumptions are stronger than needed. By examining which typeclass instances are actually used in proofs, the tool identifies possible generalizations of theorems automatically.
Results
The metaprogram finds and reports possible generalizations of theorems by analyzing typeclass usage, enabling users to weaken hypotheses and broaden the applicability of formalized results.