Verifying an algorithm computing Discrete Vector Fields for digital imaging

TL;DR

This paper formalizes an algorithm for constructing admissible discrete vector fields within the Coq proof assistant, enabling homological analysis of digital images that was previously infeasible.

Contribution

It introduces a formalized algorithm in Coq for discrete vector fields, enhancing the capability to analyze digital images' homological properties.

Findings

Successfully formalized the algorithm in Coq using SSReflect

Enabled homological analysis of biomedical images within Coq

Reduced information in digital images while preserving homological features

Abstract

In this paper, we present a formalization of an algorithm to construct admissible discrete vector fields in the Coq theorem prover taking advantage of the SSReflect library. Discrete vector fields are a tool which has been welcomed in the homological analysis of digital images since it provides a procedure to reduce the amount of information but preserving the homological properties. In particular, thanks to discrete vector fields, we are able to compute, inside Coq, homological properties of biomedical images which otherwise are out of the reach of this system.