A Coq tool for proof automation of bounded arithmetical inequalities

After facing the frequent practical problem of bounding an arithmetical expression (for instance, to prove that overflow will not occur) and experiencing the intrinsic difficulties of proving such inequalities using mathematical arguments inside Coq, the team was able to develop a tool for automating this kind of task. In particular, the tool instructs Coq to the extent that it can compute all the cases and check that the inequality holds for each of them, and thus deduce that the inequality holds in general. This tool is developed for inequalities on types Int63 and Sint63, and is planned to be released for other Coq types.

Related