Simplifying Casts and Coercions
Programming Languages
2020-04-30 v2
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.
Keywords
Cite
@article{arxiv.2001.10594,
title = {Simplifying Casts and Coercions},
author = {Robert Y. Lewis and Paul-Nicolas Madelaine},
journal= {arXiv preprint arXiv:2001.10594},
year = {2020}
}