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

Require Export RegExp.Utility.
Require Export RegExp.Definitions.

(** ** [Empty] *)
(** [Empty] corresponds to 0 in Kleene algebra. *)

Lemma Empty_false : forall s, Empty ~!= s.
Proof.
(* Goal: forall (s : string) (r : RegExp), @eq bool (matches (Or Empty r) s) (matches r s) *)
  induction s.
(* Goal: forall r : RegExp, @eq bool (nu r) (nu r) *)
(* Goal: forall r : RegExp, @eq bool (matches (Or Empty r) (String a s)) (matches r (String a s)) *)
    reflexivity.
(* Goal: forall r : RegExp, @eq bool (matches (Or Empty r) (String a s)) (matches r (String a s)) *)
    simpl.  apply IHs.
Qed.

(** ** [Eps] *)
(** [Eps] corresponds to 1 in Kleene algebra. *)

Lemma Eps_true : Eps ~== EmptyString.
Proof.
(* Goal: forall r : RegExp, @eq bool (nu r) (nu r) *)
(* Goal: forall r : RegExp, @eq bool (matches (Or Empty r) (String a s)) (matches r (String a s)) *)
  simpl.  reflexivity.
Qed.

Lemma Eps_false : forall s, s <> ""%string -> Eps ~!= s.
Proof.
(* Goal: forall (s : string) (r : RegExp), @eq bool (matches (Or Empty r) s) (matches r s) *)
  induction s.
(* Goal: forall _ : not (@eq string EmptyString EmptyString), @eq bool (matches Eps EmptyString) false *)
(* Goal: forall _ : not (@eq string (String a s) EmptyString), @eq bool (matches Eps (String a s)) false *)
    intro Hs. elim Hs. auto.
(* Goal: forall r : RegExp, @eq bool (matches (Or Empty r) (String a s)) (matches r (String a s)) *)
    intro Has. simpl. eapply Empty_false.
Qed.

(** ** Boolean operations on [RegExp] are morphism. *)
(** [Or] corresponds to plus in Kleene algebra. *)

Add Parametric Morphism : Or with
signature re_eq ==> re_eq ==> re_eq as Or_morphism.
Proof.
(* Goal: forall (x y : RegExp) (_ : re_eq x y) (x0 y0 : RegExp) (_ : re_eq x0 y0), re_eq (And x x0) (And y y0) *)
  intros x y H x0 y0 H0.  unfold re_eq in *.  intro s.
(* Goal: @eq bool (matches (Not x) s) (matches (Not y) s) *)
  generalize dependent x.  generalize dependent y. 
(* Goal: forall (y x : RegExp) (_ : forall s : string, @eq bool (matches x s) (matches y s)), @eq bool (matches (And x x0) s) (matches (And y y0) s) *)
  generalize dependent x0. generalize dependent y0. 
(* Goal: forall (s : string) (r : RegExp), @eq bool (matches (Or Empty r) s) (matches r s) *)
  induction s.
    (* s = "" *)
(* Goal: forall (y0 x0 : RegExp) (_ : forall s : string, @eq bool (matches x0 s) (matches y0 s)) (y x : RegExp) (_ : forall s : string, @eq bool (matches x s) (matches y s)), @eq bool (matches (And (derive a x) (derive a x0)) s) (matches (And (derive a y) (derive a y0)) s) *)
    intros y0 x0 H0 y x H.  specialize (H0 ""%string).  specialize (H ""%string).
(* Goal: forall r : RegExp, @eq bool (nu r) (nu r) *)
(* Goal: forall r : RegExp, @eq bool (matches (Or Empty r) (String a s)) (matches r (String a s)) *)
    simpl in *.  rewrite <- H0.  rewrite <- H.  reflexivity.
    (* s = String a s *)
(* Goal: forall r : RegExp, @eq bool (matches (Or Empty r) (String a s)) (matches r (String a s)) *)
    simpl.  intros y0 x0 H0 y x H.  eapply IHs.
(* Goal: forall r : RegExp, re_eq (Or r Empty) r *)
      intros.  repeat rewrite <- derivation.  eapply H0.
(* Goal: forall r : RegExp, re_eq (Or r Empty) r *)
      intros.  repeat rewrite <- derivation.  eapply H.
Qed.

Add Parametric Morphism : And with
signature re_eq ==> re_eq ==> re_eq as And_morphism.
Proof.
(* Goal: forall (x y : RegExp) (_ : re_eq x y) (x0 y0 : RegExp) (_ : re_eq x0 y0), re_eq (And x x0) (And y y0) *)
  intros x y H x0 y0 H0.  unfold re_eq in *.  intros s.
(* Goal: @eq bool (matches (Not x) s) (matches (Not y) s) *)
  generalize dependent x.  generalize dependent y. 
(* Goal: forall (y x : RegExp) (_ : forall s : string, @eq bool (matches x s) (matches y s)), @eq bool (matches (And x x0) s) (matches (And y y0) s) *)
  generalize dependent x0. generalize dependent y0. 
