regexp.v

regexp.v

Require Export SfLib.

Inductive regexp :=
  | empty : regexp
  | atom : nat -> regexp
  | any : regexp
  | seq : regexp -> regexp -> regexp
  | disj : regexp -> regexp -> regexp
  | star : regexp -> regexp
  | plus : regexp -> regexp.

Inductive regexp_match : regexp -> list nat -> list nat -> Prop :=
  | regexp_match_empty : forall vs:list nat,
    regexp_match empty vs vs
  | regexp_match_atom : forall n:nat, forall vs:list nat,
    regexp_match (atom n) (cons n vs) vs
  | regexp_match_any : forall n:nat, forall vs:list nat,
    regexp_match (any) (cons n vs) vs
  | regexp_match_seq : forall e1 e2:regexp, forall vs1 vs2 vs3:list nat,
    regexp_match e1 vs1 vs2 ->
    regexp_match e2 vs2 vs3 ->
    regexp_match (seq e1 e2) vs1 vs3
  | regexp_match_disj1 : forall e1 e2:regexp, forall vs1 vs2:list nat,
    regexp_match e1 vs1 vs2 ->
    regexp_match (disj e1 e2) vs1 vs2
  | regexp_match_disj2 : forall e1 e2:regexp, forall vs1 vs2:list nat,
    regexp_match e2 vs1 vs2 ->
    regexp_match (disj e1 e2) vs1 vs2
  | regexp_match_star1 : forall e:regexp, forall vs:list nat,
    regexp_match (star e) vs vs
  | regexp_match_star2 : forall e:regexp, forall vs:list nat,
    regexp_match e vs vs ->
    regexp_match (star e) vs vs
  | regexp_match_star3 : forall e:regexp, forall vs1 vs2 vs3:list nat,
    vs1 <> vs2 ->
    regexp_match e vs1 vs2 ->
    regexp_match (star e) vs2 vs3 ->
    regexp_match (star e) vs1 vs3
  | regexp_match_plus : forall e:regexp, forall vs1 vs2:list nat,
    regexp_match (seq e (star e)) vs1 vs2 ->
    regexp_match (plus e) vs1 vs2.

Theorem seq_associative : forall e1 e2 e3:regexp, forall vs1 vs4: list nat,
  regexp_match (seq (seq e1 e2) e3) vs1 vs4 <->
  regexp_match (seq e1 (seq e2 e3)) vs1 vs4.
Proof.
  intros e1 e2 e3 vs1 vs4.
  split.
  Case "->".
    intros H.
    inversion H.
    inversion H2.
    apply regexp_match_seq with (vs2:=vs6).
    apply H8.
    apply regexp_match_seq with (vs2:=vs2).
    apply H11.
    apply H5.
  Case "<-".
    intros H.
    inversion H.
    inversion H5.
    apply regexp_match_seq with (vs2:=vs6).
    apply regexp_match_seq with (vs2:=vs2).
    apply H2.
    apply H8.
    apply H11.  Qed.