TY - JOUR
AU - Affeldt, Reynald
AU - Cohen, Cyril
AU - Rouhling, Damien
PY - 2018/01/01
Y2 - 2024/02/27
TI - Formalization Techniques for Asymptotic Reasoning in Classical Analysis
JF - Journal of Formalized Reasoning
JA - JFR
VL - 11
IS - 1
SE - Articles
DO - 10.6092/issn.1972-5787/8124
UR - https://jfr.unibo.it/article/view/8124
SP - 43 - 76
AB - Formalizing analysis on a computer involves a lot of “epsilon-delta” reasoning, while informal reasoning may use some asymptotical hand-waving. Whether or not the arithmetic details are hidden using some abstraction like filters, a human user eventually has to break it down for the proof assistant anyway, and provide a witness for the existential variable “delta”. We describe formalization techniques that take advantage of existential variables to delay the input of witnesses until a stage where the proof assistant can actually infer them. We use these techniques to prove theorems about classical analysis and to provide equational Bachmann-Landau notations. This partially restores the simplicity of informal hand-waving without compromising the proof. As expected this also reduces the size of proof scripts and the time to write them, and it also makes proofs more stable.
ER -