Sciweavers

TPHOL
2008
IEEE

Canonical Big Operators

13 years 10 months ago
Canonical Big Operators
In this paper, we present an approach to describe uniformly iterated “big” operations, like Pn i=0 f(i) or maxi∈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.
Yves Bertot, Georges Gonthier, Sidi Ould Biha, Ioa
Added 01 Jun 2010
Updated 01 Jun 2010
Type Conference
Year 2008
Where TPHOL
Authors Yves Bertot, Georges Gonthier, Sidi Ould Biha, Ioana Pasca
Comments (0)