Anzeige
Erschienen in:
2008 | OriginalPaper | Buchkapitel
Canonical Big Operators
verfasst von : Yves Bertot, Georges Gonthier, Sidi Ould Biha, Ioana Pasca
Erschienen in: Theorem Proving in Higher Order Logics
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
In this paper, we present an approach to describe uniformly iterated “big” operations, like
$\sum_{i=0}^n f(i)$
or max
i
∈
I
f
(
i
) and to provide lemmas that encapsulate all the commonly used reasoning steps on these constructs.
We show that these iterated operations can be handled generically using the syntactic notation and canonical structure facilities provided by the
Coq
system. We then show how these canonical big operations played a crucial enabling role in the study of various parts of linear algebra and multi-dimensional real analysis, as illustrated by the formal proofs of the properties of determinants, of the Cayley-Hamilton theorem and of Kantorovitch’s theorem.