Set Implicit Arguments.

Require Import Utils.
Require Import Strings.
Require Import Sequences.
Require Import NFAs.
Require Import FiniteSemigroups.

NFAs Accepting Regular Languages

Formalizing Büchi automata (especially constructions on Büchi automata) gets easier if we use some basic knowledge of regular languages. We use an inductive characterization of acceptance, where we have one version of strings and one for empty strings. This is technically easier because one obtains in both cases the correct induction principle. We give NFAs accepting the following regular languages:

the universal languages
the language consisting of exactly one string
the language of all strings of length one, such that the single symbol satisfied some predicate
the language of strings with the same sum in a finite semigroup

These NFAs will be usefull when building Büchi automata later.

Section RegularLanguages.

Definition of Acceptance

We give an inductive definition for strings and empty strings and show that they agree (on nonempty strings).

  Context{Sigma: finType}.
  Context (aut: NFA Sigma).
  Implicit Types (r: NStr (state aut))(x: Str Sigma).

  Inductive saccepting_ind : state aut -> Str Sigma -> Prop :=
    | accept_empty q : accepting_state q -> saccepting_ind q []
    | accept_step q p a x : transition q a p -> saccepting_ind p x -> saccepting_ind q (a ::x).

  Inductive snaccepting_ind : state aut -> NStr Sigma -> Prop :=
    | naccept_sing p a q : transition p a q -> accepting_state q -> snaccepting_ind p (sing a)
    | naccept_step q p a (x:NStr Sigma) : transition q a p -> snaccepting_ind p x -> snaccepting_ind q (ncons a x).

  Definition slanguage_ind := fun x => exists q, initial_state q /\ saccepting_ind q x.
  Definition snlanguage_ind := fun (x:NStr Sigma) => exists q, initial_state q /\ snaccepting_ind q x.

  Lemma saccepting_ind_iff_snaccepting_ind (x: NStr Sigma) q: saccepting_ind q x <-> snaccepting_ind q x.
  Proof.
    split.
    - setoid_rewrite nstr_to_str_to_nstr_idem at 2.
      pose proof (nstr_nonempty x) as H2. revert H2.
      generalize (nstr_to_str x) as y. intros y. intros N T.
      induction T.
      + now exfalso.
      + simpl. destruct x0.
        * apply (naccept_sing H). now inversion T.
        * apply (naccept_step H). now apply IHT.
    - intros T. induction T.
      + apply (accept_step H). now apply accept_empty.
      + simpl. now apply (accept_step H).
  Qed.

  Lemma snlanguage_ind_iff_slanguage_ind (x: NStr Sigma) : snlanguage_ind x <-> slanguage_ind x.
  Proof.
    split; intros [p [I Ac]]; exists p; split; auto; now apply saccepting_ind_iff_snaccepting_ind.
  Qed.

End RegularLanguages.

Notation "'L_R'" := slanguage_ind.
Notation "'L_NR'" := snlanguage_ind.

The universal automaton is correct for regular languages, too

Lemma univ_aut_scorrect (Sigma:finType): L_R (@univ_aut Sigma ) =$= universal_language.
Proof.
  intros x; split; firstorder.
  exists tt. split; auto.
  induction x.
  - now constructor.
  - apply accept_step with (p:=tt); auto.
Qed.

NFAs Accepting Exactly One String

We give an NFA that accepts only one string. The postfixes of that strings serve as state. We need some easy facts on postfixes.

Section OneStringNFA.

We fix and alphabet an a string x that should be accepted

  Context (Sigma:finType).
  Variable (x : Str Sigma).

  Fixpoint postfixes (y: Str Sigma) := match y with
    | nil => [[]]
