Download PDFOpen PDF in browser

Automatically Generalizing Theorems Using Typeclasses

EasyChair Preprint 6216

6 pagesDate: August 1, 2021

Abstract

When producing large formally verified mathematical developments that make use of typeclasses it is easy to introduce overly strong assumptions for theorems and definitions. We consider the problem of recognizing from the elaborated proof terms when typeclass assumptions are stronger than necessary. We introduce a metaprogram for the Lean theorem prover that finds and informs the user about possible generalizations.

Keyphrases: Automation, Lean theorem prover, formal proof, interactive theorem prover, library maintainence, theorem prover, typeclasses

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@booklet{EasyChair:6216,
  author    = {Alexander Best},
  title     = {Automatically Generalizing Theorems Using Typeclasses},
  howpublished = {EasyChair Preprint 6216},
  year      = {EasyChair, 2021}}
Download PDFOpen PDF in browser