Reviewer #1: This paper demonstrates that a) the Myhill-Nerode theorem can be
proved without relying on the notion of automata and b) argues
shallowly thorough the paper that not having to formalize the notion
of automata is easier.

While I do agree that point a) is a an interesting theoretical
contribution that deserves publication, I disagree with the second
argument.

It should be noted that the handling of the notion of automata has
been difficult historically for two reasons. On the one hand, giving
an identifier to every state of an automata indeed yields proofs that
may be characterized as "clunky" (even if the wording is a bit
strong), but is a necessary condition for efficient implementation of
automata algorithms. This yields sizable formalizations as is
demonstrated by the Lammich and Tuerk's work or Braibant and Pous's
work [1]. On the other hand, it seems to be the case that the
"principle of definition" in HOL makes it impossible to use parametric
definitions of automata (but there is no problem with such a
definition in Coq).

But, the startup cost of a formalization depends on the scope of what
one intends to formalize. Perhaps Braibant concedes that your
development is more concise that his, yet Braibant's work dealt with
the formalization of an _efficient_ decision procedure for Kleene
algebras that required _two_ formalizations of automata (the matrices
are only used in the proof of correctness of this decision procedure,
while the computational part uses efficient representations for DAGs
-- see for instance [1] p. 21 or Braibant's thesis p. 49). I am only
adding emphasis here to demonstrate that this does not compare easily
with the formalization of the proof of Myhill-Nerode by itself.

(At this point, let me comment on your answer: "As far as we know
Braibant also uses ssreflect".  It is not the case. One may wonder to
what extent the use of ssreflect there could have alleviated the
"intrinsic difficulties of working with rectangular matrices".)

In the same fashion, Lammich and Tuerk's work uses efficient
data-structures (.e.g, for collections, automatas), and some amount of
data-refinement to link various representations together. 

My most stringent remark about the paper is that it should make clear
from the beginning whether or not the algorithms are computational,
and if they are executable, how efficient. Then, comparing with the
two aforementioned work will make sense. 

In fact, I have been made aware of the following work [2] that do
formalize automata and regular language theory without using explicit
identifiers for state numbers in automata. The upside is that it
yields much smoother proofs than previous works in Coq. The downside
is that this formalization strategy does not yield efficient algorithm
for automata constructions. I reckon that this is a technical report
that should be taken with a grain of salt in the context of this
review, but I think that it gives evidence that it is not always the
case that the startup cost is higher with automata rather than with
regular expressions: they formalize the Myhill-Nerode theorem,
Kleene's theorem, the relationships between various representations of
regular languages in around 1500 lines of ssreflect/Coq. (Again, let
me emphasize that this is not a computational representation of
automata, and thus, it does not easily compare in terms of size with
Lammich and Tuerk's work or Braibant and Pous's work.) I think this
work would make for a much more relevant comparison with your work. 

I agree that comparing with related work is hard, and that the authors
have already been careful in their comparison with the formalization
sizes from other works. Yet, I am afraid an uninformed outsider would
miss the distinction between related work that are executable and
efficient and this formalization. 


Minor comments about the paper
==============================

- I am still confused about the explanation about the way the
equational system is set up (your comment in the conclusion does not
help me to pinpoint why you have to do that): I understand that
Brzozowski annotates the final states with lambdas, and propagates
them to the unique initial state. On the other hand you start with a
set of equivalence classes, and you want to compute a regular
expression for all classes that are in finals. In other words, I still
fail to see why the following system does not suit your needs

X1 = a,X2 + b,X4 
X2 = b,X3 + a,X4 + lambda(ONE)
X3 = a,X4 + b,X4 + lambda(ONE)
X4 = a,X4 + b,X4

with L(r,X) = L(r) \cdot X

and then propagate the equation to compute to compute a value for
X1. (And, you could draw the automata underlying the transitions at
the top of p. 7 to help the reader understand what is going on, and
the relationship with the current equational system.)

Maybe it is simply that you could have done it, but that it would have
been less pleasant to work with in the context of a Myhill-Nerode
relation?

- I really appreciate the rephrasing of section 4, especially the
final remark. I think it clearly helps the reader to understand the
proof arguments, and the relationship with automata. 

- I concur with the second reviewer to say that the executability of
the first half of the M-N theorem should be discussed in the
conclusion. Moreover, I am puzzled by your comments in the response to
reviewers: to what extent does your formalization need to be
_modified_ to make it executable? Do you need to change the code, or
to add more things? (More precisely, you discuss the executability of
the second half of the M-N theorem -- that constructs a partition of
the set of strings -- in the conclusion, in the context of Haftmann
executable sets; you should do the same for the first-half---that
constructs a regular expression). I am not sure I am happy with the
things you wrote about executable sets, because it is not clear from
my point of view if you need to modify the code, or add things. 

- More generally, it should be made clear that when you say algorithm,
the reader should not understand it as something that is computable as
it is. In particular, I think that the following sentence is
misleading: "our algorithm for solving equational systems actually
calculates a regular expression for the complement language." You
actually define such an expression, but it seems not possible, as it
is, to open the box to see what is inside.

- You answered: 

> In our opinion, Coquand and Siles' development strongly justifies our
> comment about formalisation of Brzozowski's argument being painful.
> If you like to have this reference added in the paper, we are happy
> to do so.

I think that it is worth adding a comment like this one either in
section 5 (at the beginning of p. 20) or in the conclusion.

- There are still some spell-checking mistakes in the paper, e.g.,
  "refular" p. 26, and 

- The authors provide a detailed figure for the number of line of code
  of Almeida et al's implementation of Mirkin construction, but there
  is no such figure for some of other works that are cited. Maybe this
  number could be dropped, or similar figures could be given for other
  works, in order to give a more accurate picture.

- I wonder if you have direction for future works, that would satisfy
  your predicate "results from regular language theory, not results
  from automata theory". It would be nice to give a few examples if
  you have some in mind. 



[1] Deciding Kleene algebras in Coq, Thomas Braibant, Damien Pous
http://dx.doi.org/10.2168/LMCS-8(1:16)2012

[2] A Constructive Theory of Regular Languages in Coq, Christian
Doczkal and Jan-Oliver Kaiser and Gert Smolka
http://www.ps.uni-saarland.de/Publications/details/DoczkalEtAl:2013:A-Constructive.html