(* Goal: forall (s : string) (r : RegExp), @eq bool (matches (Or Empty r) s) (matches r s) *)
  induction s.
    (* s = "" *)
(* Goal: forall (y0 x0 : RegExp) (_ : forall s : string, @eq bool (matches x0 s) (matches y0 s)) (y x : RegExp) (_ : forall s : string, @eq bool (matches x s) (matches y s)), @eq bool (matches (And (derive a x) (derive a x0)) s) (matches (And (derive a y) (derive a y0)) s) *)
    intros y0 x0 H0 y x H.  specialize (H0 ""%string).  specialize (H ""%string).
(* Goal: forall r : RegExp, @eq bool (nu r) (nu r) *)
(* Goal: forall r : RegExp, @eq bool (matches (Or Empty r) (String a s)) (matches r (String a s)) *)
    simpl in *.  rewrite <- H0.  rewrite <- H.  reflexivity.
    (* s = String a s *)
(* Goal: forall r : RegExp, @eq bool (matches (Or Empty r) (String a s)) (matches r (String a s)) *)
    simpl.  intros y0 x0 H0 y x H.  eapply IHs.
(* Goal: @eq bool (matches (derive a x) s0) (matches (derive a y) s0) *)
      intros s0.  repeat rewrite <- derivation.  eapply H0.
(* Goal: @eq bool (matches (derive a x) s0) (matches (derive a y) s0) *)
      intros s0.  repeat rewrite <- derivation.  eapply H.
Qed.

Add Parametric Morphism : Not with
signature re_eq ==> re_eq as Not_morphism.
Proof.
(* Goal: re_eq (Not x) (Not y) *)
  intros x y H.  unfold re_eq in *.  intros s.
(* Goal: @eq bool (matches (Not x) s) (matches (Not y) s) *)
  generalize dependent x. generalize dependent y. 
(* Goal: forall (s : string) (r : RegExp), @eq bool (matches (Or Empty r) s) (matches r s) *)
  induction s.
    (* s = "" *)
(* Goal: forall r : RegExp, @eq bool (nu r) (nu r) *)
(* Goal: forall r : RegExp, @eq bool (matches (Or Empty r) (String a s)) (matches r (String a s)) *)
    intros y x H.  specialize (H ""%string).  simpl in *.  rewrite <- H.  reflexivity.
    (* s = String a s *)
(* Goal: forall r : RegExp, @eq bool (matches (Or Empty r) (String a s)) (matches r (String a s)) *)
    simpl.  intros y x H.  eapply IHs.
(* Goal: @eq bool (matches (derive a x) s0) (matches (derive a y) s0) *)
    intros s0.  repeat rewrite <- derivation.  eapply H.
Qed.

(** [matches] is a homomorphism from [RegExp] to bool for [And], [Or], and [Not]. *)

