Skip to Main content Skip to Navigation
Journal articles

Formalization Techniques for Asymptotic Reasoning in Classical Analysis

Abstract : 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.
Complete list of metadata

Cited literature [40 references]  Display  Hide  Download
Contributor : Cyril Cohen Connect in order to contact the contributor
Submitted on : Tuesday, October 30, 2018 - 6:52:29 AM
Last modification on : Thursday, January 20, 2022 - 5:30:44 PM
Long-term archiving on: : Thursday, January 31, 2019 - 12:29:44 PM


Files produced by the author(s)


  • HAL Id : hal-01719918, version 3



Reynald Affeldt, Cyril Cohen, Damien Rouhling. Formalization Techniques for Asymptotic Reasoning in Classical Analysis. Journal of Formalized Reasoning, ASDD-AlmaDL, 2018. ⟨hal-01719918v3⟩



Les métriques sont temporairement indisponibles