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

Require Export RegExp.Utility.
Require Export RegExp.Definitions.
Require Export RegExp.Boolean.
Require Export RegExp.Concat.

Unset Standard Proposition Elimination Names.

(** ** [Char] *)

Lemma Char_true : forall c, (Char c) ~== (String c ""%string).
Proof.
(* Goal: forall c : ascii, @eq bool (matches (Char c) (String c EmptyString)) true *)
  intro c.  simpl.
(* Goal: @eq bool (matches (string_to_re (String a s)) (String a0 s')) false *)
  destruct(ascii_dec c c); simpl.
(* Goal: @eq bool false false *)
    auto.
(* Goal: @eq bool false false *)
    elim n. auto.
Qed.

Lemma Char_false : forall s c, s <> (String c ""%string) -> (Char c) ~!= s.
Proof.
(* Goal: forall (s s' : string) (_ : not (@eq string s s')), @eq bool (matches (string_to_re s) s') false *)
  induction s.
(* Goal: @eq bool (matches (string_to_re (String a s)) (String a0 s')) false *)
    intros c Hs.  simpl.  auto.
(* Goal: @eq bool (matches (string_to_re (String a s)) (String a0 s')) false *)
    induction s; intros c Hs; simpl.  
(* Goal: @eq bool (matches (string_to_re (String a s)) (String a0 s')) false *)
      destruct(ascii_dec c a); simpl.
(* Goal: @eq bool false false *)
        rewrite e in Hs.  elim Hs.  auto. 
(* Goal: @eq bool false false *)
        auto.
(* Goal: @eq bool (matches (string_to_re (String a s)) (String a0 s')) false *)
      destruct(ascii_dec c a); simpl.
(* Goal: @eq bool (matches Empty s) false *)
        eapply Empty_false.
(* Goal: @eq bool (matches Empty s) false *)
        eapply Empty_false.
Qed.

Add Parametric Morphism : Char with
signature ascii_eq ==> re_eq as Char_mor.
Proof.
(* Goal: forall (x y : ascii) (_ : ascii_eq x y), re_eq (Char x) (Char y) *)
  intros x y Hxy.  destruct Hxy.  setoid_reflexivity.
Qed.

Lemma derive_Char_is_id : forall a r, derive a (Char a ++ r) =R= r.
Proof.
(* Goal: @eq bool (matches (string_to_re (String a s)) (String a0 s')) false *)
  intros a r.  simpl.  
(* Goal: @eq bool (matches (Cat (if ascii_dec a a then Eps else Empty) (string_to_re s)) s) true *)
  destruct(ascii_dec a a).
(* Goal: re_eq r r *)
(* Goal: re_eq (Cat Empty r) r *)
    setoid_rewrite Cat_left_id.  setoid_reflexivity.
(* Goal: @eq bool false false *)
    elim n.  auto.
Qed.

(** ** String *)
(** For simplicity, there is no [RegExp] constructor for string; however, the conversion is easy. *)

Fixpoint string_to_re (s:string):RegExp :=
match s with
| EmptyString => Eps
| String a s' => (Char a) ++ (string_to_re s')
end.

Lemma string_to_re_true : forall s:string, (string_to_re s) ~== s.
Proof.
(* Goal: forall (s s' : string) (_ : not (@eq string s s')), @eq bool (matches (string_to_re s) s') false *)
  induction s.
(* Goal: @eq bool (matches (string_to_re (String a s)) (String a0 s')) false *)
    simpl.  auto.
(* Goal: @eq bool (matches (string_to_re (String a s)) (String a0 s')) false *)
    simpl.  destruct(ascii_dec a a).
(* Goal: @eq bool false false *)
      erewrite Cat_left_id_s.  auto.
(* Goal: @eq bool false false *)
      elim n.  auto. 
Qed.

Lemma string_to_re_false : forall s s':string, s <> s' -> (string_to_re s) ~!= s'.
Proof.
(* Goal: forall (s s' : string) (_ : not (@eq string s s')), @eq bool (matches (string_to_re s) s') false *)
  induction s.
(* Goal: @eq bool (matches (string_to_re (String a s)) (String a0 s')) false *)
    intros s' Hs.  simpl.  eapply Eps_false.  auto.
(* Goal: forall (s' : string) (_ : not (@eq string (String a s) s')), @eq bool (matches (string_to_re (String a s)) s') false *)
    induction s'.  
(* Goal: @eq bool (matches (string_to_re (String a s)) (String a0 s')) false *)
      intros Hs.  simpl.  auto.
(* Goal: @eq bool (matches (string_to_re (String a s)) (String a0 s')) false *)
      intro Hs.  simpl.  destruct(ascii_dec a a0).
(* Goal: @eq bool (matches (string_to_re s) s') false *)
(* Goal: @eq bool (matches (Cat Empty (string_to_re s)) s') false *)
        erewrite Cat_left_id_s.  rewrite e in Hs.  eapply IHs.
(* Goal: not (@eq string s s') *)
(* Goal: @eq bool (matches (Cat Empty (string_to_re s)) s') false *)
        destruct(string_dec s s').
(* Goal: @eq bool false false *)
          rewrite e0 in Hs.  elim Hs. auto.
(* Goal: @eq bool false false *)
          auto.
(* Goal: @eq bool false false *)
        erewrite Cat_left_zero_s.  auto.
Qed.
