(** * 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.
Require Export RegExp.Star.

(** ** Define [includes] *)

Definition includes (x y:RegExp) : Prop := (x || y) =R= y. 
Notation "x <= y" := (includes x y) (at level 70).

Definition prop_eq (p q:Prop) : Prop := (p <-> q).
Lemma prop_eq_equiv : equiv Prop prop_eq.
Proof.
(* Goal: equiv Prop prop_eq *)
  unfold equiv.  split.
(* Goal: and (includes y (Or x y)) (forall (z : RegExp) (_ : includes x z) (_ : includes y z), includes (Or x y) z) *)
    unfold reflexive.  intros.  unfold prop_eq.  tauto.  split.
(* Goal: forall (x y : Prop) (_ : prop_eq x y), prop_eq y x *)
    unfold transitive.  intros.  unfold prop_eq in *.  tauto.  
(* Goal: forall (x y : Prop) (_ : prop_eq x y), prop_eq y x *)
    unfold symmetric.  intros.  unfold prop_eq in *.  tauto.  
Qed.

Add Parametric Morphism : includes with
signature re_eq ==> re_eq ==> prop_eq as includes_morphism.
Proof.
(* Goal: and (includes y (Or x y)) (forall (z : RegExp) (_ : includes x z) (_ : includes y z), includes (Or x y) z) *)
  intros x y H x0 y0 H0.  unfold prop_eq.  split.
(* Goal: includes (Cat b (Star a)) x *)
    unfold includes.  intros H1.  setoid_rewrite <- H.  setoid_rewrite <- H0.  auto.
(* Goal: includes (Cat b (Star a)) x *)
    unfold includes.  intros H1.  setoid_rewrite H.  setoid_rewrite H0.  auto.
Qed.

Lemma includes_reflexive : reflexive RegExp includes.
Proof.
(* Goal: reflexive RegExp includes *)
  unfold reflexive.  intro x.  unfold includes.  eapply Or_idem. 
Qed.

Lemma includes_antisymmetric : forall x y, x <= y -> y <= x -> x =R= y.
Proof.
(* Goal: forall (x y : RegExp) (_ : includes x y) (_ : includes y x), re_eq x y *)
  intros x y Hxy Hyx.  unfold includes in *.
(* Goal: re_eq x y *)
  setoid_rewrite Or_comm in Hyx.  setoid_symmetry in Hyx.
(* Goal: @eq bool (matches a s''0) true *)
  setoid_transitivity (x || y); auto.  
Qed.

Lemma includes_transitive : transitive RegExp includes.
Proof.
(* Goal: transitive RegExp includes *)
  unfold transitive.  intros x y z Hxy Hyz.  unfold includes in *.
(* Goal: re_eq (Or x z) z *)
  setoid_replace (x || z) with (x || (y || z)).
(* Goal: re_eq (Or z (Or z x)) (Or z x) *)
(* Goal: re_eq (Or x z) (Or z x) *)
  setoid_rewrite <- Or_assoc.
(* Goal: @eq bool (matches a s''0) true *)
  setoid_rewrite Hxy.  auto.
(* Goal: re_eq (Or x z) (Or x (Or y z)) *)
  setoid_rewrite Hyz.  setoid_reflexivity.
Qed.

Lemma implies_to_includes : forall x y, (forall s, x ~== s -> y ~== s) -> x <= y.
Proof.
(* Goal: forall (x y : RegExp) (_ : forall (s : string) (_ : @eq bool (matches x s) true), @eq bool (matches y s) true), includes x y *)
  intros x y Hsxy.
(* Goal: includes x y *)
  unfold includes; unfold re_eq.  intros s.
(* Goal: @eq bool (matches (Or (Star x) (Star y)) s) (matches (Star y) s) *)
  erewrite matches_Or.  
(* Goal: @eq bool (matches a s''0) true *)
  case_eq(x ~= s); case_eq(y ~= s); try auto.
(* Goal: forall (_ : @eq bool (matches y s) false) (_ : @eq bool (matches x s) true), @eq bool (orb true false) false *)
    intros Hys Hxs.  rewrite (Hsxy s Hxs) in Hys.  discriminate Hys.
Qed.

Lemma includes_to_implies : forall x y, x <= y -> (forall s, x ~== s -> y ~== s).
Proof.
(* Goal: forall (x y : RegExp) (_ : includes x y), includes (Star x) (Star y) *)
  intros x y Hxy.  unfold includes in Hxy.  unfold re_eq in Hxy.
(* Goal: forall (s : string) (_ : @eq bool (matches x s) true), @eq bool (matches y s) true *)
  intros s Hx.  specialize(Hxy s).  erewrite matches_Or in Hxy.
(* Goal: @eq bool (matches a s''0) true *)
  destruct(x ~= s); destruct(y ~= s); try discriminate Hx; try discriminate Hxy; auto.
Qed.

(** [x || y] is the least upper bound of [x] and [y] *) 

Lemma Cat_least_upper_bound : forall x y, x <= (x || y) /\ y <= (x || y) /\
  (forall z, x <= z -> y <= z -> (x || y) <= z).
Proof.
(* Goal: and (includes y (Or x y)) (forall (z : RegExp) (_ : includes x z) (_ : includes y z), includes (Or x y) z) *)
  intros x y.  split.
    (* x <= x || y *)
(* Goal: includes (Cat b (Star a)) x *)
    unfold includes.  setoid_rewrite <- Or_assoc.  setoid_rewrite Or_idem.
(* Goal: re_eq (Star r) (Star r) *)
    setoid_reflexivity.
(* Goal: and (includes y (Or x y)) (forall (z : RegExp) (_ : includes x z) (_ : includes y z), includes (Or x y) z) *)
    split.
    (* y <= x || y *)
(* Goal: includes (Cat b (Star a)) x *)
    unfold includes.  setoid_replace (y || (x || y)) with (y || (y || x)).
(* Goal: re_eq (Or z (Or z x)) (Or z x) *)
(* Goal: re_eq (Or x z) (Or z x) *)
    setoid_rewrite <- Or_assoc.  setoid_rewrite Or_idem.
(* Goal: re_eq (Or x z) (Or z x) *)
    eapply Or_comm.
(* Goal: re_eq (Star r) (Star r) *)
    setoid_replace (x || y) with (y || x).  setoid_reflexivity.
(* Goal: re_eq (Or x z) (Or z x) *)
    eapply Or_comm.
    (* forall z : RegExp, x <= z -> y <= z -> x || y <= z *)
(* Goal: includes (Cat z x) (Cat z y) *)
    intros z Hxz Hyz.  unfold includes in *.
(* Goal: re_eq (Or (Or z x) z) (Or z x) *)
    setoid_rewrite Or_assoc.  setoid_replace (y || z) with z.
(* Goal: @eq bool (matches a s''0) true *)
    auto.  auto.
Qed.

(** ** Monotonicity of [includes] *)

Lemma includes_right_Or_monotone : forall x y z, x <= y -> (x || z) <= (y || z).
Proof.
(* Goal: includes (Cat z x) (Cat z y) *)
  intros x y z Hxy.  unfold includes in *.  
(* Goal: re_eq (Or z (Or z x)) (Or z x) *)
(* Goal: re_eq (Or x z) (Or z x) *)
  setoid_rewrite <- Or_assoc.  setoid_replace (y || z) with ((x || y) || z).
(* Goal: re_eq (Or (Or (Or x z) y) z) (Or (Or x y) z) *)
(* Goal: re_eq (Or y z) (Or (Or x y) z) *)
  setoid_replace (x || z || y) with (x || y || z).
(* Goal: re_eq (Or (Or (Or x y) z) z) (Or (Or x y) z) *)
(* Goal: re_eq (Or (Or x z) y) (Or (Or x y) z) *)
(* Goal: re_eq (Or y z) (Or (Or x y) z) *)
  setoid_replace (x || y || z || z) with (x || y || (z || z)).
(* Goal: re_eq (Star r) (Star r) *)
  setoid_rewrite Or_idem.  setoid_reflexivity.
(* Goal: re_eq (Or z (Or z x)) (Or z x) *)
(* Goal: re_eq (Or x z) (Or z x) *)
  repeat setoid_rewrite <- Or_assoc.  setoid_reflexivity.
(* Goal: re_eq (Or (Or z x) z) (Or z x) *)
  setoid_rewrite Or_assoc.  setoid_replace (z || y) with (y || z).
(* Goal: re_eq (Star r) (Star r) *)
  setoid_rewrite Or_comm.  setoid_reflexivity.
(* Goal: re_eq (Or x z) (Or z x) *)
  eapply Or_comm.
(* Goal: @eq bool (matches a s''0) true *)
  setoid_replace (x || y) with y.  setoid_reflexivity.  auto.
Qed.

Lemma includes_left_Or_monotone : forall x y z, x <= y -> (z || x) <= (z || y).
Proof.
(* Goal: includes (Cat z x) (Cat z y) *)
  intros x y z Hxy.  unfold includes in *.
(* Goal: re_eq (Or z (Or z x)) (Or z x) *)
(* Goal: re_eq (Or x z) (Or z x) *)
  repeat setoid_rewrite <- Or_assoc.
(* Goal: re_eq (Or (Or (Or z x) z) y) (Or z y) *)
  setoid_replace (z || x || z) with (z || x).
(* Goal: re_eq (Cat z (Or x y)) (Cat z y) *)
  setoid_rewrite Or_assoc.  setoid_rewrite Hxy.  setoid_reflexivity.
(* Goal: re_eq (Or (Or z x) z) (Or z x) *)
  setoid_rewrite Or_assoc.  setoid_replace (x || z) with (z || x).
(* Goal: re_eq (Or z (Or z x)) (Or z x) *)
(* Goal: re_eq (Or x z) (Or z x) *)
  setoid_rewrite <- Or_assoc.  setoid_rewrite Or_idem.  setoid_reflexivity.
(* Goal: re_eq (Or x z) (Or z x) *)
  eapply Or_comm.
Qed.

Lemma includes_right_Cat_monotone : forall x y z, x <= y -> (x ++ z) <= (y ++ z).
Proof.
(* Goal: includes (Cat z x) (Cat z y) *)
  intros x y z Hxy.  unfold includes in *.
(* Goal: re_eq (Cat z (Or x y)) (Cat z y) *)
  erewrite <- Cat_right_distr.  setoid_rewrite Hxy.  setoid_reflexivity.
Qed.

Lemma includes_left_Cat_monotone : forall x y z, x <= y -> (z ++ x) <= (z ++ y).
Proof.
(* Goal: includes (Cat z x) (Cat z y) *)
  intros x y z Hxy.  unfold includes in *.
(* Goal: re_eq (Cat z (Or x y)) (Cat z y) *)
  erewrite <- Cat_left_distr.  setoid_rewrite Hxy.  setoid_reflexivity.
Qed.

Lemma includes_Star_monotone : forall x y, x <= y -> (Star x) <= (Star y).
Proof.
(* Goal: forall (x y : RegExp) (_ : includes x y), includes (Star x) (Star y) *)
  intros x y Hxy.  specialize(includes_to_implies x y Hxy).  intro H01.
(* Goal: includes (Star x) (Star y) *)
  assert(H1: forall s, Star x ~== s -> Star y ~== s).
(* Goal: forall (s : string) (_ : @eq bool (matches (Star x) s) true), @eq bool (matches (Star y) s) true *)
(* Goal: includes (Star x) (Star y) *)
    intros s HSx.  specialize(Star_to_list s x HSx).  intros H.
(* Goal: @eq bool (matches (Star y) s) true *)
(* Goal: includes (Star x) (Star y) *)
    destruct H as [ss [Ha [Hb Hc]]].
    assert(H1': forall zs, forallb (fun s : string => x ~= s) zs = true ->
      forallb (fun s : string => y ~= s) zs = true).
(* Goal: @eq bool (matches a s''0) true *)
      induction zs.  simpl.  intro H.  auto.        
(* Goal: gt (str_length (String a0 s''0)) O *)
(* Goal: @eq bool (matches x s) true *)
      simpl.  intro H.
        case_eq(x ~= a); case_eq(forallb (fun s : string => x ~= s) zs); 
        intros H' H''; rewrite H' in H; rewrite H'' in H; simpl in H; 
        try discriminate H.
(* Goal: @eq bool (matches a s''0) true *)
        replace (y ~= a) with true.  erewrite (IHzs H').  auto.
(* Goal: @eq bool (matches a s''0) true *)
        symmetry.  eapply H01.  auto.
(* Goal: forall _ : @eq bool (matches (Or (Or b (Cat x a)) x) s) true, @eq bool (matches x s) true *)
(* Goal: @eq bool (matches (Or (Or b (Cat x a)) x) s) true *)
(* Goal: @eq bool (matches x s) true *)
    specialize(H1' ss Ha).  specialize(list_to_Star ss y H1').  intros H.
(* Goal: @eq bool (matches a s''0) true *)
    erewrite Hb in H.  auto.  
(* Goal: includes (Star x) (Star y) *)
  assert(H02: forall s, y ~!= s -> x ~!= s).
(* Goal: @eq bool (matches x s) false *)
(* Goal: includes (Star x) (Star y) *)
    intros s Hy.  specialize(Hxy s).  erewrite matches_Or in Hxy.  
(* Goal: @eq bool (matches x s) false *)
(* Goal: includes (Star x) (Star y) *)
    rewrite Hy in Hxy.
(* Goal: @eq bool (matches x s) false *)
(* Goal: includes (Star x) (Star y) *)
    destruct(x ~= s).  
(* Goal: @eq bool true false *)
(* Goal: @eq bool false false *)
(* Goal: includes (Star x) (Star y) *)
      simpl in Hxy.  discriminate Hxy.  
(* Goal: @eq bool (matches a s''0) true *)
      auto.
(* Goal: includes (Cat b (Star a)) x *)
  unfold includes. unfold re_eq. intro s. erewrite matches_Or.
  case_eq (Star x ~= s); case_eq (Star y ~= s); simpl; 
  intros H' H''; try reflexivity.
(* Goal: @eq bool true false *)
    specialize(H1 s H'').  rewrite H' in H1.  discriminate H1.
Qed.

(** ** Axioms for [includes] *)
(** See also lemma [matches_Star_right] which is stronger lemma. *)

Theorem Star_right : forall r, (Eps || (r ++ Star r)) <= Star r.
Proof. 
(* Goal: forall r : RegExp, includes (Or Eps (Cat (Star r) r)) (Star r) *)
  intros r.
(* Goal: includes (Cat b (Star a)) x *)
  unfold includes.  setoid_rewrite <- matches_Star_right.
(* Goal: re_eq (Star r) (Star r) *)
  setoid_rewrite Or_idem.  setoid_reflexivity. 
Qed.

(** See also lemma [matches_Star_left] which is stronger lemma. *)

Theorem Star_left : forall r, (Eps || (Star r ++ r)) <= Star r.
Proof.
(* Goal: forall r : RegExp, includes (Or Eps (Cat (Star r) r)) (Star r) *)
  intros r.
(* Goal: includes (Cat b (Star a)) x *)
  unfold includes.  setoid_rewrite <- matches_Star_left.
(* Goal: re_eq (Star r) (Star r) *)
  setoid_rewrite Or_idem.  setoid_reflexivity. 
Qed.




Lemma Star_eq_left_s : forall s a b x, (b || (a ++ x)) <= x -> 
  ((Star a) ++ b) ~== s -> x ~== s.
Proof.
(* Goal: forall (s : string) (a b x : RegExp) (_ : includes (Or b (Cat x a)) x) (_ : @eq bool (matches (Cat b (Star a)) s) true), @eq bool (matches x s) true *)
  refine (induction_ltof2 string str_length _ _).
(* Goal: forall (x : string) (_ : forall (y : string) (_ : ltof string str_length y x) (a b x0 : RegExp) (_ : includes (Or b (Cat a x0)) x0) (_ : @eq bool (matches (Cat (Star a) b) y) true), @eq bool (matches x0 y) true) (a b x0 : RegExp) (_ : includes (Or b (Cat a x0)) x0) (_ : @eq bool (matches (Cat (Star a) b) x) true), @eq bool (matches x0 x) true *)
  intros s IH a b x Hbax HSab.
(* Goal: @eq bool (matches x s) true *)
  specialize(divide_Cat s (Star a) b HSab).  intro H'.
(* Goal: @eq bool (matches x s) true *)
  destruct H' as [s' [s'' [H01 [H02 H03]]]].
(* Goal: @eq bool (matches x s) true *)
  case_eq (string_dec s' ""%string); intros Hs _.
    (* s = "" *)
(* Goal: @eq bool (matches x s) true *)
(* Goal: @eq bool (matches x s) true *)
    rewrite Hs in *.  simpl in H01.
(* Goal: forall _ : @eq bool (matches (Or (Or b (Cat x a)) x) s) true, @eq bool (matches x s) true *)
(* Goal: @eq bool (matches (Or (Or b (Cat x a)) x) s) true *)
(* Goal: @eq bool (matches x s) true *)
    unfold includes in Hbax.  cut ((b || (a ++ x) || x) ~== s).  intros H.
(* Goal: @eq bool (matches a s''0) true *)
    unfold re_eq in Hbax.  specialize(Hbax s).  rewrite <- Hbax.  auto.
(* Goal: @eq bool (matches a s''0) true *)
    repeat rewrite matches_Or.  rewrite H01.  rewrite H03.  simpl.  auto.
    (* s <> "" *)
(* Goal: @eq bool (matches x s) true *)
    specialize(divide_Star_right s' a H02 Hs).  intro H0.
(* Goal: @eq bool (matches x s) true *)
    destruct H0 as [s'0 [s''0 [H11 [H12 [H13 H14]]]]].
    (* y = s''0 ++ s'' *)
(* Goal: @eq bool (matches x s) true *)
    assert(Hltof: ltof string str_length (s''0 ++ s'')%string s).
(* Goal: @eq bool (matches (Cat x a) s) true *)
     unfold ltof.  rewrite H01.  rewrite H11.
(* Goal: lt (str_length (append s' s'0)) (str_length (append s' (append s'0 s''0))) *)
(* Goal: @eq bool (matches x s) true *)
     repeat rewrite str_length_append.
(* Goal: lt (Init.Nat.add (str_length s''0) (str_length s'')) (Init.Nat.add (Init.Nat.add (str_length s'0) (str_length s''0)) (str_length s'')) *)
(* Goal: @eq bool (matches x s) true *)
     cut(str_length s'0 > 0).  intro Hs'0.  omega.
(* Goal: gt (str_length s'0) O *)
(* Goal: @eq bool (matches x s) true *)
     induction s'0.
(* Goal: @eq bool (matches a s''0) true *)
       elim H12.  auto.  
(* Goal: gt (str_length (String a0 s''0)) O *)
(* Goal: @eq bool (matches x s) true *)
       simpl.  omega.
(* Goal: @eq bool (matches x s) true *)
    assert(Hy: (Star a ++ b) ~== (s''0 ++ s'')).
(* Goal: @eq bool (matches a s''0) true *)
      eapply matches_Cat.  auto.  auto.
(* Goal: @eq bool (matches x s) true *)
    assert(Hy': x ~== (s''0 ++ s'')%string).
(* Goal: @eq bool (matches x (append s''0 s'')) true *)
(* Goal: @eq bool (matches x s) true *)
      apply (IH (s''0 ++ s'')%string Hltof a b x Hbax Hy).
(* Goal: @eq bool (matches x s) true *)
    unfold includes in Hbax.  unfold re_eq in Hbax.
(* Goal: @eq bool (matches a s''0) true *)
    cut(b || (a ++ x) || x ~== s).  intro H.  rewrite <- (Hbax s).  auto.
(* Goal: forall _ : includes (Or b (Cat x a)) x, includes (Cat b (Star a)) x *)
    repeat rewrite matches_Or.  cut((a ++ x) ~== s).  intro H.  rewrite H.
(* Goal: @eq bool (orb (orb (matches b s) true) (matches x s)) true *)
(* Goal: @eq bool (matches (Cat x a) s) true *)
    destruct(b ~= s); destruct(x ~= s); reflexivity.
(* Goal: @eq bool (matches (Cat x a) s) true *)
    rewrite H01.  rewrite H11.  rewrite string_assoc.
(* Goal: @eq bool (matches a s''0) true *)
    eapply matches_Cat.  auto.  auto.
Qed.

Theorem Star_eq_left : forall a b x, (b || (a ++ x)) <= x -> ((Star a) ++ b) <= x.
Proof.
(* Goal: includes (Cat b (Star a)) x *)
  intros a b x. intro H.  unfold includes.  unfold re_eq.  intro s.
  case_eq((Star a ++ b) ~= s); case_eq(x ~= s); intros H1 H2;  rewrite matches_Or;
  rewrite H1; rewrite H2; try reflexivity.
(* Goal: @eq bool (orb true false) false *)
  specialize(Star_eq_left_s s a b x H H2).  intro H'.  rewrite H' in H1.  
(* Goal: @eq bool (orb true false) false *)
  discriminate H1.
Qed.

Theorem Star_eq_right_s : forall s a b x, (b || (x ++ a)) <= x -> 
  (b ++ (Star a)) ~== s -> x ~== s.
Proof.
(* Goal: forall (s : string) (a b x : RegExp) (_ : includes (Or b (Cat x a)) x) (_ : @eq bool (matches (Cat b (Star a)) s) true), @eq bool (matches x s) true *)
  refine (induction_ltof2 string str_length _ _).
(* Goal: forall (x : string) (_ : forall (y : string) (_ : ltof string str_length y x) (a b x0 : RegExp) (_ : includes (Or b (Cat x0 a)) x0) (_ : @eq bool (matches (Cat b (Star a)) y) true), @eq bool (matches x0 y) true) (a b x0 : RegExp) (_ : includes (Or b (Cat x0 a)) x0) (_ : @eq bool (matches (Cat b (Star a)) x) true), @eq bool (matches x0 x) true *)
  intros s IH a b x Hbxa HbSa.
(* Goal: forall _ : @eq bool (matches x s) true, @eq bool (orb true false) false *)
  specialize(divide_Cat s b (Star a) HbSa).  intro H'.
(* Goal: @eq bool (matches x s) true *)
  destruct H' as [s' [s'' [H01 [H02 H03]]]].
(* Goal: @eq bool (matches x s) true *)
  case_eq (string_dec s'' ""%string); intros Hs _.
    (* s'' = "" *)
(* Goal: @eq bool (matches x s) true *)
(* Goal: @eq bool (matches x s) true *)
    rewrite Hs in *.  rewrite string_right_id in H01.
(* Goal: forall _ : @eq bool (matches (Or (Or b (Cat x a)) x) s) true, @eq bool (matches x s) true *)
(* Goal: @eq bool (matches (Or (Or b (Cat x a)) x) s) true *)
(* Goal: @eq bool (matches x s) true *)
    unfold includes in Hbxa.  cut ((b || (x ++ a) || x) ~== s).  intros H.
(* Goal: @eq bool (matches a s''0) true *)
    unfold re_eq in Hbxa.  specialize(Hbxa s).  rewrite <- Hbxa.  auto.
(* Goal: @eq bool (matches a s''0) true *)
    repeat rewrite matches_Or.  rewrite H01.  rewrite H02.  simpl.  auto.
    (* s'' <> "" *)
(* Goal: forall _ : @sigT string (fun s' : string => @sig string (fun s''0 : string => and (@eq string s'' (append s' s''0)) (and (not (@eq string s''0 EmptyString)) (and (@eq bool (matches (Star a) s') true) (@eq bool (matches a s''0) true))))), @eq bool (matches x s) true *)
    specialize(divide_Star_left s'' a H03 Hs).  intro H0.
(* Goal: @eq bool (matches x s) true *)
    destruct H0 as [s'0 [s''0 [H11 [H12 [H13 H14]]]]].
    (* y = s' ++ s'0 *)
(* Goal: @eq bool (matches x s) true *)
    assert(Hltof: ltof string str_length (s' ++ s'0)%string s).
(* Goal: @eq bool (matches (Cat x a) s) true *)
      unfold ltof.  rewrite H01.  rewrite H11.
(* Goal: lt (str_length (append s' s'0)) (str_length (append s' (append s'0 s''0))) *)
(* Goal: @eq bool (matches x s) true *)
      repeat rewrite str_length_append.
(* Goal: gt (S (str_length s''0)) O *)
(* Goal: @eq bool (matches x s) true *)
      cut(str_length s''0 > 0).  intro Hs''0.  omega.
(* Goal: gt (str_length s''0) O *)
(* Goal: @eq bool (matches x s) true *)
      induction s''0.  
(* Goal: @eq bool (matches a s''0) true *)
        elim H12.  auto.  
(* Goal: gt (str_length (String a0 s''0)) O *)
(* Goal: @eq bool (matches x s) true *)
        simpl.  omega.
(* Goal: @eq bool (matches x s) true *)
    assert(Hy: (b ++ Star a) ~== (s' ++ s'0)).
(* Goal: @eq bool (matches a s''0) true *)
      eapply matches_Cat.  auto.  auto.
(* Goal: @eq bool (matches x s) true *)
    assert(Hy': x ~== (s' ++ s'0)%string).
(* Goal: @eq bool (matches x (append s' s'0)) true *)
(* Goal: @eq bool (matches x s) true *)
      apply (IH (s' ++ s'0)%string Hltof a b x Hbxa Hy).
(* Goal: @eq bool (matches x s) true *)
    unfold includes in Hbxa.  unfold re_eq in Hbxa.
(* Goal: @eq bool (matches a s''0) true *)
    cut(b || (x ++ a) || x ~== s).  intro H.  rewrite <- (Hbxa s).  auto.
(* Goal: forall _ : includes (Or b (Cat x a)) x, includes (Cat b (Star a)) x *)
    repeat rewrite matches_Or.  cut((x ++ a) ~== s).  intro H.  rewrite H.
(* Goal: @eq bool (orb (orb (matches b s) true) (matches x s)) true *)
(* Goal: @eq bool (matches (Cat x a) s) true *)
    destruct(b ~= s); destruct(x ~= s); reflexivity.
(* Goal: @eq bool (matches (Cat x a) s) true *)
    rewrite H01.  rewrite H11.  rewrite <- string_assoc.  
(* Goal: @eq bool (matches a s''0) true *)
    eapply matches_Cat.  auto.  auto.
Qed.

Theorem Star_eq_right : forall a b x, (b || (x ++ a)) <= x -> (b ++ (Star a)) <= x.
Proof.
(* Goal: includes (Cat b (Star a)) x *)
  intros a b x. intro H.  unfold includes.  unfold re_eq.  intro s.
  case_eq((b ++ Star a) ~= s); case_eq(x ~= s); intros H1 H2;  rewrite matches_Or;
  rewrite H1; rewrite H2; try reflexivity.
(* Goal: @eq bool (orb true false) false *)
  specialize(Star_eq_right_s s a b x H H2).  intro H'.  rewrite H' in H1.  
(* Goal: @eq bool (orb true false) false *)
  discriminate H1.
Qed.













