Technical Report: DCC-2011-06

Deciding Regular Expressions (In-)Equivalence in Coq

Nelma Moreira

CMUP & DCC-FC, Universidade do Porto

David Pereira

LIACC & DCC-FC, Universidade do Porto

SiMão Melo de Sousa

LIACC & DI -- Universidade da Beira Interior
November 2011


In this paper we present a mechanically verified implementation of an algorithm for deciding regular expression (in-)equivalence within the COQ proof assistant. This algorithm is a version of a functional algorithm proposed by Almeida et al. which decides regular expression equivalence through an iterated process of testing the equivalence of their partial derivatives. In particular, this algorithm has a refutation step which improves the process of checking if two regular expressions are not equivalent.