← All papers
A Novice-Friendly Induction Tactic for Lean
cs.LO
Dec 16, 2020 · v1
TL;DR
Implements a new induction tactic in Lean 3 that improves hypothesis generation and naming.
Abstract
Induction is the primary proof technique for inductive types and for inductive predicates and relations defined on top of them. In dependently-typed theorem provers such as Coq and Lean, the ergonomics of existing induction tactics are not ideal: they do not reliably support inductive predicates and relations; they sometimes generate overly specific or unnecessarily complex induction hypotheses; and they occasionally choose confusing names for the hypotheses they introduce. This paper describes a new induction tactic implemented in Lean 3 that addresses these issues. It is particularly suitable for educational use, but experts should also find it more convenient than existing induction tactics. As a moderately complex case study for the metaprogramming framework of Lean 3, the paper also describes implementation difficulties and suggests improvements to the framework.
Problem
Existing induction tactics in dependently-typed theorem provers like Lean do not reliably support inductive predicates and relations, sometimes generate overly specific induction hypotheses, and choose confusing names for introduced hypotheses.
Approach
A new induction tactic is implemented in Lean 3 that addresses these ergonomic issues. It reliably handles inductive predicates and relations, produces clearer induction hypotheses, and generates meaningful names for introduced variables and hypotheses. The tactic is designed to be novice-friendly.
Results
The tactic improves the experience for new Lean users working with inductive types, predicates, and relations by producing more intuitive proof states with better-named hypotheses.