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.
@article{8124,
title = {Formalization Techniques for Asymptotic Reasoning in Classical Analysis},
journal = {Journal of Formalized Reasoning},
volume = {11},
year = {2018},
doi = {10.6092/issn.1972-5787/8124},
language = {EN},
url = {http://dml.mathdoc.fr/item/8124}
}
Affeldt, Reynald; Cohen, Cyril; Rouhling, Damien. Formalization Techniques for Asymptotic Reasoning in Classical Analysis. Journal of Formalized Reasoning, Tome 11 (2018) . doi : 10.6092/issn.1972-5787/8124. http://gdmltest.u-ga.fr/item/8124/