Induction and Co-Induction in Sparkle

 

Leonard Lensink, Marko van Eekelen

 

Abstract:

Sparkle is a proof assistant designed for the lazy functional programming language Clean.

It is designed to facilitate proofs of first order logical predicates on existing and newly written programs.

In order to achieve this it is of the utmost importance that the proof system is easy to use and integrated into the IDE.

The implementation of Sparkle only has a basic induction principle so far.

For many programs and complex proofs this will not suffice.

To address this issue we have expanded Sparkle with several induction and co-induction proof techniques for mutually recursive functions and data types.

By providing examples of proofs on programs, taken from various research papers, we show how the programmer can benefit from these added tactics.

With our extensions Sparkle can be used to prove properties of a wide class of programs.