Showing 1–1 of 1 results for author: Madelaine, P

Simplifying Casts and Coercions

Authors: Robert Y. Lewis, Paul-Nicolas Madelaine

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… ▽ More 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. △ Less

Submitted 29 April, 2020; v1 submitted 28 January, 2020; originally announced January 2020.