Verification of redecoration for infinite triangular matrices using coinduction

Abstract

Finite triangular matrices with a dedicated type for the diagonal
elements can be profitably represented by a nested data type, i. e., a
heterogeneous family of inductive data types, while infinite
triangular matrices form an example of a nested coinductive type,
which is a heterogeneous family of coinductive data types. 

Redecoration for infinite triangular matrices is taken up from
previous work involving the first author, and it is shown that
redecoration forms a comonad with respect to bisimilarity.

The main result, however, is a validation of the original algorithm
against a model based on infinite streams of infinite streams. The
two formulations are even provably equivalent, and the second is
identified as a special instance of the generic cobind operation
resulting from the well-known comultiplication operation on streams
that creates the stream of successive tails of a given stream. Thus,
perhaps surprisingly, the verification of redecoration is easier for
infinite triangular matrices than for their finite counterpart.

All the results have been obtained and are fully formalized in the
current version of the Coq theorem proving environment where these
coinductive datatypes are fully supported since the version 8.1,
released in 2007.  Nonetheless, instead of displaying the Coq
development, we have chosen to write the paper in standard
mathematical and type-theoretic language. Thus, it should be
accessible without any specific knowledge about Coq.