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.
Unset Strict Implicit.

Lemma pigeon (T : finType) (s : seq T) : #|T| < size s -> ~~ uniq s.
Proof.
  move => T_s. apply/negP. case/card_uniqP => e.
  move: T_s. by rewrite -e ltnNge max_card.
Qed.

Lemma uniqFE (T : eqType) (s : seq T) :
  ~~ uniq s -> exists x s1 s2 s3, s = rcons s1 x ++ rcons s2 x ++ s3.
Proof.
  elim: s => //= a s IHs. rewrite negb_and negbK.
  case/orP => [H | /IHs [b] [s1] [s2] [s3] e].
  - exists a; exists [::]. case: (splitP H) => s1 s2. by do 2 eexists.
  - exists b. exists (a::s1). exists s2. exists s3. by rewrite e.
Qed.

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.
  Proof. elim: w x => //= a s IHs x. by rewrite IHs. Qed.

  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.
  Proof. elim: i => //= i IH H. by rewrite dfa_run_cat last_cat H IH. Qed.

  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].
  Proof.
    move => H. exists (take (size r1) w). exists (drop (size r1) w).
    have size_r1 : size r1 <= size w by rewrite -(run_size x) H size_cat leq_addr.
    have Hw : w = take (size r1) w ++ drop (size r1) w by rewrite cat_take_drop.
    rewrite Hw dfa_run_cat in H. move/eqP : H. rewrite eqseq_cat.
    case/andP => [/eqP e1 /eqP e2]. rewrite e1 in e2. by split.
    by rewrite run_size size_takel.
  Qed.

  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].
  Proof.
    rewrite delta_accept !delta_cat [delta _ y]/delta => H.
    set x' := delta (_ A) _ in H *. rewrite -(@run_size A x') => /pigeon.
    move/uniqFE => [q] [r1] [r2] [r3] Hr. rewrite Hr in H.
    move: (run_word_split Hr) => [u] [u'] [Ey Hu]. rewrite last_rcons.
    move/run_word_split => [v] [w] [Eu' Hv]. rewrite last_rcons => Hw.
    exists u; exists v; exists w. split.
    - move: Hv ; destruct v => //=. by destruct r2.
    - by subst.
    - move => i. rewrite delta_accept [u ++ _]catA [_ ++ w ++ _]catA -[_ ++ w] catA.
      rewrite delta_cat [delta _ (_ ++ z)]delta_cat -/x' [delta x']/delta.
      rewrite (_ : (last x' (dfa_run x' (u ++ rep v i ++ w)))
                 = (last x' (rcons r1 q ++ rcons r2 q ++ r3))) //.
      rewrite dfa_run_cat Hu 2!last_cat !last_rcons.
      by rewrite dfa_run_cat last_cat run_cycle ?Hv ?last_cat ?last_rcons // Hw.
  Qed.

  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.
  Proof.
    move => H [e He]. pose A := re_to_dfa e.
    have LA: forall w, L w <-> w \in dfa_lang A.
      move => w. by rewrite He re_to_dfa_correct.
    move/(_ #|A|.+1) : H => [x] [y] [z] [size_y [/LA Lxyz]].
    move: (pump_dfa Lxyz size_y) => [u] [v] [w] [Hn Hy Hv] /(_ u v w Hy Hn).
    move => [i]. apply. exact/LA.
  Qed.

End Pumping.

Lemma cat_nseq_eq (char : eqType) n1 n2 (a : char) :
  nseq n1 a ++ nseq n2 a = nseq (n1+n2) a.
Proof. elim: n1 => [|n1 IHn1] //=. by rewrite -cat1s IHn1. Qed.

Example pump_Lab (char : finType) (a b : char) : a != b -> ~ regular (Lab char a b).
Proof.
  move => neq. apply: pumping => k.
  exists [::]. exists (nseq k a). exists (nseq k b). repeat split.
  - by rewrite size_nseq.
  - by exists k.
  - move => u [|c v] w // /eqP e _. exists 0 => /= H.
    have Hk: k = size (u ++ (c::v) ++ w) by rewrite -[k](@size_nseq _ _ a) (eqP e).
    rewrite Hk !size_cat -!cat_nseq_eq !eqseq_cat ?size_nseq // in e.
    case/and3P : e => [/eqP Hu /eqP Hv /eqP Hw].
    rewrite -Hu -Hw catA cat_nseq_eq in H. case/(Lab_eq char a b neq) : H.
    move/eqP. by rewrite Hk !size_cat eqn_add2l -{1}[size w]add0n eqn_add2r.
Qed.