Technical Report: DCC-2011-06

Deciding Regular Expressions (In-)Equivalence in Coq

Nelma Moreira

CMUP & DCC-FC, Universidade do Porto
e-mail: nam@dcc.fc.up.pt

David Pereira

LIACC & DCC-FC, Universidade do Porto
e-mail: dpereira@ncc.up.pt

SiMão Melo de Sousa

LIACC & DI -- Universidade da Beira Interior
e-mail:desousa@di.ubi.pt
November 2011

Abstract

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.