Module Pumping.

Fixpoint pumping_constant {T} (re : @reg_exp T) : nat :=
  match re with
  | EmptySet => 0
  | EmptyStr => 1
  | Char _ => 2
  | App re1 re2 =>
      pumping_constant re1 + pumping_constant re2
  | Union re1 re2 =>
      pumping_constant re1 + pumping_constant re2
  | Star re => S (pumping_constant re)
  end.

(** Next, it is useful to define an auxiliary function that repeats a
    string (appends it to itself) some number of times. *)

Fixpoint napp {T} (n : nat) (l : list T) : list T :=
  match n with
  | 0 => []
  | S n' => l ++ napp n' l
  end.

Lemma napp_plus: forall T (n m : nat) (l : list T),
  napp (n + m) l = napp n l ++ napp m l.
Proof.
  intros T n m l.
  induction n as [|n IHn].
  - reflexivity.
  - simpl. rewrite IHn, app_assoc. reflexivity.
Qed.

(** Now, the pumping lemma itself says that, if [s =~ re] and if the
    length of [s] is at least the pumping constant of [re], then [s]
    can be split into three substrings [s1 ++ s2 ++ s3] in such a way
    that [s2] can be repeated any number of times and the result, when
    combined with [s1] and [s3] will still match [re].  Since [s2] is
    also guaranteed not to be the empty string, this gives us
    a (constructive!) way to generate strings matching [re] that are
    as long as we like. *)

Lemma app_reassoc : forall {X} (a b c d:list X),
  a ++ b ++ c ++ d = ((a ++ b) ++ c) ++ d.
Proof.
  intros X a b c d.
  rewrite app_assoc.
  rewrite app_assoc.
  reflexivity.
Qed.

Lemma app_reassoc_2 : forall {X} (a b c d:list X),
  a ++ b ++ c ++ d = (a ++ b ++ c) ++ d.
Proof.
  intros X a b c d.
  rewrite app_assoc.
  rewrite app_assoc.
  rewrite <- (app_assoc _ a b c).
  reflexivity.
Qed.

Lemma star_napp : forall T (re : @reg_exp T) (s:list T) ,
    s =~ Star re -> forall m:nat, napp m s =~ Star re.
Proof.
  intros T re s H m.
  induction m.
  - apply MStar0.
  - simpl. apply star_app.
    + apply H.
    + apply IHm.
Qed.


Import Coq.omega.Omega.

(* Added condition "length (s1 ++ s2 ) <= pumping_constant re"
   so now it is a true pumping lemma *)
Lemma pumping2 : forall T (re : @reg_exp T) s,
  s =~ re ->
  pumping_constant re <= length s ->
  exists s1 s2 s3,
    s = s1 ++ s2 ++ s3 /\
    length (s1 ++ s2 ) <= pumping_constant re /\
    s2 <> [] /\
    forall m, s1 ++ napp m s2 ++ s3 =~ re.
