Verification of redecoration for infinite triangular matrices in Coq

Celia Picard

Institut de Recherche en Informatique de Toulouse
Université Paul Sabatier (Toulouse 3)

Thursday, 13 September 2012, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101

Slides from the talk [pdf]

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. Both kinds of families are fully supported since the version 8.1 of the Coq theorem proving environment, released in 2007.

Still today, reasoning about nested coinductive types in Coq constantly faces challenges due to the guardedness condition that imposes syntactic conditions on otherwise well-defined corecursive definitions and proofs. In this talk, we concentrate on results that could smoothly be obtained by rather modest generalizations of the statements that could not directly be proven by coinduction.

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

We then validate the original algorithm against another visualization of the triangles, provably equivalent to the first one. It is then 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.

(Joint work with Ralph Matthes.)

Celia Picard's visit to Tallinn is supported by the ETF/Egide Parrot programme.

Tarmo Uustalu
Last update 19.9.2012