Proofs by induction in equational theories with constructors

Abstract

We show how to prove (and disprove) theorems in the initial algebra of an equational variety by a simple extension of the Knuth-Bendix completion algorithm. This allows us to prove by purely equational reasoning theorems whose proof usually requires induction. We show applications of this method to proofs of programs computing over data structures, and to proofs of algebraic summation identities. This work extends and simplifies recent results of Musser15 and Goguen6.