Star lemma

star_lemma.v

Set Implicit Arguments.

Require Import Ascii String.

Inductive regex : Set :=
| Emp : regex  
| Eps : regex          
| Chr : ascii -> regex
| Cat : regex -> regex -> regex
| Choice : regex -> regex -> regex
| Star : regex -> regex.

Open Scope string_scope.

Notation "'#0'" := Emp.
Notation "'#1'" := Eps.
Notation "'$' c" := (Chr c)(at level 40).
Notation "e '@' e1" := (Cat e e1)(at level 15, left associativity).
Notation "e ':+:' e1" := (Choice e e1)(at level 20, left associativity).
Notation "e '^*'" := (Star e)(at level 40).
  
(** Semantics of regular expressions *)

Reserved Notation "s '<<-' e" (at level 40).

Inductive in_regex : string -> regex -> Prop :=
| InEps
  : "" <<- #1
| InChr
  : forall c
  , (String c EmptyString) <<- ($ c)
| InCat
  :  forall e e' s s' s1
  ,  s <<- e
  -> s' <<- e'
  -> s1 = s ++ s'
  -> s1 <<- (e @ e')
| InLeft
  :  forall s e e'
  ,  s <<- e
  -> s <<- (e :+: e')
| InRight
  :  forall s' e e'
  ,  s' <<- e'
  -> s' <<- (e :+: e')
| InStar
  :  forall s e
  ,  s <<- (#1 :+: (e @ (e ^*)))
  -> s <<- (e ^*)
where "s '<<-' e" := (in_regex s e).

Hint Constructors in_regex.

Fixpoint ntimes (n : nat) (e : regex) : regex :=
match n with
  | O    => #1
  | S n' => e @ ntimes n' e
end.

Fixpoint star_unfold s e (pr : s <<- (e ^*)) { struct pr } :
  exists n, s <<- ntimes n e.
Proof.
inversion pr as [ | | | | | s1 e1 pr1 ]; subst.
inversion pr1 as [ | | | | s2 e2 e2' pr2 | ]; subst.
 - exists 0; assumption.
 - inversion pr2; subst.
  destruct (star_unfold _ _ H3) as [n Hn].
  exists (S n); eapply InCat; (eassumption || reflexivity).
Qed.

Lemma star_lemma : forall s, s <<- (#1 ^*) -> s = "".
Proof.
intros s pr; destruct (star_unfold pr) as [n Hn].
 clear pr; induction n.
 - inversion Hn; reflexivity.
 - inversion Hn; subst.
   apply IHn; inversion H1; assumption.
Qed.