Abstract
This paper introduces norm_cast, a toolbox of tactics for the Lean proof assistant designed to manipulate expressions containing coercions and casts. These expressions can be frustrating for beginning and expert users alike; the presence of coercions can cause seemingly identical expressions to fail to unify and rewrites to fail. The norm_cast tactics aim to make reasoning with such expressions as transparent as possible. They are used extensively to eliminate boilerplate arguments in the Lean mathematical library and in external developments.
| Original language | English |
|---|---|
| Title of host publication | PAAR+SC-Square 2020 Practical Aspects of Automated Reasoning and Satisfiability Checking and Symbolic Computation Workshop 2020 |
| Subtitle of host publication | Joint Proceedings of the 7th Workshop on Practical Aspects of Automated Reasoning (PAAR) and the 5th Satisfiability Checking and Symbolic Computation Workshop (SC-Square) Workshop, 2020 co-located with the 10th International Joint Conference on Automated Reasoning (IJCAR 2020) Paris, France, June-July, 2020 (Virtual) |
| Editors | Pascal Fontaine, Konstantin Korovin, Ilias S. Kotsireas, Philipp Rümmer, Sophie Tourret |
| Publisher | CEUR-WS |
| Pages | 53-62 |
| Number of pages | 10 |
| Publication status | Published - 26 Nov 2020 |
| Event | Joint of the 7th Workshop on Practical Aspects of Automated Reasoning and the 5th Satisfiability Checking and Symbolic Computation Workshop, PAAR+SC-Square 2020 - Virtual, Paris, France Duration: 5 Jul 2020 → … |
Publication series
| Name | CEUR Workshop Proceedings |
|---|---|
| Publisher | CEUR Workshop Proceedings |
| Volume | 2752 |
| ISSN (Print) | 1613-0073 |
Conference
| Conference | Joint of the 7th Workshop on Practical Aspects of Automated Reasoning and the 5th Satisfiability Checking and Symbolic Computation Workshop, PAAR+SC-Square 2020 |
|---|---|
| Country/Territory | France |
| City | Virtual, Paris |
| Period | 5/07/20 → … |
Funding
We acknowledge support from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation program (grant agreement No. 713999, Matryoshka) and from the Dutch Research Council (NWO) under the Vidi program (project No. 016.Vidi.189.037, Lean Forward).
Keywords
- Cast
- Coercion
- Formal proof
- Lean
