Skip to content

Instantly share code, notes, and snippets.

@mikeday

mikeday/20221115-regexp-derivatives.md

Created November 20, 2022 22:33
Show Gist options
  • Save mikeday/597213043e1356d76c53069452076e26 to your computer and use it in GitHub Desktop.
Save mikeday/597213043e1356d76c53069452076e26 to your computer and use it in GitHub Desktop.
Download ZIP
20221115 PL&V Reading Group: Regexp Derivatives
Raw
20221115-regexp-derivatives.md

Regular-expression derivatives re-examined was the paper for the Programming Languages and Verification Reading Group this week, unfortunately I wasn't able to attend but I went through it by myself and thankfully understood most of it as it's a clear introduction to a topic I have spent some time on in the past.

Back in 2008 I implemented Brzozowski derivatives in Coq, which was quite fun (see attached file basic.v). It describes regular expression semantics and proves that a regexp matches a string if repeatedly taking the derivative for each character in the string results in a nullable regexp. (I didn't implement automata construction as I had other plans for that).

For an additional challenge I implemented logical and/intersection and also an "interleave" operator allowing two regular expressions to be combined into one that matches every possible interleaving of the strings that each match (see attached file extended.v).

I wasn't able to successfully prove the correctness of derivatives with not/complement, so that failed attempt remains as a challenge for another day (see attached file negation.v).

This was all preparation for my more ambitious goal of formalising Antimirov's paper on constructing automata using partial derivatives of regular expressions, which was far beyond my abilities at the time (and now!) but was a lot of fun and got me writing my own tactics in Ltac and all kinds of things (see attached file partial.v, which starts off strong before descending into madness).

At this point I roped in Vladimir Komendantsky from the University of St Andrews to help and the result was eventually his paper which used Coq with SSReflect and some further work applying partial derivatives to regular expressions that contain variables/backreferences.

I still think it's a fascinating topic and well worth revisiting, although today perhaps it would be worth taking more inspiration from automata theory and coalegbras (???) to see where that leads.

References

Regular-expression derivatives re-examined
https://people.cs.uchicago.edu/~jhr/papers/2009/jfp-re-derivatives.pdf

Partial derivatives of regular expressions and finite automaton constructions
https://www.sciencedirect.com/science/article/pii/0304397595001824

Reflexive toolbox for regular expression matching: verification of functional programs in Coq+Ssreflect
https://dl.acm.org/doi/10.1145/2103776.2103784

Matching Problem for Regular Expressions with Variables
https://link.springer.com/chapter/10.1007/978-3-642-40447-4_10

Raw
basic.v
(* Copyright (C) 2008, 2022 YesLogic Pty. Ltd
* This file is distributed under the GNU General Public License, version 3.0
* http://www.gnu.org/licenses/gpl-3.0.html
*
* This module defines basic regular expressions and Brzozowski derivatives
*)
Require Import Bool.
Require Import List.
(* symbol alphabet *)
Variable A : Set.
Variable eq_A_dec : forall (a1 a2:A), {a1=a2}+{a1<>a2}.
(* regular expressions *)
Inductive regexp : Set :=
| Rzero : regexp
| Runit : regexp
| Rsym : A -> regexp
| Ralt : regexp -> regexp -> regexp
| Rcat : regexp -> regexp -> regexp
| Rstar : regexp -> regexp.
(* matching semantics *)
Inductive regexp_match : regexp -> list A -> Prop :=
| Match_unit : regexp_match Runit nil
| Match_sym : forall (c:A),
regexp_match (Rsym c) (c::nil)
| Match_alt_l : forall (a b:regexp) (l:list A),
regexp_match a l ->
regexp_match (Ralt a b) l
| Match_alt_r : forall (a b:regexp) (l:list A),
regexp_match b l ->
regexp_match (Ralt a b) l
| Match_cat : forall (a b:regexp) (la lb:list A),
regexp_match a la ->
regexp_match b lb ->
regexp_match (Rcat a b) (la ++ lb)
| Match_star_nil : forall (a:regexp),
regexp_match (Rstar a) nil
| Match_star_cons : forall (a:regexp) (l1 l2:list A),
regexp_match a l1 ->
regexp_match (Rstar a) l2 ->
regexp_match (Rstar a) (l1 ++ l2).
(* nullable expressions can match the empty string *)
Fixpoint nullable (r:regexp) : bool :=
match r with
| Rzero => false
| Runit => true
| Rsym _ => false
| Ralt a b => orb (nullable a) (nullable b)
| Rcat a b => andb (nullable a) (nullable b)
| Rstar a => true
end.
Inductive bool_equiv : bool -> Prop -> Prop :=
| BEquiv_true : forall (P:Prop), P -> bool_equiv true P
| BEquiv_false : forall (P:Prop), ~P -> bool_equiv false P.
Lemma matches_nil_nullable : forall (r:regexp),
bool_equiv (nullable r) (regexp_match r nil).
Proof.
induction r ; simpl.
(* Case: Rzero *)
apply BEquiv_false ; inversion 1.
(* Case: Runit *)
apply BEquiv_true ; constructor.
(* Case: Rsym *)
apply BEquiv_false ; inversion 1.
(* Case: Ralt *)
induction (nullable r1) ; simpl.
apply BEquiv_true.
apply Match_alt_l ; inversion IHr1 ; auto.
induction (nullable r2).
apply BEquiv_true.
apply Match_alt_r ; inversion IHr2 ; auto.
apply BEquiv_false.
inversion IHr1 ; inversion IHr2 ; subst.
inversion 1 ; auto.
(* Case: Rcat *)
induction (nullable r1) ; simpl.
induction (nullable r2).
apply BEquiv_true.
rewrite app_nil_end.
apply Match_cat.
inversion IHr1 ; auto.
inversion IHr2 ; auto.
apply BEquiv_false.
inversion 1 ; subst.
apply app_eq_nil in H2.
destruct H2 ; subst.
inversion IHr2 ; auto.
apply BEquiv_false.
inversion 1 ; subst.
apply app_eq_nil in H2.
destruct H2 ; subst.
inversion IHr1 ; auto.
(* Case: Rstar *)
apply BEquiv_true.
apply Match_star_nil.
Qed.
(* another approach implementing nullable directly without a separate proof *)
Definition nullable_dec (r:regexp) : {regexp_match r nil}+{~regexp_match r nil}.
induction r.
(* Rzero *)
right ; inversion 1.
(* Runit *)
left ; constructor.
(* Rsym *)
right ; inversion 1.
(* Ralt *)
destruct IHr1.
left ; constructor ; assumption.
destruct IHr2.
left ; constructor ; assumption.
right ; inversion 1 ; subst ; auto.
(* Rcat *)
replace nil with ((nil : list A) ++ nil) ; auto.
destruct IHr1.
destruct IHr2.
left ; constructor ; assumption.
right ; inversion 1 ; subst.
destruct (app_eq_nil la lb H2) ; subst ; auto.
right ; inversion 1 ; subst.
destruct (app_eq_nil la lb H2) ; subst ; auto.
(* Rstar *)
left ; constructor.
Qed.
(* Brzozowski derivatives of regular expressions *)
Definition o (r:regexp) : regexp :=
if nullable r then Runit else Rzero.
Fixpoint derivative (x:A) (r:regexp) {struct r} : regexp :=
match r with
| Rzero => Rzero
| Runit => Rzero
| Rsym y => if eq_A_dec x y then Runit else Rzero
| Ralt a b => Ralt (derivative x a) (derivative x b)
| Rcat a b => Ralt (Rcat (derivative x a) b) (Rcat (o a) (derivative x b))
| Rstar a => Rcat (derivative x a) (Rstar a)
end.
Theorem derivative_match1 : forall (r:regexp) (x:A) (l:list A),
regexp_match r (x::l) -> regexp_match (derivative x r) l.
Proof.
induction r ; intros x l H.
(* Case: Rzero *)
inversion H.
(* Case: Runit *)
inversion H.
(* Case: Rsym *)
inversion H ; subst ; simpl.
case (eq_A_dec x x) ; intro P.
apply Match_unit.
elim P ; trivial.
(* Case: Ralt *)
inversion H ; subst ; simpl.
apply Match_alt_l ; auto.
apply Match_alt_r ; auto.
(* Case: Rcat *)
inversion H ; subst ; simpl.
induction la.
(* la = nil *)
simpl in H2 ; subst.
apply Match_alt_r.
unfold o.
destruct (matches_nil_nullable r1).
rewrite <- app_nil_l ; apply Match_cat ; auto.
apply Match_unit.
elim H0 ; auto.
(* la = cons *)
apply Match_alt_l.
rewrite <- app_comm_cons in H2.
injection H2 ; intros ; subst.
apply Match_cat ; auto.
(* Case: Rstar *)
remember (Rstar r) as rs.
remember (x::l) as xl.
induction H ; try discriminate Heqrs ; inversion Heqrs ; subst.
discriminate Heqxl.
induction l1.
auto.
rewrite <- app_comm_cons in Heqxl.
injection Heqxl ; intros ; subst.
simpl.
apply Match_cat ; auto.
Qed.
Theorem derivative_match2 : forall (r:regexp) (x:A) (l:list A),
regexp_match (derivative x r) l -> regexp_match r (x::l).
Proof.
intros r x.
induction r ; intros l H ; simpl in H.
(* Case: Rzero *)
inversion H.
(* Case: Runit *)
inversion H.
(* Case: Rsym *)
induction (eq_A_dec x a) ; subst.
inversion H.
apply Match_sym.
inversion H.
(* Case: Ralt *)
inversion H ; subst.
apply Match_alt_l ; auto.
apply Match_alt_r ; auto.
(* Case: Rcat *)
inversion H ; subst.
inversion H3 ; subst.
rewrite app_comm_cons.
apply Match_cat ; auto.
unfold o in H3.
replace (x::l) with (nil ++ (x::l)) ; auto.
generalize (matches_nil_nullable r1) ; intro N.
induction (nullable r1).
apply Match_cat.
inversion N ; auto.
apply IHr2.
inversion H3 ; subst.
inversion H2 ; auto.
inversion H3 ; subst.
inversion H2.
(* Case: Rstar *)
inversion H ; subst.
rewrite app_comm_cons.
apply Match_star_cons ; auto.
Qed.
Theorem derivative_match : forall (r:regexp) (x:A) (l:list A),
regexp_match r (x::l) <-> regexp_match (derivative x r) l.
Proof.
intros r x l.
split.
apply derivative_match1.
apply derivative_match2.
Qed.
Fixpoint word_derivative (w:list A) (r:regexp) {struct w} : regexp :=
match w with
| nil => r
| x::w' => word_derivative w' (derivative x r)
end.
Theorem word_derivative_match1 : forall (w:list A) (r:regexp),
nullable (word_derivative w r) = true -> regexp_match r w.
Proof.
induction w ; simpl ; intros r H.
(* nil *)
generalize (matches_nil_nullable r) ; intro N ; inversion N ; auto.
rewrite H in H0 ; discriminate.
(* cons *)
apply derivative_match2.
auto.
Qed.
Theorem word_derivative_match2 : forall (w:list A) (r:regexp),
regexp_match r w -> nullable (word_derivative w r) = true.
Proof.
induction w ; simpl ; intros r H.
(* nil *)
generalize (matches_nil_nullable r) ; intro N ; inversion N ; auto.
(* cons *)
apply IHw.
apply derivative_match1 ; auto.
Qed.
Theorem word_derivative_match : forall (w:list A) (r:regexp),
nullable (word_derivative w r) = true <-> regexp_match r w.
Proof.
intros w r.
split.
apply word_derivative_match1.
apply word_derivative_match2.
Qed.
Raw
extended.v
(* Copyright (C) 2008 YesLogic Pty. Ltd
* This file is distributed under the GNU General Public License, version 3.0
* http://www.gnu.org/licenses/gpl-3.0.html
*
* This module defines regular expressions extended with interleave, and, and dot.
*)
Require Import Bool.
Require Import List.
Require Import Le.
Require Import Plus.
(* symbol alphabet *)
Variable A : Set.
Variable eq_A_dec : forall (a1 a2:A), {a1=a2}+{a1<>a2}.
(* regular expressions *)
Inductive regexp : Set :=
| Rzero : regexp
| Runit : regexp
| Rsym : A -> regexp
| Rany : regexp
| Ralt : regexp -> regexp -> regexp
| Rand : regexp -> regexp -> regexp
| Rcat : regexp -> regexp -> regexp
| Rstar : regexp -> regexp
| Rinter : regexp -> regexp -> regexp.
Definition eq_regexp_dec (a b:regexp) : {a=b}+{a<>b}.
decide equality ; apply eq_A_dec.
Defined.
(* list interleaving *)
Inductive interleave : list A -> list A -> list A -> Prop :=
| Inter_nil : interleave nil nil nil
| Inter_cons_l : forall (a:A) (la lb l:list A),
interleave la lb l -> interleave (a::la) lb (a::l)
| Inter_cons_r : forall (b:A) (la lb l:list A),
interleave la lb l -> interleave la (b::lb) (b::l).
Lemma interleave_nil_l : forall (l:list A), interleave nil l l.
Proof.
induction l.
apply Inter_nil.
apply Inter_cons_r ; auto.
Qed.
Lemma interleave_nil_r : forall (l:list A), interleave l nil l.
Proof.
induction l.
apply Inter_nil.
apply Inter_cons_l ; auto.
Qed.
Lemma interleave_length : forall (la lb l:list A),
interleave la lb l -> length l = length la + length lb.
Proof.
intros la lb l H.
induction H ; simpl ; auto.
rewrite IHinterleave.
apply plus_n_Sm.
Qed.
Lemma interleave_in : forall (a b:A) (la lb l:list A),
interleave la lb l -> (In a la -> In a l) /\ (In b lb -> In b l).
Proof.
intros a b la lb l H.
induction H ; simpl ; split ; intro H1 ; auto ; try contradiction ;
elim IHinterleave ; clear IHinterleave ; intros H2 H3 ;
try (elim H1 ; clear H1 ; intro H1) ; auto.
Qed.
(* matching semantics *)
Inductive regexp_match : regexp -> list A -> Prop :=
| Match_unit : regexp_match Runit nil
| Match_sym : forall (c:A),
regexp_match (Rsym c) (c::nil)
| Match_any : forall (c:A),
regexp_match Rany (c::nil)
| Match_alt_l : forall (a b:regexp) (l:list A),
regexp_match a l ->
regexp_match (Ralt a b) l
| Match_alt_r : forall (a b:regexp) (l:list A),
regexp_match b l ->
regexp_match (Ralt a b) l
| Match_and : forall (a b:regexp) (l:list A),
regexp_match a l ->
regexp_match b l ->
regexp_match (Rand a b) l
| Match_cat : forall (a b:regexp) (la lb:list A),
regexp_match a la ->
regexp_match b lb ->
regexp_match (Rcat a b) (la ++ lb)
| Match_star_nil : forall (a:regexp),
regexp_match (Rstar a) nil
| Match_star_cons : forall (a:regexp) (l1 l2:list A),
regexp_match a l1 ->
regexp_match (Rstar a) l2 ->
regexp_match (Rstar a) (l1 ++ l2)
| Match_inter : forall (a b:regexp) (la lb l:list A),
regexp_match a la ->
regexp_match b lb ->
interleave la lb l ->
regexp_match (Rinter a b) l.
(* nullable expressions can match the empty string *)
Fixpoint nullable (r:regexp) : bool :=
match r with
| Rzero => false
| Runit => true
| Rsym _ => false
| Rany => false
| Ralt a b => orb (nullable a) (nullable b)
| Rand a b => andb (nullable a) (nullable b)
| Rcat a b => andb (nullable a) (nullable b)
| Rstar a => true
| Rinter a b => andb (nullable a) (nullable b)
end.
Inductive bool_equiv : bool -> Prop -> Prop :=
| BEquiv_true : forall (P:Prop), P -> bool_equiv true P
| BEquiv_false : forall (P:Prop), ~P -> bool_equiv false P.
Lemma matches_nil_nullable : forall (a:regexp),
bool_equiv (nullable a) (regexp_match a nil).
Proof.
induction a ; simpl.
(* Case: Rzero *)
apply BEquiv_false.
unfold not ; intro H ; inversion H.
(* Case: Runit *)
apply BEquiv_true.
apply Match_unit.
(* Case: Rsym *)
apply BEquiv_false.
unfold not ; intro H ; inversion H.
(* Case: Rany *)
apply BEquiv_false.
unfold not ; intro H ; inversion H.
(* Case: Ralt *)
induction (nullable a1) ; simpl.
apply BEquiv_true.
apply Match_alt_l ; inversion IHa1 ; auto.
induction (nullable a2).
apply BEquiv_true.
apply Match_alt_r ; inversion IHa2 ; auto.
apply BEquiv_false.
inversion IHa1 ; inversion IHa2 ; subst.
unfold not in * ; intro H1.
inversion H1 ; auto.
(* Case: Rand *)
induction (nullable a1) ; simpl.
induction (nullable a2).
apply BEquiv_true.
apply Match_and.
inversion IHa1 ; auto.
inversion IHa2 ; auto.
apply BEquiv_false.
unfold not ; intro H.
inversion H ; inversion IHa2 ; auto.
apply BEquiv_false.
unfold not ; intro H.
inversion H ; inversion IHa1 ; auto.
(* Case: Rcat *)
induction (nullable a1) ; simpl.
induction (nullable a2).
apply BEquiv_true.
rewrite app_nil_end.
apply Match_cat.
inversion IHa1 ; auto.
inversion IHa2 ; auto.
apply BEquiv_false.
unfold not ; intro H.
inversion H ; subst.
apply app_eq_nil in H2.
elim H2 ; intros ; subst.
inversion IHa2 ; auto.
apply BEquiv_false.
unfold not ; intro H.
inversion H ; subst.
apply app_eq_nil in H2.
elim H2 ; intros ; subst.
inversion IHa1 ; auto.
(* Case: Rstar *)
apply BEquiv_true.
apply Match_star_nil.
(* Case: Rinter *)
induction (nullable a1) ; simpl.
induction (nullable a2).
apply BEquiv_true.
apply (Match_inter a1 a2 nil nil nil).
inversion IHa1 ; auto.
inversion IHa2 ; auto.
apply Inter_nil.
apply BEquiv_false.
unfold not ; intro H.
inversion H ; subst.
inversion H5 ; subst.
inversion IHa2 ; auto.
apply BEquiv_false.
unfold not ; intro H.
inversion H ; subst.
inversion H5 ; subst.
inversion IHa1 ; auto.
Qed.
(* Brzozowski derivatives of regular expressions *)
Definition o (r:regexp) : regexp :=
if nullable r then Runit else Rzero.
Fixpoint derivative (x:A) (r:regexp) {struct r} : regexp :=
match r with
| Rzero => Rzero
| Runit => Rzero
| Rsym y => if eq_A_dec x y then Runit else Rzero
| Rany => Runit
| Ralt a b => Ralt (derivative x a) (derivative x b)
| Rand a b => Rand (derivative x a) (derivative x b)
| Rcat a b => Ralt (Rcat (derivative x a) b) (Rcat (o a) (derivative x b))
| Rstar a => Rcat (derivative x a) (Rstar a)
| Rinter a b => Ralt (Rinter (derivative x a) b) (Rinter a (derivative x b))
end.
Fixpoint derivative_word (w:list A) (r:regexp) {struct w} : regexp :=
match w with
| nil => r
| x::w' => derivative_word w' (derivative x r)
end.
Theorem derivative_match : forall (r:regexp) (x:A) (l:list A),
regexp_match r (x::l) -> regexp_match (derivative x r) l.
Proof.
intros r x.
induction r ; intros l H.
(* Case: Rzero *)
inversion H.
(* Case: Runit *)
inversion H.
(* Case: Rsym *)
inversion H ; subst ; simpl.
case (eq_A_dec x x) ; intro P.
apply Match_unit.
elim P ; trivial.
(* Case: Rany *)
inversion H ; subst.
simpl.
apply Match_unit.
(* Case: Ralt *)
inversion H ; subst ; simpl.
apply Match_alt_l ; auto.
apply Match_alt_r ; auto.
(* Case: Rand *)
inversion H ; subst.
simpl.
apply Match_and ; auto.
(* Case: Rcat *)
inversion H ; subst ; simpl.
induction la.
(* la = nil *)
simpl in H2 ; subst.
apply Match_alt_r.
unfold o.
generalize (matches_nil_nullable r1) ; intro P ; inversion P ; subst.
replace l with (nil ++ l) ; auto.
apply Match_cat ; auto.
apply Match_unit.
elim H1 ; auto.
(* la = cons *)
apply Match_alt_l.
rewrite <- app_comm_cons in H2.
injection H2 ; intros ; subst.
apply Match_cat ; auto.
(* Case: Rstar *)
remember (Rstar r) as rs.
remember (x::l) as xl.
induction H ; try discriminate Heqrs ; inversion Heqrs ; subst.
discriminate Heqxl.
induction l1.
auto.
rewrite <- app_comm_cons in Heqxl.
injection Heqxl ; intros ; subst.
simpl.
apply Match_cat ; auto.
(* Case: Rinter *)
inversion H ; subst.
simpl.
inversion H5 ; subst.
apply Match_alt_l.
apply (Match_inter (derivative x r1) r2 la0 lb) ; auto.
apply Match_alt_r.
apply (Match_inter r1 (derivative x r2) la lb0) ; auto.
Qed.
Raw
negation.v
(* Copyright (C) 2008 YesLogic Pty. Ltd
* This file is distributed under the GNU General Public License, version 3.0
* http://www.gnu.org/licenses/gpl-3.0.html
*
* This module defines regular expressions extended with negation.
*)
Require Import Bool.
Require Import List.
Require Import Le.
Require Import Plus.
(* symbol alphabet *)
Variable A : Set.
Variable eq_A_dec : forall (a1 a2:A), {a1=a2}+{a1<>a2}.
(* regular expressions *)
Inductive regexp : Set :=
| Rzero : regexp
| Runit : regexp
| Rsym : A -> regexp
| Ralt : regexp -> regexp -> regexp
| Rcat : regexp -> regexp -> regexp
| Rnot : regexp -> regexp
| Rstar : regexp -> regexp.
Definition eq_regexp_dec (a b:regexp) : {a=b}+{a<>b}.
decide equality ; apply eq_A_dec.
Defined.
(* matching semantics *)
Inductive regexp_match : regexp -> list A -> Prop :=
| Match_unit : regexp_match Runit nil
| Match_sym : forall (c:A),
regexp_match (Rsym c) (c::nil)
| Match_alt_l : forall (a b:regexp) (l:list A),
regexp_match a l ->
regexp_match (Ralt a b) l
| Match_alt_r : forall (a b:regexp) (l:list A),
regexp_match b l ->
regexp_match (Ralt a b) l
| Match_cat : forall (a b:regexp) (la lb:list A),
regexp_match a la ->
regexp_match b lb ->
regexp_match (Rcat a b) (la ++ lb)
| Match_star_nil : forall (a:regexp),
regexp_match (Rstar a) nil
| Match_star_cons : forall (a:regexp) (l1 l2:list A),
regexp_match a l1 ->
regexp_match (Rstar a) l2 ->
regexp_match (Rstar a) (l1 ++ l2)
| Match_not_zero : forall (l:list A), regexp_match (Rnot Rzero) l
| Match_not_unit : forall (c:A) (l:list A), regexp_match (Rnot Runit) (c::l)
| Match_not_sym_nil : forall (c:A), regexp_match (Rnot (Rsym c)) nil
| Match_not_sym_single : forall (c1 c2:A),
c1 <> c2 -> regexp_match (Rnot (Rsym c1)) (c2::nil)
| Match_not_sym_multiple : forall (c1 c2 c3:A) (l:list A),
regexp_match (Rnot (Rsym c1)) (c2::c3::l)
| Match_not_alt : forall (a b:regexp) (l:list A),
regexp_match (Rnot a) l ->
regexp_match (Rnot b) l ->
regexp_match (Rnot (Ralt a b)) l
| Match_not_cat : forall (a b:regexp) (l:list A),
(forall (la lb:list A), l = la ++ lb -> regexp_match (Rnot a) la \/ regexp_match (Rnot b) lb) ->
regexp_match (Rnot (Rcat a b)) l
| Match_not_star : forall (a:regexp) (l:list A),
l <> nil -> regexp_match (Rstar (Rnot a)) l -> regexp_match (Rnot (Rstar a)) l
| Match_not_not : forall (a:regexp) (l:list A),
regexp_match a l -> regexp_match (Rnot (Rnot a)) l.
Inductive exclusive : Prop -> Prop -> Prop :=
| Ex : forall (A B:Prop), (A -> ~B) -> (~A -> B) -> (B -> ~A) -> (~B -> A) -> exclusive A B.
Lemma exclusive_symmetric : forall (A B:Prop),
exclusive A B <-> exclusive B A.
Proof.
intros A0 B.
unfold iff ; split ; intro H ; inversion H ; subst ; apply Ex ; auto.
Qed.
(* This would appear to be provable by case analysis, but how to do it more concisely? *)
Variable regexp_match_de_morgan : forall (a b:regexp) (l:list A),
~(regexp_match a l /\ regexp_match b l) -> (~regexp_match a l \/ ~regexp_match b l).
(* This would appear to be provable by case analysis, but how to do it more concisely? *)
Variable regexp_match_not_alt : forall (a b:regexp) (l:list A),
~regexp_match a l /\ ~regexp_match b l -> ~regexp_match (Ralt a b) l.
Lemma foo : forall (A1 N1 A2 N2:Prop),
exclusive A1 N1 -> exclusive A2 N2 -> ~A1 \/ ~A2 -> N1 \/ N2.
Proof.
intros A1 N1 A2 N2 E1 E2 H.
inversion E1 ; inversion E2 ; subst.
elim H ; clear H ; intro P ; tauto.
Qed.
Lemma bar : forall (a b:regexp) (l:list A),
(forall (la lb:list A), l = la ++ lb -> ~regexp_match a la \/ ~regexp_match b lb) ->
regexp_match (Rcat a b) l -> False.
Proof.
intros a b l H1 H2.
inversion H2 ; subst.
generalize (H1 la lb) ; clear H1 ; unfold not ; intro H1.
elim H1 ; auto.
Qed.
Variable not_is_exclusive : forall (a:regexp) (l:list A),
exclusive (regexp_match a l) (regexp_match (Rnot a) l).
(*
Lemma not_is_exclusive : forall (a:regexp) (l:list A),
exclusive (regexp_match a l) (regexp_match (Rnot a) l).
Proof.
induction a ; intro l.
(* Case: Rzero *)
apply Ex ; intro H.
inversion H.
apply Match_not_zero.
unfold not ; intro H1 ; inversion H1.
unfold not in H ; elimtype False; apply H.
apply Match_not_zero.
(* Case: Runit *)
apply Ex ; intro H ; try (unfold not ; intro H1).
inversion H ; subst.
inversion H1.
induction l.
unfold not in H ; elimtype False ; apply H.
apply Match_unit.
apply Match_not_unit.
inversion H1 ; subst.
inversion H.
induction l.
apply Match_unit.
unfold not in H ; elimtype False ; apply H.
apply Match_not_unit.
(* Case: Rsym *)
apply Ex ; intro H ; try (unfold not ; intro H1).
inversion H ; subst.
inversion H1.
elim H3 ; auto.
induction l.
apply Match_not_sym_nil.
induction l.
apply Match_not_sym_single.
unfold not.
intro H1 ; subst.
unfold not in H.
apply H.
apply Match_sym.
apply Match_not_sym_multiple.
inversion H1 ; subst.
inversion H.
elim H3 ; auto.
unfold not in H.
induction l.
elimtype False ; apply H.
apply Match_not_sym_nil.
induction l.
elim (eq_A_dec a a0) ; intro P.
subst.
apply Match_sym.
elimtype False ; apply H.
apply Match_not_sym_single ; auto.
elimtype False ; apply H.
apply Match_not_sym_multiple.
(* Case: Ralt *)
generalize (IHa1 l) ; clear IHa1 ; intro IHa1.
generalize (IHa2 l) ; clear IHa2 ; intro IHa2.
apply Ex ; intro H ; try (unfold not ; intro H1) ;
inversion IHa1 ; inversion IHa2 ; subst ; unfold not in *.
inversion H ; inversion H1 ; auto.
apply Match_not_alt.
apply H1 ; intro ; apply H ; apply Match_alt_l ; auto.
apply H7 ; intro ; apply H ; apply Match_alt_r ; auto.
inversion H ; inversion H1 ; auto.
assert (P:(regexp_match (Rnot a1) l /\ regexp_match (Rnot a2) l) -> False).
intro Q ; elim Q ; clear Q ; intros Q1 Q2.
apply H ; apply Match_not_alt ; auto.
generalize (regexp_match_de_morgan (Rnot a1) (Rnot a2) l P).
clear P ; intro P ; elim P ; clear P ; intro P.
apply Match_alt_l ; auto.
apply Match_alt_r ; auto.
(* Case: Rcat *)
apply Ex ; intro H ; try (unfold not ; intro H1).
inversion H1 ; subst.
inversion H ; subst.
generalize (IHa1 la) ; clear IHa1 ; intro IHa1.
generalize (IHa2 lb) ; clear IHa2 ; intro IHa2.
inversion IHa1 ; inversion IHa2 ; subst.
elim (H4 la lb) ; auto ; clear H4 ; intro N ; tauto.
(* tricky... *)
apply Match_not_cat.
intros la lb H1.
unfold not in H.
generalize (bar a1 a2 l).
intro H2.
generalize (H2 la lb).
left.
intros la lb H1 ; subst.
generalize (IHa1 la) ; clear IHa1 ; intro IHa1.
generalize (IHa2 lb) ; clear IHa2 ; intro IHa2.
inversion IHa1 ; inversion IHa2 ; subst.
apply (foo (regexp_match a1 la) (regexp_match (Rnot a1) la)
(regexp_match a2 lb) (regexp_match (Rnot a2) lb)) ; auto.
unfold not.
left.
unfold not in H.
split.
apply H1 ; unfold not ; intro P.
apply (foo (regexp_match a1 la) (regexp_match a2 lb)) ; auto.
unfold not in H.
split ; unfold not ; intro P.
apply H.
apply Match_cat ; auto.
split.
apply H1 ; unfold not ; intro M1.
(* Case: Rnot *)
inversion IHa ; subst.
apply Ex ; intro H3 ; try (unfold not ; intro H4).
inversion H4 ; subst.
tauto.
apply Match_not_not ; auto.
inversion H3 ; subst.
tauto.
apply H0.
unfold not ; intro H4.
unfold not in H3.
apply Match_not_not in H4.
tauto.
Qed.
*)
(* nullable expressions can match the empty string *)
Fixpoint nullable (r:regexp) : bool :=
match r with
| Rzero => false
| Runit => true
| Rsym _ => false
| Ralt a b => orb (nullable a) (nullable b)
| Rcat a b => andb (nullable a) (nullable b)
| Rnot a => negb (nullable a)
| Rstar a => true
end.
Inductive bool_equiv : bool -> Prop -> Prop :=
| BEquiv_true : forall (P:Prop), P -> bool_equiv true P
| BEquiv_false : forall (P:Prop), ~P -> bool_equiv false P.
Lemma matches_nil_nullable : forall (a:regexp),
bool_equiv (nullable a) (regexp_match a nil).
Proof.
induction a ; simpl.
(* Case: Rzero *)
apply BEquiv_false.
unfold not ; intro H ; inversion H.
(* Case: Runit *)
apply BEquiv_true.
apply Match_unit.
(* Case: Rsym *)
apply BEquiv_false.
unfold not ; intro H ; inversion H.
(* Case: Ralt *)
induction (nullable a1) ; simpl.
apply BEquiv_true.
apply Match_alt_l ; inversion IHa1 ; auto.
induction (nullable a2).
apply BEquiv_true.
apply Match_alt_r ; inversion IHa2 ; auto.
apply BEquiv_false.
inversion IHa1 ; inversion IHa2 ; subst.
apply regexp_match_not_alt ; auto.
(* Case: Rcat *)
induction (nullable a1) ; simpl.
induction (nullable a2).
apply BEquiv_true.
rewrite app_nil_end.
apply Match_cat.
inversion IHa1 ; auto.
inversion IHa2 ; auto.
apply BEquiv_false.
unfold not ; intro H ; inversion H ; subst.
apply app_eq_nil in H2 ; elim H2 ; intros ; subst.
inversion IHa2 ; auto.
apply BEquiv_false.
unfold not ; intro H ; inversion H ; subst.
apply app_eq_nil in H2 ; elim H2 ; intros ; subst.
inversion IHa1 ; auto.
(* Case: Rnot *)
induction (nullable a) ; simpl ; inversion IHa ; subst.
apply BEquiv_false.
generalize (not_is_exclusive a nil) ; intro P ; inversion P ; auto.
apply BEquiv_true.
generalize (not_is_exclusive a nil) ; intro P ; inversion P ; auto.
(* Case: Rstar *)
apply BEquiv_true.
apply Match_star_nil.
Qed.
(* Brzozowski derivatives of regular expressions *)
Definition o (r:regexp) : regexp :=
if nullable r then Runit else Rzero.
Fixpoint derivative (x:A) (r:regexp) {struct r} : regexp :=
match r with
| Rzero => Rzero
| Runit => Rzero
| Rsym y => if eq_A_dec x y then Runit else Rzero
| Ralt a b => Ralt (derivative x a) (derivative x b)
| Rcat a b => Ralt (Rcat (derivative x a) b) (Rcat (o a) (derivative x b))
| Rnot a => Rnot (derivative x a)
| Rstar a => Rcat (derivative x a) (Rstar a)
end.
Fixpoint derivative_word (w:list A) (r:regexp) {struct w} : regexp :=
match w with
| nil => r
| x::w' => derivative_word w' (derivative x r)
end.
Theorem derivative_match : forall (r:regexp) (x:A) (l:list A),
regexp_match r (x::l) -> regexp_match (derivative x r) l.
Proof.
intros r x.
induction r ; intros l H.
(* Case: Rzero *)
inversion H.
(* Case: Runit *)
inversion H.
(* Case: Rsym *)
inversion H ; subst ; simpl.
case (eq_A_dec x x) ; intro P.
apply Match_unit.
elim P ; trivial.
(* Case: Ralt *)
inversion H ; subst ; simpl.
apply Match_alt_l ; auto.
apply Match_alt_r ; auto.
(* Case: Rcat *)
inversion H ; subst ; simpl.
induction la.
(* la = nil *)
simpl in H2 ; subst.
apply Match_alt_r.
unfold o.
generalize (matches_nil_nullable r1) ; intro H5.
inversion H5 ; subst.
replace l with (nil ++ l) ; auto.
apply Match_cat ; auto.
apply Match_unit.
tauto.
(* la = cons *)
apply Match_alt_l.
rewrite <- app_comm_cons in H2.
injection H2 ; intros ; subst.
apply Match_cat ; auto.
(* Case: Rnot *)
remember (x::l) as l'.
induction H ; simpl ; subst ; try apply Match_not_zero.
inversion Heql'.
inversion Heql' ; subst.
case (eq_A_dec x x) ; intro P.
apply Match_unit.
elim P ; trivial.
apply Match_alt_l ; auto.
apply Match_alt_r ; auto.
HELP?
inversion Heql'.
inversion Heql' ; subst.
case (eq_A_dec x c1) ; intro P.
subst ; elim H ; auto.
apply Match_not_zero.
inversion Heql' ; subst.
case (eq_A_dec x c1) ; intro P.
apply Match_not_unit.
apply Match_not_zero.
apply Match_not_alt ; auto.
apply Match_not_not ; auto.
(* Case: Rstar *)
remember (Rstar r) as rs.
remember (x::l) as xl.
induction H ; try discriminate Heqrs ; inversion Heqrs ; subst.
discriminate Heqxl.
induction l1.
auto.
rewrite <- app_comm_cons in Heqxl.
injection Heqxl ; intros ; subst.
simpl.
apply Match_cat ; auto.
Qed.
Raw
partial.v
(* Copyright (C) 2008 YesLogic Pty. Ltd
* This file is distributed under the GNU General Public License, version 3.0
* http://www.gnu.org/licenses/gpl-3.0.html
*
* This module is based on a paper by Valentin Antimirov:
* Partial derivatives of regular expressions and finite automaton constructions
* http://citeseer.ist.psu.edu/43569.html
*)
Require Import Bool.
Require Import List.
Require Import Le.
Require Import Plus.
(* symbol alphabet *)
Variable A : Set.
Variable eq_A_dec : forall (a1 a2:A), {a1=a2}+{a1<>a2}.
(* regular expressions *)
Inductive regexp : Set :=
| Rzero : regexp
| Runit : regexp
| Rsym : A -> regexp
| Ralt : regexp -> regexp -> regexp
| Rcat : regexp -> regexp -> regexp
| Rstar : regexp -> regexp.
(*
Notation "a + b" := (Ralt a b) (at level 50, left associativity).
Notation "a * b" := (Rcat a b) (at level 40, left associativity).
*)
Definition eq_regexp_dec (a b:regexp) : {a=b}+{a<>b}.
decide equality ; apply eq_A_dec.
Defined.
(* matching semantics *)
Inductive regexp_match : regexp -> list A -> Prop :=
| Match_unit : regexp_match Runit nil
| Match_sym : forall (c:A),
regexp_match (Rsym c) (c::nil)
| Match_alt_l : forall (a b:regexp) (l:list A),
regexp_match a l ->
regexp_match (Ralt a b) l
| Match_alt_r : forall (a b:regexp) (l:list A),
regexp_match b l ->
regexp_match (Ralt a b) l
| Match_cat : forall (a b:regexp) (la lb:list A),
regexp_match a la ->
regexp_match b lb ->
regexp_match (Rcat a b) (la ++ lb)
| Match_star_nil : forall (r:regexp),
regexp_match (Rstar r) nil
| Match_star_cons : forall (r:regexp) (l1 l2:list A),
regexp_match r l1 ->
regexp_match (Rstar r) l2 ->
regexp_match (Rstar r) (l1 ++ l2).
(* nullable expressions can match the empty string *)
Fixpoint nullable (r:regexp) : bool :=
match r with
| Rzero => false
| Runit => true
| Rsym _ => false
| Ralt a b => orb (nullable a) (nullable b)
| Rcat a b => andb (nullable a) (nullable b)
| Rstar a => true
end.
Lemma matches_nil_nullable : forall (a:regexp),
regexp_match a nil -> nullable a = true.
Proof.
intros a H.
remember (nil:list A) as l.
induction H ; try discriminate Heql ; simpl ; subst ; trivial.
(* Case: Match_alt_l *)
rewrite IHregexp_match ; auto.
(* Case: Match_alt_r *)
rewrite IHregexp_match ; auto.
case (nullable a) ; auto.
(* Case: Match_cat *)
elim (app_eq_nil la lb Heql) ; intros L1 L2.
rewrite IHregexp_match1 ; auto.
Qed.
Lemma nullable_matches_nil : forall (a:regexp),
nullable a = true -> regexp_match a nil.
Proof.
intros a H.
induction a.
(* Case: Rzero *)
inversion H.
(* Case: Runit *)
apply Match_unit.
(* Case: Rsym *)
inversion H.
(* Case: Ralt *)
simpl in H.
apply orb_prop in H.
elim H ; intro P.
apply Match_alt_l ; auto.
apply Match_alt_r ; auto.
(* Case: Rcat *)
simpl in H.
apply andb_prop in H.
elim H ; intros P1 P2.
rewrite app_nil_end.
apply Match_cat ; auto.
(* Case: Rstar *)
apply Match_star_nil.
Qed.
(* Brzozowski derivatives of regular expressions *)
Definition o (r:regexp) : regexp :=
if nullable r then Runit else Rzero.
Fixpoint derivative (x:A) (r:regexp) {struct r} : regexp :=
match r with
| Rzero => Rzero
| Runit => Rzero
| Rsym y => if eq_A_dec x y then Runit else Rzero
| Ralt a b => Ralt (derivative x a) (derivative x b)
| Rcat a b => Ralt (Rcat (derivative x a) b) (Rcat (o a) (derivative x b))
| Rstar a => Rcat (derivative x a) (Rstar a)
end.
Fixpoint derivative_word (w:list A) (r:regexp) {struct w} : regexp :=
match w with
| nil => r
| x::w' => derivative_word w' (derivative x r)
end.
Theorem derivative_match : forall (r:regexp) (x:A) (l:list A),
regexp_match r (x::l) -> regexp_match (derivative x r) l.
Proof.
intros r x.
induction r ; intros l H.
(* Case: Rzero *)
inversion H.
(* Case: Runit *)
inversion H.
(* Case: Rsym *)
inversion H ; subst ; simpl.
case (eq_A_dec x x) ; intro P.
apply Match_unit.
elim P ; trivial.
(* Case: Ralt *)
inversion H ; subst ; simpl.
apply Match_alt_l ; auto.
apply Match_alt_r ; auto.
(* Case: Rcat *)
inversion H ; subst ; simpl.
induction la.
(* la = nil *)
simpl in H2 ; subst.
apply Match_alt_r.
unfold o.
rewrite matches_nil_nullable ; auto.
replace l with (nil ++ l) ; auto.
apply Match_cat ; auto.
apply Match_unit.
(* la = cons *)
apply Match_alt_l.
rewrite <- app_comm_cons in H2.
injection H2 ; intros ; subst.
apply Match_cat ; auto.
(* Case: Rstar *)
remember (Rstar r) as rs.
remember (x::l) as xl.
induction H ; try discriminate Heqrs ; inversion Heqrs ; subst.
discriminate Heqxl.
induction l1.
auto.
rewrite <- app_comm_cons in Heqxl.
injection Heqxl ; intros ; subst.
simpl.
apply Match_cat ; auto.
Qed.
(* FIXME new bit *)
Theorem derivative_match_cat : forall (a b:regexp) (x:A) (l:list A),
(forall la, regexp_match (derivative x a) la -> regexp_match a (x :: la)) ->
(forall lb, regexp_match (derivative x b) lb -> regexp_match b (x :: lb)) ->
regexp_match (derivative x (Rcat a b)) l -> regexp_match (Rcat a b) (x::l).
Proof.
intros a b x l Ha Hb.
simpl ; unfold o.
assert (P:nullable a = true \/ nullable a = false).
case (nullable a) ; [left ; trivial | right ; trivial].
elim P ; clear P ; intro P ; rewrite P.
(* nullable a = true *)
inversion 1 ; subst.
inversion H3 ; subst.
rewrite app_comm_cons.
apply Match_cat ; auto.
inversion H3 ; subst.
inversion H2 ; subst.
replace (x :: nil ++ lb) with (nil ++ x :: lb) ; auto.
apply Match_cat.
apply nullable_matches_nil ; assumption.
auto.
inversion 1 ; subst.
inversion H3 ; subst.
rewrite app_comm_cons.
apply Match_cat ; auto.
inversion H3 ; inversion H2.
Qed.
Theorem derivative_match_star : forall (a:regexp) (x:A) (l:list A),
(forall la, regexp_match (derivative x a) la -> regexp_match a (x :: la)) ->
regexp_match (derivative x (Rstar a)) l -> regexp_match (Rstar a) (x::l).
Proof.
intros a x l Ha.
simpl.
intro H1.
inversion H1 ; subst.
rewrite app_comm_cons.
apply Match_star_cons ; auto.
Qed.
Theorem derivative_match2 : forall (r:regexp) (x:A) (l:list A),
regexp_match (derivative x r) l -> regexp_match r (x::l).
Proof.
induction r ; simpl ; intros.
inversion H.
inversion H.
destruct (eq_A_dec x a).
subst ; inversion H.
constructor.
inversion H.
inversion H ; subst.
apply Match_alt_l ; auto.
apply Match_alt_r ; auto.
apply derivative_match_cat ; auto.
inversion H ; subst.
apply derivative_match_star ; auto.
Qed.
Definition matches (r:regexp) (w:list A) : bool :=
nullable (derivative_word w r).
Lemma matches_dec1 : forall w r,
matches r w = true -> regexp_match r w.
Proof.
unfold matches.
induction w ; simpl.
apply nullable_matches_nil.
intros r Hn.
apply derivative_match2.
apply IHw.
assumption.
Qed.
Lemma matches_dec2 : forall w r,
regexp_match r w -> matches r w = true.
Proof.
unfold matches.
induction w ; simpl.
apply matches_nil_nullable.
intros r Hm.
apply IHw.
apply derivative_match.
assumption.
Qed.
Lemma matches_dec : forall w r,
{regexp_match r w}+{~regexp_match r w}.
Proof.
intros.
assert (P:{matches r w = true}+{matches r w = false}).
case (matches r w) ; [left | right] ; reflexivity.
destruct P.
left ; apply matches_dec1 ; assumption.
right ; red ; intro H.
generalize (matches_dec2 w r H).
rewrite e.
intro P ; discriminate P.
Qed.
(* equivalence axioms *)
Inductive equiv_regexp : regexp -> regexp -> Prop :=
| Equiv_refl : forall (a:regexp), equiv_regexp a a
| Equiv_symmetric : forall (a b:regexp),
equiv_regexp a b -> equiv_regexp b a
| Equiv_transitive : forall (a b c:regexp),
equiv_regexp a b -> equiv_regexp b c -> equiv_regexp a c
| Equiv_alt_rec : forall (a b c d:regexp),
equiv_regexp a c -> equiv_regexp b d -> equiv_regexp (Ralt a b) (Ralt c d)
| Equiv_cat_rec : forall (a b c d:regexp),
equiv_regexp a c -> equiv_regexp b d -> equiv_regexp (Rcat a b) (Rcat c d)
| Equiv_star_rec : forall (a b:regexp),
equiv_regexp a b -> equiv_regexp (Rstar a) (Rstar b)
(* Axiom 1: a + (b + c) = (a + b) + c *)
| Equiv_alt_distributes : forall (a b c:regexp), equiv_regexp (Ralt a (Ralt b c)) (Ralt (Ralt a b) c)
(* Axiom 2: a + b = b + a *)
| Equiv_alt_symmetric : forall (a b:regexp), equiv_regexp (Ralt a b) (Ralt b a)
(* Axiom 3: a + a = a *)
| Equiv_alt_same : forall (a:regexp), equiv_regexp a (Ralt a a)
(* Axiom 4: a + 0 = a *)
| Equiv_alt_zero_r : forall (a:regexp), equiv_regexp a (Ralt a Rzero)
(* Axiom 5: (a.b).c = a.(b.c) *)
| Equiv_cat_distributes : forall (a b c:regexp), equiv_regexp (Rcat a (Rcat b c)) (Rcat (Rcat a b) c)
(* Axiom 6: a.1 = 1.a = a *)
| Equiv_cat_unit_l : forall (a:regexp), equiv_regexp a (Rcat Runit a)
| Equiv_cat_unit_r : forall (a:regexp), equiv_regexp a (Rcat a Runit)
(* Axiom 7: a.0 = 0.a = 0 *)
| Equiv_cat_zero_l : forall (a:regexp), equiv_regexp Rzero (Rcat Rzero a)
| Equiv_cat_zero_r : forall (a:regexp), equiv_regexp Rzero (Rcat a Rzero)
(* Axiom 8: a.(b + c) = a.b + a.c *)
| Equiv_cat_distributes_l : forall (a b c:regexp),
equiv_regexp (Rcat a (Ralt b c)) (Ralt (Rcat a b) (Rcat a c))
(* Axiom 9: (a + b).c = a.c + b.c *)
| Equiv_cat_distributes_r : forall (a b c:regexp),
equiv_regexp (Rcat (Ralt a b) c) (Ralt (Rcat a c) (Rcat b c))
(* Kleene star axioms *)
| Equiv_star_unit : equiv_regexp Runit (Rstar Runit)
| Equiv_star_alt_unit : forall (a:regexp), equiv_regexp (Rstar a) (Rstar (Ralt Runit a))
| Equiv_star_cat : forall (a:regexp), equiv_regexp (Rstar a) (Ralt Runit (Rcat a (Rstar a)))
| Equiv_star_nested : forall (a:regexp), equiv_regexp (Rstar a) (Rstar (Rstar a)).
Ltac subst_regexp b :=
match goal with
| [ |- (equiv_regexp ?a ?c) ] => apply (Equiv_transitive a b c)
end.
Lemma Equiv_alt_zero_l : forall (a:regexp), equiv_regexp a (Ralt Rzero a).
Proof.
intro a.
subst_regexp (Ralt a Rzero).
apply Equiv_alt_zero_r.
apply Equiv_alt_symmetric.
Qed.
Ltac auto_iff :=
match goal with
| [ H:(forall l:list A, regexp_match ?a l <-> regexp_match ?b l) |- (regexp_match ?b ?l) ] =>
elim (H l) ; intros M1 M2 ; apply M1 ; clear H M1 M2 ; auto ; auto_iff
| [ H:(forall l:list A, regexp_match ?a l <-> regexp_match ?b l) |- (regexp_match ?a ?l) ] =>
elim (H l) ; intros M1 M2 ; apply M2 ; clear H M1 M2 ; auto ; auto_iff
end.
(* equivalent regular expressions match the same strings *)
Theorem equiv_matches : forall (a b:regexp),
equiv_regexp a b -> (forall l:list A, regexp_match a l <-> regexp_match b l).
Proof.
intros a b H1.
induction H1 ; intros l ; split ; intro H2.
(* Case: Equiv_refl *)
auto.
auto.
(* Case: Equiv_symmetric *)
auto_iff.
auto_iff.
(* Case: Equiv_transitive *)
auto_iff.
auto_iff.
(* Case: Equiv_alt_rec *)
inversion H2.
apply Match_alt_l ; auto_iff.
apply Match_alt_r ; auto_iff.
inversion H2.
apply Match_alt_l ; auto_iff.
apply Match_alt_r ; auto_iff.
(* Case: Equiv_cat_rec *)
inversion H2 ; apply Match_cat ; auto_iff.
inversion H2 ; apply Match_cat ; auto_iff.
(* Case: Equiv_star_rec *)
remember (Rstar a) as ra.
induction H2 ; try discriminate Heqra.
apply Match_star_nil.
apply Match_star_cons.
inversion Heqra ; subst.
auto_iff.
auto.
(* <- *)
remember (Rstar b) as rb.
induction H2 ; try discriminate Heqrb.
apply Match_star_nil.
apply Match_star_cons.
inversion Heqrb ; subst.
auto_iff.
auto.
(* Case: Equiv_alt_distributes *)
inversion H2.
apply Match_alt_l ; apply Match_alt_l ; auto.
inversion H3.
apply Match_alt_l ; apply Match_alt_r ; auto.
apply Match_alt_r ; auto.
(* <- *)
inversion H2.
inversion H3.
apply Match_alt_l ; auto.
apply Match_alt_r ; apply Match_alt_l ; auto.
apply Match_alt_r ; apply Match_alt_r ; auto.
(* Case: Equiv_alt_symmetric *)
inversion H2.
apply Match_alt_r ; auto.
apply Match_alt_l ; auto.
(* <- *)
inversion H2.
apply Match_alt_r ; auto.
apply Match_alt_l ; auto.
(* Case: Equiv_alt_same *)
apply Match_alt_l ; auto.
(* <- *)
inversion H2 ; auto.
(* Case: Equiv_alt_zero_r *)
apply Match_alt_l ; auto.
(* <- *)
inversion H2 ; auto.
inversion H3.
(* Case: Equiv_cat_distributes *)
inversion H2.
inversion H4.
rewrite <- app_ass.
apply Match_cat.
apply Match_cat ; auto.
auto.
(* <- *)
inversion H2.
inversion H1.
rewrite app_ass.
apply Match_cat ; auto.
apply Match_cat ; auto.
(* Case: Equiv_cat_unit_l *)
replace l with (nil ++ l) ; auto.
apply Match_cat ; auto ; apply Match_unit.
(* <- *)
inversion H2.
inversion H1.
simpl ; auto.
(* Case: Equiv_cat_unit_r *)
rewrite app_nil_end.
apply Match_cat ; auto ; apply Match_unit.
(* <- *)
inversion H2.
inversion H4.
rewrite <- app_nil_end.
auto.
(* Case: Equiv_cat_zero_l *)
inversion H2.
(* <- *)
inversion H2.
inversion H1.
(* Case: Equiv_cat_zero_r *)
inversion H2.
(* <- *)
inversion H2.
inversion H4.
(* Case: Equiv_cat_distributes_l *)
inversion H2.
inversion H4.
apply Match_alt_l ; apply Match_cat ; auto.
apply Match_alt_r ; apply Match_cat ; auto.
(* <- *)
inversion H2.
inversion H3.
apply Match_cat ; auto.
apply Match_alt_l ; auto.
inversion H3.
apply Match_cat ; auto.
apply Match_alt_r ; auto.
(* Case: Equiv_cat_distributes_r *)
inversion H2.
inversion H1.
apply Match_alt_l ; apply Match_cat ; auto.
apply Match_alt_r ; apply Match_cat ; auto.
(* <- *)
inversion H2.
inversion H3.
apply Match_cat ; auto.
apply Match_alt_l ; auto.
inversion H3.
apply Match_cat ; auto.
apply Match_alt_r ; auto.
(* Case: Equiv_star_unit *)
inversion H2.
apply Match_star_nil.
(* <- *)
remember (Rstar Runit) as ru.
induction H2 ; try discriminate Heqru.
apply Match_unit.
inversion Heqru ; subst.
inversion H2_.
simpl ; auto.
(* Case: Equiv_star_alt_unit *)
remember (Rstar a) as ra.
induction H2 ; try discriminate Heqra.
apply Match_star_nil.
apply Match_star_cons.
inversion Heqra ; subst.
apply Match_alt_r ; auto.
auto.
(* <- *)
remember (Rstar (Ralt Runit a)) as ra.
induction H2 ; try discriminate Heqra.
apply Match_star_nil.
inversion Heqra ; subst.
clear IHregexp_match1.
inversion H2_.
inversion H2.
simpl ; auto.
apply Match_star_cons ; auto.
(* Case: Equiv_star_cat *)
inversion H2.
apply Match_alt_l ; apply Match_unit.
apply Match_alt_r ; apply Match_cat ; auto.
(* <- *)
inversion H2.
inversion H3.
apply Match_star_nil.
inversion H3.
apply Match_star_cons ; auto.
(* Case: Equiv_star_nested *)
rewrite app_nil_end.
apply Match_star_cons ; auto || apply Match_star_nil.
(* <- *)
remember (Rstar (Rstar a)) as rra.
induction H2 ; try discriminate Heqrra.
apply Match_star_nil.
inversion Heqrra ; subst.
clear IHregexp_match1.
remember (Rstar a) as ra.
induction H2_ ; try discriminate Heqra.
simpl ; auto.
rewrite app_ass.
apply Match_star_cons ; auto.
Qed.
Definition setreg := list regexp.
Fixpoint p (r:regexp) : setreg :=
match r with
| Rzero => nil
| Ralt a b => p a ++ p b
| _ => r :: nil
end.
Fixpoint sigma (l:list regexp) : regexp :=
match l with
| nil => Rzero
| r::l' => Ralt r (sigma l')
end.
Record mono : Set := Mono { mono_letter : A; mono_term : list regexp }.
Definition lin := list mono.
Definition lcat0 (b:list regexp) (m:mono) : mono :=
match m with
| Mono x p => Mono x (p ++ b)
end.
Definition lcat (l:lin) (b:regexp) : lin :=
match b with
| Rzero => nil
| Runit => l
| _ => map (lcat0 (b::nil)) l
end.
Fixpoint lf (r:regexp) : lin :=
match r with
| Rzero => nil
| Runit => nil
| Rsym x => (Mono x nil) :: nil
| Ralt a b => (lf a) ++ (lf b)
| Rcat a b => (lcat (lf a) b) ++ (if nullable a then lf b else nil)
| Rstar a => lcat (lf a) (Rstar a)
end.
Definition llcat (l:lin) (b:list regexp) : lin := map (lcat0 b) l.
Fixpoint llf (l:list regexp) : lin :=
match l with
| nil => nil
| a::l' => (llcat (lf a) l') ++ (if nullable a then llf l' else nil)
end.
Fixpoint fold_cat (l:list regexp) : regexp :=
match l with
| nil => Runit
| a::l' => Rcat a (fold_cat l')
end.
Definition unpack (m:mono) : regexp :=
match m with
| Mono x l => Rcat (Rsym x) (fold_cat l)
end.
Definition sigma_lin (l:lin) : regexp :=
sigma (map unpack l).
Definition choose (x':A) (m:mono) : bool :=
match m with
| Mono x p =>
if eq_A_dec x' x then true else false
end.
Definition delta (x:A) (t:regexp) : list regexp :=
map fold_cat (map mono_term (filter (choose x) (lf t))).
Fixpoint condense (l:list (list regexp)) : list regexp :=
match l with
| nil => nil
| x::l' => x ++ condense l'
end.
Definition delta_set (x:A) (r:list regexp) : list regexp :=
condense (map (delta x) r).
Fixpoint delta_word (w:list A) (t:regexp) {struct w} : list regexp :=
match w with
| nil => nil
| x::w' => delta_set x (delta_word w' t)
end.
Fixpoint cat_star_occurs (t:regexp) : nat :=
match t with
| Rzero => 0
| Runit => 0
| Rsym _ => 0
| Ralt a b => cat_star_occurs a + cat_star_occurs b
| Rcat a b => cat_star_occurs a + cat_star_occurs b + 1
| Rstar a => cat_star_occurs a + 1
end.
Fixpoint alphabetic_width (t:regexp) : nat :=
match t with
| Rzero => 0
| Runit => 0
| Rsym _ => 1
| Ralt a b => alphabetic_width a + alphabetic_width b
| Rcat a b => alphabetic_width a + alphabetic_width b
| Rstar a => alphabetic_width a
end.
Ltac simplify_regexp_step r :=
let simplify_alt_step r :=
match r with
| Ralt ?a ?a => a
| Ralt Rzero ?a => a
| Ralt ?a Rzero => a
| Ralt ?a ?b => let a' := simplify_regexp_step a in constr: (Ralt a' b)
| Ralt ?a ?b => let b' := simplify_regexp_step b in constr: (Ralt a b')
end in
let simplify_cat_step r :=
match r with
| Rcat Rzero _ => Rzero
| Rcat _ Rzero => Rzero
| Rcat Runit ?a => a
| Rcat ?a Runit => a
| Rcat ?a ?b => let a' := simplify_regexp_step a in constr: (Rcat a' b)
| Rcat ?a ?b => let b' := simplify_regexp_step b in constr: (Rcat a b')
end in
let simplify_star_step r :=
match r with
| Rzero => Runit
| Runit => Runit
| Rstar ?a => constr: (Rstar a)
| ?a => let a' := simplify_regexp_step a in constr: (Rstar a')
end in
match r with
| Ralt ?a ?b => simplify_alt_step (Ralt a b)
| Rcat ?a ?b => simplify_cat_step (Rcat a b)
| Rstar ?a => simplify_star_step a
end.
Ltac show_equiv_done :=
match goal with
| [ _:(equiv_regexp ?a ?b) |- (equiv_regexp ?a ?b) ] => auto
| [ |- (equiv_regexp ?a ?a) ] => apply Equiv_refl
| [ |- (equiv_regexp ?a (Ralt ?a ?a)) ] => apply Equiv_alt_same
| [ |- (equiv_regexp (Ralt ?a ?b) (Ralt ?b ?a)) ] => apply Equiv_alt_symmetric
| [ |- (equiv_regexp (Ralt ?a (Ralt ?b ?c)) (Ralt (Ralt ?a ?b) ?c)) ] => apply Equiv_alt_distributes
| [ |- (equiv_regexp ?a (Ralt Rzero ?a)) ] => apply Equiv_alt_zero_l
| [ |- (equiv_regexp ?a (Ralt ?a Rzero)) ] => apply Equiv_alt_zero_r
| [ |- (equiv_regexp (Rcat ?a (Rcat ?b ?c)) (Rcat (Rcat ?a ?b) ?c)) ] => apply Equiv_cat_distributes
| [ |- (equiv_regexp Rzero (Rcat Rzero ?a)) ] => apply Equiv_cat_zero_l
| [ |- (equiv_regexp Rzero (Rcat ?a Rzero)) ] => apply Equiv_cat_zero_r
| [ |- (equiv_regexp ?a (Rcat Runit ?a)) ] => apply Equiv_cat_unit_l
| [ |- (equiv_regexp ?a (Rcat ?a Runit)) ] => apply Equiv_cat_unit_r
| [ |- (equiv_regexp (Rcat ?a (Rcat ?b ?c)) (Rcat (Rcat ?a ?b) ?c)) ] => apply Equiv_cat_distributes
| [ |- (equiv_regexp (Rcat ?a (Ralt ?b ?c)) (Ralt (Rcat ?a ?b) (Rcat ?a ?c))) ] => apply Equiv_cat_distributes_l
| [ |- (equiv_regexp (Rcat (Ralt ?a ?b) ?c) (Ralt (Rcat ?a ?c) (Rcat ?b ?c))) ] => apply Equiv_cat_distributes_r
| [ |- (equiv_regexp (Rstar ?a) (Rstar (Ralt Runit ?a))) ] => apply Equiv_star_alt_unit
end.
Ltac show_equiv_step :=
match goal with
| [ |- (equiv_regexp (Ralt ?a ?b) (Ralt ?c ?d)) ] => apply Equiv_alt_rec
| [ |- (equiv_regexp (Rcat ?a ?b) (Rcat ?c ?d)) ] => apply Equiv_cat_rec
| [ |- (equiv_regexp (Rstar ?a) (Rstar ?b)) ] => apply Equiv_star_rec
| [ |- (equiv_regexp ?a ?b) ] => let b' := simplify_regexp_step b in subst_regexp b'
end.
Ltac show_equiv :=
(show_equiv_done || (apply Equiv_symmetric ; show_equiv_done)) ||
(show_equiv_step ; show_equiv) || (apply Equiv_symmetric ; show_equiv_step ; show_equiv).
Ltac alt_flip r :=
match r with
| Ralt ?a ?b => constr: (Ralt b a)
end.
Ltac alt_distribute_l r :=
match r with
| Ralt ?a (Ralt ?b ?c) => constr: (Ralt (Ralt a b) c)
end.
Ltac alt_distribute_r r :=
match r with
| Ralt (Ralt ?a ?b) ?c => constr: (Ralt a (Ralt b c))
end.
Ltac cat_distribute_l r :=
match r with
| Rcat ?a (Ralt ?b ?c) => constr: (Ralt (Rcat a b) (Rcat a c))
| Rcat ?a (Rcat ?b ?c) => constr: (Rcat (Rcat a b) c)
end.
Ltac cat_distribute_r r :=
match r with
| Rcat (Ralt ?a ?b) ?c => constr: (Ralt (Rcat a c) (Rcat b c))
| Rcat (Rcat ?a ?b) ?c => constr: (Rcat a (Rcat b c))
end.
Ltac left_branch t r :=
match r with
| Ralt ?a ?b => let a' := t a in constr: (Ralt a' b)
| Rcat ?a ?b => let a' := t a in constr: (Rcat a' b)
| Rstar ?a => let a' := t a in constr: (Rstar a')
end.
Ltac right_branch t := fun r =>
match r with
| Ralt ?a ?b => let b' := t b in constr: (Ralt a b')
| Rcat ?a ?b => let b' := t b in constr: (Rcat a b')
end.
Ltac apply_tac t :=
match goal with
| [ |- (equiv_regexp ?a ?b) ] => let b' := t b in subst_regexp b' ; show_equiv || idtac
end.
Ltac apply_tac_left t :=
match goal with
| [ |- (equiv_regexp ?a ?b) ] =>
let b' := left_branch t b in subst_regexp b' ; show_equiv || idtac
end.
Ltac apply_tac_right t :=
match goal with
| [ |- (equiv_regexp ?a ?b) ] =>
let b' := right_branch t b in subst_regexp b' ; show_equiv || idtac
end.
Lemma o_alt_equiv : forall (a b:regexp), equiv_regexp (o (Ralt a b)) (Ralt (o a) (o b)).
Proof.
intros a b.
unfold o ; simpl.
case (nullable a) ; case (nullable b) ; simpl ; show_equiv.
Qed.
Lemma o_cat_equiv : forall (a b:regexp), equiv_regexp (o (Rcat a b)) (Rcat (o a) (o b)).
Proof.
intros a b.
unfold o ; simpl.
case (nullable a) ; case (nullable b) ; simpl ; show_equiv.
Qed.
Lemma sigma_app_equiv : forall (la lb:list regexp),
equiv_regexp (sigma (la ++ lb)) (Ralt (sigma la) (sigma lb)).
Proof.
intros la lb.
induction la ; simpl.
apply Equiv_alt_zero_l.
apply_tac alt_distribute_r.
Qed.
Lemma sigma_lin_app_equiv : forall (la lb:lin),
equiv_regexp (sigma_lin (la ++ lb)) (Ralt (sigma_lin la) (sigma_lin lb)).
Proof.
intros la lb.
unfold sigma_lin.
rewrite map_app.
apply sigma_app_equiv.
Qed.
Lemma setreg_equiv_regexp : forall (a:regexp),
equiv_regexp a (sigma (p a)).
Proof.
induction a ; simpl ; show_equiv || idtac.
subst_regexp (Ralt (sigma (p a1)) (sigma (p a2))).
show_equiv.
apply Equiv_symmetric.
apply sigma_app_equiv.
Qed.
Lemma fold_cat_equiv : forall (l:list regexp) (a:regexp),
equiv_regexp (fold_cat (l ++ a::nil)) (Rcat (fold_cat l) a).
Proof.
intros l a.
induction l ; simpl.
subst_regexp a ; show_equiv.
apply_tac cat_distribute_r.
Qed.
Lemma fold_cat_app_equiv : forall (la lb:list regexp),
equiv_regexp (fold_cat (la ++ lb)) (Rcat (fold_cat la) (fold_cat lb)).
Proof.
intros la lb.
induction la ; simpl ; try show_equiv.
apply_tac cat_distribute_r.
Qed.
Lemma lcat_cases : forall (a:regexp),
a = Rzero \/ a = Runit \/ a <> Rzero /\ a <> Runit.
Proof.
intro a.
case a ; auto ; right ; right ; split ; discriminate.
Qed.
Lemma map_lcat0 : forall (l:lin) (b:regexp),
b <> Rzero -> b <> Runit -> map (lcat0 (b::nil)) l = lcat l b.
Proof.
intros a b.
induction b ; intros H1 H2 ; auto.
elim H1 ; trivial.
elim H2 ; trivial.
Qed.
Lemma lcat0_nil : forall (m:mono),
lcat0 nil m = m.
Proof.
intro m.
case m ; intros ml mt.
simpl ; rewrite <- app_nil_end ; auto.
Qed.
Lemma lcat_nil : forall (b:regexp),
lcat nil b = nil.
Proof.
intro b ; case b ; auto.
Qed.
Lemma llcat_nil : forall (l:lin),
llcat l nil = l.
Proof.
induction l ; simpl ; auto.
rewrite IHl.
rewrite lcat0_nil ; auto.
Qed.
Lemma lcat_app : forall (la1 la2:lin) (b:regexp),
lcat (la1 ++ la2) b = lcat la1 b ++ lcat la2 b.
Proof.
intros la1 la2 b.
elim (lcat_cases b).
(* b = Rzero *)
intro P ; subst ; auto.
intros [ P | [ P1 P2 ] ].
(* b = Runit *)
subst ; auto.
(* b <> Rzero /\ b <> Runit *)
rewrite <- map_lcat0 ; auto.
rewrite map_app.
rewrite map_lcat0 ; auto.
rewrite map_lcat0 ; auto.
Qed.
Lemma lcat_cons : forall (l:lin) (m:mono) (b:regexp),
lcat (m::l) b = lcat (m::nil) b ++ lcat l b.
Proof.
intros l m b.
elim (lcat_cases b).
(* b = Rzero *)
intro P ; subst ; auto.
intros [ P | [ P1 P2 ] ].
(* b = Runit *)
subst ; auto.
(* b <> Rzero /\ b <> Runit *)
rewrite <- map_lcat0 ; auto.
rewrite <- map_lcat0 ; auto.
rewrite <- map_lcat0 ; auto.
Qed.
Lemma llcat_app : forall (la lb:lin) (lc:list regexp),
llcat (la ++ lb) lc = llcat la lc ++ llcat lb lc.
Proof.
intros la lb lc.
induction la ; simpl ; auto.
rewrite IHla ; auto.
Qed.
Lemma llf_single_equiv_lf : forall (a:regexp),
llf (a::nil) = lf a.
Proof.
intro a ; simpl.
rewrite llcat_nil.
case (nullable a) ; rewrite <- app_nil_end ; auto.
Qed.
Lemma llcat_single_equiv_lcat : forall (l:lin) (b:regexp),
b <> Rzero -> b <> Runit ->
llcat l (b::nil) = lcat l b.
Proof.
intros l b P1 P2.
unfold llcat.
rewrite map_lcat0 ; auto.
Qed.
Lemma llf_double_equiv_lf : forall (a b:regexp),
b <> Rzero -> b <> Runit ->
llf (a::b::nil) = lf (Rcat a b).
Proof.
intros a b P1 P2.
simpl.
rewrite llcat_nil.
rewrite llcat_single_equiv_lcat ; auto.
case (nullable b) ; rewrite <- app_nil_end ; auto.
Qed.
Lemma llcat_equiv_lcat : forall (l:lin) (b:list regexp),
equiv_regexp (sigma_lin (llcat l b)) (sigma_lin (lcat l (fold_cat b))).
Proof.
intros l b.
induction l ; simpl.
(* l = nil *)
rewrite lcat_nil ; show_equiv.
(* l = cons *)
unfold sigma_lin.
simpl.
fold (sigma_lin (llcat l b)).
rewrite lcat_cons.
rewrite map_app.
subst_regexp (Ralt (sigma (map unpack (lcat (a::nil) (fold_cat b))))
(sigma (map unpack (lcat l (fold_cat b))))).
fold (sigma_lin (lcat l (fold_cat b))).
apply Equiv_alt_rec ; auto.
case a ; intros ml mt.
simpl.
subst_regexp (Rcat (Rsym ml) (Rcat (fold_cat mt) (fold_cat b))).
apply Equiv_cat_rec ; try show_equiv ; apply fold_cat_app_equiv.
elim (lcat_cases (fold_cat b)).
(* fold_cat b = Rzero *)
intro P ; rewrite P ; simpl ; show_equiv.
intros [ P | [ P1 P2 ] ].
(* fold_cat b = Runit *)
rewrite P ; simpl ; show_equiv.
(* fold_cat b <> Rzero /\ fold_cat b <> Runit *)
rewrite <- map_lcat0 ; auto.
simpl.
subst_regexp (Rcat (Rsym ml) (fold_cat (mt ++ fold_cat b::nil))) ; try show_equiv.
apply Equiv_cat_rec ; try show_equiv.
subst_regexp (Rcat (fold_cat mt) (fold_cat (fold_cat b :: nil))).
simpl ; show_equiv.
apply Equiv_symmetric ; apply fold_cat_app_equiv.
apply Equiv_symmetric ; apply sigma_app_equiv.
Qed.
Lemma llf_equiv_lf : forall (l:list regexp),
equiv_regexp (sigma_lin (llf l)) (sigma_lin (lf (fold_cat l))).
Proof.
induction l ; simpl ; try show_equiv.
subst_regexp (Ralt (sigma_lin (llcat (lf a) l)) (sigma_lin (if nullable a then llf l else nil))).
apply sigma_lin_app_equiv.
subst_regexp (Ralt (sigma_lin (lcat (lf a) (fold_cat l))) (sigma_lin (if nullable a then lf (fold_cat l) else nil))).
apply Equiv_alt_rec.
apply llcat_equiv_lcat.
case (nullable a) ; auto ; show_equiv.
apply Equiv_symmetric ; apply sigma_lin_app_equiv.
Qed.
Lemma sigma_lin_lcat : forall (la:lin) (b:regexp),
equiv_regexp (Rcat (sigma_lin la) b) (sigma_lin (lcat la b)).
Proof.
intros la b.
elim (lcat_cases b) ; intro P.
(* b = Rzero *)
subst ; unfold sigma_lin ; simpl ; show_equiv.
elim P ; clear P ; intro P.
(* b = Runit *)
subst ; simpl ; show_equiv.
elim P ; clear P ; intros P1 P2.
(* b <> Rzero /\ b <> Runit *)
rewrite <- map_lcat0 ; auto.
induction la ; unfold sigma_lin ; simpl ; try show_equiv.
fold (sigma_lin la).
fold (sigma_lin (map (lcat0 (b::nil)) la)).
apply Equiv_symmetric.
apply_tac cat_distribute_r.
apply Equiv_alt_rec ; try show_equiv.
case a ; intros ml mt.
unfold lcat0.
unfold unpack.
apply_tac cat_distribute_r.
apply Equiv_cat_rec ; try show_equiv.
apply fold_cat_equiv.
Qed.
Lemma sigma_cat_equiv : forall (a b:regexp),
(equiv_regexp b (Ralt (o b) (sigma_lin (lf b)))) ->
equiv_regexp (sigma_lin (lf (Rcat a b)))
(Ralt (Rcat (sigma_lin (lf a)) (o b)) (Rcat (Ralt (o a) (sigma_lin (lf a))) (sigma_lin (lf b)))).
Proof.
intros a b H.
simpl.
subst_regexp (Ralt (sigma_lin (lcat (lf a) b)) (sigma_lin (if nullable a then lf b else nil))).
apply sigma_lin_app_equiv.
subst_regexp (Ralt (sigma_lin (lcat (lf a) b)) (Rcat (o a) (sigma_lin (lf b)))).
apply Equiv_alt_rec ; try show_equiv.
unfold o ; case (nullable a) ; unfold sigma_lin ; simpl ; show_equiv.
subst_regexp (Ralt (Rcat (sigma_lin (lf a)) b) (Rcat (o a) (sigma_lin (lf b)))).
apply Equiv_alt_rec ; (apply Equiv_symmetric ; apply sigma_lin_lcat) || apply Equiv_refl.
subst_regexp (Ralt (Rcat (sigma_lin (lf a)) (Ralt (o b) (sigma_lin (lf b)))) (Rcat (o a) (sigma_lin (lf b)))).
show_equiv.
apply_tac_right cat_distribute_r.
apply_tac_right alt_flip.
apply_tac alt_distribute_l.
Qed.
Lemma sigma_rstar_equiv : forall (r:regexp),
equiv_regexp r (Ralt (o r) (sigma_lin (lf r))) ->
equiv_regexp (Rstar r) (Rstar (sigma_lin (lf r))).
Proof.
intros r H.
subst_regexp (Rstar (Ralt (o r) (sigma_lin (lf r)))) ; try show_equiv.
unfold o ; case (nullable r) ; show_equiv.
Qed.
Theorem linear_factorization : forall (r:regexp),
equiv_regexp r (Ralt (o r) (sigma_lin (lf r))).
Proof.
induction r ; try (unfold o ; unfold sigma_lin ; simpl ; show_equiv).
(* Case: Ralt *)
simpl.
subst_regexp (Ralt (Ralt (o r1) (o r2)) (Ralt (sigma_lin (lf r1)) (sigma_lin (lf r2)))).
apply_tac alt_distribute_r.
apply_tac_right alt_flip.
apply_tac_right alt_distribute_r.
apply_tac alt_distribute_l.
apply_tac_right alt_flip.
apply Equiv_alt_rec ; apply Equiv_symmetric.
apply o_alt_equiv.
apply sigma_lin_app_equiv.
(* Case: Rcat *)
subst_regexp (Rcat (Ralt (o r1) (sigma_lin (lf r1))) (Ralt (o r2) (sigma_lin (lf r2)))).
show_equiv.
subst_regexp (Ralt (Rcat (o r1) (o r2)) (sigma_lin (lf (Rcat r1 r2)))).
apply Equiv_symmetric.
apply_tac cat_distribute_l.
apply_tac_left cat_distribute_r.
apply_tac alt_distribute_r.
apply Equiv_alt_rec ; try show_equiv.
apply sigma_cat_equiv ; apply IHr2.
apply Equiv_alt_rec ; try show_equiv.
apply Equiv_symmetric ; apply o_cat_equiv.
(* Case: Rstar *)
unfold o ; unfold nullable.
replace (lf (Rstar r)) with (lcat (lf r) (Rstar r)) ; auto.
subst_regexp (Ralt Runit (Rcat (sigma_lin (lf r)) (Rstar r))).
subst_regexp (Ralt Runit (Rcat (sigma_lin (lf r)) (Rstar (sigma_lin (lf r))))).
subst_regexp (Rstar (sigma_lin (lf r))).
apply sigma_rstar_equiv ; apply IHr.
apply Equiv_star_cat.
apply Equiv_alt_rec ; try show_equiv.
apply Equiv_cat_rec ; try show_equiv.
apply Equiv_symmetric.
apply sigma_rstar_equiv ; apply IHr.
apply Equiv_alt_rec ; try show_equiv.
apply sigma_lin_lcat.
Qed.
Lemma condense_app : forall (la lb:list (list regexp)),
condense (la ++ lb) = condense la ++ condense lb.
Proof.
induction la ; intro lb ; simpl.
trivial.
rewrite IHla.
rewrite app_ass.
trivial.
Qed.
Lemma choose_app : forall (x:A) (la lb:lin),
filter (choose x) (la ++ lb) = filter (choose x) la ++ filter (choose x) lb.
Proof.
induction la ; simpl.
trivial.
intro lb.
case (choose x a).
rewrite <- app_comm_cons.
rewrite IHla.
trivial.
apply IHla.
Qed.
Lemma sigma_delta_lcat : forall (a b:regexp) (x:A),
equiv_regexp
(Rcat (sigma (delta x a)) b)
(sigma (map fold_cat (map mono_term (filter (choose x) (lcat (lf a) b))))).
Proof.
intros a b x.
unfold delta.
elim (lcat_cases b) ; intro P.
(* b = Rzero *)
subst ; simpl ; show_equiv.
elim P ; clear P ; intro P.
(* b = Runit *)
subst ; simpl ; show_equiv.
elim P ; clear P ; intros P1 P2.
(* b <> Rzero /\ b <> Runit *)
rewrite <- map_lcat0 ; auto.
induction (lf a) ; simpl ; try show_equiv.
case a0 ; intros ml mt ; simpl.
case (eq_A_dec x ml) ; intro ; simpl.
apply Equiv_symmetric.
apply_tac cat_distribute_r.
apply Equiv_alt_rec ; try show_equiv.
apply fold_cat_equiv.
apply IHl.
Qed.
Lemma sigma_delta_alt : forall (a b:regexp) (x:A),
equiv_regexp (Ralt (sigma (delta x a)) (sigma (delta x b))) (sigma (delta x (Ralt a b))).
Proof.
intros a b x.
unfold delta at 3 ; simpl.
rewrite choose_app.
rewrite map_app.
rewrite map_app.
fold (delta x a).
fold (delta x b).
subst_regexp (Ralt (sigma (delta x a)) (sigma (delta x b))).
show_equiv.
apply Equiv_symmetric.
apply sigma_app_equiv.
Qed.
Lemma sigma_delta_cat : forall (a b:regexp) (x:A),
equiv_regexp (Ralt (Rcat (sigma (delta x a)) b) (Rcat (o a) (sigma (delta x b))))
(sigma (delta x (Rcat a b))).
Proof.
intros a b x.
unfold delta at 3.
simpl ; unfold o.
assert (P:nullable a = true \/ nullable a = false).
case (nullable a) ; auto.
elim P ; clear P ; intro P ; rewrite P.
(* Case: nullable a = true *)
rewrite choose_app.
rewrite map_app.
rewrite map_app.
fold (delta x b).
subst_regexp (Ralt
(sigma (map fold_cat (map mono_term (filter (choose x) (lcat (lf a) b)))))
(sigma (delta x b))).
apply Equiv_alt_rec ; try show_equiv.
apply sigma_delta_lcat.
apply Equiv_symmetric.
apply sigma_app_equiv.
(* Case: nullable a = false *)
rewrite <- app_nil_end.
subst_regexp (Rcat (sigma (delta x a)) b) ; try show_equiv.
apply sigma_delta_lcat.
Qed.
Lemma sigma_delta_star : forall (a:regexp) (x:A),
equiv_regexp (Rcat (sigma (delta x a)) (Rstar a)) (sigma (delta x (Rstar a))).
Proof.
intros a x.
unfold delta at 2 ; simpl.
fold (lcat (lf a) (Rstar a)).
apply sigma_delta_lcat.
Qed.
Theorem partial_derivative : forall (t:regexp) (x:A),
equiv_regexp (derivative x t) (sigma (delta x t)).
Proof.
intros t x.
induction t ; simpl ; try show_equiv.
(* Case: Rsym *)
unfold delta ; simpl.
case (eq_A_dec x a) ; intro ; simpl ; show_equiv.
(* Case: Ralt *)
subst_regexp (Ralt (sigma (delta x t1)) (sigma (delta x t2))).
show_equiv.
apply sigma_delta_alt.
(* Case: Rcat *)
subst_regexp (Ralt (Rcat (sigma (delta x t1)) t2) (Rcat (o t1) (sigma (delta x t2)))).
show_equiv.
apply sigma_delta_cat.
(* Case: Rstar *)
subst_regexp (Rcat (sigma (delta x t)) (Rstar t)).
show_equiv.
apply sigma_delta_star.
Qed.
Inductive subterm : regexp -> regexp -> Prop :=
| Subterm_star_refl : forall (a:regexp), subterm (Rstar a) (Rstar a)
| Subterm_trans : forall (a b c:regexp), subterm a b -> subterm b c -> subterm a c
| Subterm_alt_l : forall (a b:regexp), subterm a (Ralt a b)
| Subterm_alt_r : forall (a b:regexp), subterm b (Ralt a b)
| Subterm_cat_l : forall (a b:regexp), subterm a (Rcat a b)
| Subterm_cat_r : forall (a b:regexp), subterm b (Rcat a b)
| Subterm_star : forall (a:regexp), subterm a (Rstar a).
Definition subterm_list (l:list regexp) (r:regexp) :=
forall (s:regexp), In s l -> subterm s r.
Definition subterm_lin (l:lin) (r:regexp) :=
forall (m:mono), In m l -> subterm_list (mono_term m) r.
Lemma subterm_list_nil : forall (r:regexp), subterm_list nil r.
Proof.
unfold subterm_list.
intros r s H.
elim H.
Qed.
Lemma subterm_lin_nil : forall (r:regexp), subterm_lin nil r.
Proof.
unfold subterm_lin.
intros r m H.
elim H.
Qed.
Lemma subterm_list_cons : forall (r s:regexp) (l:list regexp),
subterm s r -> subterm_list l r -> subterm_list (s::l) r.
Proof.
unfold subterm_list.
intros r s l H1 H2 s0 H3.
elim H3 ; clear H3 ; intro H3 ; subst ; auto.
Qed.
Lemma subterm_lin_cons : forall (r:regexp) (m:mono) (l:lin),
subterm_list (mono_term m) r -> subterm_lin l r -> subterm_lin (m::l) r.
Proof.
unfold subterm_lin.
intros r m l H1 H2 m0 H3.
elim H3 ; clear H3 ; intro H3 ; subst ; auto.
Qed.
Lemma subterm_list_app : forall (l1 l2:list regexp) (r:regexp),
subterm_list l1 r -> subterm_list l2 r -> subterm_list (l1 ++ l2) r.
Proof.
unfold subterm_list.
intros l1 l2 r H1 H2 s H3.
apply in_app_or in H3.
elim H3 ; auto.
Qed.
Lemma subterm_lin_app : forall (l1 l2:lin) (r:regexp),
subterm_lin l1 r -> subterm_lin l2 r -> subterm_lin (l1 ++ l2) r.
Proof.
unfold subterm_lin.
intros l1 l2 r H1 H2 m H3.
apply in_app_or in H3.
elim H3 ; auto.
Qed.
Lemma subterm_list_trans : forall (l:list regexp) (a b:regexp),
subterm_list l a -> subterm a b -> subterm_list l b.
Proof.
unfold subterm_list.
intros l a b H1 H2 s H3.
apply (Subterm_trans s a b) ; auto.
Qed.
Lemma subterm_lin_trans : forall (l:lin) (a b:regexp),
subterm_lin l a -> subterm a b -> subterm_lin l b.
Proof.
unfold subterm_lin.
intros l a b H1 H2 m H3.
eapply subterm_list_trans ; auto.
Qed.
Lemma subterm_lin_map : forall (l:lin) (r:regexp) (f:mono -> mono),
(forall m:mono, subterm_list (mono_term m) r -> subterm_list (mono_term (f m)) r) ->
subterm_lin l r -> subterm_lin (map f l) r.
Proof.
unfold subterm_lin.
intros l r f H1 H2 m H3.
elim (in_map_iff f l m).
intros H4 H5 ; clear H5.
elim (H4 H3) ; clear H4.
intros x H4 ; elim H4 ; clear H4.
intros H4 H5.
subst ; auto.
Qed.
Lemma lcat0_structure : forall (b r:regexp) (m:mono),
subterm b r ->
subterm_list (mono_term m) r ->
subterm_list (mono_term (lcat0 (b::nil) m)) r.
Proof.
intros b r m H1 H2.
replace (mono_term (lcat0 (b::nil) m)) with (mono_term m ++ b::nil).
apply subterm_list_app ; auto.
apply subterm_list_cons ; auto.
apply subterm_list_nil.
case m ; auto.
Qed.
Theorem lf_structure : forall (a:regexp),
subterm_lin (lf a) a.
Proof.
induction a ; simpl.
(* Case: Rzero *)
apply subterm_lin_nil.
(* Case: Runit *)
apply subterm_lin_nil.
(* Case: Rsym *)
apply subterm_lin_cons.
simpl.
apply subterm_list_nil.
apply subterm_lin_nil.
(* Case: Ralt *)
apply subterm_lin_app.
apply (subterm_lin_trans (lf a1) a1 (Ralt a1 a2)) ; auto.
apply Subterm_alt_l.
apply (subterm_lin_trans (lf a2) a2 (Ralt a1 a2)) ; auto.
apply Subterm_alt_r.
(* Case: Rcat *)
apply subterm_lin_app.
elim (lcat_cases a2) ; intro P.
(* a2 = Rzero *)
subst ; simpl.
apply subterm_lin_nil.
elim P ; clear P ; intro P.
(* a2 = Runit *)
subst ; simpl.
apply (subterm_lin_trans (lf a1) a1 (Rcat a1 Runit)) ; auto.
apply Subterm_cat_l.
elim P ; clear P ; intros P1 P2.
(* a2 <> Rzero /\ a2 <> Runit *)
rewrite <- map_lcat0 ; auto.
apply subterm_lin_map.
intros m H.
apply lcat0_structure ; auto.
apply Subterm_cat_r.
apply (subterm_lin_trans (lf a1) a1 (Rcat a1 a2)) ; auto.
apply Subterm_cat_l.
case (nullable a1).
apply (subterm_lin_trans (lf a2) a2 (Rcat a1 a2)) ; auto.
apply Subterm_cat_r.
apply subterm_lin_nil.
(* Case: Rstar *)
apply subterm_lin_map.
intros m H.
apply lcat0_structure ; auto.
apply Subterm_star_refl.
apply (subterm_lin_trans (lf a) a (Rstar a)) ; auto.
apply Subterm_star.
Qed.
Theorem lf_size : forall (a:regexp) (m:mono),
In m (lf a) -> length (mono_term m) <= cat_star_occurs a.
Proof.
induction a ; simpl ; intros m H ; try (elim H ; fail).
(* Case: Rsym *)
elim H ; clear H ; intro H.
subst ; simpl ; auto.
elim H.
(* Case: Ralt *)
apply in_app_or in H.
elim H ; clear H ; intro H.
apply le_plus_trans ; auto.
rewrite plus_comm.
apply le_plus_trans ; auto.
(* Case: Rcat *)
apply in_app_or in H.
elim H ; clear H ; intro H.
elim (lcat_cases a2) ; intro P.
(* a2 = Rzero *)
subst ; simpl in H ; elim H.
elim P ; clear P ; intro P.
(* a2 = Runit *)
subst ; simpl in H.
apply le_plus_trans ; apply le_plus_trans ; auto.
elim P ; clear P ; intros P1 P2.
(* a2 <> Rzero /\ a2 <> Runit *)
rewrite <- map_lcat0 in H ; auto.
elim (in_map_iff (lcat0 (a2::nil)) (lf a1) m).
intros H1 H2 ; clear H2.
elim (H1 H) ; clear H1 ; intros x [ H1 H2 ].
subst.
replace (mono_term (lcat0 (a2::nil) x)) with (mono_term x ++ a2::nil).
rewrite app_length ; simpl.
apply plus_le_compat_r.
apply le_plus_trans ; auto.
case x ; auto.
revert H ; case (nullable a1) ; intro H.
apply le_plus_trans.
rewrite plus_comm.
apply le_plus_trans ; auto.
elim H.
(* Case: Rstar *)
elim (in_map_iff (lcat0 ((Rstar a)::nil)) (lf a) m).
intros H1 H2 ; clear H2.
elim (H1 H) ; clear H1 ; intros x [ H1 H2 ].
subst.
replace (mono_term (lcat0 ((Rstar a)::nil) x)) with (mono_term x ++ (Rstar a)::nil).
rewrite app_length ; simpl.
apply plus_le_compat_r ; auto.
case x ; auto.
Qed.
Lemma lf_nonzero_nonunit : forall (a:regexp) (m:mono) (s:regexp),
In m (lf a) -> In s (mono_term m) -> s <> Rzero /\ s <> Runit.
Proof.
induction a ; simpl ; intros m s H1 H2.
(* Case: Rzero *)
elim H1.
(* Case: Runit *)
elim H1.
(* Case: Rsym *)
elim H1 ; clear H1 ; intro H1.
subst ; simpl in H2 ; elim H2.
elim H1.
(* Case: Ralt *)
apply in_app_or in H1.
elim H1 ; clear H1 ; intro H1.
apply (IHa1 m) ; auto.
apply (IHa2 m) ; auto.
(* Case: Rcat *)
apply in_app_or in H1.
elim H1 ; clear H1 ; intro H1.
elim (lcat_cases a2) ; intro P.
(* a2 = Rzero *)
subst ; simpl in H1 ; elim H1.
elim P ; clear P ; intro P.
(* a2 = Runit *)
subst ; simpl in H1.
apply (IHa1 m) ; auto.
elim P ; clear P ; intros P1 P2.
(* a2 <> Rzero /\ a2 <> Runit *)
rewrite <- map_lcat0 in H1 ; auto.
elim (in_map_iff (lcat0 (a2::nil)) (lf a1) m).
intros H3 H4 ; clear H4.
elim (H3 H1) ; clear H3 ; intros x [ H3 H4 ].
subst.
replace (mono_term (lcat0 (a2::nil) x)) with (mono_term x ++ a2::nil) in H2.
apply in_app_or in H2.
elim H2 ; clear H2 ; intro H2.
apply (IHa1 x) ; auto.
elim H2 ; clear H2 ; intro H2.
subst ; auto.
elim H2.
case x ; auto.
revert H1 ; case (nullable a1) ; simpl ; intro H1.
apply (IHa2 m) ; auto.
elim H1.
(* Case: Rstar *)
elim (in_map_iff (lcat0 ((Rstar a)::nil)) (lf a) m).
intros H3 H4 ; clear H4.
elim (H3 H1) ; clear H3 ; intros x [ H3 H4 ].
subst.
replace (mono_term (lcat0 ((Rstar a)::nil) x)) with (mono_term x ++ (Rstar a)::nil) in H2.
apply in_app_or in H2.
elim H2 ; clear H2 ; intro H2.
apply (IHa x) ; auto.
elim H2 ; clear H2 ; intro H2.
subst ; split ; discriminate.
elim H2.
case x ; auto.
Qed.
(* WARNING: very random from here onwards *)
(*
Lemma plus_trans : forall (a b c:nat),
b = c -> a + b = a + c.
Proof.
intros a b c H.
induction a ; auto.
Qed.
Lemma fold_cat_alphabetic_width : forall (l:list regexp) (a:regexp),
alphabetic_width (fold_cat (l ++ a::nil)) = alphabetic_width (fold_cat l) + alphabetic_width a.
Proof.
intros l a.
induction l ; simpl.
auto with arith.
rewrite <- plus_assoc.
apply plus_trans ; auto.
Qed.
Lemma foo : forall (a:regexp) (m:mono),
In m (lf a) -> alphabetic_width (fold_cat (mono_term m)) < alphabetic_width a.
Proof.
induction a ; simpl ; intros m H.
(* Case: Rzero *)
elim H.
(* Case: Runit *)
elim H.
(* Case: Rsym *)
elim H ; clear H ; intro H.
subst ; auto.
elim H.
(* Case: Ralt *)
apply in_app_or in H.
elim H ; clear H ; intro H.
apply lt_plus_trans ; auto.
rewrite plus_comm.
apply lt_plus_trans ; auto.
(* Case: Rcat *)
apply in_app_or in H.
elim H ; clear H ; intro H.
elim (lcat_cases a2) ; intro P.
(* a2 = Rzero *)
subst ; simpl in H ; elim H.
elim P ; clear P ; intro P.
(* a2 = Runit *)
subst ; simpl in H.
apply lt_plus_trans ; auto.
elim P ; clear P ; intros P1 P2.
(* a2 <> Rzero /\ a2 <> Runit *)
rewrite <- map_lcat0 in H ; auto.
elim (in_map_iff (lcat0 a2) (lf a1) m).
intros H1 H2 ; clear H2.
elim (H1 H) ; clear H1.
intros x H1.
elim H1 ; clear H1 ; intros ; subst.
replace (mono_term (lcat0 a2 x)) with (mono_term x ++ a2::nil).
rewrite fold_cat_alphabetic_width.
apply plus_lt_compat_r ; auto.
case x ; auto.
(* ++ *)
revert H ; case (nullable a1) ; intro H.
rewrite plus_comm.
apply lt_plus_trans ; auto.
elim H.
(* Case: Rstar *)
elim (in_map_iff (lcat0 (Rstar a)) (lf a) m).
intros H1 H2 ; clear H2.
elim (H1 H) ; clear H1.
intros x H1.
elim H1 ; clear H1 ; intros ; subst.
replace (mono_term (lcat0 (Rstar a) x)) with (mono_term x ++ (Rstar a)::nil).
rewrite fold_cat_alphabetic_width.
*)
Inductive last : regexp -> list regexp -> Prop :=
| last_single : forall (a:regexp), last a (a::nil)
| last_cons : forall (a b:regexp) (l:list regexp), last a l -> last a (b::l).
Lemma last_app : forall (a:regexp) (l:list regexp), last a (l ++ a::nil).
Proof.
induction l ; simpl.
apply last_single.
apply last_cons ; auto.
Qed.
Inductive split_tail : list regexp -> list regexp -> regexp -> Prop :=
| Tail_single : forall (a:regexp), split_tail (a::nil) nil a
| Tail_cons : forall (a b:regexp) (l la:list regexp),
split_tail l la a -> split_tail (b::l) (b::la) a.
Lemma split_tail_app : forall (a:regexp) (l:list regexp),
split_tail (l ++ a::nil) l a.
Proof.
intros a l.
induction l ; simpl.
apply Tail_single.
apply Tail_cons ; auto.
Qed.
Lemma split_tail_app2 : forall (a b:regexp) (l:list regexp),
split_tail (l ++ a::nil) l b -> a = b.
Proof.
intros a b l.
induction l ; simpl ; intro H ; inversion H ; auto.
Qed.
(*
Lemma split_tail_app3 : forall (a:regexp) (la l:list regexp),
split_tail (l ++ a::nil) la a -> l = la.
Proof.
induction l ; simpl ; intro H.
(* l = nil *)
inversion H ; subst ; auto.
inversion H4.
(* l = cons *)
inversion H ; subst.
generalize (app_cons_not_nil l nil a) ; unfold not ; intro H3 ; elim H3 ; auto.
Lemma split_tail_app3 : forall (a b:regexp) (l la:list regexp),
split_tail (l ++ a::nil) la b -> a = b /\ l = la.
Proof.
intros a b l la.
induction l ; simpl ; intro H.
(* l = nil *)
inversion H ; subst ; auto.
inversion H4.
(* l = cons *)
*)
Axiom split_tail_app_hack : forall (a b:regexp) (l la:list regexp),
split_tail (l ++ a::nil) la b -> a = b /\ l = la.
Inductive PD : list regexp -> regexp -> Prop :=
(* | PD_refl : forall (a:regexp), PD (a::nil) a *)
| PD_step : forall (a:regexp) (m:mono), In m (lf a) -> PD (mono_term m) a
| PD_trans : forall (a:regexp) (l:list regexp) (m:mono),
PD l a -> In m (lf (fold_cat l)) -> PD (mono_term m) a.
Lemma PD_cat_star : forall (a b c:regexp) (l la:list regexp),
PD l (Rcat a (Rstar b)) -> split_tail l la c -> (PD la a \/ PD la b) /\ c = (Rstar b).
Proof.
intros a b c l la H1 H2.
inversion H1 ; subst.
(* PD_step *)
simpl in H.
apply in_app_or in H.
elim H ; clear H ; intro H.
elim (in_map_iff (lcat0 ((Rstar b)::nil)) (lf a) m).
intros H3 H4 ; clear H4.
elim (H3 H) ; clear H3 ; intros x [ H3 _ ].
subst.
replace (mono_term (lcat0 ((Rstar b)::nil) x)) with (mono_term x ++ (Rstar b)::nil) in *.
generalize (split_tail_app_hack (Rstar b) c (mono_term x) la H2).
intros [ H4 H5 ].
split ; auto.
subst.
left ; apply PD_step ; auto.
case x ; auto.
revert H ; case (nullable a) ; intro H.
elim (in_map_iff (lcat0 ((Rstar b)::nil)) (lf b) x).
intros H3 H4 ; clear H4.
elim (H3 H) ; clear H3.
intros x H3.
elim H3 ; clear H3 ; intros ; subst.
replace (mono_term (lcat0 (Rstar b) x)) with (mono_term x ++ (Rstar b)::nil) in *.
generalize (split_tail_app_hack (Rstar b) c (mono_term x) la H2).
intro H4 ; elim H4 ; clear H4 ; intros H4 H5.
split ; auto.
subst.
right ; apply PD_step ; auto.
case x ; auto.
elim H.
(* PD_trans *)
Inductive LF : list regexp -> regexp -> Prop :=
| LF_step : forall (a:regexp) (m:mono), In m (lf a) -> LF (mono_term m) a
| LF_trans : forall (a:regexp) (l:list regexp) (m:mono),
LF l a -> In m (lf (fold_cat l)) -> LF (mono_term m) a.
Lemma LF_star : forall (a b:regexp) (l la:list regexp),
LF l (Rstar a) -> split_tail l la b -> LF la a /\ b = (Rstar a).
Proof.
intros a b l la H1 H2.
inversion H1 ; subst.
(* Case: LF_step *)
simpl in H.
elim (in_map_iff (lcat0 (Rstar a)) (lf a) m).
intros H3 H4 ; clear H4.
elim (H3 H) ; clear H3.
intros x H3.
elim H3 ; clear H3 ; intros ; subst.
replace (mono_term (lcat0 (Rstar a) x)) with (mono_term x ++ (Rstar a)::nil) in H2.
generalize (split_tail_app_hack (Rstar a) b (mono_term x) la H2).
intro H4 ; elim H4 ; clear H4 ; intros H4 H5.
split ; auto.
subst.
apply LF_step ; auto.
case x ; auto.
(* Case: LF_trans *)
induction l0 ; simpl in H0.
elim H0.
apply in_app_or in H0.
elim H0 ; clear H0 ; intro H0.
apply IHl0.
Lemma lf_star : forall (a:regexp) (m:mono),
In m (lf (Rstar a)) -> last (Rstar a) (mono_term m).
Proof.
intros a m.
simpl.
induction (lf a) ; simpl ; intro H.
elim H.
elim H ; clear H ; intro H ; auto.
subst.
case a0 ; intros ml mt.
simpl.
apply last_app.
Qed.
Definition pd_single (t:regexp) : list regexp :=
map fold_cat (map mono_term (lf t)).
Definition pd_step (l:list regexp) : list regexp :=
flat_map pd_single l.
Fixpoint pd (l:list regexp) : list regexp :=
match l with
| nil => nil
| a::al =>
match pd_single a with
| nil => a :: pd al
| b::bl =>
end
end.
Inductive pd : regexp -> list regexp -> Prop :=
| PD_refl : forall (a:regexp), pd a (a::nil)
| PD_lf : forall (a:regexp) (m:mono),
In m (lf a) -> pd a (mono_term m)
| PD_rec : forall (a:regexp) (d:list regexp) (m:mono),
pd a d -> In m (lf (fold_cat d)) -> pd a (mono_term m).
Record states : Set := States {
states_pd : list regexp;
states_ds : list regexp
}.
Fixpoint delta_step (s:states) : states :=
let pd := states_pd s ++ states_ds s in
let ds :=
Lemma delta_word_zero : forall (w:list A),
delta_word w Rzero = nil.
Proof.
induction w ; simpl.
trivial.
rewrite IHw.
simpl ; trivial.
Qed.
Lemma delta_word_unit : forall (w:list A),
delta_word w Runit = nil.
Proof.
induction w ; simpl.
trivial.
rewrite IHw.
simpl ; trivial.
Qed.
Lemma delta_word_sym : forall (x:A) (w:list A),
delta_word w (Rsym x) = nil.
Proof.
induction w ; simpl.
auto.
rewrite IHw.
simpl ; auto.
Qed.
Lemma delta_word_alt : forall (w:list A) (a b:regexp),
delta_word w (Ralt a b) = delta_word w a ++ delta_word w b.
Proof.
intros w a b.
induction w ; simpl.
auto.
unfold delta_set.
rewrite <- condense_app.
rewrite <- map_app.
rewrite IHw.
trivial.
Qed.
Theorem something : forall (t:regexp) (w:list A),
length (delta_word w t) <= alphabetic_width t.
Proof.
induction t ; intro w ; simpl.
(* Case: Rzero *)
rewrite delta_word_zero ; auto.
(* Case: Runit *)
rewrite delta_word_unit ; auto.
(* Case: Rsym *)
rewrite delta_word_sym ; auto.
(* Case: Ralt *)
rewrite delta_word_alt.
rewrite app_length.
apply plus_le_compat ; auto.
(* Case: Rcat *)
induction w ; simpl.
auto with arith.
(*
Open Local Scope char_scope.
Definition r := Rcat (Rsym "a") (Rstar (Rsym "b")).
Definition w1 := "a" :: nil.
Eval compute in simplify (simplify (deltaw w1 r)).
*)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment