Authors: Christian Doczkal and Jan-Oliver Kaiser
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype path fingraph tuple finfun finset div.
Require Import misc regexp automata dfa_to_re myhill_nerode homomorphism.
Require Import misc regexp automata dfa_to_re myhill_nerode homomorphism.
Regular Languages are Fully determined and since propositions
can be embedded into languages, there are some languages that are regular
iff we assume excluded middle. (take P to be any independent proposition)
Lemma regular_det (char : finType) L (w : word char): regular L -> L w \/ ~ L w.
Lemma regular_xm (char : finType) P : regular (fun _ : word char => P) <-> P \/ ~ P.
Section NonRegular.
Variables (char : finType) (a b : char).
Hypothesis (Hab : a != b).
Implicit Types (L : word char -> Prop) (l : dlang char).
Lemma regular_eq L1 L2 : (forall w, L1 w <-> L2 w) -> regular L1 -> regular L2.
Lemma regularE (L : word char -> Prop) : regular L ->
exists L' : dlang char, (forall w, L w <-> w \in L') /\ inhabited (nerodePar L').
Lemma nerodeIN (f : nat -> word char) (L : dlang char) :
(forall n1 n2, (forall w, (f n1 ++ w \in L) = (f n2 ++ w \in L)) -> n1 = n2) ->
~ regular L.
Lemma count_nseq (T : eqType) (c d : T) n :
count (pred1 c) (nseq n d) = (c == d) * n.
Lemma countL n1 n2 : count (pred1 a) (nseq n1 a ++ nseq n2 b) = n1.
Lemma countR n1 n2 : count (pred1 b) (nseq n1 a ++ nseq n2 b) = n2.
Definition Lab w := exists n, w = nseq n a ++ nseq n b.
Lemma Lab_eq n1 n2 : Lab (nseq n1 a ++ nseq n2 b) -> n1 = n2.
Lemma Lab_not_regular : ~ regular Lab.
End NonRegular.