Nondeterminisic Finite Automata (NFAs)
We define NFAs, finite and infinite runs of NFAs and show basic properties for this runs. We conclude with the relations ===> and =!=>, show both decidable, and that for both we have constructive choice for the corresponding run.Structure NFA (Sigma:finType) := mknfa
{ state: finType;
transition : state -> Sigma -> state -> Prop;
transition_dec : forall p a q, dec(transition p a q);
initial_state : state -> Prop;
initial_state_dec : forall p, dec(initial_state p);
accepting_state: state -> Prop;
accepting_state_dec: forall p, dec(accepting_state p)
}.
Arguments mknfa [Sigma] [state] transition {transition_dec} initial_state {initial_state_dec} accepting_state {accepting_state_dec}.
Arguments transition [Sigma] [aut] _ _ _ : rename.
Arguments initial_state [Sigma] [aut] _ : rename.
Arguments accepting_state [Sigma] [aut] _ : rename.
Arguments transition_dec [Sigma] [aut] _ _ _ : rename.
Arguments initial_state_dec [Sigma] [aut] _ : rename.
Arguments accepting_state_dec [Sigma] [aut] _ : rename.
Instance transition_dec_public (Sigma:finType)(aut:NFA Sigma): forall p a q , dec (transition (aut:=aut) p a q).
Proof. apply transition_dec. Defined.
Instance initial_dec_public (Sigma:finType)(aut:NFA Sigma): forall p, dec (initial_state (aut:=aut) p).
Proof. apply initial_state_dec. Defined.
Instance accepting_dec_public (Sigma:finType)(aut:NFA Sigma): forall p, dec (accepting_state (aut:=aut) p).
Proof. apply accepting_state_dec. Defined.
NFA with one state allowing all transitions
Definition univ_aut {Sigma:finType} := mknfa (fun (p:finType_unit) (a:Sigma) (q:finType_unit) => True) (fun _ => True) (fun _ => True).
Section TransitionGraph.
Context {Sigma : finType}.
Context {aut: NFA Sigma}.
Definition Run := Seq (state aut).
Identity Coercion run_to_seq: Run >-> Seq.
Implicit Types (rho : Run ) (sigma: Seq Sigma) (x: Str Sigma) (r: NStr (state aut)) (q: state aut) (a b:Sigma).
Definition valid_run rho sigma:= forall n, transition (rho n) (sigma n) (rho (S n)).
Inductive valid_path : NStr (state aut) -> Str Sigma -> Prop :=
| valid_path_base q : valid_path (sing q) []
| valid_path_step q r a (x: Str Sigma) : transition q a (r 0) -> valid_path r x -> valid_path (ncons q r) (a::x).
Definition naligned (r: NStr (state aut)) (x:NStr Sigma) := delta r = delta x /\ forall n, n < delta r -> transition (r n) (x n) (r (S n)).
Definition nlst_step (r: NStr (state aut)) (x:NStr Sigma) q := transition (r (delta r)) (x (delta x)) q.
Lemma valid_path_nth {DSigma: Dummy Sigma}{DS:Dummy (state aut)} r x:
valid_path r x <-> (|x| = delta r /\ forall n, n < |x| -> transition (r n) (str_nth x n) (r (S n))).
Proof.
split.
- intros V. induction V; simpl; split; auto.
+ intros n L. now exfalso.
+ intros n L. destruct n; auto. apply IHV. omega.
- intros [L E]. revert x L E. induction r as [q | q r]; intros x L E.
+ destruct x as [| a x].
* apply valid_path_base.
* exfalso. simpl in L. omega.
+ destruct x as [|a x].
* simpl in L. now exfalso.
* apply valid_path_step.
-- apply (E 0). comega.
-- apply IHr.
++ simpl in *. omega.
++ intros n G. apply (E (S n)). comega.
Qed.
Lemma valid_path_length r x : valid_path r x -> delta r = | x|.
Proof.
intros V. induction V; cbn; auto.
Qed.
Global Instance dec_valid_path r x: dec(valid_path r x).
Proof.
(* Need to destruct x because valid_path_nth needs a Dummy value *)
destruct x as [| a x].
- destruct r as [q | q r].
+ left. apply valid_path_base.
+ right. intros V. inversion V.
- pose proof (valid_path_nth r (a::x)). symmetry in H.
apply (dec_trans _ H).
Qed.
Context {Sigma : finType}.
Context {aut: NFA Sigma}.
Definition Run := Seq (state aut).
Identity Coercion run_to_seq: Run >-> Seq.
Implicit Types (rho : Run ) (sigma: Seq Sigma) (x: Str Sigma) (r: NStr (state aut)) (q: state aut) (a b:Sigma).
Definition valid_run rho sigma:= forall n, transition (rho n) (sigma n) (rho (S n)).
Inductive valid_path : NStr (state aut) -> Str Sigma -> Prop :=
| valid_path_base q : valid_path (sing q) []
| valid_path_step q r a (x: Str Sigma) : transition q a (r 0) -> valid_path r x -> valid_path (ncons q r) (a::x).
Definition naligned (r: NStr (state aut)) (x:NStr Sigma) := delta r = delta x /\ forall n, n < delta r -> transition (r n) (x n) (r (S n)).
Definition nlst_step (r: NStr (state aut)) (x:NStr Sigma) q := transition (r (delta r)) (x (delta x)) q.
Lemma valid_path_nth {DSigma: Dummy Sigma}{DS:Dummy (state aut)} r x:
valid_path r x <-> (|x| = delta r /\ forall n, n < |x| -> transition (r n) (str_nth x n) (r (S n))).
Proof.
split.
- intros V. induction V; simpl; split; auto.
+ intros n L. now exfalso.
+ intros n L. destruct n; auto. apply IHV. omega.
- intros [L E]. revert x L E. induction r as [q | q r]; intros x L E.
+ destruct x as [| a x].
* apply valid_path_base.
* exfalso. simpl in L. omega.
+ destruct x as [|a x].
* simpl in L. now exfalso.
* apply valid_path_step.
-- apply (E 0). comega.
-- apply IHr.
++ simpl in *. omega.
++ intros n G. apply (E (S n)). comega.
Qed.
Lemma valid_path_length r x : valid_path r x -> delta r = | x|.
Proof.
intros V. induction V; cbn; auto.
Qed.
Global Instance dec_valid_path r x: dec(valid_path r x).
Proof.
(* Need to destruct x because valid_path_nth needs a Dummy value *)
destruct x as [| a x].
- destruct r as [q | q r].
+ left. apply valid_path_base.
+ right. intros V. inversion V.
- pose proof (valid_path_nth r (a::x)). symmetry in H.
apply (dec_trans _ H).
Qed.
Extensionality facts
Lemma valid_run_extensional rho rho' sigma sigma': valid_run rho sigma -> rho == rho' -> sigma == sigma' -> valid_run rho' sigma'.
Proof.
intros V R W n. now rewrite <- W, <-R.
Qed.
Global Instance valid_run_proper : Proper (@seq_equiv _ (state aut) ==> @seq_equiv _ Sigma ==> iff) valid_run.
Proof.
intros rho rho' EqR sigma sigma' EqW. split; intros V; now eapply valid_run_extensional.
Qed.
Manipulations of valid paths and runs
Lemma valid_run_tl rho sigma: valid_run rho sigma -> valid_run (tl rho) (tl sigma ).
Proof.
intros V m. rewrite <-!nth_step_tl. apply V.
Qed.
Lemma valid_run_drop rho sigma n: valid_run rho sigma -> valid_run (drop rho n) (drop sigma n).
Proof.
intros V m. rewrite !drop_nth'. simpl. apply V.
Qed.
Lemma valid_run_cons rho sigma p a : transition p a (rho 0) -> valid_run rho sigma -> valid_run (p ::: rho)( a::: sigma).
Proof.
intros T V [|n].
- now rewrite nth_step, !nth_first.
- now rewrite !nth_step.
Qed.
Lemma valid_run_is_path_everywhere rho sigma: valid_run rho sigma -> forall n m, valid_path (closed_substr rho n m) (substr sigma n m).
Proof.
intros V n m. apply valid_path_nth. split.
- now rewrite substr_length, closed_substr_delta.
- intros k L. rewrite substr_length in L.
rewrite 2closed_substr_nth, substr_nth by omega. simpl. apply V.
Qed.
Lemma flatten_valid (rho: Seq (NStr (state aut))) (tau: Seq (NStr Sigma)):
(forall n, naligned (rho n) (tau n) /\
nlst_step (rho n) (tau n) (rho (S n) 0) )
-> valid_run (flatten rho) (flatten tau).
Proof.
intros H n. revert rho tau H. induction n; intros rho tau H.
- rewrite (flatten_step rho), (flatten_step tau).
specialize ( H 0). rewrite nth_step_tl,!nth_first_hd in H.
destruct hd as [q | q r]; destruct hd as [a | a x].
+ rewrite nth_step, !nth_first. simpl in H.
rewrite flatten_correct, prepend_nstr_nth_first by omega. now apply H.
+ exfalso. destruct H as [[H _] _]. now simpl in H.
+ exfalso. destruct H as [[H _] _]. now simpl in H.
+ rewrite !nth_first, nth_step.
destruct H as [[_ H] _]. specialize (H 0). simpl in H.
rewrite flatten_correct, hd_correct.
rewrite prepend_nstr_nth_first by omega. apply H. omega.
- rewrite (flatten_step rho), (flatten_step tau).
pose proof (H 0) as H0. destruct H0 as [[H01 H02] H03].
rewrite nth_step_tl in H03. rewrite <-!nth_first_hd.
destruct (rho 0) as [q | q r]; destruct (tau 0) as [a | a x]; simpl; rewrite !nth_step; simpl in H03, H01; try (now exfalso).
+ apply IHn. intros m. repeat split; apply (H (S m)).
+ apply IHn. intros [|m].
* rewrite nth_step, !nth_first. repeat split; simpl.
-- omega.
-- intros k L. apply (H02 (S k)). comega.
-- apply H03.
* rewrite !nth_step. repeat split; apply (H (S m)).
Qed.
End TransitionGraph.
Arguments Run [Sigma] _ .
Section TransformsRelations.
Context {Sigma:finType}.
Variable (aut:NFA Sigma).
Implicit Types (x y z: NStr Sigma)(p q : state aut).
Context {Sigma:finType}.
Variable (aut:NFA Sigma).
Implicit Types (x y z: NStr Sigma)(p q : state aut).
We use an inductive definition of the follwing predicates instead of
quantifying over a finite run.
Inductive transforms : state aut -> state aut -> NStr Sigma -> Prop :=
| trans_base p q a: transition p a q -> transforms p q (sing a)
| trans_step p p' q a x : transition p a p' -> transforms p' q x -> transforms p q (ncons a x) .
Inductive transforms_accepting : state aut -> state aut -> NStr Sigma -> Prop :=
| trans_accepting_base p q x: accepting_state p -> transforms p q x -> transforms_accepting p q x
| trans_accepting_step p p' q a x: transition p a p' -> transforms_accepting p' q x -> transforms_accepting p q (ncons a x).
Notation " p '===>' q 'on' x" := (transforms p q x) (at level 10).
Notation " p '=!=>' q 'on' x" := (transforms_accepting p q x) (at level 10).
| trans_base p q a: transition p a q -> transforms p q (sing a)
| trans_step p p' q a x : transition p a p' -> transforms p' q x -> transforms p q (ncons a x) .
Inductive transforms_accepting : state aut -> state aut -> NStr Sigma -> Prop :=
| trans_accepting_base p q x: accepting_state p -> transforms p q x -> transforms_accepting p q x
| trans_accepting_step p p' q a x: transition p a p' -> transforms_accepting p' q x -> transforms_accepting p q (ncons a x).
Notation " p '===>' q 'on' x" := (transforms p q x) (at level 10).
Notation " p '=!=>' q 'on' x" := (transforms_accepting p q x) (at level 10).
Facts about ===> and =!=> for concatenation
Lemma transforms_accepting_implies_transform x p q: p =!=> q on x -> p ===> q on x.
Proof.
intros TF. induction TF as [p q x _ T| p p' q a x T TF]; auto.
now apply (trans_step T).
Qed.
Lemma transforms_inv p q a x : p ===> q on (ncons a x) -> exists p', transition p a p' /\ p' ===> q on x.
Proof.
intros H. inversion H. subst p q a x.
now exists p'.
Qed.
Lemma transforms_accepting_inv p q a x : p =!=> q on (ncons a x) -> exists p', transition p a p' /\ (accepting_state p /\ p' ===> q on x \/ p' =!=> q on x).
Proof.
intros H. inversion H.
- subst p q x0. apply transforms_inv in H1. destruct H1 as [p [T1 T2]].
exists p. split; auto.
- subst p q a x. exists p'. split; auto.
Qed.
Lemma split_transforms x y p q: p ===> q on (nstr_concat' x y) -> exists p', p ===> p' on x /\ p' ===> q on y.
Proof.
revert p. induction x; intros p T.
- simpl in T. apply transforms_inv in T. destruct T as [p' [T Ts]].
exists p'. split; auto. now apply trans_base.
- simpl in T. apply transforms_inv in T. destruct T as [p' [T1 T2]].
destruct (IHx p' T2) as [p'' [T3 T]]. exists p''. split.
+ now apply (trans_step T1).
+ assumption.
Qed.
Lemma combine_transforms x y p p' q : p ===> p' on x -> p' ===> q on y -> p ===> q on (nstr_concat' x y).
Proof.
intros T1 T2.
induction T1 as [p a q' T|p p' q' a x T]; simpl.
- now apply (trans_step T).
- apply (trans_step T). auto.
Qed.
Lemma transforms_concat x y p q : p ===> q on (nstr_concat' x y) <-> exists p', p ===> p' on x /\ p' ===> q on y.
Proof.
split. apply split_transforms. intros [p' H]. now apply combine_transforms with (p':=p').
Qed.
Lemma split_transforms_accepting x y p q: p =!=> q on (nstr_concat' x y) -> exists p',
(p=!=> p' on x /\ p' ===> q on y) \/ (p ===> p' on x /\ p' =!=> q on y).
Proof.
revert p. induction x; intros p TF.
- simpl in TF. apply transforms_accepting_inv in TF. destruct TF as [p' [T [[F TF]|TF]]];
exists p'.
+ left. split; auto using trans_base, trans_accepting_base.
+ right. split; auto using trans_base.
- simpl in TF. apply transforms_accepting_inv in TF.
destruct TF as [p' [T1 [[F T2]|T2]]].
+ apply split_transforms in T2. destruct T2 as [p'' [T3 T4]].
exists p''. left. split; auto.
apply trans_accepting_base; auto. now apply (trans_step T1).
+ destruct (IHx p' T2) as [p'' [[T3 T4]|[T3 T4]]].
* exists p''. left. split; auto. now apply (trans_accepting_step T1).
* exists p''. right. split; auto. now apply (trans_step T1).
Qed.
Lemma combine_transforms_accepting_left x y p p' q : p =!=> p' on x -> p' ===> q on y -> p =!=> q on (nstr_concat' x y).
Proof.
intros TF T. induction TF as [p q' x F T1| p p' q' a x T1 TF].
- apply trans_accepting_base; auto.
eapply combine_transforms. now apply T1. apply T.
- simpl. apply (trans_accepting_step T1). now apply IHTF.
Qed.
Lemma combine_transforms_accepting_right x y p p' q : p ===> p' on x -> p' =!=> q on y -> p =!=> q on (nstr_concat' x y).
Proof.
intros T TF. induction T as [p q' a T | p p' q' a x T1 T2]; auto.
- simpl. now apply (trans_accepting_step T).
- simpl. apply (trans_accepting_step T1). auto.
Qed.
Lemma transforms_accepting_concat x y p q: p =!=> q on (nstr_concat' x y) <-> exists p',
(p=!=> p' on x /\ p' ===> q on y) \/ (p ===> p' on x /\ p' =!=> q on y).
Proof.
split. apply split_transforms_accepting.
intros [s [H|H]]. now apply combine_transforms_accepting_left with (p':=s).
now apply combine_transforms_accepting_right with (p':=s).
Qed.
Equivalent formulations to the relations. Sometimes the other ones are more useful.
Lemma transforms_accepting_iff x p q : p =!=>q on x <-> ((accepting_state p /\ p ===>q on x) \/ exists y z q', accepting_state q' /\ x = nstr_concat' y z /\ p ===> q' on y /\ q' ===> q on z).
Proof.
split.
- intros T. induction T.
+ now left.
+ destruct IHT as [[F Tr]| [y [z [q' [H1 [H2 [H3 H4]]]]]]].
* right. exists (sing a), x, p'. repeat split; auto.
now apply trans_base.
* right. exists (ncons a y), z, q'. repeat split; auto.
-- now rewrite H2.
-- now apply trans_step with (p' := p').
- intros [[F T]| [y [z [q' [H1 [H2 [H3 H4]]]]]]].
+ now apply trans_accepting_base.
+ subst x. revert p H3. induction y; intros p H3.
* cbn. apply trans_accepting_step with (p':=q').
-- now inversion H3.
-- now apply trans_accepting_base.
* cbn. apply transforms_inv in H3. destruct H3 as [p' [T H3]].
apply trans_accepting_step with (p' := p'); auto.
Qed.
Lemma transforms_equiv p q x: p ===> q on x <-> (exists r, naligned r x /\ r 0 = p /\ nlst_step r x q).
Proof.
split.
- intros T. induction T as [p q' a T | p p' q' a x T1 T2].
+ exists (sing p). repeat split; auto.
simpl. intros n F. now exfalso.
+ destruct IHT2 as [r [[L Ts] [B E]]].
exists (ncons p r). repeat split; auto.
* simpl. now rewrite L.
* intros [|n]; simpl; intros L'; auto.
now rewrite B.
- intros [r [[L Ts] [B E]]]. revert r p B L E Ts. induction x; intros r p B L E Ts.
+ apply trans_base. rewrite <-B.
destruct r.
* apply E.
* simpl in L. now exfalso.
+ destruct r.
* simpl in L. now exfalso.
* simpl in B. subst p.
apply trans_step with (p' := r 0).
-- apply (Ts 0). comega.
-- apply IHx with (r:=r); simpl; auto.
intros n L'. apply (Ts (S n)). comega.
Qed.
Lemma transforms_iff_valid_path p q x: p ===> q on x <-> (exists r, valid_path r x /\ r 0 = p /\ nstr_last r = q).
Proof.
split.
- intros T. induction T as [p q' a T | p p' q' a x T1 T2].
+ exists (ncons p (sing q')). repeat split; auto.
apply valid_path_step; auto. apply valid_path_base.
+ destruct IHT2 as [r [V [B E]]].
exists (ncons p r). repeat split; auto.
apply valid_path_step; auto. now rewrite B.
- intros [r [V [B E]]]. revert r p V B E . induction x; intros r p V B E.
+ apply trans_base. rewrite <-B.
destruct r.
* exfalso. inversion V.
* cbn in *. inversion V. inversion H4. now subst.
+ destruct r.
* cbn in *. exfalso. now inversion V.
* cbn in *. inversion V. subst. apply trans_step with (p':= r 0); auto.
now apply IHx with (r0 := r).
Qed.
Lemma transforms_accepting_equiv p q x: p =!=> q on x <-> (exists r, naligned r x /\ r 0 = p /\ nlst_step r x q /\ once (@accepting_state _ _ ) r).
Proof.
split.
- intros T. induction T as [p q x T |p p' q a x T1 T2].
+ apply transforms_equiv in H. destruct H as [r [[L Ts] [B E]]].
exists r. repeat split; simpl; auto. exists 0. repeat split; auto. now rewrite B.
+ destruct IHT2 as [r [[L Ts] [B [E F]]]]. exists (ncons p r). repeat split; auto.
* comega.
* intros [|n]; simpl; intros L'; auto. now rewrite B.
* destruct F as [m [P Q]]. exists (S m). split; simpl; auto.
- intros [r [[L Ts] [B [E F]]]]. revert r p E F L B Ts. induction x; intros r p E F L B Ts.
+ destruct r.
* apply trans_accepting_base.
-- destruct F as [m [P Q]]. simpl in Q, B. now subst p.
-- apply trans_base. simpl in *. subst p. apply E.
* simpl in L. now exfalso.
+ destruct r.
* simpl in L. now exfalso.
* destruct F as [m [P Q]]. rewrite <-B. destruct m.
-- apply trans_accepting_base; auto.
apply transforms_equiv. exists (ncons a0 r); repeat split; auto.
-- apply trans_accepting_step with (p' := r 0).
++ apply (Ts 0). comega.
++ apply IHx with (r:=r); auto.
** exists m. simpl in P. split; auto.
** intros n L'. apply (Ts (S n)). comega.
Qed.
Decidability and Constructive Choice
We first show that the relations are decidable for a given strings
and later that we can decide whether there is one string making the relations
hold for two given states.
Global Instance dec_transforms : forall p q x, dec (p ===> q on x).
Proof.
intros p q x.
pose proof (transforms_equiv p q x) as H. symmetry in H. unfold naligned in H.
apply (@dec_trans _ _ _ H).
Qed.
Global Instance dec_transforms_accepting : forall p q x, dec(p =!=> q on x).
Proof.
intros p q x.
pose proof (transforms_accepting_equiv p q x) as H. symmetry in H.
apply (@dec_trans _ _ _ H).
Qed.
Lemma transforms_run_cc p q (x: NStr Sigma) : p ===> q on x -> {r : NStr (state aut)| naligned r x /\ r 0 = p /\ nlst_step r x q}.
Proof.
unfold naligned. intros H % transforms_equiv. apply string_fixed_length_cc'; auto.
Defined.
Lemma transforms_accepting_run_cc p q (x:NStr Sigma) : p =!=> q on x -> {r | naligned r x /\ r 0 = p /\ nlst_step r x q /\ (once (@accepting_state _ _) r)}.
Proof.
unfold naligned. intros H % transforms_accepting_equiv. apply string_fixed_length_cc'; auto.
Qed.
Lemma valid_run_transforms_everywhere rho sigma: valid_run rho sigma -> forall n m, n <= m -> (rho n) ===> (rho (S m)) on (closed_substr sigma n m).
Proof.
intros V n m L. apply transforms_iff_valid_path.
exists (closed_substr rho n (S m)). repeat split.
- rewrite <-nonempty_substr_is_closed by assumption.
now apply valid_run_is_path_everywhere.
- rewrite closed_substr_nth; auto.
- rewrite nstr_last_delta, closed_substr_nth; rewrite closed_substr_delta; auto.
Qed.
It suffices to decide exists x, p ===> q on x for all x to decide exists x, p =!=> q on x
due to lemma transforms_accepting_iff.
Deciding ===> is just deciding reachability in graphs which is possible since the
length of a path connecting to states is bounded by the number of states.
Section Decidability.
Implicit Types (t: (NStr (state aut) * NStr Sigma)).
Implicit Types (r: NStr (state aut)).
Lemma valid_path_remove (x: Str Sigma) (r1 : Str (state aut)) r2 : valid_path (nstr_concat r1 r2) x -> exists (x: Str Sigma), valid_path r2 x.
Proof.
intros V. revert x V. induction r1; intros x V.
- now exists x.
- inversion V; subst.
now apply IHr1 with (x:=x0).
Qed.
Lemma remove_loop (x: Str Sigma) r (H: valid_path r x) : exists (x': Str Sigma) r', valid_path r' x' /\ r' 0 = r 0 /\ nstr_last r' = nstr_last r /\ (dupfree r' /\ r = r' \/ delta r' < delta r).
Proof.
induction H as [q | q r a].
- exists [], (sing q). repeat split; auto.
* constructor.
* left. cbn. split; auto. constructor; auto. constructor.
- destruct IHvalid_path as [x' [r' [Q1 [Q2 [Q3 [[Q4 Q5]|Q4]]]]]].
+ subst r'. decide (q el r) as [D'|D'].
* destruct (in_nstr D') as [l1 [l2 [E F]]]. rewrite E in Q1.
destruct (valid_path_remove Q1) as [y V].
exists y, l2. repeat split; auto.
-- cbn. rewrite E. now rewrite nstr_concat_last.
-- right. rewrite E. cbn. rewrite nstr_concat_delta. omega.
* exists (a :: x'), (ncons q r). repeat split; auto.
-- apply valid_path_step; auto.
-- left. cbn. split; auto. constructor; auto.
+ exists (a :: x'), (ncons q r'). repeat split; auto.
* apply valid_path_step; auto. now rewrite Q2.
* right. cbn. omega.
Qed.
Lemma remove_loops (x: Str Sigma) r (H: valid_path r x) : exists (x': Str Sigma) r', valid_path r' x' /\ r' 0 = r 0 /\ nstr_last r' = nstr_last r /\ dupfree r'.
Proof.
revert x H.
apply nstr_size_induction with (y := r). clear r. intros r IHr x H.
destruct (remove_loop H) as [x' [r' [Q1 [Q2 [Q3 [Q4|Q4]]]]]].
- now exists x', r'.
- destruct (IHr r' Q4 x' Q1) as [x''[ r'' [H1 [H2 [H3 H4]]]]].
exists x'', r''. repeat split; auto; congruence.
Qed.
Lemma remove_loops_nstr (x: NStr Sigma) r (H: valid_path r x) : exists (x': NStr Sigma) r', valid_path r' x' /\ r' 0 = r 0 /\ nstr_last r' = nstr_last r /\ delta r' <= Cardinality (state aut).
Proof.
assert (| x| > 0) as L. { rewrite <-nstr_to_str_length. omega. }
destruct H.
- exfalso. now cbn in L.
- apply remove_loops in H0. destruct H0 as [x' [r' [V [H1 [H2 H3]]]]].
destruct x'.
+ exists (sing a), (ncons q (sing (r 0))). repeat split; auto.
* apply valid_path_step; auto. apply valid_path_base.
* cbn. inversion V. subst. cbn in *. congruence.
* cbn. enough (0 < Cardinality (state aut)) by omega. now apply Card_positiv.
+ exists ( (!(a :: e :: x'))), (ncons q r'). repeat split; auto.
* rewrite <-str_to_nstr_idem'. apply valid_path_step; auto. now rewrite H1.
* cbn. rewrite nstr_to_str_length. now apply dupfree_length.
Qed.
Lemma dec_transforms_informative_bound p q: {x | p ===> q on x /\ delta x <= Cardinality (state aut)} + {forall x, ~ p ===> q on x}.
Proof.
decide (exists r, delta r <= Cardinality (state aut) /\ exists (x: NStr Sigma), delta x <= Cardinality (state aut) /\ valid_path r x /\ r 0 = p /\ nstr_last r = q)
as [[r [Lr [x [Lx [H1 H2]]]%string_bounded_length_cc ]] % string_bounded_length_cc|D]; auto.
- left. exists x. repeat split; auto.
apply transforms_iff_valid_path. now exists r.
- right. intros x T. apply D.
apply transforms_iff_valid_path in T. destruct T as [r [V [B E]]].
apply remove_loops_nstr in V. destruct V as [x' [r' [V [H1 [H2 H3]]]]].
exists r'. split; auto.
exists x'. repeat split; auto.
+ apply valid_path_length in V. rewrite <-nstr_to_str_length in V. omega.
+ congruence.
+ congruence.
Qed.
Lemma dec_ex_transforms_informative p q: {x | p ===> q on x} + {forall x, ~ p ===> q on x}.
Proof.
destruct (dec_transforms_informative_bound p q) as [[x [T _]] | D].
- left. now exists x.
- now right.
Qed.
Lemma ex_transforms_cc p q :( exists x, p ===> q on x) -> {x| p ===> q on x}.
Proof.
intros H. destruct (dec_ex_transforms_informative p q) as [Q|Q]; auto.
exfalso. firstorder.
Qed.
Global Instance dec_ex_transforms p q: dec(exists x, p ===> q on x).
Proof.
destruct (dec_ex_transforms_informative p q) as [[x T]|D].
- left. now exists x.
- right. intros [x T]. now apply (D x).
Qed.
Lemma dec_ex_transforms_accepting_informative p q: {x | p =!=> q on x } + {forall x, ~ p =!=> q on x}.
Proof.
decide (accepting_state p /\ exists x, p ===> q on x) as [[D1 [x T]%ex_transforms_cc]|D].
- left. exists x. now apply trans_accepting_base.
- decide (exists y, delta y <= Cardinality (state aut) /\ exists z, delta z <= Cardinality (state aut) /\ exists q', accepting_state q' /\ p ===> q' on y /\ q' ===> q on z)
as [[x [Lx [y [Ly [q' [H1 [H2 H3]]]%finType_cc]]%string_bounded_length_cc]] % string_bounded_length_cc|D']; auto.
+ left. exists (nstr_concat' x y). apply transforms_accepting_iff. right. now exists x, y, q'.
+ right. intros x [T|T] % transforms_accepting_iff.
* apply D. firstorder.
* destruct T as [y [z [q' [H1 [H2 [H3 H4]]]]]].
destruct (dec_transforms_informative_bound p q') as [[y' [Q1 Q2]] |D''].
-- destruct (dec_transforms_informative_bound q' q) as [[z' [Q3 Q4]] |D''']; firstorder.
-- firstorder.
Qed.
Lemma ex_transforms_accepting_cc p q :( exists x, p =!=> q on x) -> {x| p =!=> q on x}.
Proof.
intros H. destruct (dec_ex_transforms_accepting_informative p q) as [Q|Q]; auto.
exfalso. firstorder.
Qed.
Global Instance dec_ex_transforms_accepting p q: dec(exists x, p =!=> q on x).
Proof.
destruct (dec_ex_transforms_accepting_informative p q) as [[x T]|D].
- left. now exists x.
- right. intros [x T]. now apply (D x).
Qed.
End Decidability.
End TransformsRelations.
Notation " p '===>' q 'on' x" := (transforms p q x) (at level 10).
Notation " p '=!=>' q 'on' x" := (transforms_accepting p q x) (at level 10).
Implicit Types (t: (NStr (state aut) * NStr Sigma)).
Implicit Types (r: NStr (state aut)).
Lemma valid_path_remove (x: Str Sigma) (r1 : Str (state aut)) r2 : valid_path (nstr_concat r1 r2) x -> exists (x: Str Sigma), valid_path r2 x.
Proof.
intros V. revert x V. induction r1; intros x V.
- now exists x.
- inversion V; subst.
now apply IHr1 with (x:=x0).
Qed.
Lemma remove_loop (x: Str Sigma) r (H: valid_path r x) : exists (x': Str Sigma) r', valid_path r' x' /\ r' 0 = r 0 /\ nstr_last r' = nstr_last r /\ (dupfree r' /\ r = r' \/ delta r' < delta r).
Proof.
induction H as [q | q r a].
- exists [], (sing q). repeat split; auto.
* constructor.
* left. cbn. split; auto. constructor; auto. constructor.
- destruct IHvalid_path as [x' [r' [Q1 [Q2 [Q3 [[Q4 Q5]|Q4]]]]]].
+ subst r'. decide (q el r) as [D'|D'].
* destruct (in_nstr D') as [l1 [l2 [E F]]]. rewrite E in Q1.
destruct (valid_path_remove Q1) as [y V].
exists y, l2. repeat split; auto.
-- cbn. rewrite E. now rewrite nstr_concat_last.
-- right. rewrite E. cbn. rewrite nstr_concat_delta. omega.
* exists (a :: x'), (ncons q r). repeat split; auto.
-- apply valid_path_step; auto.
-- left. cbn. split; auto. constructor; auto.
+ exists (a :: x'), (ncons q r'). repeat split; auto.
* apply valid_path_step; auto. now rewrite Q2.
* right. cbn. omega.
Qed.
Lemma remove_loops (x: Str Sigma) r (H: valid_path r x) : exists (x': Str Sigma) r', valid_path r' x' /\ r' 0 = r 0 /\ nstr_last r' = nstr_last r /\ dupfree r'.
Proof.
revert x H.
apply nstr_size_induction with (y := r). clear r. intros r IHr x H.
destruct (remove_loop H) as [x' [r' [Q1 [Q2 [Q3 [Q4|Q4]]]]]].
- now exists x', r'.
- destruct (IHr r' Q4 x' Q1) as [x''[ r'' [H1 [H2 [H3 H4]]]]].
exists x'', r''. repeat split; auto; congruence.
Qed.
Lemma remove_loops_nstr (x: NStr Sigma) r (H: valid_path r x) : exists (x': NStr Sigma) r', valid_path r' x' /\ r' 0 = r 0 /\ nstr_last r' = nstr_last r /\ delta r' <= Cardinality (state aut).
Proof.
assert (| x| > 0) as L. { rewrite <-nstr_to_str_length. omega. }
destruct H.
- exfalso. now cbn in L.
- apply remove_loops in H0. destruct H0 as [x' [r' [V [H1 [H2 H3]]]]].
destruct x'.
+ exists (sing a), (ncons q (sing (r 0))). repeat split; auto.
* apply valid_path_step; auto. apply valid_path_base.
* cbn. inversion V. subst. cbn in *. congruence.
* cbn. enough (0 < Cardinality (state aut)) by omega. now apply Card_positiv.
+ exists ( (!(a :: e :: x'))), (ncons q r'). repeat split; auto.
* rewrite <-str_to_nstr_idem'. apply valid_path_step; auto. now rewrite H1.
* cbn. rewrite nstr_to_str_length. now apply dupfree_length.
Qed.
Lemma dec_transforms_informative_bound p q: {x | p ===> q on x /\ delta x <= Cardinality (state aut)} + {forall x, ~ p ===> q on x}.
Proof.
decide (exists r, delta r <= Cardinality (state aut) /\ exists (x: NStr Sigma), delta x <= Cardinality (state aut) /\ valid_path r x /\ r 0 = p /\ nstr_last r = q)
as [[r [Lr [x [Lx [H1 H2]]]%string_bounded_length_cc ]] % string_bounded_length_cc|D]; auto.
- left. exists x. repeat split; auto.
apply transforms_iff_valid_path. now exists r.
- right. intros x T. apply D.
apply transforms_iff_valid_path in T. destruct T as [r [V [B E]]].
apply remove_loops_nstr in V. destruct V as [x' [r' [V [H1 [H2 H3]]]]].
exists r'. split; auto.
exists x'. repeat split; auto.
+ apply valid_path_length in V. rewrite <-nstr_to_str_length in V. omega.
+ congruence.
+ congruence.
Qed.
Lemma dec_ex_transforms_informative p q: {x | p ===> q on x} + {forall x, ~ p ===> q on x}.
Proof.
destruct (dec_transforms_informative_bound p q) as [[x [T _]] | D].
- left. now exists x.
- now right.
Qed.
Lemma ex_transforms_cc p q :( exists x, p ===> q on x) -> {x| p ===> q on x}.
Proof.
intros H. destruct (dec_ex_transforms_informative p q) as [Q|Q]; auto.
exfalso. firstorder.
Qed.
Global Instance dec_ex_transforms p q: dec(exists x, p ===> q on x).
Proof.
destruct (dec_ex_transforms_informative p q) as [[x T]|D].
- left. now exists x.
- right. intros [x T]. now apply (D x).
Qed.
Lemma dec_ex_transforms_accepting_informative p q: {x | p =!=> q on x } + {forall x, ~ p =!=> q on x}.
Proof.
decide (accepting_state p /\ exists x, p ===> q on x) as [[D1 [x T]%ex_transforms_cc]|D].
- left. exists x. now apply trans_accepting_base.
- decide (exists y, delta y <= Cardinality (state aut) /\ exists z, delta z <= Cardinality (state aut) /\ exists q', accepting_state q' /\ p ===> q' on y /\ q' ===> q on z)
as [[x [Lx [y [Ly [q' [H1 [H2 H3]]]%finType_cc]]%string_bounded_length_cc]] % string_bounded_length_cc|D']; auto.
+ left. exists (nstr_concat' x y). apply transforms_accepting_iff. right. now exists x, y, q'.
+ right. intros x [T|T] % transforms_accepting_iff.
* apply D. firstorder.
* destruct T as [y [z [q' [H1 [H2 [H3 H4]]]]]].
destruct (dec_transforms_informative_bound p q') as [[y' [Q1 Q2]] |D''].
-- destruct (dec_transforms_informative_bound q' q) as [[z' [Q3 Q4]] |D''']; firstorder.
-- firstorder.
Qed.
Lemma ex_transforms_accepting_cc p q :( exists x, p =!=> q on x) -> {x| p =!=> q on x}.
Proof.
intros H. destruct (dec_ex_transforms_accepting_informative p q) as [Q|Q]; auto.
exfalso. firstorder.
Qed.
Global Instance dec_ex_transforms_accepting p q: dec(exists x, p =!=> q on x).
Proof.
destruct (dec_ex_transforms_accepting_informative p q) as [[x T]|D].
- left. now exists x.
- right. intros [x T]. now apply (D x).
Qed.
End Decidability.
End TransformsRelations.
Notation " p '===>' q 'on' x" := (transforms p q x) (at level 10).
Notation " p '=!=>' q 'on' x" := (transforms_accepting p q x) (at level 10).