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.

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).