Library ATBR.DKA_CheckLabels
Reflexive algorithm to check that two regex have the same sets of variables.
We also prove that equal regex necessarily have the same set of labels, and that the conversion into strict star form preserves this set.
We also prove that equal regex necessarily have the same set of labels, and that the conversion into strict star form preserves this set.
Require Import Common.
Require Import Classes.
Require Import Graph.
Require Import DKA_Definitions.
Require Import StrictStarForm.
Fixpoint collect e acc :=
match e with
| RegExp.var i => NumSet.add i acc
| RegExp.plus a b => collect a (collect b acc)
| RegExp.dot a b => collect a (collect b acc)
| RegExp.star a => collect a acc
| _ => acc
end.
Definition same_labels a b : bool :=
NumSet.equal (collect a NumSet.empty) (collect b NumSet.empty).
Infix " [=] " := NumSet.Equal (at level 80).
Section protect.
Local Instance collect_compat a: Proper (NumSet.Equal ==> NumSet.Equal) (collect a).
Definition collect_compat' a x := @collect_compat a x.
Lemma collect_incr_2: forall a i acc,
NumSet.In i acc -> NumSet.In i (collect a acc).
Lemma collect_incr_1: forall a i acc acc',
NumSet.In i (collect a acc') -> NumSet.In i (collect a acc) \/ NumSet.In i acc'.
Lemma collect_com: forall a b acc, collect a (collect b acc) [=] collect b (collect a acc).
Lemma collect_idem: forall a acc, collect a (collect a acc) [=] collect a acc.
Lemma NumSetEqual_refl: forall x, x [=] x.
Local Hint Resolve collect_compat' collect_idem collect_com NumSetEqual_refl.
Notation clean := RegExp.Clean.rewrite.
Ltac contradict :=
match goal with
| H: RegExp.equal ?x ?y , Hx: RegExp.is_zero (clean ?x) = _ , Hy: RegExp.is_zero (clean ?y) = _ |- _ =>
exfalso; apply RegExp.Clean.equal_rewrite_zero_equiv in H; rewrite H, Hy in Hx; discriminate Hx
end.
Lemma equal_collect: forall a b, a==b ->
forall acc, collect (clean a) acc [=] collect (clean b) acc.
Theorem complete: forall a b, same_labels (clean a) (clean b) = false -> ~ a == b.
Proof that rewriting a regex in strict star form preserves its set of labels
Lemma collect_ssf_remove: forall a acc, collect (remove a) acc [=] collect a acc.
Lemma collect_ssf: forall a acc, collect (ssf a) acc [=] collect a acc.
Theorem same_labels_ssf: forall a b, same_labels a b = true -> same_labels (ssf a) (ssf b) = true.
End protect.