| a::y => (a::y )::postfixes y
  end.

  Inductive postfix: Str Sigma -> Str Sigma -> Prop :=
    | postfix_base y: postfix y y
    | postfix_step a y z : postfix y z -> postfix y (a ::z).

  Lemma postfix_inversion a y z : postfix (a ::y) z -> postfix y z.
  Proof.
    intros H. remember (a::y) as z'. induction H as [z|b y' z].
    - subst z. apply postfix_step, postfix_base.
    - apply postfix_step. now apply IHpostfix.
  Qed.

  Lemma postfixes_contains_postfixes z y : postfix z y -> z el (postfixes y ).
  Proof.
    intros H. induction H as [y | a z y]; simpl.
    - destruct y; simpl; auto.
    - now right.
  Qed.

  Implicit Types (p q : finType_fromList (postfixes x)).

  Definition os_nfa := mknfa
     (fun q a p => match (proj1_sig q) with
       | nil => False
       | b::y => a = b /\ proj1_sig p = y end)
     (fun q => proj1_sig q = x)
     (fun q => proj1_sig q = []).

Given a postfix of x we build the corresponding state.

  Definition postfix_state (y :Str Sigma): postfix y x -> finType_fromList (postfixes x) :=
    fun H => exist _ y (proj1 (pure_equiv _ ) (postfixes_contains_postfixes H)).

  Lemma os_nfa_accepts_x : L_R os_nfa x.
  Proof.
    exists (postfix_state (postfix_base x)). split.
    - reflexivity.
    - enough (forall y (H:postfix y x),saccepting_ind (aut:= os_nfa) (postfix_state H) y) as H.
      + apply H.
      + intros y H. induction y.
        * apply accept_empty. reflexivity.
        * pose proof (postfix_inversion H) as H'.
          apply accept_step with (p:= postfix_state H').
          -- simpl. split; reflexivity.
          -- apply IHy.
  Qed.

  Lemma os_nfa_only_accepts_x y : L_R os_nfa y -> y = x.
  Proof.
    intros [q [I A]].
    enough (forall (q: state (os_nfa)), saccepting_ind q y -> proj1_sig q = y) as H.
    - apply H in A. now rewrite <-A, I.
    - clear q I A. intros q A. induction A.
      + apply H.
      + destruct q as [[|b y] P].
        * now exfalso.
        * destruct H as [H1 H2]. f_equal; auto. simpl. congruence.
  Qed.

  Lemma os_nfa_correct : L_R os_nfa =$= fun y => y = x.
  Proof.
    intros y. split.
    - apply os_nfa_only_accepts_x.
    - intros ->. now apply os_nfa_accepts_x.
  Qed.

End OneStringNFA.

Lemma nstr_os_nfa_correct (Sigma: finType) (x: NStr Sigma) : L_NR (os_nfa x ) =$= fun y => y = x.
Proof.
  intros y. rewrite snlanguage_ind_iff_slanguage_ind, (os_nfa_correct _ _).
  split. apply nstr_to_str_eq. now intros <-.
Qed.

NFAs Accepting Symbols Satisfying a Predicate

We define an NFA that accepts all strings of length one such that the single symbol in the strings satisfies a given (decidable) predicate.

Section SingletonNFA.

We fix an alphabet an a decidable predicate on it.

  Context {Sigma:finType}.
  Variable (P: Sigma -> Prop).
  Context {decP: forall x, dec (P x)}.

  Definition singleton_nfa := mknfa (fun p a q => match p, q with
                                | false, true => P a
                                | _,_ => False end)
                                (fun p => p = false)
                                (fun p => p = true).

The NFA should accept this language.

  Definition singleton_lang := fun x => exists a , x = [a ] /\ P a.

  Lemma singleton_nfa_correct : L_R (singleton_nfa ) =$= singleton_lang.
  Proof.
    intros x. split.
    - intros L.
      destruct L as [p [H1 H2]]. destruct H2 as [q H2 |p q a x T H2].
      + exfalso. simpl in H1 ,H2. congruence.
      + destruct H2.
        * exists a. split; auto. simpl in *. subst p q. apply T.
        * exfalso. simpl in *. subst p. now destruct q.
    - intros [a [H1 H2]].
      subst x. exists false. split; auto.
      + reflexivity.
      + apply accept_step with (p:= true); auto.
        now apply accept_empty.
  Qed.

  Lemma singleton_nfa_nstr_correct : L_NR (singleton_nfa ) =$= singleton_lang.
  Proof.
    intros x. rewrite snlanguage_ind_iff_slanguage_ind. apply singleton_nfa_correct.
  Qed.

End SingletonNFA.

NFAs Accepting Strings of Given Color in a Semigroup

We define an NFA on a finite semigroup Gamma that accepts exactly the strings that have a given sum in this semigroup. For reusability, we do not use Gamma as input alphabet but some finite type Sigma given a homomorphism from NStr Sigma to Gamma

Section OneColorNFA.

  Context {Gamma: FiniteSemigroup}.
  Context {Sigma: finType}.
  Variable (c: Gamma).
  Variable (f : NStr Sigma -> Gamma).
  Variable (HM : is_homomorphism f).

The NFA calculates the sum of the input string.

  Definition color_transition p a q := match p,q with
    | None , Some b => f(sing a) = b
    | Some b, Some c => c = add b (f(sing a))
    | _, _ => False
  end.

  Definition one_color_nfa := mknfa color_transition (fun q => q = None) (fun q => q = Some c).

  Lemma homomorphism_cons a x : f (ncons a x) = add (f (sing a)) (f x).
  Proof. now rewrite <-HM. Qed.

  Lemma one_color_nfa_accepts_strings_of_color: L_NR one_color_nfa <$= (fun x => f x = c ).
  Proof.
    intros x [p [I Ac]].
    enough (match p with
                 | None => f x = c
                 | Some a => add a (f x) = c end) as H.
    - now destruct p; try now exfalso.
    - clear I. induction Ac as [p a q T F| p q a x T L].
      + simpl in *. subst. now destruct p.
      + simpl in *. destruct p as [b|]; destruct q as [d|]; rewrite !homomorphism_cons; cbn in *; subst; auto.
        now rewrite Assoc.
  Qed.

  Lemma strings_of_color_accepted_by_one_color_nfa : (fun x => f x = c ) <$= L_NR one_color_nfa.
  Proof.
    intros x C.
    enough ((forall x b, add b (f x) = c -> snaccepting_ind (aut:=one_color_nfa) (Some b) x)) as H.
    - exists None. split; simpl; auto. destruct x as [a| a x].
      + cbn in *. apply naccept_sing with (q:=Some (f (sing a))); cbn; subst; auto.
      + rewrite homomorphism_cons in C. apply naccept_step with (p:= Some (f (sing a))); cbn; auto.
    - clear x C. intros x. induction x as [a|a x]; intros b C.
      + cbn in *. apply naccept_sing with (q := Some c); [rewrite <-C|]; cbn; auto.
      + cbn in *. rewrite homomorphism_cons,Assoc in C. apply naccept_step with (p := Some (add b (f (sing a)))); cbn; auto.
  Qed.

  Lemma one_color_nfa_correct : L_NR one_color_nfa =$= (fun x => f x = c ).
  Proof.
    intros x. split. apply one_color_nfa_accepts_strings_of_color. apply strings_of_color_accepted_by_one_color_nfa.
  Qed.

The NFA can only accept nonempty strings (as there is not necessarily a neutral element).

  Lemma one_color_nfa_nonempty x : L_R one_color_nfa x -> nonempty x.
  Proof.
    intros [p [I Ac]]. destruct x; try reflexivity.
    exfalso. inversion Ac. cbn in *. subst. congruence.
  Qed.

  Lemma one_color_nfa_correct' : L_R one_color_nfa =$= (fun x => exists (x': NStr Sigma ), x = x' /\ f x' = c ).
  Proof.
    intros x. split.
    - intros A. assert (Dummy Sigma). { destruct x; auto. now apply one_color_nfa_nonempty in A. }
      exists (!x). split.
      + now apply str_to_nstr_idem, one_color_nfa_nonempty.
      + apply one_color_nfa_correct, snlanguage_ind_iff_slanguage_ind.
        now rewrite str_to_nstr_idem in A by now apply one_color_nfa_nonempty.
    - intros [x' [E C]]. rewrite E. now apply snlanguage_ind_iff_slanguage_ind, one_color_nfa_correct.
  Qed.

End OneColorNFA.