← All papers
Arithmetic and Casting in Lean
cs.LO
Aug 1, 2019 · v1
TL;DR
Develops a Lean tactic for automated reasoning about arithmetic with numeric type coercions.
Abstract
This report describes a Lean metaprogram for automatically solving arithmetic goals involving casts between numeric types. The tool normalizes expressions involving coercions between naturals, integers, and rationals, and discharges side conditions. It addresses a practical pain point in Lean formalization where type casts create verification obligations that are tedious to prove manually.
Problem
Type casts between numeric types (naturals, integers, rationals) in Lean create verification obligations that are tedious to prove manually, impeding practical formalization work.
Approach
The author develops a Lean metaprogram that automatically solves arithmetic goals involving casts between numeric types. The tool normalizes expressions involving coercions between naturals, integers, and rationals and discharges the resulting side conditions.
Results
The metaprogram addresses a practical pain point in Lean formalization by automating cast-related proof obligations that previously required manual intervention.