← All papers
Simplifying Casts and Coercions
cs.PL
Jan 28, 2020 · v2
TL;DR
Introduces the norm_cast tactic toolbox for handling coercions and casts in Lean.
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.
Problem
Expressions containing coercions and casts in Lean cause seemingly identical expressions to fail to unify and rewrites to fail, frustrating both beginning and expert users.
Approach
The authors introduce norm_cast, a toolbox of tactics for the Lean proof assistant that manipulates expressions containing coercions and casts. The tactics normalize cast expressions so that reasoning with coerced types becomes transparent, eliminating boilerplate arguments.
Results
The norm_cast tactics are used extensively in the Lean mathematical library (Mathlib) and external developments to eliminate boilerplate cast-related arguments, making proofs involving type coercions significantly more readable and maintainable.