Set Implicit Arguments.
Require Import Coq.Init.Nat.
Require Import Coq.Relations.Relation_Definitions.
Require Import BasicDefs.
Require Import FinType.
Require Import Seqs.
Require Import NFAs.
Open Scope string_scope.
Require Import Coq.Init.Nat.
Require Import Coq.Relations.Relation_Definitions.
Require Import BasicDefs.
Require Import FinType.
Require Import Seqs.
Require Import NFAs.
Open Scope string_scope.
Regular Languages
String Languages accepted by NFAs ands selected facts about regular languages needed for formalization of Büchi languagesSection NFAStringLanguage.
Context{X: finType}.
Context (aut: NFA X).
Implicit Types (r: Run aut)(v: String X).
Definition svalid r v:= valid_path (aut:=aut) r v.
Definition sinitial r := initial_state (r 0).
Definition sfinal r v := final_state (r (S(|v|))).
Definition saccepting r v := svalid r v /\ sinitial r /\ sfinal r v.
Definition slanguage := fun v => exists r, saccepting r v.
Lemma slanguage_extensional:StringLang_Extensional (slanguage).
Proof.
intros w w' [ r [V [I F]]] E.
exists r. repeat split.
- unfold svalid. now rewrite <-E.
- auto.
- unfold sfinal. destruct E as [E ]. now rewrite <-E.
Qed.
End NFAStringLanguage.
Notation "'L_S'" := slanguage.
Hint Unfold svalid.
Hint Unfold sinitial.
Hint Unfold sfinal.
Instance dec_svalid A (aut:NFA A) r w : dec (svalid (aut:=aut) r w).
Proof. auto. Qed.
Instance dec_sinitial A (aut:NFA A) r : dec (sinitial (aut:=aut) r ).
Proof. auto. Qed.
Instance dec_sfinal A (aut:NFA A) r w: dec (sfinal (aut:=aut) r w).
Proof. auto. Qed.
Instance dec_saccepting A (aut:NFA A) r w: dec (saccepting (aut:=aut) r w).
Proof. auto. Qed.
Lemma nfa_string_lang_cc X (aut:NFA X) w: (L_S aut w) -> { r | saccepting (aut := aut) r w }.
Proof.
intros L.
enough (exists (r : ConstLengthString (S (|w|))), saccepting (aut:=aut) (to_seq r) w) as [r A] % finType_cc.
- now exists (to_seq r).
- auto.
- destruct L as [r A]. exists (to_bounded r). repeat split.
+ unfold svalid. intros n L. repeat rewrite bounded_unchanged by omega. now apply A.
+ unfold sinitial. rewrite bounded_unchanged by omega. apply A.
+ unfold sfinal. rewrite bounded_unchanged by omega. apply A.
Qed.
Section NormalizeNFA.
Context {A:finType}.
Variable (aut:NFA A).
Definition special_states := finType_bool.
Notation "'Initial'" := false.
Notation "'Final'" := true.
Definition norm_state := (state aut) (+) special_states.
Definition norm_initial_state (s:norm_state):= s = inr (Initial).
Definition norm_final_state (s:norm_state) := s = inr(Final).
Definition norm_transition (s:norm_state) (a:A) (s':norm_state) := match s, s' with
| inl s, inl s' => transition s a s'
| inr Initial, inl s' => exists s, initial_state s /\ transition s a s'
| inl s , inr Final => exists s', final_state s' /\ transition s a s'
| inr Initial, inr Final => exists (s s':state aut), initial_state s /\ final_state s' /\ transition s a s'
| _, _ => False
end.
Instance dec_norm_transition s a s' : dec (norm_transition s a s').
Proof. destruct s as [s | [|]]; destruct s' as [s' | [|]]; auto. Qed.
Definition normalize := mknfa norm_transition norm_initial_state norm_final_state.
Lemma first_norm_is_initial (r:Run normalize) : sinitial r -> (r 0) = inr Initial.
Proof. auto. Qed.
Lemma last_norm_is_final (r: Run normalize) w : sfinal r w -> (r (S(|w|))) = inr Final.
Proof. auto. Qed.
Lemma other_norm_is_aut_state (r: Run normalize) w : svalid r w -> forall n, 1 <= n <= |w| -> exists s, r n = inl s.
Proof.
intros V n L. destruct n.
- exfalso. omega.
- assert (norm_transition (r n) (w [n]) (r (S n))) as Vn. {apply V. omega. }
assert (norm_transition (r (S n)) (w [(S n)]) (r (S (S n)))) as VSn. {apply V. omega. }
destruct (r (S n)) as [s| [|]]; cbn in *.
+ now exists s.
+ now exfalso.
+ exfalso. destruct (r n) as [s' | [|]]; cbn in *; now exfalso.
Qed.
Lemma aut_accepts_normalize: L_S normalize <$= L_S aut.
Proof.
intros w [r [V [I F]]].
decide (|w| = 0) as [D|D].
- specialize (V 0). cbn in V. unfold norm_transition in V.
rewrite first_norm_is_initial in V by auto.
rewrite_eq (1 = S(|w|)) in V.
rewrite last_norm_is_final in V by auto.
destruct V as [s0 [s1 [sI [sF T]]]]. omega.
exists (fun n => match n with
| 0 => s0
| 1 => s1
| n => s0 end).
repeat split.
+ unfold svalid. intros n L. now rewrite_eq (n = 0).
+ auto.
+ unfold sfinal. now rewrite D.
- pose (V0 := (V 0)). rewrite first_norm_is_initial in V0 by auto.
cbn in V0. destruct (other_norm_is_aut_state V (n:=1)) as [s1 P1]. omega.
rewrite P1 in V0. destruct V0 as [s0 [sI tI]]. omega.
pose (Ve := (V (|w|))). rewrite last_norm_is_final in Ve by auto.
cbn in Ve. destruct (other_norm_is_aut_state V (n:= |w|)) as [se' Pe']. omega.
rewrite Pe' in Ve. cbn in Ve. destruct Ve as [se [eF eT]]. omega.
exists (fun n => match n with
| 0 => s0
| S n => if decision ( n = |w|)
then se
else match (r (S n)) with
| inl s => s
| inr _ => s0
end end).
repeat split.
+ intros n L. destruct n; trivial_decision.
* now rewrite P1.
* destruct decision as [D'|D'].
-- now rewrite D', Pe'.
-- destruct (other_norm_is_aut_state V (n:= S n)) as [sSn HSn]. omega.
destruct (other_norm_is_aut_state V (n:= S (S n))) as [sSSn HSSn]. omega.
rewrite HSn, HSSn.
specialize (V (S n)). rewrite HSn, HSSn in V. cbn in V.
apply V. omega.
+ auto.
+ unfold sfinal. now trivial_decision.
Qed.
Lemma normalize_accepts_aut: L_S aut <$= L_S normalize.
Proof.
intros w [r [V [I F]]].
exists (fun n => match n with
| 0 => inr Initial
| S n => if (decision (n = |w|))
then inr Final
else inl (r (S n)) end).
repeat split.
- intros n L. destruct n; trivial_decision.
+ destruct decision as [D|D]; cbn.
* exists (r 0), (r 1). repeat split; auto.
rewrite D. apply F.
* exists (r 0). repeat split; auto.
+ destruct decision as [D|D]; cbn; auto.
exists (r (S (|w|))). repeat split; auto.
rewrite D. now apply V.
- unfold sfinal. now trivial_decision.
Qed.
Definition sautomaton_normalized (aut: NFA A) (initialS finalS : state aut):=
(initial_state initialS /\ (forall s, initial_state s -> s = initialS) /\ (forall s a, ~ transition (aut:=aut) s a initialS)) /\
(final_state finalS /\ (forall s, final_state s -> s = finalS) /\ (forall a s, ~transition (aut:=aut) finalS a s)) /\
(finalS <> initialS).
Arguments sautomaton_normalized _ _ _ : clear implicits.
Lemma normalize_correct: L_S aut =$= L_S normalize.
Proof.
intros w; split. apply normalize_accepts_aut. apply aut_accepts_normalize.
Qed.
Definition normalize_inital : state normalize := inr Initial.
Definition normalize_final : state normalize := inr Final.
Lemma normalize_is_normalized: sautomaton_normalized normalize normalize_inital normalize_final.
Proof.
repeat split; auto.
- intros s a T. destruct s as [s |[|]]; now cbn in T.
- compute. congruence.
Qed.
End NormalizeNFA.
Context {A:finType}.
Variable (aut:NFA A).
Definition special_states := finType_bool.
Notation "'Initial'" := false.
Notation "'Final'" := true.
Definition norm_state := (state aut) (+) special_states.
Definition norm_initial_state (s:norm_state):= s = inr (Initial).
Definition norm_final_state (s:norm_state) := s = inr(Final).
Definition norm_transition (s:norm_state) (a:A) (s':norm_state) := match s, s' with
| inl s, inl s' => transition s a s'
| inr Initial, inl s' => exists s, initial_state s /\ transition s a s'
| inl s , inr Final => exists s', final_state s' /\ transition s a s'
| inr Initial, inr Final => exists (s s':state aut), initial_state s /\ final_state s' /\ transition s a s'
| _, _ => False
end.
Instance dec_norm_transition s a s' : dec (norm_transition s a s').
Proof. destruct s as [s | [|]]; destruct s' as [s' | [|]]; auto. Qed.
Definition normalize := mknfa norm_transition norm_initial_state norm_final_state.
Lemma first_norm_is_initial (r:Run normalize) : sinitial r -> (r 0) = inr Initial.
Proof. auto. Qed.
Lemma last_norm_is_final (r: Run normalize) w : sfinal r w -> (r (S(|w|))) = inr Final.
Proof. auto. Qed.
Lemma other_norm_is_aut_state (r: Run normalize) w : svalid r w -> forall n, 1 <= n <= |w| -> exists s, r n = inl s.
Proof.
intros V n L. destruct n.
- exfalso. omega.
- assert (norm_transition (r n) (w [n]) (r (S n))) as Vn. {apply V. omega. }
assert (norm_transition (r (S n)) (w [(S n)]) (r (S (S n)))) as VSn. {apply V. omega. }
destruct (r (S n)) as [s| [|]]; cbn in *.
+ now exists s.
+ now exfalso.
+ exfalso. destruct (r n) as [s' | [|]]; cbn in *; now exfalso.
Qed.
Lemma aut_accepts_normalize: L_S normalize <$= L_S aut.
Proof.
intros w [r [V [I F]]].
decide (|w| = 0) as [D|D].
- specialize (V 0). cbn in V. unfold norm_transition in V.
rewrite first_norm_is_initial in V by auto.
rewrite_eq (1 = S(|w|)) in V.
rewrite last_norm_is_final in V by auto.
destruct V as [s0 [s1 [sI [sF T]]]]. omega.
exists (fun n => match n with
| 0 => s0
| 1 => s1
| n => s0 end).
repeat split.
+ unfold svalid. intros n L. now rewrite_eq (n = 0).
+ auto.
+ unfold sfinal. now rewrite D.
- pose (V0 := (V 0)). rewrite first_norm_is_initial in V0 by auto.
cbn in V0. destruct (other_norm_is_aut_state V (n:=1)) as [s1 P1]. omega.
rewrite P1 in V0. destruct V0 as [s0 [sI tI]]. omega.
pose (Ve := (V (|w|))). rewrite last_norm_is_final in Ve by auto.
cbn in Ve. destruct (other_norm_is_aut_state V (n:= |w|)) as [se' Pe']. omega.
rewrite Pe' in Ve. cbn in Ve. destruct Ve as [se [eF eT]]. omega.
exists (fun n => match n with
| 0 => s0
| S n => if decision ( n = |w|)
then se
else match (r (S n)) with
| inl s => s
| inr _ => s0
end end).
repeat split.
+ intros n L. destruct n; trivial_decision.
* now rewrite P1.
* destruct decision as [D'|D'].
-- now rewrite D', Pe'.
-- destruct (other_norm_is_aut_state V (n:= S n)) as [sSn HSn]. omega.
destruct (other_norm_is_aut_state V (n:= S (S n))) as [sSSn HSSn]. omega.
rewrite HSn, HSSn.
specialize (V (S n)). rewrite HSn, HSSn in V. cbn in V.
apply V. omega.
+ auto.
+ unfold sfinal. now trivial_decision.
Qed.
Lemma normalize_accepts_aut: L_S aut <$= L_S normalize.
Proof.
intros w [r [V [I F]]].
exists (fun n => match n with
| 0 => inr Initial
| S n => if (decision (n = |w|))
then inr Final
else inl (r (S n)) end).
repeat split.
- intros n L. destruct n; trivial_decision.
+ destruct decision as [D|D]; cbn.
* exists (r 0), (r 1). repeat split; auto.
rewrite D. apply F.
* exists (r 0). repeat split; auto.
+ destruct decision as [D|D]; cbn; auto.
exists (r (S (|w|))). repeat split; auto.
rewrite D. now apply V.
- unfold sfinal. now trivial_decision.
Qed.
Definition sautomaton_normalized (aut: NFA A) (initialS finalS : state aut):=
(initial_state initialS /\ (forall s, initial_state s -> s = initialS) /\ (forall s a, ~ transition (aut:=aut) s a initialS)) /\
(final_state finalS /\ (forall s, final_state s -> s = finalS) /\ (forall a s, ~transition (aut:=aut) finalS a s)) /\
(finalS <> initialS).
Arguments sautomaton_normalized _ _ _ : clear implicits.
Lemma normalize_correct: L_S aut =$= L_S normalize.
Proof.
intros w; split. apply normalize_accepts_aut. apply aut_accepts_normalize.
Qed.
Definition normalize_inital : state normalize := inr Initial.
Definition normalize_final : state normalize := inr Final.
Lemma normalize_is_normalized: sautomaton_normalized normalize normalize_inital normalize_final.
Proof.
repeat split; auto.
- intros s a T. destruct s as [s |[|]]; now cbn in T.
- compute. congruence.
Qed.
End NormalizeNFA.
Closure Properties of Regular Languages
I borrow closure properties from finite type library. Therefore I need to convert my noninductive acceptance conditions to an inductive one. For the inductive ones, there are already proofs for closure properties. Note that it is not even visible that my strings cannot represent to empty strings (because it does not matter whether the empty string is in the accepted language of an inductive NFA or not).
Conversion from strings to lists
Fixpoint seqToList (w : Seq A) k := match k with
| 0 => cons (w 0) nil
| S k => cons (w 0) (seqToList (drop 1 w) k)
end.
Definition stringToList (w: String A) := seqToList w (|w|).
| 0 => cons (w 0) nil
| S k => cons (w 0) (seqToList (drop 1 w) k)
end.
Definition stringToList (w: String A) := seqToList w (|w|).
Language definitions for inductive NFAs and DFAs
Definition L_ind (B : Automata.nfa A) := fun w => Automata.n_accept B ( stringToList w).
Definition L_dind (B : Automata.dfa A) := fun w => Automata.accept B ( stringToList w).
Lemma ind_nfa_to_dfa_correct (B: Automata.nfa A) : L_ind B =$= L_dind (Automata.toDFA B).
Proof. intros w. apply Automata.toDFA_correct. Qed.
Lemma ind_dfa_to_nfa_correct (B: Automata.dfa A) : L_dind B =$= L_ind (Automata.toNFA B).
Proof. intros w. apply Automata.toNFA_correct. Qed.
Conversion from runs to inductive acceptance and vice versa
Lemma detlaQstar_decrease_step (w:Seq A) (l:nat)
(B: Automata.nfa A) (qFin: Automata.Q B) :
Automata.delta_Q_star Automata.q0 (stringToList (mkstring w (S l))) qFin <-> exists s,
Automata.delta_Q_star Automata.q0 (stringToList (mkstring w l)) s /\ Automata.delta_Q s (w (S l)) qFin.
Proof.
split.
- remember (Automata.q0) as s. clear Heqs.
revert s. revert w. induction l; intros w s QS; cbn in *.
+ destruct QS as [q [T [q' [T' E]]]].
exists q. split.
* now exists q.
* now rewrite E.
+ destruct QS as [q [T QS]].
specialize (IHl (drop 1 w) q QS).
destruct IHl as [q' P].
exists q'. split.
* exists q. split; auto. apply P.
* apply P.
- remember (Automata.q0) as s. clear Heqs.
revert s. revert w. induction l; intros w s QS; cbn in *.
+ destruct QS as [q [[q' [P1 P2]] Q]].
exists q. split.
* now rewrite P2.
* exists qFin. auto.
+ destruct QS as [q [[q' [T' QS]] T]].
exists q'. split; auto.
specialize (IHl (drop 1 w) q'). apply IHl.
exists q. auto.
Qed.
Lemma detlaQstar_convert(w:String A)
(B: Automata.nfa A) (qFin: Automata.Q B) :
Automata.delta_Q_star Automata.q0 (stringToList w) qFin -> exists (r: Seq (Automata.Q B)),
r 0 = Automata.q0 /\ r (S (|w|)) = qFin /\ forall n, n <= |w| -> Automata.delta_Q (r n) (w[n]) (r (S n)).
Proof.
revert qFin. destruct w as [w l]. induction l ; intros qFin QS.
- exists (fun n => match n with |0 => Automata.q0 | _ => qFin end). repeat split; cbn; auto.
intros n L. rewrite_eq (n = 0). destruct QS as [q' [R F]].
now rewrite F.
- apply detlaQstar_decrease_step in QS.
destruct QS as [s [QS Q]].
specialize (IHl s QS).
destruct IHl as [r [P0 [P1 P2]]].
exists (fun n => if (decision (n = S (S l))) then qFin else r n).
repeat split; cbn; try now trivial_decision.
intros n L.
decide (n = (S l)) as [D|D]; trivial_decision.
+ rewrite D. cbn in P1. now rewrite P1.
+ apply P2. comega.
Qed.
Lemma detlaQstar_convert_inverse(w:String A) (B: Automata.nfa A) (qFin: Automata.Q B) :
(exists (r: Seq (Automata.Q B)),
r 0 = Automata.q0 /\ r (S (|w|)) = qFin /\ forall n, n <= |w| -> Automata.delta_Q (r n) (w[n]) (r (S n))) ->
Automata.delta_Q_star Automata.q0 (stringToList w) qFin .
Proof.
intros [r [Be [E T]]].
enough (forall n, n <= (|w|) -> Automata.delta_Q_star Automata.q0 (stringToList (mkstring (seq w) n )) (r (S n))) as H. {
rewrite <-E. now apply (H (|w|)).
}
intros n. induction n; intros L; cbn.
- exists (r 1 ). split; auto.
rewrite <-Be. now apply T.
- apply detlaQstar_decrease_step. exists (r (S n)). split.
+ apply IHn. omega.
+ now apply T.
Qed.
Conversion automata in both directions
Definition to_ind_nfa := Automata.NFA (normalize_inital aut) (DecPred (final_state (aut:= normalize aut) )) (fun s a => DecPred (fun s' => transition (aut:=normalize aut) s a s')).
Lemma to_ind_nfa_correct: L_ind (to_ind_nfa) =$= L_S aut.
Proof.
intros w. split.
- intros [qFin [Pacc Preach]]. apply normalize_correct.
apply detlaQstar_convert in Preach.
destruct Preach as [r [B [E T]]].
exists r. repeat split; auto.
unfold sfinal. now rewrite E.
- intros [r [V [ I F]]] % normalize_correct.
exists (r (S(|w|))). split; auto.
apply detlaQstar_convert_inverse.
exists r. split; auto.
Qed.
Definition from_ind_nfa (B : Automata.nfa A) := mknfa (Automata.delta_Q (n:=B)) (fun s => s = Automata.q0) Automata.Q_acc.
Lemma from_ind_nfa_correct (B : Automata.nfa A): L_S (from_ind_nfa B) =$= L_ind B.
Proof.
intros w. split.
- intros [r [V [I F]]].
exists (r (S(|w|))). split; auto.
apply detlaQstar_convert_inverse.
exists r. split; auto.
- intros [qFin [Pacc Preach]].
apply detlaQstar_convert in Preach.
destruct Preach as [r [Be [E T]]].
exists r. repeat split; auto.
unfold sfinal. now rewrite E.
Qed.
End ConvertToNFA.
Closure properties of regular languages follow immediately
from the closure properties of the inducively defined NFAs.
Section ClosureProperties.
Context{A:finType}.
Lemma sclosure_union (aut1 aut2: NFA A) : Sigma aut, L_S aut =$= L_S aut1 \$/ L_S aut2.
Proof.
exists (from_ind_nfa (Automata.toNFA (Automata.U (Automata.toDFA (to_ind_nfa aut1)) (Automata.toDFA (to_ind_nfa aut2))))).
rewrite from_ind_nfa_correct, <-ind_dfa_to_nfa_correct, <-2to_ind_nfa_correct, 2ind_nfa_to_dfa_correct.
intros w. unfold L_dind, language_union. now rewrite Automata.U_correct.
Qed.
Lemma sclosure_intersection (aut1 aut2: NFA A) : Sigma aut, L_S aut =$= L_S aut1 /$\ L_S aut2.
Proof.
exists (from_ind_nfa (Automata.toNFA (Automata.intersect (Automata.toDFA (to_ind_nfa aut1)) (Automata.toDFA (to_ind_nfa aut2))))).
rewrite from_ind_nfa_correct, <-ind_dfa_to_nfa_correct, <-2to_ind_nfa_correct, 2ind_nfa_to_dfa_correct.
intros w. unfold L_dind, language_union. now rewrite Automata.intersect_correct.
Qed.
Lemma sclosure_diff (aut1 aut2 : NFA A) : Sigma aut, L_S aut =$= language_difference (L_S aut1) (L_S aut2).
Proof.
exists (from_ind_nfa (Automata.toNFA (Automata.diff (Automata.toDFA (to_ind_nfa aut1)) (Automata.toDFA (to_ind_nfa aut2))))).
rewrite from_ind_nfa_correct, <-ind_dfa_to_nfa_correct, <-2to_ind_nfa_correct, 2ind_nfa_to_dfa_correct.
intros w. unfold L_dind, language_union. now rewrite Automata.diff_correct.
Qed.
Lemma univ_aut_scorrect: L_S (univ_aut (X:=A)) =$= universal_language.
Proof.
intros w; split; firstorder.
exact (fun n => tt).
Qed.
Lemma sclosure_complement (aut : NFA A) : Sigma aut', L_S aut' =$= (L_S aut)^$~.
Proof.
destruct ( sclosure_diff univ_aut aut) as [aut' EA].
exists aut'.
rewrite EA. rewrite univ_aut_scorrect. firstorder.
Qed.
(* I do not define the closure NFAs as definition but hide them in existentials because
I do not want that the conversions to the inductive definitions become visible.
In order to have closure operators, I need to unpack the existentials. *)
Definition sunion (aut1 aut2: NFA A) := match (sclosure_union aut1 aut2) with existT _ aut _ => aut end.
Definition sdiff (aut1 aut2: NFA A) := match (sclosure_diff aut1 aut2) with existT _ aut _ => aut end.
Definition scomplement (aut: NFA A) := match (sclosure_complement aut) with existT _ aut' _ => aut' end.
Definition sintersect (aut1 aut2: NFA A) := match (sclosure_intersection aut1 aut2) with existT _ aut _ => aut end.
Lemma sdiff_correct aut1 aut2 : language_eq (L_S (sdiff aut1 aut2)) (language_difference (L_S aut1) (L_S aut2)).
Proof. unfold sdiff. now destruct sclosure_diff. Qed.
Lemma scomplement_correct aut: language_eq (L_S (scomplement aut)) (language_complement (L_S aut)).
Proof. unfold scomplement. now destruct sclosure_complement. Qed.
Lemma sunion_correct aut1 aut2 : language_eq (L_S(sunion aut1 aut2)) (language_union (L_S aut1) (L_S aut2)).
Proof. unfold sunion. now destruct sclosure_union. Qed.
Lemma sintersect_correct aut1 aut2: language_eq (L_S (sintersect aut1 aut2)) (language_intersection (L_S aut1) (L_S aut2)).
Proof. unfold sintersect. now destruct sclosure_intersection. Qed.
End ClosureProperties.
Definition big_sintersection (A:finType) (l:list (NFA A)) := fold_right sintersect univ_aut l.
Lemma big_intersection_scorrect (A:finType) (l:list (NFA A)):
L_S (big_sintersection l) =$= fun w => forall a, (a el l) -> L_S a w.
Proof.
intros w. split.
- intros I a L. induction l.
+ now exfalso.
+ cbn in I. apply sintersect_correct in I. destruct I as [I1 I2].
destruct L.
* now subst a.
* now apply IHl.
- intros I. induction l.
+ cbn. now apply univ_aut_scorrect.
+ cbn. apply sintersect_correct. split.
* now apply I.
* apply IHl. firstorder.
Qed.
Context{A:finType}.
Lemma sclosure_union (aut1 aut2: NFA A) : Sigma aut, L_S aut =$= L_S aut1 \$/ L_S aut2.
Proof.
exists (from_ind_nfa (Automata.toNFA (Automata.U (Automata.toDFA (to_ind_nfa aut1)) (Automata.toDFA (to_ind_nfa aut2))))).
rewrite from_ind_nfa_correct, <-ind_dfa_to_nfa_correct, <-2to_ind_nfa_correct, 2ind_nfa_to_dfa_correct.
intros w. unfold L_dind, language_union. now rewrite Automata.U_correct.
Qed.
Lemma sclosure_intersection (aut1 aut2: NFA A) : Sigma aut, L_S aut =$= L_S aut1 /$\ L_S aut2.
Proof.
exists (from_ind_nfa (Automata.toNFA (Automata.intersect (Automata.toDFA (to_ind_nfa aut1)) (Automata.toDFA (to_ind_nfa aut2))))).
rewrite from_ind_nfa_correct, <-ind_dfa_to_nfa_correct, <-2to_ind_nfa_correct, 2ind_nfa_to_dfa_correct.
intros w. unfold L_dind, language_union. now rewrite Automata.intersect_correct.
Qed.
Lemma sclosure_diff (aut1 aut2 : NFA A) : Sigma aut, L_S aut =$= language_difference (L_S aut1) (L_S aut2).
Proof.
exists (from_ind_nfa (Automata.toNFA (Automata.diff (Automata.toDFA (to_ind_nfa aut1)) (Automata.toDFA (to_ind_nfa aut2))))).
rewrite from_ind_nfa_correct, <-ind_dfa_to_nfa_correct, <-2to_ind_nfa_correct, 2ind_nfa_to_dfa_correct.
intros w. unfold L_dind, language_union. now rewrite Automata.diff_correct.
Qed.
Lemma univ_aut_scorrect: L_S (univ_aut (X:=A)) =$= universal_language.
Proof.
intros w; split; firstorder.
exact (fun n => tt).
Qed.
Lemma sclosure_complement (aut : NFA A) : Sigma aut', L_S aut' =$= (L_S aut)^$~.
Proof.
destruct ( sclosure_diff univ_aut aut) as [aut' EA].
exists aut'.
rewrite EA. rewrite univ_aut_scorrect. firstorder.
Qed.
(* I do not define the closure NFAs as definition but hide them in existentials because
I do not want that the conversions to the inductive definitions become visible.
In order to have closure operators, I need to unpack the existentials. *)
Definition sunion (aut1 aut2: NFA A) := match (sclosure_union aut1 aut2) with existT _ aut _ => aut end.
Definition sdiff (aut1 aut2: NFA A) := match (sclosure_diff aut1 aut2) with existT _ aut _ => aut end.
Definition scomplement (aut: NFA A) := match (sclosure_complement aut) with existT _ aut' _ => aut' end.
Definition sintersect (aut1 aut2: NFA A) := match (sclosure_intersection aut1 aut2) with existT _ aut _ => aut end.
Lemma sdiff_correct aut1 aut2 : language_eq (L_S (sdiff aut1 aut2)) (language_difference (L_S aut1) (L_S aut2)).
Proof. unfold sdiff. now destruct sclosure_diff. Qed.
Lemma scomplement_correct aut: language_eq (L_S (scomplement aut)) (language_complement (L_S aut)).
Proof. unfold scomplement. now destruct sclosure_complement. Qed.
Lemma sunion_correct aut1 aut2 : language_eq (L_S(sunion aut1 aut2)) (language_union (L_S aut1) (L_S aut2)).
Proof. unfold sunion. now destruct sclosure_union. Qed.
Lemma sintersect_correct aut1 aut2: language_eq (L_S (sintersect aut1 aut2)) (language_intersection (L_S aut1) (L_S aut2)).
Proof. unfold sintersect. now destruct sclosure_intersection. Qed.
End ClosureProperties.
Definition big_sintersection (A:finType) (l:list (NFA A)) := fold_right sintersect univ_aut l.
Lemma big_intersection_scorrect (A:finType) (l:list (NFA A)):
L_S (big_sintersection l) =$= fun w => forall a, (a el l) -> L_S a w.
Proof.
intros w. split.
- intros I a L. induction l.
+ now exfalso.
+ cbn in I. apply sintersect_correct in I. destruct I as [I1 I2].
destruct L.
* now subst a.
* now apply IHl.
- intros I. induction l.
+ cbn. now apply univ_aut_scorrect.
+ cbn. apply sintersect_correct. split.
* now apply I.
* apply IHl. firstorder.
Qed.
NFA accepting only a single string
Section OneStringNFA.
Context (X:finType).
Variable (v : String X).
Definition os_state := Le_K (S (|v|)).
Definition os_initial (q : os_state) := proj1_sig q = 0.
Definition os_final (q : os_state) := proj1_sig q = S(|v|).
Definition os_transition (q: os_state) (x:X) (p: os_state) := v [proj1_sig q] = x /\ proj1_sig p = S(proj1_sig q ) .
Definition os_nfa := mknfa os_transition os_initial os_final.
Definition os_accepting_run (n:nat) : os_state.
Proof.
decide (n <= S(|v|)) as [D|D].
- exists n. apply pure_equiv. apply D.
- exists 0. apply pure_equiv. cbv. omega.
Defined.
Lemma os_nfa_accepts_v u : u==v -> L_S os_nfa u.
Proof.
intros [H1 H2].
exists os_accepting_run. unfold os_accepting_run; cbn. repeat split.
- simpl. destruct decision as [D|D].
+ simpl. now rewrite H2.
+ exfalso. omega.
- simpl. destruct decision as [D|D].
+ simpl. destruct decision as [D'|D'].
* reflexivity.
* exfalso. omega.
+ exfalso. omega.
- simpl. destruct decision as [D|D].
+ unfold os_final. simpl. omega.
+ exfalso. omega.
Qed.
Lemma os_nfa_only_accepts_v u : L_S os_nfa u -> u == v.
Proof.
intros [r [V [I F]]].
assert (forall n, n <= S(|u|) -> proj1_sig (r n) = n ) as H. {
intros n L. induction n.
- apply I.
- specialize (V (n)). simpl in V. unfold os_transition in V.
rewrite IHn in V by omega. apply V. omega. }
split.
- simpl in F. unfold os_final in F. rewrite H in F by omega. omega.
- intros n L. specialize (V n). simpl in V. unfold os_transition in V.
rewrite H in V by omega. symmetry. now apply V.
Qed.
Lemma os_nfa_correct : L_S os_nfa =$= fun u => u == v.
Proof.
intros u. split.
- apply os_nfa_only_accepts_v.
- intros E. now apply os_nfa_accepts_v.
Qed.
End OneStringNFA.
Context (X:finType).
Variable (v : String X).
Definition os_state := Le_K (S (|v|)).
Definition os_initial (q : os_state) := proj1_sig q = 0.
Definition os_final (q : os_state) := proj1_sig q = S(|v|).
Definition os_transition (q: os_state) (x:X) (p: os_state) := v [proj1_sig q] = x /\ proj1_sig p = S(proj1_sig q ) .
Definition os_nfa := mknfa os_transition os_initial os_final.
Definition os_accepting_run (n:nat) : os_state.
Proof.
decide (n <= S(|v|)) as [D|D].
- exists n. apply pure_equiv. apply D.
- exists 0. apply pure_equiv. cbv. omega.
Defined.
Lemma os_nfa_accepts_v u : u==v -> L_S os_nfa u.
Proof.
intros [H1 H2].
exists os_accepting_run. unfold os_accepting_run; cbn. repeat split.
- simpl. destruct decision as [D|D].
+ simpl. now rewrite H2.
+ exfalso. omega.
- simpl. destruct decision as [D|D].
+ simpl. destruct decision as [D'|D'].
* reflexivity.
* exfalso. omega.
+ exfalso. omega.
- simpl. destruct decision as [D|D].
+ unfold os_final. simpl. omega.
+ exfalso. omega.
Qed.
Lemma os_nfa_only_accepts_v u : L_S os_nfa u -> u == v.
Proof.
intros [r [V [I F]]].
assert (forall n, n <= S(|u|) -> proj1_sig (r n) = n ) as H. {
intros n L. induction n.
- apply I.
- specialize (V (n)). simpl in V. unfold os_transition in V.
rewrite IHn in V by omega. apply V. omega. }
split.
- simpl in F. unfold os_final in F. rewrite H in F by omega. omega.
- intros n L. specialize (V n). simpl in V. unfold os_transition in V.
rewrite H in V by omega. symmetry. now apply V.
Qed.
Lemma os_nfa_correct : L_S os_nfa =$= fun u => u == v.
Proof.
intros u. split.
- apply os_nfa_only_accepts_v.
- intros E. now apply os_nfa_accepts_v.
Qed.
End OneStringNFA.