(** * Coq codes *)
(** ** Dependencies *)

Require Import Recdef.
Require Import Arith.Wf_nat.
Require Import Omega.
Require Export RegExp.Utility.
Require Export RegExp.Definitions.
Require Export RegExp.Boolean.
Require Export RegExp.Concat.

Unset Standard Proposition Elimination Names.

(** ** Lemmas for Star *)

Lemma matches_Star_EmptyString : forall r, (Star r) ~== EmptyString.
Proof.
(* Goal: forall r : RegExp, @eq bool (matches (Star r) EmptyString) true *)
  intros r.  simpl; auto.  
Qed.

Lemma matches_Star_r : forall s r, r ~== s -> (Star r) ~== s.
Proof.
(* Goal: @eq bool false (matches Eps s) *)
  induction s; simpl.
(* Goal: forall (r : RegExp) (_ : @eq bool (nu r) true), @eq bool true true *)
(* Goal: forall (r : RegExp) (_ : @eq bool (matches (derive a r) s) true), @eq bool (matches (Cat (derive a r) (Star r)) s) true *)
    intros r nu_r.  auto.
(* Goal: forall (r : RegExp) (_ : @eq bool (matches (derive a r) s) true), @eq bool (matches (Cat (derive a r) (Star r)) s) true *)
    intros r Hra.  replace s with (s ++ "")%string.
(* Goal: @eq string EmptyString EmptyString *)
(* Goal: @eq bool false (matches Empty s) *)
    eapply (matches_Cat s ""%string (r/a) (Star r)); try auto.
(* Goal: @eq string (append s EmptyString) s *)
      eapply string_right_id.
Qed.

(** ** $ 1 + x x^{\ast} = x $ #1 + x x* = x# *)

Lemma matches_Star_right_s : forall s r, 
  (Star r) ~= s = (Eps || (r ++ Star r)) ~= s.
Proof.
(* Goal: forall (s : string) (r : RegExp), @eq bool (matches (Star r) s) (matches (Or Eps (Cat r (Star r))) s) *)
  induction s; simpl; intro r.
(* Goal: @eq string EmptyString EmptyString *)
(* Goal: @eq bool false (matches Empty s) *)
    auto.
(* Goal: @eq bool (matches (Cat (derive a r) (Star r)) s) (matches (Or Empty (if nu r then Or (Cat (derive a r) (Star r)) (Cat (derive a r) (Star r)) else Cat (derive a r) (Star r))) s) *)
    repeat erewrite matches_Or.  erewrite Empty_false.  simpl.
(* Goal: @eq bool (matches (Cat (derive a r) (Star r)) s) (matches (if nu r then Or (Cat (derive a r) (Star r)) (Cat (derive a r) (Star r)) else Cat (derive a r) (Star r)) s) *)
    destruct (nu r).
(* Goal: @eq string EmptyString EmptyString *)
(* Goal: @eq bool false (matches Empty s) *)
      erewrite Or_idem_s.  auto. 
(* Goal: @eq string EmptyString EmptyString *)
(* Goal: @eq bool false (matches Empty s) *)
      auto.
Qed.

Lemma matches_Star_right : forall r, Star r =R= Eps || (r ++ Star r).
Proof.
(* Goal: forall r : RegExp, re_eq (Star r) (Or Eps (Cat (Star r) r)) *)
  unfold re_eq.  intros r s.  eapply matches_Star_right_s.
Qed.

Lemma divide_Star_right : forall s r, (Star r) ~== s -> s <> ""%string -> 
  {s':string & {s'':string | s = (s' ++ s'')%string /\ s' <> ""%string /\ 
   r ~== s' /\ (Star r) ~== s''}}.
Proof.
(* Goal: forall (s : string) (r : RegExp) (_ : @eq bool (matches (Star r) s) true) (_ : not (@eq string s EmptyString)), @sigT string (fun s' : string => @sig string (fun s'' : string => and (@eq string s (append s' s'')) (and (not (@eq string s' EmptyString)) (and (@eq bool (matches r s') true) (@eq bool (matches (Star r) s'') true))))) *)
  induction s; intros r Hstar Hs.
(* Goal: @eq string EmptyString EmptyString *)
(* Goal: @eq bool false (matches Empty s) *)
    elim Hs.  auto.
(* Goal: @eq bool false true *)
(* Goal: @eq bool false true *)
    simpl in Hstar.
(* Goal: @sigT string (fun s' : string => @sig string (fun s'' : string => and (@eq string (String a s) (append s' s'')) (and (not (@eq string s' EmptyString)) (and (@eq bool (matches r s') true) (@eq bool (matches (Star r) s'') true))))) *)
    specialize (divide_Cat s (r/a) (Star r) Hstar).  intro H0.
