Library ATBR.StrictStarForm
Definition of the "strict star form" property for regular expressions,
together with an algorithm to put any regex into a strict star form one.
Proof of correctness and completeness. Definition of the corresponding kleene_ssf tactic.
Proof of correctness and completeness. Definition of the corresponding kleene_ssf tactic.
Require Import Common.
Require Import Classes.
Require Import Graph.
Require Import SemiLattice.
Require Import Monoid.
Require Import SemiRing.
Require Import KleeneAlgebra.
Require Import Model_RegExp.
Import RegExp.Load.
Require Reification.
Require Import Bool. Open Scope lazy_bool_scope.
Inductive strict: regex -> Prop :=
| strict_zero: strict 0
| strict_var: forall i, strict (RegExp.var i)
| strict_plus: forall a b, strict a -> strict b -> strict (a+b)
| strict_dot_l: forall a b, strict a -> strict (a*b)
| strict_dot_r: forall a b, strict b -> strict (a*b).
Inductive non_strict: regex -> Prop :=
| non_strict_one: non_strict 1
| non_strict_star: forall a, non_strict (a#)
| non_strict_dot: forall a b, non_strict a -> non_strict b -> non_strict (a*b)
| non_strict_plus_l: forall a b, non_strict a -> non_strict (a+b)
| non_strict_plus_r: forall a b, non_strict b -> non_strict (a+b).
Lemma non_strict_not_strict: forall a, non_strict a -> ~ strict a.
Inductive strict_star_form: regex -> Prop :=
| ssf_zero: strict_star_form 0
| ssf_one: strict_star_form 1
| ssf_var: forall i, strict_star_form (RegExp.var i)
| ssf_star: forall a, strict_star_form a -> strict a -> strict_star_form (a#)
| ssf_plus: forall a b, strict_star_form a -> strict_star_form b -> strict_star_form (a+b)
| ssf_dot: forall a b, strict_star_form a -> strict_star_form b -> strict_star_form (a*b).
Fixpoint contains_one e : bool :=
match e with
| RegExp.star a => true
| RegExp.one => true
| RegExp.plus a b => contains_one a ||| contains_one b
| RegExp.dot a b => contains_one a &&& contains_one b
| e => false
end.
Definition plus_but_one a b :=
if RegExp.is_one a then b
else if RegExp.is_one b then a
else RegExp.plus a b.
Fixpoint remove e :=
if contains_one e then
match e with
| RegExp.plus a b => plus_but_one (remove a) (remove b)
| RegExp.dot a b => plus_but_one (remove a) (remove b)
| RegExp.star e => e
| e => e
end
else e.
Definition dot' a b :=
if RegExp.is_one a then b
else if RegExp.is_one b then a
else RegExp.dot a b.
Definition star' a :=
if RegExp.is_one a then RegExp.one else RegExp.star a.
Fixpoint ssf e :=
match e with
| RegExp.plus a b => RegExp.plus (ssf a) (ssf b)
| RegExp.dot a b => dot' (ssf a) (ssf b)
| RegExp.star e => star' (remove (ssf e))
| e => e
end.
Lemma star_plus_one: forall a: regex, (1+a)# == a#.
Lemma star_plus_star_1: forall a b: regex, (a+b)# == (a#+b)#.
Lemma star_plus_star: forall a b: regex, (a+b)# == (a#+b#)#.
Lemma star_plus_but_one: forall a b: regex, (plus_but_one a b) # == (a + b)#.
Lemma star'_star: forall a: regex, star' a == a# .
Lemma dot'_dot: forall a b: regex, dot' a b == a * b.
Lemma contains_one_correct: forall a: regex, contains_one a = true -> a == a + 1.
Lemma star_dot_leq_star_plus: forall a b: regex, (a*b)# <== (a+b)#.
Lemma star_plus_star_dot: forall a b: regex,
contains_one a = true -> contains_one b = true -> (a+b)# == (a*b)#.
Lemma star_remove: forall a: regex, remove a # == a #.
correctness of the rewriting procedure
tactic to put Kleene algebra expressions into strict star form
Theorem ssf_correct': forall e, RegExp.equal e (ssf e).
Ltac kleene_ssf := kleene_normalize_ ssf_correct'.
Ltac kleene_ssf := kleene_normalize_ ssf_correct'.
below: completeness of the rewriting procedure
Local Hint Constructors strict_star_form.
Local Hint Constructors strict.
Lemma remove_nf: forall a, strict_star_form a -> strict_star_form (remove a).
Lemma contains_one_false_strict: forall a, contains_one a = false -> strict a.
Local Hint Resolve contains_one_false_strict.
Lemma remove_strict: forall a, strict_star_form a -> RegExp.is_one (remove a) = false -> strict (remove a).
completeness of the rewriting procedure