1730 @{text "A"} to @{term "lang r"} and thus complete the proof.\qed |
1730 @{text "A"} to @{term "lang r"} and thus complete the proof.\qed |
1731 \end{proof} |
1731 \end{proof} |
1732 |
1732 |
1733 \begin{rmk} |
1733 \begin{rmk} |
1734 While our proof using tagging functions might seem like a rabbit pulled |
1734 While our proof using tagging functions might seem like a rabbit pulled |
1735 out of a hat, the intuition behind can be somewhat rationalised taking the |
1735 out of a hat, the intuition behind can be somewhat rationalised by taking the |
1736 view that the equivalence classes @{term "UNIV // \<approx>(lang r)"} stand for the |
1736 view that the equivalence classes @{term "UNIV // \<approx>(lang r)"} stand for the |
1737 states of the minimal automaton for the language @{term "lang r"}. The theorem |
1737 states of the minimal automaton for the language @{term "lang r"}. The theorem |
1738 amounts to showing that this minimal automaton has finitely many states. |
1738 amounts to showing that this minimal automaton has finitely many states. |
1739 However, by showing that our @{text "\<^raw:$\threesim$>\<^bsub>tag\<^esub>"} relation |
1739 However, by showing that our @{text "\<^raw:$\threesim$>\<^bsub>tag\<^esub>"} relation |
1740 refines @{term "\<approx>A"} we do not actually have to show that the minimal automata |
1740 refines @{term "\<approx>A"} we do not actually have to show that the minimal automata |
2644 expression using partial derivatives. This took approximately 10600 |
2644 expression using partial derivatives. This took approximately 10600 |
2645 lines of code. \citeN{Braibant12} formalised a large part of |
2645 lines of code. \citeN{Braibant12} formalised a large part of |
2646 regular language theory and Kleene algebras in Coq. While he is |
2646 regular language theory and Kleene algebras in Coq. While he is |
2647 mainly interested in implementing decision procedures for Kleene |
2647 mainly interested in implementing decision procedures for Kleene |
2648 algebras, his library includes a proof of the Myhill-Nerode |
2648 algebras, his library includes a proof of the Myhill-Nerode |
2649 theorem. He reckons that our ``development is more concise'' than |
2649 theorem. He reckons that our Myhill-Nerode ``development is more concise'' than |
2650 his one based on matrices \cite[Page 67]{Braibant12}. He writes |
2650 his one based on matrices \cite[Page 67]{Braibant12}. He writes |
2651 that there is no conceptual problems with formally reasoning about |
2651 that there is no conceptual problems with formally reasoning about |
2652 matrices for automata, but notes ``intrinsic difficult[ies]'' when |
2652 matrices for automata, but notes ``intrinsic difficult[ies]'' when |
2653 working with matrices in Coq, which is the sort of `fighting' one |
2653 working with matrices in Coq, which is the sort of `fighting' one |
2654 would encounter also in other theorem provers. |
2654 would encounter also in other theorem provers. |