Simplifying Casts and Coercions

TL;DR

This paper presents norm_cast, a set of tactics for the Lean proof assistant that simplifies reasoning about coercions and casts, reducing boilerplate and improving proof automation.

Contribution

It introduces norm_cast tactics that effectively manipulate coercions and casts in Lean, enhancing proof development and library maintenance.

Findings

norm_cast reduces boilerplate in Lean proofs

It improves unification and rewriting involving coercions

The tactics are widely used in Lean mathematical libraries

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.