A constructive and formal proof of Lebesgue’s Dominated Convergence Theorem in the interactive theorem prover Matita

Claudio Sacerdoti Coen, Enrico Tassi

Abstract


We present a formalisation of a constructive proof of Lebesgue’s Dominated Convergence Theorem given by the Sacerdoti Coen and Zoli in [CSCZ]. The proof is done in the abstract setting of ordered uniformities, also introduced by the two authors as a simplification of Weber’s lattice uniformities given in [Web91, Web93]. The proof is fully constructive, in the sense that it is done in Bishop’s style and, under certain assumptions, it is also fully predicative. The formalisation is done in the Calculus of (Co)Inductive Constructions using the interactive theorem prover Matita [ASTZ07]. It exploits some peculiar features of Matita and an advanced technique to represent algebraic hierarchies previously introduced by the authors in [ST07]. Moreover, we introduce a new technique to cope with duality to halve the formalisation effort.

Full Text:

PDF (English)


DOI: 10.6092/issn.1972-5787/1334

Copyright (c) 2008 Claudio Sacerdoti Coen, Enrico Tassi

Creative Commons License
This work is licensed under a Creative Commons Attribution 3.0 Unported License.