Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Sun 17 Jan 2021 17:00 - 17:15 at CPP - Proof Tactics Chair(s): Jesper Cockx

In theorem provers based on dependent type theory such as Coq and Lean, induction is a fundamental proof method and induction tactics are omnipresent in proof scripts. Yet 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, which addresses these issues. The tactic is particularly suitable for educational use, but experts should also find it more convenient than existing induction tactics. In addition, the tactic serves as a moderately complex case study for the metaprogramming framework of Lean 3. The paper describes some difficulties encountered during the implementation and suggests improvements to the framework.

Sun 17 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

17:00 - 17:30
Proof TacticsCPP at CPP
Chair(s): Jesper CockxTU Delft

Streamed session: https://youtu.be/PAxUO84tUE8?t=3781

A Novice-Friendly Induction Tactic for Lean
Jannis LimpergVrije Universiteit Amsterdam
Pre-print Media Attached
Lassie: HOL4 Tactics by Example
Heiko BeckerMPI-SWS, Nathaniel BosMcGill University, Ivan GavranMPI-SWS, Eva DarulovaMPI-SWS, Rupak MajumdarMPI-SWS
Pre-print Media Attached File Attached