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.
Liste complète des métadonnées

https://hal.inria.fr/hal-01719918
Contributor : Cyril Cohen <>
Submitted on : Tuesday, October 30, 2018 - 6:52:29 AM
Last modification on : Wednesday, October 31, 2018 - 1:15:08 AM
Document(s) archivé(s) le : Thursday, January 31, 2019 - 12:29:44 PM

File

8124-27375-1-PB.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01719918, version 3

Collections

Citation

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

Share

Metrics

Record views

82

Files downloads

53