Proof.
  intros T re s Hmatch.
  induction Hmatch
    as [ | x | s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2
       | s1 re1 re2 Hmatch IH | re1 s2 re2 Hmatch IH
       | re | s1 s2 re Hmatch1 IH1 Hmatch2 IH2 ].
  - (* MEmpty *)
    simpl. omega.
  - (* MChar *)
    simpl. omega.
  - (* MApp *)
    simpl.
    intros Hconst.
    assert ( H : pumping_constant re1 <= length s1 \/ ~pumping_constant re1 <= length s1 ).
    { omega. }
    destruct H as [H'|H'].
    + assert (exists s2 s3 s4 : list T,
        s1 = s2 ++ s3 ++ s4 /\
        length (s2 ++ s3) <= pumping_constant re1 /\
        s3 <> [ ] /\ (forall m : nat, s2 ++ napp m s3 ++ s4 =~ re1)).
      { apply IH1. apply H'. }
      destruct H as [s3 [s4 [s5 [H1 [Hq [H2 H3]]]]]].
      clear IH1 IH2.
      exists s3, s4, (s5 ++ s2).
      repeat split.
      { rewrite app_reassoc.
        rewrite <- (app_assoc _ s3).
        rewrite <- H1.
        reflexivity. }
      { rewrite app_length in *. omega. }
      { apply H2. }
      { intros m. rewrite app_reassoc.
        apply MApp.
        * rewrite <- app_assoc.
          apply H3.
        * apply Hmatch2. }
    + assert (exists s1 s3 s4 : list T,
        s2 = s1 ++ s3 ++ s4 /\
        length (s1 ++ s3) <= pumping_constant re2 /\
        s3 <> [ ] /\ (forall m : nat, s1 ++ napp m s3 ++ s4 =~ re2)).
      { apply IH2. rewrite app_length in Hconst. omega. }
      destruct H as [s3 [s4 [s5 [H1 [Hq [H2 H3]]]]]].
      clear IH1 IH2.
      exists (s1 ++ s3), s4, s5.
      repeat split.
      { rewrite <- app_assoc.
        rewrite <- H1. reflexivity. }
      { rewrite <- app_assoc. rewrite app_length. omega. }
      { apply H2. }
      { intros m. rewrite <- app_assoc.
        apply MApp.
        * apply Hmatch1.
        * apply H3. }
  - intros Hconst.
    simpl in Hconst.
    assert (exists s2 s3 s4 : list T,
       s1 = s2 ++ s3 ++ s4 /\
       length (s2 ++ s3) <= pumping_constant re1 /\
       s3 <> [ ] /\ (forall m : nat, s2 ++ napp m s3 ++ s4 =~ re1)).
    { apply IH. omega. }
    destruct H as [s2 [s3 [s4 [H1 [Hq [H2 H3]]]]]].
    exists s2, s3, s4.
    repeat split.
    { apply H1. }
    { simpl. omega. }
    { apply H2. }
    { intros m. apply MUnionL. apply H3. }
  - intros Hconst.
    simpl in Hconst.
    assert (exists s1 s3 s4 : list T,
       s2 = s1 ++ s3 ++ s4 /\
       length (s1 ++ s3) <= pumping_constant re2 /\
       s3 <> [ ] /\ (forall m : nat, s1 ++ napp m s3 ++ s4 =~ re2)).
    { apply IH. omega. }
    destruct H as [s3 [s4 [s5 [H1 [Hq [H2 H3]]]]]].
    exists s3, s4, s5.
    repeat split.
    { apply H1. }
    { simpl. omega. }
    { apply H2. }
    { intros m. apply MUnionR. apply H3. }
  - intros Hconst. inversion Hconst.
  - simpl. intros Hconst.
    destruct s1.
    + simpl in Hconst. simpl in IH2.
      assert (exists s1 s3 s4 : list T,
        s2 = s1 ++ s3 ++ s4 /\
        length (s1 ++ s3) <= S (pumping_constant re) /\
        s3 <> [ ] /\ (forall m : nat, s1 ++ napp m s3 ++ s4 =~ Star re)).
      { apply IH2. apply Hconst. }
      destruct H as [s3 [s4 [s5 [H1 [Hq [H2 H3]]]]]].
      exists s3, s4, s5.
      repeat split.
      { simpl. apply H1. }
      { apply Hq. }
      { apply H2. }
      { apply H3. }
    + assert (H : pumping_constant re <= length (t :: s1) \/ ~pumping_constant re <= length (t :: s1)).
      { omega. }
      destruct H as [H'|H'].
      * assert (exists s2 s3 s4 : list T,
          t :: s1 = s2 ++ s3 ++ s4 /\
          length (s2 ++ s3) <= pumping_constant re /\
          s3 <> [ ] /\ (forall m : nat, s2 ++ napp m s3 ++ s4 =~ re)).
        { apply IH1. apply H'. }
        destruct H as [s3 [s4 [s5 [H1 [Hq [H2 H3]]]]]].
        exists s3, s4, (s5 ++ s2).
        repeat split.
        { rewrite app_reassoc_2. rewrite <- H1. reflexivity. }
        { omega. }
        { assumption. }
        { intros m. rewrite app_reassoc_2. apply MStarApp.
          - apply H3.
          - apply Hmatch2.  }
      * exists [], (t::s1), s2.
        repeat split.
        { simpl. simpl in H'. omega. }
        { intros H. inversion H. }
        { intros m. simpl. apply star_app.
          - apply star_napp. rewrite <- (app_nil_r _ (t :: s1)).
            apply MStarApp.
            + apply Hmatch1.
            + apply MStar0.
          - apply Hmatch2. }
Qed.

End Pumping.