Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype path fingraph finfun finset.
Require Import misc regexp automata dfa_to_re non_regular.
Set Implicit Arguments.
Import Prenex Implicits.
Lemma pigeon (T : finType) (s : seq T) : #|T| < size s -> ~~ uniq s.
Lemma uniqFE (T : eqType) (s : seq T) :
~~ uniq s -> exists x s1 s2 s3, s = rcons s1 x ++ rcons s2 x ++ s3.
Require Import misc regexp automata dfa_to_re non_regular.
Set Implicit Arguments.
Import Prenex Implicits.
Lemma pigeon (T : finType) (s : seq T) : #|T| < size s -> ~~ uniq s.
Lemma uniqFE (T : eqType) (s : seq T) :
~~ uniq s -> exists x s1 s2 s3, s = rcons s1 x ++ rcons s2 x ++ s3.
Section Pumping.
Fixpoint rep (T : eqType) (s : seq T) n :=
if n is n'.+1 then s ++ rep s n' else [::].
Variable char : finType.
Lemma run_size (A : dfa char) (x : A) w : size (dfa_run x w) = size w.
Lemma run_cycle (A : dfa char) (x : A) s i :
last x (dfa_run x s) = x -> last x (dfa_run x (rep s i)) = x.
Lemma run_word_split (A : dfa char) (x : A) w r1 r2 :
dfa_run x w = r1 ++ r2 ->
exists w1 w2, [/\ w = w1 ++ w2, dfa_run x w1 = r1 & dfa_run (last x r1) w2 = r2].
Lemma pump_dfa (A : dfa char) x y z :
x ++ y ++ z \in dfa_lang A -> #|A| < size y ->
exists u v w,
[/\ ~~ nilp v, y = u ++ v ++ w & forall i, (x ++ u ++ rep v i ++ w ++ z) \in dfa_lang A].
Lemma pumping (L : word char -> Prop) :
(forall k, exists x y z, k <= size y /\ L (x ++ y ++ z) /\
(forall u v w, y = u ++ v ++ w -> ~~ nilp v ->
exists i, L (x ++ u ++ rep v i ++ w ++ z) -> False))
-> ~ regular L.
End Pumping.
Lemma cat_nseq_eq (char : eqType) n1 n2 (a : char) :
nseq n1 a ++ nseq n2 a = nseq (n1+n2) a.
Example pump_Lab (char : finType) (a b : char) : a != b -> ~ regular (Lab char a b).