Computing in Coq with Infinite Algebraic Data Structures

TL;DR

This paper explores using Coq's constructive type theory to perform computations on infinite algebraic data structures, specifically chain complexes, for formalizing homological algebra.

Contribution

It introduces a method for representing and computing with infinite algebraic structures within Coq's proof environment.

Findings

Demonstrates formalization of infinite chain complexes in Coq

Shows feasibility of computational experiments with infinite data structures

Contributes to formalized homological algebra in proof assistants

Abstract

Computational content encoded into constructive type theory proofs can be used to make computing experiments over concrete data structures. In this paper, we explore this possibility when working in Coq with chain complexes of infinite type (that is to say, generated by infinite sets) as a part of the formalization of a hierarchy of homological algebra structures.