Lemma matches_Or : forall s r r',  r || r' ~= s = ((r ~= s) || (r' ~= s))%bool.
Proof.
(* Goal: forall (s : string) (r : RegExp), @eq bool (matches (Or Empty r) s) (matches r s) *)
  induction s.
(* Goal: forall r : RegExp, @eq bool (nu r) (nu r) *)
(* Goal: forall r : RegExp, @eq bool (matches (Or Empty r) (String a s)) (matches r (String a s)) *)
    simpl.  reflexivity.
(* Goal: forall r : RegExp, @eq bool (matches (Or Empty r) (String a s)) (matches r (String a s)) *)
    simpl.  intros r r'.  eapply IHs.
Qed.

Lemma matches_And : forall s r r',  matches (And r r') s = ((r ~= s) && (r' ~= s))%bool.
Proof.
(* Goal: forall (s : string) (r : RegExp), @eq bool (matches (Or Empty r) s) (matches r s) *)
  induction s.
(* Goal: forall r : RegExp, @eq bool (nu r) (nu r) *)
(* Goal: forall r : RegExp, @eq bool (matches (Or Empty r) (String a s)) (matches r (String a s)) *)
    simpl.  reflexivity.
(* Goal: forall r : RegExp, @eq bool (matches (Or Empty r) (String a s)) (matches r (String a s)) *)
    simpl.  intros.  eapply IHs.
Qed.

Lemma matches_Not : forall s r,  (Not r) ~= s = negb (r ~= s).
Proof.
(* Goal: forall (s : string) (r : RegExp), @eq bool (matches (Or Empty r) s) (matches r s) *)
  induction s.
(* Goal: forall r : RegExp, @eq bool (nu r) (nu r) *)
(* Goal: forall r : RegExp, @eq bool (matches (Or Empty r) (String a s)) (matches r (String a s)) *)
    simpl.  reflexivity.
(* Goal: forall r : RegExp, @eq bool (matches (Or Empty r) (String a s)) (matches r (String a s)) *)
    simpl.  intros.  eapply IHs.
Qed.

(** ** Axioms for [Or] *)
(** Commutativity and associativity of [Or] and [And]. *)

Lemma Or_comm_s : forall s r r', (r || r') ~= s = (r' || r) ~= s.
Proof.
(* Goal: forall (s : string) (r r' : RegExp), @eq bool (matches (Or r r') s) (matches (Or r' r) s) *)
  intros s r r'.  repeat erewrite matches_Or.
(* Goal: forall r : RegExp, @eq bool (nu r) (nu r) *)
(* Goal: forall r : RegExp, @eq bool (matches (Or Empty r) (String a s)) (matches r (String a s)) *)
  destruct (r ~= s); destruct (r' ~= s); reflexivity.
Qed.

Theorem Or_comm : forall r r', r || r' =R= r' || r.
Proof.
(* Goal: forall r : RegExp, re_eq (Or r r) r *)
  unfold re_eq.  intros r r' s.  eapply Or_comm_s.
Qed.

Lemma Or_assoc_s : forall s r r' r'', 
  ((r || r') || r'') ~= s = (r || (r' || r'')) ~= s.
Proof.
(* Goal: forall r : RegExp, re_eq (Or r Empty) r *)
  intros.   repeat erewrite matches_Or.
(* Goal: forall r : RegExp, @eq bool (nu r) (nu r) *)
(* Goal: forall r : RegExp, @eq bool (matches (Or Empty r) (String a s)) (matches r (String a s)) *)
  destruct (r ~= s); destruct (r' ~= s); destruct (r'' ~= s); reflexivity.
Qed.

Theorem Or_assoc : forall r r' r'', (r || r') || r'' =R= r || (r' || r'').
Proof.
(* Goal: forall r : RegExp, re_eq (Or r r) r *)
  unfold re_eq.  intros r r' r'' s.  eapply Or_assoc_s.
Qed.

Lemma And_comm : forall r r', And r r' =R= And r' r.
Proof.
(* Goal: forall r : RegExp, re_eq (Or r r) r *)
  unfold re_eq.  intros r r' s.  repeat erewrite matches_And.  
(* Goal: forall r : RegExp, @eq bool (nu r) (nu r) *)
(* Goal: forall r : RegExp, @eq bool (matches (Or Empty r) (String a s)) (matches r (String a s)) *)
  destruct (r ~= s); destruct (r' ~= s); reflexivity.
Qed.

Lemma And_assoc : forall r r' r'', And (And r r') r'' =R= And r (And r' r'').
Proof.
(* Goal: forall r : RegExp, re_eq (Or r r) r *)
  unfold re_eq.  intros r r' r'' s.  repeat erewrite matches_And.
(* Goal: forall r : RegExp, @eq bool (nu r) (nu r) *)
(* Goal: forall r : RegExp, @eq bool (matches (Or Empty r) (String a s)) (matches r (String a s)) *)
  destruct (r ~= s); destruct (r' ~= s); destruct (r'' ~= s); reflexivity.
Qed.

(** [Empty] is the identity element 0 for [Or]. *)

Lemma Or_left_id_s : forall s r, (Empty || r) ~= s = r ~= s.
Proof.
(* Goal: forall (s : string) (r : RegExp), @eq bool (matches (Or Empty r) s) (matches r s) *)
  induction s.
(* Goal: forall r : RegExp, @eq bool (nu r) (nu r) *)
(* Goal: forall r : RegExp, @eq bool (matches (Or Empty r) (String a s)) (matches r (String a s)) *)
    simpl.  reflexivity.
(* Goal: forall r : RegExp, @eq bool (matches (Or Empty r) (String a s)) (matches r (String a s)) *)
    simpl.  intros r.  eapply IHs.
Qed.

Theorem Or_left_id : forall r, Empty || r =R= r.
Proof.
(* Goal: forall r : RegExp, re_eq (Or r r) r *)
  unfold re_eq.  intros r s.  eapply Or_left_id_s.
Qed.

Theorem Or_right_id : forall r, r || Empty =R= r.
(* Goal: forall r : RegExp, re_eq (Or r Empty) r *)
  intros.  setoid_rewrite Or_comm.
(* Goal: re_eq (Or Empty r) r *)
  eapply Or_left_id.
Qed.

Corollary Or_right_id_s : forall s r, (r || Empty) ~= s = r ~= s.
Proof.
(* Goal: forall (s : string) (r : RegExp), @eq bool (matches (Or r r) s) (matches r s) *)
  intros s r.  specialize Or_right_id.  
(* Goal: @eq bool (matches (Or r Empty) s) (matches r s) *)
  intros H.  unfold re_eq in H.  eapply H.
Qed.

(** [Or] is idempotent. *)

Lemma Or_idem_s : forall s r, (r || r) ~= s = r ~= s.
Proof.
(* Goal: forall r : RegExp, @eq bool (nu r) (nu r) *)
(* Goal: forall r : RegExp, @eq bool (matches (Or Empty r) (String a s)) (matches r (String a s)) *)
  intros s r.  erewrite matches_Or.  destruct (r ~= s); reflexivity.
Qed.

Theorem Or_idem : forall r, r || r =R= r.
Proof.
(* Goal: forall r : RegExp, re_eq (Or r r) r *)
  unfold re_eq.  intros r s.  eapply Or_idem_s.
Qed.