(* Goal: @sigT string (fun s' : string => @sig string (fun s'' : string => and (@eq string (String a s) (append s' s'')) (and (not (@eq string s' EmptyString)) (and (@eq bool (matches r s') true) (@eq bool (matches (Star r) s'') true))))) *)
    destruct H0 as [s0' [s0'' [H01 [H02 H03]]]].
(* Goal: @sigT string (fun s' : string => @sig string (fun s'' : string => and (@eq string (String a s) (append s' s'')) (and (not (@eq string s' EmptyString)) (and (@eq bool (matches r s') true) (@eq bool (matches (Star r) s'') true))))) *)
    rewrite <- derivation in H02.
(* Goal: @sigT string (fun s' : string => @sig string (fun s'' : string => and (@eq string (String a s) (append s' s'')) (and (not (@eq string s' EmptyString)) (and (@eq bool (matches r s') true) (@eq bool (matches (Star r) s'') true))))) *)
    exists (String a s0'). exists s0''.
(* Goal: and (@eq bool (matches (Star r) (concat_list_string ss0)) true) (@eq bool (matches r s0) true) *)
    split.
(* Goal: @eq string EmptyString EmptyString *)
(* Goal: @eq bool false (matches Empty s) *)
      simpl.  rewrite <- H01.  auto.
(* Goal: and (@eq bool (matches (Star r) (concat_list_string ss0)) true) (@eq bool (matches r s0) true) *)
      split.
(* Goal: forall _ : iff (@eq bool (@forallb string (fun s : string => matches r s) ss') true) (forall (x : string) (_ : @In string x ss'), @eq bool ((fun s : string => matches r s) x) true), @eq bool (matches r s0) true *)
        intro H.  discriminate H.
(* Goal: @eq string EmptyString EmptyString *)
(* Goal: @eq bool false (matches Empty s) *)
        auto.
Qed.

(** ** Split [Star] to [list string] *)

Lemma Star_to_list : forall s r, (Star r) ~== s -> 
  {ss:list string | forallb (fun s => r ~= s) ss = true /\
   concat_list_string ss = s /\
   forallb (fun s => bneq_empty_string s) ss = true }. 
Proof.
(* Goal: forall (s : string) (r : RegExp) (_ : @eq bool (matches (Star r) s) true), @sig (list string) (fun ss : list string => and (@eq bool (@forallb string (fun s0 : string => matches r s0) ss) true) (and (@eq string (concat_list_string ss) s) (@eq bool (@forallb string (fun s0 : string => bneq_empty_string s0) ss) true))) *)
  refine (induction_ltof2 string str_length _ _).
(* Goal: forall (x : string) (_ : forall (y : string) (_ : ltof string str_length y x) (r : RegExp) (_ : @eq bool (matches (Star r) y) true), @sig (list string) (fun ss : list string => and (@eq bool (@forallb string (fun s : string => matches r s) ss) true) (and (@eq string (concat_list_string ss) y) (@eq bool (@forallb string (fun s : string => bneq_empty_string s) ss) true)))) (r : RegExp) (_ : @eq bool (matches (Star r) x) true), @sig (list string) (fun ss : list string => and (@eq bool (@forallb string (fun s : string => matches r s) ss) true) (and (@eq string (concat_list_string ss) x) (@eq bool (@forallb string (fun s : string => bneq_empty_string s) ss) true))) *)
  intros s IHs r Hstar.
(* Goal: @sig (list string) (fun ss : list string => and (@eq bool (@forallb string (fun s : string => matches r s) ss) true) (and (@eq string (concat_list_string ss) s) (@eq bool (@forallb string (fun s : string => bneq_empty_string s) ss) true))) *)
  specialize(string_dec s ""%string).  intro Hs_dec.  destruct Hs_dec.
    (* s = "" *)
(* Goal: @eq string EmptyString EmptyString *)
(* Goal: @eq bool false (matches Empty s) *)
    exists nil.  auto.
    (* s <> "" *)
(* Goal: @sig (list string) (fun ss : list string => and (@eq bool (@forallb string (fun s : string => matches r s) ss) true) (and (@eq string (concat_list_string ss) s) (@eq bool (@forallb string (fun s : string => bneq_empty_string s) ss) true))) *)
    specialize(divide_Star_right s r Hstar n).  intro H1.
(* Goal: @sig (list string) (fun ss : list string => and (@eq bool (@forallb string (fun s : string => matches r s) ss) true) (and (@eq string (concat_list_string ss) s) (@eq bool (@forallb string (fun s : string => bneq_empty_string s) ss) true))) *)
    destruct H1 as [s' [s'' [H11 [H12 [H13 H14]]]]].
(* Goal: @sig (list string) (fun ss : list string => and (@eq bool (@forallb string (fun s : string => matches r s) ss) true) (and (@eq string (concat_list_string ss) s) (@eq bool (@forallb string (fun s : string => bneq_empty_string s) ss) true))) *)
    assert(Hltof: ltof string str_length s'' s).
(* Goal: ltof string str_length s'' s *)
(* Goal: @sig (list string) (fun ss : list string => and (@eq bool (@forallb string (fun s : string => matches r s) ss) true) (and (@eq string (concat_list_string ss) s) (@eq bool (@forallb string (fun s : string => bneq_empty_string s) ss) true))) *)
      unfold ltof.  rewrite H11.  rewrite str_length_append.
(* Goal: lt (str_length s'') (Init.Nat.add (str_length s') (str_length s'')) *)
(* Goal: @sig (list string) (fun ss : list string => and (@eq bool (@forallb string (fun s : string => matches r s) ss) true) (and (@eq string (concat_list_string ss) s) (@eq bool (@forallb string (fun s : string => bneq_empty_string s) ss) true))) *)
      assert(Hlen_s: forall s, s <> ""%string -> str_length s <> 0).
(* Goal: forall (s : string) (_ : not (@eq string s EmptyString)), not (@eq nat (str_length s) O) *)
(* Goal: lt (str_length s'') (Init.Nat.add (str_length s') (str_length s'')) *)
(* Goal: @sig (list string) (fun ss : list string => and (@eq bool (@forallb string (fun s : string => matches r s) ss) true) (and (@eq string (concat_list_string ss) s) (@eq bool (@forallb string (fun s : string => bneq_empty_string s) ss) true))) *)
        induction s0.
(* Goal: @eq string EmptyString EmptyString *)
(* Goal: @eq bool false (matches Empty s) *)
          intro H'. elim H'. auto. 
(* Goal: @eq bool (matches (Star r) (String a s)) (matches (Star r') (String a s)) *)
          simpl. intro H'. intro H''. discriminate H''. 
(* Goal: lt (str_length s'') (Init.Nat.add (str_length s') (str_length s'')) *)
(* Goal: @sig (list string) (fun ss : list string => and (@eq bool (@forallb string (fun s : string => matches r s) ss) true) (and (@eq string (concat_list_string ss) s) (@eq bool (@forallb string (fun s : string => bneq_empty_string s) ss) true))) *)
      specialize(Hlen_s s' H12).  omega.
(* Goal: @sig (list string) (fun ss : list string => and (@eq bool (@forallb string (fun s : string => matches r s) ss) true) (and (@eq string (concat_list_string ss) s) (@eq bool (@forallb string (fun s : string => bneq_empty_string s) ss) true))) *)
    specialize(IHs s'' Hltof r H14).
(* Goal: @sig (list string) (fun ss : list string => and (@eq bool (@forallb string (fun s : string => matches r s) ss) true) (and (@eq string (concat_list_string ss) s) (@eq bool (@forallb string (fun s : string => bneq_empty_string s) ss) true))) *)
    destruct IHs as [ss' [IH1 [IH2 IH3]]].
(* Goal: and (@eq bool (matches (Star r) (concat_list_string ss0)) true) (@eq bool (matches r s0) true) *)
    exists (s' :: ss').  split.
(* Goal: @eq string EmptyString EmptyString *)
(* Goal: @eq bool false (matches Empty s) *)
      simpl. rewrite H13. rewrite IH1. auto.  split.
(* Goal: @eq string EmptyString EmptyString *)
(* Goal: @eq bool false (matches Empty s) *)
        simpl. rewrite IH2. rewrite <- H11. auto.
(* Goal: @eq bool (matches (Star r) (String a s)) (matches (Star r') (String a s)) *)
        simpl. rewrite IH3. unfold bneq_empty_string. destruct (string_dec s' ""%string).
(* Goal: @eq string EmptyString EmptyString *)
(* Goal: @eq bool false (matches Empty s) *)
          simpl. elim H12. auto.
(* Goal: @eq string EmptyString EmptyString *)
(* Goal: @eq bool false (matches Empty s) *)
          auto.
Defined.

Lemma Star_to_list_not_nil : forall s r, (Star r) ~== s -> s <> ""%string ->
  {ss:list string | forallb (fun s => r ~= s) ss = true /\
   concat_list_string ss = s /\ ss <> nil /\
   forallb (fun s => bneq_empty_string s) ss = true }.
Proof.
(* Goal: forall (s : string) (r : RegExp) (_ : @eq bool (matches (Star r) s) true) (_ : not (@eq string s EmptyString)), @sigT string (fun s' : string => @sig string (fun s'' : string => and (@eq string s (append s' s'')) (and (not (@eq string s'' EmptyString)) (and (@eq bool (matches (Star r) s') true) (@eq bool (matches r s'') true))))) *)
  intros s r Hstar Hs.
(* Goal: forall _ : iff (@eq bool (@forallb string (fun s : string => matches r s) ss') true) (forall (x : string) (_ : @In string x ss'), @eq bool ((fun s : string => matches r s) x) true), @eq bool (matches r s0) true *)
  specialize(Star_to_list s r Hstar). intro H.
(* Goal: @sig (list string) (fun ss : list string => and (@eq bool (@forallb string (fun s : string => matches r s) ss) true) (and (@eq string (concat_list_string ss) s) (and (not (@eq (list string) ss (@nil string))) (@eq bool (@forallb string (fun s : string => bneq_empty_string s) ss) true)))) *)
  destruct H as [ss' [IH1 [IH2 IH3]]].
(* Goal: @eq string EmptyString EmptyString *)
(* Goal: @eq bool false (matches Empty s) *)
  exists ss'.  split; try auto.
(* Goal: @eq string EmptyString EmptyString *)
(* Goal: @eq bool false (matches Empty s) *)
    split; try auto.
(* Goal: @eq string EmptyString EmptyString *)
(* Goal: @eq bool false (matches Empty s) *)
      split; try auto.
(* Goal: @eq string EmptyString EmptyString *)
(* Goal: @eq bool false (matches Empty s) *)
      intro Hss'.  rewrite Hss' in IH2.  simpl in IH2.  elim Hs.  auto.
Defined.

Lemma list_to_Star : forall xs r, 
  forallb (fun s : string => r ~= s) xs = true ->
  Star r ~== concat_list_string xs.
Proof.
(* Goal: @eq bool (matches (Star r) (String a s)) (matches (Star r') (String a s)) *)
  induction xs; intros r0 Hf; simpl.
(* Goal: @eq string EmptyString EmptyString *)
(* Goal: @eq bool false (matches Empty s) *)
    auto.
(* Goal: @eq bool (matches (Star r0) (append a (concat_list_string xs))) true *)
    simpl in Hf.
(* Goal: @eq bool (matches (Star r0) (append a (concat_list_string xs))) true *)
    case_eq (r0 ~= a); case_eq (forallb (fun s : string => r0 ~= s) xs); intros H1 H2.
      (* true true *)
(* Goal: @eq bool (matches (Star r0) (append a (concat_list_string xs))) true *)
(* Goal: @eq bool (matches (Star r0) (append a (concat_list_string xs))) true *)
(* Goal: @eq bool (matches (Star r0) (append a (concat_list_string xs))) true *)
(* Goal: @eq bool (matches (Star r0) (append a (concat_list_string xs))) true *)
      cut(Eps || (r0 ++ (Star r0)) ~== (a ++ concat_list_string xs)). intro H3.
(* Goal: @eq string EmptyString EmptyString *)
(* Goal: @eq bool false (matches Empty s) *)
      erewrite matches_Star_right.  auto.
(* Goal: @eq bool (matches (Or Eps (Cat r0 (Star r0))) (append a (concat_list_string xs))) true *)
(* Goal: @eq bool (matches (Star r0) (append a (concat_list_string xs))) true *)
(* Goal: @eq bool (matches (Star r0) (append a (concat_list_string xs))) true *)
(* Goal: @eq bool (matches (Star r0) (append a (concat_list_string xs))) true *)
        cut((r0 ++ (Star r0)) ~== (a ++ concat_list_string xs)). intro H4.  
(* Goal: @eq bool (matches (Or Eps (Cat r0 (Star r0))) (append a (concat_list_string xs))) true *)
(* Goal: @eq bool (matches (Cat r0 (Star r0)) (append a (concat_list_string xs))) true *)
(* Goal: @eq bool (matches (Star r0) (append a (concat_list_string xs))) true *)
(* Goal: @eq bool (matches (Star r0) (append a (concat_list_string xs))) true *)
(* Goal: @eq bool (matches (Star r0) (append a (concat_list_string xs))) true *)
        erewrite matches_Or.  rewrite H4.
(* Goal: @eq string EmptyString EmptyString *)
(* Goal: @eq bool false (matches Empty s) *)
        destruct (Eps ~= (a ++ concat_list_string xs)); auto.
(* Goal: @eq string EmptyString EmptyString *)
(* Goal: @eq bool false (matches Empty s) *)
          erewrite matches_Cat; auto.
       (* false true *)
(* Goal: @eq bool (matches (Star r0) (append a (concat_list_string xs))) true *)
       rewrite H1 in Hf; rewrite H2 in Hf; simpl in Hf; discriminate Hf.
       (* true false *)
(* Goal: @eq bool (matches (Star r0) (append a (concat_list_string xs))) true *)
       rewrite H1 in Hf; rewrite H2 in Hf; simpl in Hf; discriminate Hf.
       (* false false *)
(* Goal: @eq bool (matches (Star r0) (append a (concat_list_string xs))) true *)
       rewrite H1 in Hf; rewrite H2 in Hf; simpl in Hf; discriminate Hf.
Qed.

Lemma divide_Star_left : forall s r, (Star r) ~== s -> s <> ""%string ->
  {s':string & {s'':string | s = (s' ++ s'')%string /\ s'' <> ""%string /\ 
   (Star r) ~== s' /\ r ~== s''}}.
Proof.
(* Goal: forall (s : string) (r : RegExp) (_ : @eq bool (matches (Star r) s) true) (_ : not (@eq string s EmptyString)), @sigT string (fun s' : string => @sig string (fun s'' : string => and (@eq string s (append s' s'')) (and (not (@eq string s'' EmptyString)) (and (@eq bool (matches (Star r) s') true) (@eq bool (matches r s'') true))))) *)
  intros s r Hstar Hs.
(* Goal: forall _ : @eq bool (matches (Cat (Star r) r) (append s' s'')) true, @eq bool true false *)
(* Goal: @eq bool false true *)
  specialize(Star_to_list_not_nil s r Hstar Hs). intro H0.
(* Goal: @sigT string (fun s' : string => @sig string (fun s'' : string => and (@eq string s (append s' s'')) (and (not (@eq string s'' EmptyString)) (and (@eq bool (matches (Star r) s') true) (@eq bool (matches r s'') true))))) *)
  destruct H0 as [ss' [H01 [H02 [H03 H04]]]].
(* Goal: @sigT string (fun s' : string => @sig string (fun s'' : string => and (@eq string s (append s' s'')) (and (not (@eq string s'' EmptyString)) (and (@eq bool (matches (Star r) s') true) (@eq bool (matches r s'') true))))) *)
  specialize (exists_last H03).  intro Hlast.  
(* Goal: @sigT string (fun s' : string => @sig string (fun s'' : string => and (@eq string s (append s' s'')) (and (not (@eq string s'' EmptyString)) (and (@eq bool (matches (Star r) s') true) (@eq bool (matches r s'') true))))) *)
  destruct Hlast as [ss0 [s0 Hlast']]. 
(* Goal: and (@eq bool (matches (Star r) (concat_list_string ss0)) true) (@eq bool (matches r s0) true) *)
  exists (concat_list_string ss0).  exists s0.  split.
(* Goal: @eq string EmptyString EmptyString *)
(* Goal: @eq bool false (matches Empty s) *)
    erewrite <- concat_list_string_xs_x.  rewrite <- Hlast'.  auto.  split.
      (* goal: s0 <> ""%string *)
(* Goal: not (@eq string s0 EmptyString) *)
(* Goal: and (@eq bool (matches (Star r) (concat_list_string ss0)) true) (@eq bool (matches r s0) true) *)
      assert(H': In s0 ss').
(* Goal: @In string s0 ss' *)
(* Goal: not (@eq string s0 EmptyString) *)
(* Goal: and (@eq bool (matches (Star r) (concat_list_string ss0)) true) (@eq bool (matches r s0) true) *)
        rewrite Hlast'.  eapply In_list_append_right.  eapply in_eq.
(* Goal: not (@eq string s0 EmptyString) *)
(* Goal: and (@eq bool (matches (Star r) (concat_list_string ss0)) true) (@eq bool (matches r s0) true) *)
      specialize(forallb_forall (fun s => bneq_empty_string s) ss'). intros H''.
(* Goal: not (@eq string s0 EmptyString) *)
(* Goal: and (@eq bool (matches (Star r) (concat_list_string ss0)) true) (@eq bool (matches r s0) true) *)
      destruct H'' as [H'' _].  specialize(H'' H04).  specialize(H'' s0 H').
(* Goal: not (@eq string s0 EmptyString) *)
(* Goal: and (@eq bool (matches (Star r) (concat_list_string ss0)) true) (@eq bool (matches r s0) true) *)
      unfold bneq_empty_string in H''.  
(* Goal: @eq string EmptyString EmptyString *)
(* Goal: @eq bool false (matches Empty s) *)
      destruct (string_dec s0 ""%string). discriminate H''. auto.
(* Goal: and (@eq bool (matches (Star r) (concat_list_string ss0)) true) (@eq bool (matches r s0) true) *)
      split.
        (* goal: Star r ~== concat_list_string ss0 *)
(* Goal: @eq bool (matches (Star r) (concat_list_string ss0)) true *)
(* Goal: @eq bool (matches r s0) true *)
        eapply list_to_Star.  rewrite Hlast' in H01.
(* Goal: @eq bool (@forallb string (fun s : string => matches r s) ss0) true *)
(* Goal: @eq bool (matches r s0) true *)
        apply(forallb_divide_left string (fun s => r ~= s) ss0 (s0::nil) H01).
        (* goal: r ~== s0 *)
(* Goal: @eq bool (matches r s0) true *)
        specialize(In_snoc string s0 ss0).  
(* Goal: forall _ : @In string s0 (@app string ss0 (@cons string s0 (@nil string))), @eq bool (matches r s0) true *)
        intros HIn.  rewrite <- Hlast' in HIn.
(* Goal: forall _ : iff (@eq bool (@forallb string (fun s : string => matches r s) ss') true) (forall (x : string) (_ : @In string x ss'), @eq bool ((fun s : string => matches r s) x) true), @eq bool (matches r s0) true *)
        specialize(forallb_forall (fun s => r ~= s) ss'). intro H.
(* Goal: @eq string EmptyString EmptyString *)
(* Goal: @eq bool false (matches Empty s) *)
        destruct H as [H _].  eapply H.  auto.
        (* goal: In s0 ss' *)
(* Goal: @eq string EmptyString EmptyString *)
(* Goal: @eq bool false (matches Empty s) *)
        auto.
Qed.

(** ** [Star] is morphism *)

Lemma forallb_matches_morphism_s : forall ss r r', r =R= r' ->
  forallb (fun s0 => r ~= s0) ss = forallb (fun s0 => r' ~= s0) ss.
Proof.
(* Goal: forall (ss : list string) (r r' : RegExp) (_ : re_eq r r'), @eq bool (@forallb string (fun s0 : string => matches r s0) ss) (@forallb string (fun s0 : string => matches r' s0) ss) *)
  induction ss.
(* Goal: @eq string EmptyString EmptyString *)
(* Goal: @eq bool false (matches Empty s) *)
    intros r r' H.  simpl.  auto.
(* Goal: @eq bool (matches (Star r) (String a s)) (matches (Star r') (String a s)) *)
    intros r r' H.  simpl.  rewrite <- (IHss r r' H).  unfold re_eq in H.
(* Goal: @eq string EmptyString EmptyString *)
(* Goal: @eq bool false (matches Empty s) *)
    rewrite <- (H a).  auto.
Qed.

Lemma Star_morphism_s : forall s r r', r =R= r' -> (Star r) ~= s = (Star r') ~= s.
Proof.
(* Goal: forall (s : string) (r r' : RegExp) (_ : re_eq r r'), @eq bool (matches (Star r) s) (matches (Star r') s) *)
  induction s.
(* Goal: @eq string EmptyString EmptyString *)
(* Goal: @eq bool false (matches Empty s) *)
    intros r r' H.  simpl.  auto.
(* Goal: @eq bool (matches (Star r) (String a s)) (matches (Star r') (String a s)) *)
    intros r r' H.  simpl.
    case_eq ((r / a ++ Star r) ~= s); case_eq ((r' / a ++ Star r') ~= s); 
(* Goal: @eq string EmptyString EmptyString *)
(* Goal: @eq bool false (matches Empty s) *)
    intros H0 H1; try auto.
      (* true false *)
(* Goal: @eq bool true false *)
(* Goal: @eq bool false true *)
      specialize(divide_Cat s (r/a) (Star r) H1).  intros H2.
(* Goal: @eq bool false true *)
      destruct H2 as [s' [s'' [H01 [H02 H03]]]].
(* Goal: @sigT string (fun s' : string => @sig string (fun s'' : string => and (@eq string (String a s) (append s' s'')) (and (not (@eq string s' EmptyString)) (and (@eq bool (matches r s') true) (@eq bool (matches (Star r) s'') true))))) *)
      erewrite <- derivation in H02.
(* Goal: @eq bool false true *)
      unfold re_eq in H.  erewrite H in H02.  erewrite derivation in H02.
(* Goal: @eq bool true false *)
(* Goal: @eq bool false true *)
      specialize(Star_to_list s'' r H03).  intro H2.
(* Goal: @eq bool false true *)
      destruct H2 as [ss [H21 [H22 H23]]].
(* Goal: @eq bool true false *)
(* Goal: @eq bool false true *)
      rewrite (forallb_matches_morphism_s ss r r') in H21.
(* Goal: forall _ : @eq bool (matches (Star r) (concat_list_string ss)) true, @eq bool false true *)
(* Goal: re_eq r' r *)
      specialize(list_to_Star ss r' H21).  intro H3.  rewrite H22 in H3.
(* Goal: forall _ : @eq bool (matches (Cat (derive a r) (Star r)) (append s' s'')) true, @eq bool false true *)
(* Goal: re_eq r' r *)
      specialize(matches_Cat s' s'' (r'/a) (Star r') H02 H3).  intro H4.
(* Goal: @eq string EmptyString EmptyString *)
(* Goal: @eq bool false (matches Empty s) *)
      rewrite <- H01 in H4.  rewrite H0 in H4.  inversion H4.  auto.
      (* false true *)
(* Goal: forall _ : @sigT string (fun s' : string => @sig string (fun s'' : string => and (@eq string s (append s' s'')) (and (@eq bool (matches (derive a r') s') true) (@eq bool (matches (Star r') s'') true)))), @eq bool false true *)
      specialize(divide_Cat s (r'/a) (Star r') H0).  intros H2.
(* Goal: @eq bool false true *)
      destruct H2 as [s' [s'' [H01 [H02 H03]]]].
(* Goal: @sigT string (fun s' : string => @sig string (fun s'' : string => and (@eq string (String a s) (append s' s'')) (and (not (@eq string s' EmptyString)) (and (@eq bool (matches r s') true) (@eq bool (matches (Star r) s'') true))))) *)
      erewrite <- derivation in H02.
(* Goal: @eq bool false true *)
      unfold re_eq in H.  erewrite <- H in H02.  erewrite derivation in H02.
(* Goal: forall _ : @sig (list string) (fun ss : list string => and (@eq bool (@forallb string (fun s : string => matches r' s) ss) true) (and (@eq string (concat_list_string ss) s'') (@eq bool (@forallb string (fun s : string => bneq_empty_string s) ss) true))), @eq bool false true *)
      specialize(Star_to_list s'' r' H03).  intro H2.
(* Goal: @eq bool false true *)
      destruct H2 as [ss [H21 [H22 H23]]].
(* Goal: @eq bool false true *)
      rewrite (forallb_matches_morphism_s ss r' r) in H21.
(* Goal: forall _ : @eq bool (matches (Star r) (concat_list_string ss)) true, @eq bool false true *)
(* Goal: re_eq r' r *)
      specialize(list_to_Star ss r H21).  intro H3.  rewrite H22 in H3.
(* Goal: forall _ : @eq bool (matches (Cat (derive a r) (Star r)) (append s' s'')) true, @eq bool false true *)
(* Goal: re_eq r' r *)
      specialize(matches_Cat s' s'' (r/a) (Star r) H02 H3).  intro H4.
(* Goal: @eq bool false true *)
(* Goal: re_eq r' r *)
      rewrite <- H01 in H4.  rewrite H1 in H4.  inversion H4.  
(* Goal: @eq string EmptyString EmptyString *)
(* Goal: @eq bool false (matches Empty s) *)
      setoid_symmetry.  auto.
Qed.

Add Parametric Morphism : Star with
signature re_eq ==> re_eq as Star_morphism.
Proof.
(* Goal: forall r : RegExp, re_eq (Star r) (Or Eps (Cat (Star r) r)) *)
  intros x y H.  unfold re_eq.  intros s.  eapply Star_morphism_s.  exact H.
Qed.

(** ** $ 1 + x^{\ast} x = x $ #1 + x* x = x# *)

Lemma matches_Star_left_s : forall s r, (Star r) ~= s = (Eps || (Star r ++ r)) ~= s.
Proof.
(* Goal: forall (s : string) (r : RegExp), @eq bool (matches (Star r) s) (matches (Or Eps (Cat (Star r) r)) s) *)
  intros s r.
  case_eq (Star r ~= s); intro Hstar;
(* Goal: @eq string EmptyString EmptyString *)
(* Goal: @eq bool false (matches Empty s) *)
  case_eq ((Eps || (Star r ++ r)) ~= s); intro H; try auto.
    (* Star r ~== s *)
(* Goal: @eq bool false true *)
    destruct (string_dec s ""%string).
      (* s = "" *)
(* Goal: @eq bool true false *)
(* Goal: @eq bool true false *)
(* Goal: @eq bool false true *)
      rewrite e in H.  erewrite matches_Or in H.  simpl in H.  discriminate H.
      (* s <> "" *)
(* Goal: forall _ : @eq bool (matches (Cat (Star r) r) (append s' s'')) true, @eq bool true false *)
(* Goal: @eq bool false true *)
      specialize(divide_Star_left s r Hstar n).  intro H0.
(* Goal: @eq bool true false *)
(* Goal: @eq bool false true *)
      destruct H0 as [s' [s'' [H01 [H02 [H03 H04]]]]].
(* Goal: forall _ : @eq bool (matches (Cat (Star r) r) (append s' s'')) true, @eq bool true false *)
(* Goal: @eq bool false true *)
      specialize(matches_Cat s' s'' (Star r) r H03 H04).  intro H0.
(* Goal: @eq bool true false *)
(* Goal: @eq bool false true *)
      rewrite <- H01 in H0.   rewrite matches_Or in H.  rewrite H0 in H.
(* Goal: @eq bool true false *)
(* Goal: @eq bool true false *)
(* Goal: @eq bool false true *)
      destruct (Eps ~= s); simpl in H; discriminate H.
    (* Star r ~!= s *)
(* Goal: @eq bool false true *)
    destruct (string_dec s ""%string).
      (* s = "" *)
(* Goal: @eq bool false true *)
(* Goal: @eq bool false true *)
      rewrite e in Hstar.  simpl in Hstar.  discriminate Hstar.
      (* s <> "".  Prove (H:Eps || (Star r ++ r) ~== s) -> (~Hstar:Star r ~== s) *)
(* Goal: @eq bool false true *)
(* Goal: @eq bool false (matches Eps s) *)
      rewrite matches_Or in H.  replace (Eps ~= s) with false in H.  simpl in H.
      (* H: (Star r ++ r) ~== s. Divide s *)
(* Goal: forall _ : @sig (list string) (fun ss : list string => and (@eq bool (@forallb string (fun s : string => matches r s) ss) true) (and (@eq string (concat_list_string ss) s') (@eq bool (@forallb string (fun s : string => bneq_empty_string s) ss) true))), @eq bool false true *)
(* Goal: @eq bool false (matches Eps s) *)
      specialize(divide_Cat s (Star r) r H).  intro H'.
(* Goal: @eq bool false true *)
(* Goal: @eq bool false (matches Eps s) *)
      destruct H' as [s' [s'' [H01 [H02 H03]]]].
      (* H02 : Star r ~== s'. Parse s' to ss:list string *)
(* Goal: forall _ : @sig (list string) (fun ss : list string => and (@eq bool (@forallb string (fun s : string => matches r s) ss) true) (and (@eq string (concat_list_string ss) s') (@eq bool (@forallb string (fun s : string => bneq_empty_string s) ss) true))), @eq bool false true *)
(* Goal: @eq bool false (matches Eps s) *)
      specialize(Star_to_list s' r H02).  intro H'.
(* Goal: @eq bool false true *)
(* Goal: @eq bool false (matches Eps s) *)
      destruct H' as [ss [H11 [H12 H13]]].
      (* Prove Hf: (Star r) ~== (ss ++ s'::nil) *)
(* Goal: @eq bool false true *)
(* Goal: @eq bool false (matches Eps s) *)
      specialize(forallb_list_xs_x string (fun s => r ~= s) ss s'' H11 H03).
(* Goal: forall _ : @eq bool (@forallb string (fun s : string => matches r s) (@app string ss (@cons string s'' (@nil string)))) true, @eq bool false true *)
(* Goal: @eq bool false (matches Eps s) *)
      intros Hf.
      (* Prove Hf': ss ++ s'::nil = s *) 
(* Goal: @eq bool false true *)
(* Goal: @eq bool false (matches Eps s) *)
      specialize(concat_list_string_xs_x ss s'').  intros Hf'.
(* Goal: @eq bool false true *)
(* Goal: @eq bool false (matches Eps s) *)
      rewrite H12 in Hf'.  rewrite <- H01 in Hf'.
      (* Prove (Star r ) ~== s *)
(* Goal: @eq bool false true *)
(* Goal: @eq bool false (matches Eps s) *)
      specialize(list_to_Star (ss ++ s''::nil) r Hf).  intros Hf''.
(* Goal: @eq bool false true *)
(* Goal: @eq bool false (matches Eps s) *)
      rewrite Hf' in Hf''.
      (* Contradiction between Hstar and Hf'' *)
(* Goal: @eq bool false true *)
(* Goal: @eq bool false (matches Eps s) *)
      rewrite Hf'' in Hstar.  discriminate Hstar.
      (* Prove false = Eps ~= s *)
(* Goal: @eq bool (matches (Star r) (String a s)) (matches (Star r') (String a s)) *)
      induction s;  simpl.  
(* Goal: @eq string EmptyString EmptyString *)
(* Goal: @eq bool false (matches Empty s) *)
        elim n.  auto.
(* Goal: @eq bool false (matches Empty s) *)
        symmetry.  eapply Empty_false.
Qed.

Lemma matches_Star_left : forall r, Star r =R= Eps || (Star r ++ r).
Proof.
(* Goal: forall r : RegExp, re_eq (Star r) (Or Eps (Cat (Star r) r)) *)
  unfold re_eq.  intros r s.  eapply matches_Star_left_s.
Qed.









