Set Implicit Arguments.

Require Import Utils.
Require Import FinSets.
Require Import Strings.
Require Import Sequences.
Require Import UPSequences.
Require Import NFAs.
Require Import RegularLanguages.
Require Import FiniteSemigroups.
Require Import RamseyanFactorizations.
Require Import Buechi.
Require Import Complement.

Minimal S1S

We define minimal S1S. Because we are interested in S1S on sequences and on S1S only on UP sequences, we define minimal S1S over abstract sequences, that later can be chosen as all sequences or UP sequences to obtain minimal S1S with AS semantics. This file consists of:
  • Definition of minimal S1S
  • Reduction of S1S to abstract automata (an abstract notation of automata, that designed for the requirements of the translation)
  • Büchi automata as abstract automata (construcively for UP semantics, using RF for AS semantics)
  • Results for minimal S1S

Inductive MinForm (Var: eqType) :=
    | MLe : Var -> Var -> MinForm Var
    | MIncl: Var -> Var -> MinForm Var
    | MAnd : MinForm Var -> MinForm Var -> MinForm Var
    | MNeg : MinForm Var-> MinForm Var
    | MEx : Var -> MinForm Var -> MinForm Var.

Ltac min_s1s_ind phi := induction phi as [X Y | X Y | phi IHphi psi IHpsi | phi IHphi | X phi IHphi].

Notation "X <0 Y" := (MLe X Y) (at level 40).
Notation "X <<=0 Y" := (MIncl X Y) (at level 40).
Notation "phi /\0 psi" := (MAnd phi psi) (at level 42 ,left associativity).
Notation "~0 phi" := (MNeg phi) (at level 43).
Notation "'ex0' X , phi" := (MEx X phi) (at level 44).

Section MinS1S.

Sem represents the abstract sequences used for minimal S1S and generalizes over AS and UP semantics.
  Context {Sem: AbstractSequence}.

  Context {Var : finType}.
  Implicit Types (X Y : Var).

  Definition equiv_apart X (sigma tau : Seq (finSet Var)) := forall n, (forall Y, Y <> X -> applyVect (sigma n) Y = applyVect (tau n) Y).

  Global Instance equiv_apart_proper : Proper (eq ==> @seq_equiv _ _ ==> @seq_equiv _ _ ==> iff) equiv_apart.
  Proof.
    intros X Y <- sigma sigma' Es tau tu' Et.
    split; intros H n Y D; [rewrite <-Es, <-Et |rewrite Es, Et]; now apply H.
  Qed.

  Definition set_mem n X (sigma : Seq (finSet Var)) : Prop := X mem (sigma n).

  Reserved Notation "sigma |= phi" (at level 50).
  Fixpoint satisfies (phi:MinForm Var) (sigma: Seq (finSet Var)) : Prop := match phi with
    | X <0 Y => exists m n, m < n /\ set_mem m X sigma /\ set_mem n Y sigma
    | X <<=0 Y => forall n, set_mem n X sigma -> set_mem n Y sigma
    | phi /\0 psi => sigma |= phi /\ sigma |= psi
    | ~0 phi => ~ (sigma |= phi)
    | ex0 X, phi => exists (tau: Seq (finSet Var)), tau |= phi /\ equiv_apart X tau sigma
  end where "sigma |= phi" := (satisfies phi sigma ).

  Definition sat phi := exists sigma, sigma |= phi.

  Global Instance set_mem_proper : Proper (eq ==> eq ==> @seq_equiv _ (finSet Var) ==> iff) set_mem.
  Proof.
    intros n m <- X Y <- sigma tau E.
    unfold set_mem. now rewrite E.
  Qed.

  Lemma satisfies_extensional phi sigma tau : sigma == tau -> sigma |= phi <-> tau |= phi.
  Proof.
    revert sigma tau. min_s1s_ind phi; intros sigma tau E.
    - split; intros [n [m [H1 [H2 H3]]]]; exists n, m; repeat split; auto; try rewrite E; auto; rewrite <-E; auto.
    - split; intros H n; [rewrite <-E| rewrite E]; apply H.
    - simpl. now rewrite (IHphi sigma tau E), (IHpsi sigma tau E).
    - simpl. now rewrite (IHphi sigma tau E).
    - split; intros [nu [Sat H]]; exists nu; split; auto; [rewrite <-E | rewrite E]; assumption.
  Qed.

  Global Instance satisfies_proper : Proper (eq ==> @seq_equiv _ (finSet Var) ==> iff) satisfies.
  Proof.
    intros phi psi <- sigma tau E. split; now apply satisfies_extensional.
  Qed.


Translation to Abstract Automata

The following structure represents an abstract automaton. It provides operations mimicking the logical connectives of minimal S1S. We include decidability of emptiness such that we directly obtain decidability of satisfiability of minimal S1S.

  Class AbstractAutomata := {
    Aut :> Type;
    lang : Aut -> Language (Seq (finSet Var));
    less_aut : forall X Y, Aut;
    incl_aut : forall X Y, Aut;
    intersect_aut: Aut -> Aut -> Aut;
    complement_aut: Aut -> Aut;
    ex_aut: forall X, Aut -> Aut;
    less_aut_correct: forall X Y, lang (less_aut X Y) =$= satisfies (X <0 Y);
    incl_aut_correct: forall X Y, lang (incl_aut X Y) =$= satisfies (X <<=0 Y);
    intersect_aut_correct: forall A_1 A_2, lang (intersect_aut A_1 A_2) =$= lang A_1 /$\ lang A_2 ;
    complement_aut_disjoint: forall (A: Aut), lang A /$\ lang (complement_aut A) =$= empty_language;
    complement_aut_exhaustive: forall (A: Aut ), lang A \$/ lang (complement_aut A) =$= universal_language;
    ex_aut_correct: forall X A , lang (ex_aut X A) =$= fun sigma => exists tau, lang A tau /\ equiv_apart X tau sigma;
    dec_emptiness: forall (A: Aut ), {sigma | lang A sigma} + {lang A =$= empty_language} }.

  Context {CA: AbstractAutomata }.

  Lemma complement_aut_correct A: lang (complement_aut A) =$= (lang A) ^$~.
  Proof.
    intros sigma. split; intros H.
    - intros C. now apply (complement_aut_disjoint A sigma).
    - destruct (complement_aut_exhaustive A sigma) as [_ C].
      destruct (C I) as [Q|Q].
      + now exfalso.
      + assumption.
  Qed.

  Lemma aut_lang_sat_xm A (sigma: Seq (finSet Var)): lang A sigma \/ ~ lang A sigma.
  Proof.
    destruct (complement_aut_exhaustive A sigma) as [_ C].
    destruct (C I) as [Q|Q].
    - now left.
    - right. now apply complement_aut_correct.
  Qed.

Formulas are recursively translated to abstract automata. All following theorems and lemmas can be instatiated for AS and UP Semantics once we provide instances for abstract automata.

  Fixpoint formula_aut (phi:MinForm Var) : Aut := match phi with
    | X <0 Y => less_aut X Y
    | X <<=0 Y => incl_aut X Y
    | phi /\0 psi => intersect_aut (formula_aut phi) (formula_aut psi)
    | ~0 phi => complement_aut (formula_aut phi)
    | ex0 X, phi => ex_aut X (formula_aut phi)
  end.

  Theorem formula_aut_correct (phi: MinForm Var): lang (formula_aut phi) =$= satisfies phi.
  Proof.
    min_s1s_ind phi; cbn.
    - apply less_aut_correct.
    - apply incl_aut_correct.
    - now rewrite intersect_aut_correct, IHphi, IHpsi.
    - now rewrite complement_aut_correct, IHphi.
    - rewrite ex_aut_correct. intros sigma. split; intros [tau [H1 H2]]; exists tau; split; auto; now apply IHphi.
  Qed.

Satisfiability is Deciable and Satisfaction satisfies XM


  Lemma min_s1s_satisfies_xm (phi: MinForm Var) sigma: sat_xm(sigma |= phi).
  Proof.
    rewrite <- (formula_aut_correct _ _).
    apply aut_lang_sat_xm.
  Qed.

  Lemma sat_iff_aut_non_empty phi : (exists sigma, lang (formula_aut phi) sigma) <-> sat phi.
  Proof.
    apply iff_ex. apply formula_aut_correct.
  Qed.

  Lemma min_s1S_dec_satisfaction_informative (phi: MinForm Var) : {sigma | sigma |= phi } + {~ sat phi}.
  Proof.
    destruct (dec_emptiness (formula_aut phi)) as [[sigma Sat % formula_aut_correct]|E].
    - left. now exists sigma.
    - right. intros [sigma Sat]. now apply (E sigma), formula_aut_correct.
  Qed.

  Lemma min_s1S_dec_satisfaction (phi: MinForm Var) : dec (sat phi).
  Proof.
    destruct (min_s1S_dec_satisfaction_informative phi) as [[sigma Sat] |E].
    - left. now exists sigma.
    - now right.
  Qed.

  Lemma min_s1S_dec_obtain (phi: MinForm Var) : (sat phi) -> {sigma | sigma |= phi}.
  Proof.
    intros sat.
    destruct (min_s1S_dec_satisfaction_informative phi) as [[sigma Sat] |E].
    - now exists sigma.
    - exfalso. now apply E.
  Qed.

End MinS1S.

Büchi Automata as Abstract Automata

We now use Büchi automata to build instances for abstract automata. There will be an instance for UP sequenes and one for all sequences. The operation of both instances will be the same, but for all sequences the verification of the complement operation requires RF.

Section MinS1SToBuechi.

Operations on Büchi Automata

We provide operations for less, inclusion and existential quantification. They can easily be defined used closure operations.

  Context {Var : finType}.
  Variables (X Y : Var).

We start with less and inclusion by showing an equivalent definition of satisfaction, which than can easily be implemented in automata.

  Lemma incl_language : satisfies (X <<=0 Y) =$= OmegaIter (singleton_lang (fun v => X mem v -> Y mem v)).
  Proof.
    intros sigma. split.
    - intros L. exists (map sing sigma). split.
      + intros n. rewrite map_nth. exists (sigma n). split; auto. apply L.
      + intros n. clear L. revert sigma. induction n; intros sigma.
        * rewrite flatten_correct, map_correct, hd_correct. simpl. now rewrite nth_first, nth_first_hd.
        * rewrite flatten_correct, map_correct, hd_correct, tl_correct. simpl.
          rewrite nth_step, nth_step_tl. apply IHn.
    - intros [tau [H1 H2]] n. rewrite H2. clear sigma H2. revert tau H1. induction n; intros tau H1.
      + rewrite flatten_correct, <-nth_first_hd.
        destruct (H1 0) as [a [H2 H3]]. rewrite H2. simpl. unfold set_mem. now rewrite nth_first.
      + rewrite flatten_correct, <-nth_first_hd.
        destruct (H1 0) as [a [H2 H3]]. rewrite H2; simpl; unfold set_mem; rewrite nth_step.
        apply IHn. intros k. apply (H1 (S k)).
  Qed.

  Lemma less_language : satisfies (X <0 Y) =$= universal_language o
                                          ((singleton_lang (fun v => X mem v)) o
                                           (universal_language o
                                            ((singleton_lang (fun v => Y mem v )) o universal_language))).
  Proof.
    intros sigma. split.
    - intros [i [j [H1 [H2 H3]]]].
      exists (prefix sigma i), (drop sigma i). repeat split; auto.
      + exists (prefix (drop sigma i) 1), (drop (drop sigma i) 1). repeat split; auto.
        * exists (sigma i). split; auto.
        * exists (prefix (drop (drop sigma i) 1) (j - S i)), (drop (drop (drop sigma i) 1) (j - S i)). repeat split; auto.
          -- exists (prefix (drop (drop (drop sigma i) 1) (j - S i)) 1), (drop (drop (drop (drop sigma i) 1) (j - S i)) 1). repeat split; auto.
             ++ exists ((drop (drop (drop sigma i) 1) (j - S i)) 0). split; auto.
                rewrite !drop_plus.
                rewrite <-H3. f_equal. rewrite drop_nth. f_equal. omega.
             ++ now rewrite <-revert_drop.
          -- now rewrite <-revert_drop.
        * now rewrite <-revert_drop.
      + now rewrite <-revert_drop.
    - intros [x1 [sigma1 [_ [[x2 [sigma2 [[a [P1 P2]] [[x3 [sigma3 [_ [[x4 [sigma4 [[b [P3 P4]] [_ E4]]]] E3]]]] E2]]]] E1]]]].
      rewrite E1, E2, E3, E4.
      exists (0 + length x1), (((0 + length x3) + length x2) + length x1). repeat split.
      + rewrite P1. simpl. omega.
      + unfold set_mem. rewrite prepend_nth_rest', P1. simpl. now rewrite nth_first.
      + unfold set_mem. rewrite !prepend_nth_rest', P3. simpl. now rewrite nth_first.
  Qed.

  Definition incl_nfa := nfa_omega_iter (singleton_nfa (P:=fun v => X mem v-> Y mem v)).

  Lemma incl_nfa_correct: L_B (incl_nfa) =$= satisfies (X <<=0 Y) .
  Proof.
    unfold incl_nfa.
    now rewrite incl_language, nfa_omega_iter_correct, singleton_nfa_nstr_correct.
  Qed.

  Definition less_nfa := prepend_nfa univ_aut
                     (prepend_nfa (singleton_nfa (P:= (fun v => X mem v)) )
                       (prepend_nfa univ_aut
                         (prepend_nfa (singleton_nfa (P:= (fun v => Y mem v)) )
                            univ_aut))).

  Lemma less_nfa_correct: L_B less_nfa =$= satisfies (X <0 Y).
  Proof.
    rewrite less_language. unfold less_nfa.
    now rewrite !prepend_nfa_correct, univ_aut_correct, univ_aut_scorrect, !singleton_nfa_correct.
  Qed.


For existential quantification we use the image and preimage operation. We define a function that erases information of the variable X by setting it sequence for X to constant true. We than can regard existential quantification as the preimage of the image under this function.

  Definition clear_X : finSet Var -> finSet Var :=
     fun v => vectorise (fun Z => if (decision (Z = X)) then true else applyVect v Z).

  Lemma rem_injection_eq (sigma tau : Seq (finSet Var)):
      equiv_apart X sigma tau <->
      map (clear_X) sigma == map (clear_X) tau.
  Proof.
    unfold clear_X. split.
    - intros E n. rewrite 2map_nth. apply vector_eq.
      intros Z. rewrite 2apply_vectorise_inverse.
      destruct decision; auto.
    - intros E n Z D.
      specialize (E n). rewrite 2map_nth in E.
      apply (f_equal (fun v => applyVect v Z)) in E.
      rewrite 2apply_vectorise_inverse in E.
      now destruct decision.
  Qed.

  Definition ex_nfa aut := preimage_aut (clear_X) (image_aut (clear_X) aut).

  Lemma ex_nfa_correct aut : L_B (ex_nfa aut) =$= fun sigma => exists tau, L_B aut tau /\ equiv_apart X tau sigma.
  Proof.
    unfold ex_nfa. rewrite preimage_aut_correct, image_aut_correct.
    intros sigma; split; intros [tau [H1 H2]]; exists tau; split; auto; now apply rem_injection_eq.
  Qed.

For UP sequences it is important that the witness is UP, too.

  Lemma ex_nfa_up aut (x y : NStr (finSet Var)):
        L_B (ex_nfa aut) (x +++ omega_iter y) ->
        exists (u v: NStr (finSet Var)), L_B aut (u +++ omega_iter v) /\ equiv_apart X (u +++ omega_iter v) (x +++ omega_iter y).
  Proof.
    unfold ex_nfa. rewrite (preimage_aut_correct _ _ _). intros Acc. unfold PreImage in Acc.
    rewrite map_nstr_prepend, omega_iter_map in Acc.
    apply match_for_up in Acc.
    destruct Acc as [u [v [[u' [v' [M E']]]% image_match E]]].
    exists u', v'. repeat split; auto.
    * now apply match_accepted.
    * unfold equiv_apart. intros n Z D.
      rewrite <-E, <-omega_iter_map, <-map_nstr_prepend in E'.
      apply rem_injection_eq in E'.
      specialize (E' n Z D).
      now rewrite E'.
  Qed.

End MinS1SToBuechi.

Instances for AS and UP semantics


Local Instance BuechiAbstractAutomaton {Var: finType} (Ramsey: RF) : AbstractAutomata :=
   {Aut := NFA (finSet Var);
    lang := @accepts (finSet Var);
    less_aut := less_nfa;
    incl_aut := incl_nfa;
    intersect_aut := @intersect _ ;
    complement_aut := @complement _ ;
    ex_aut := ex_nfa}.
Proof.
  - apply less_nfa_correct.
  - apply incl_nfa_correct.
  - apply intersect_correct.
  - apply complement_disjoint.
  - intros A. apply complement_exhaustive, Ramsey.
  - apply ex_nfa_correct.
  - intros A. destruct (dec_buechi_empty_informative A) as [[x [y M % match_accepted]] % obtain_match|D].
    + left. now exists (x +++ omega_iter y).
    + now right.
Defined.

Local Instance UPBuechiAbstractAutomaton {Var : finType} : AbstractAutomata (Sem := UPSequence) :=
   {Aut := NFA (finSet Var);
    lang := (fun aut xy=> match xy with mkUPSeq x y => @accepts (finSet Var) aut (x +++ omega_iter y) end);
    less_aut := less_nfa;
    incl_aut := incl_nfa;
    intersect_aut := @intersect _ ;
    complement_aut := @complement _;
    ex_aut := ex_nfa}.
Proof.
  - intros X Y [x y]. rewrite (@less_nfa_correct Var _ _ _).
    split; intros [n [m [L [M1 M2]]]]; exists n, m; unfold set_mem in *.
    + repeat split; auto; rewrite up_nth_correct; unfold unfold. apply M1. apply M2.
    + repeat split; auto; rewrite up_nth_correct in M1, M2; unfold unfold in *. apply M1. apply M2.
  - intros X Y [x y]. rewrite (@incl_nfa_correct Var _ _ _).
    split; intros H n; specialize ( H n); unfold set_mem in *.
    + rewrite up_nth_correct. unfold unfold. apply H.
    + rewrite up_nth_correct in H. unfold unfold. apply H.
  - intros X Y [x y]. apply intersect_correct.
  - intros A [x y] . split.
    + intros [C1 C2]. eapply (complement_disjoint _ (x +++ omega_iter y)). split; [apply C1 | apply C2].
    + intros H. now exfalso.
  - intros A [x y]. split.
    + now intros _.
    + intros _. destruct (complement_exhaustive_up A x y) as [D|D].
      * now left.
      * now right.
  - intros X A [x y]. split.
    + intros [u [v [H1 H2]]] % ex_nfa_up. exists (mkUPSeq u v). split; auto.
      intros n Y D. specialize (H2 n Y D). now rewrite !up_nth_correct.
    + intros [[u v] [H1 H2]].
      apply ex_nfa_correct.
      exists (u +++ omega_iter v). split; auto.
      intros n Y D.
      specialize (H2 n Y D). now rewrite !up_nth_correct in H2.
  - intros A. destruct (dec_buechi_empty_informative A) as [[x [y M % match_accepted]] % obtain_match|D].
    + left. now exists (mkUPSeq x y).
    + right. intros [x y]. apply D.
Defined.

For Coq we need to prove that both instances produce actually the same automata.
Lemma formula_nfa_equal (V: finType) (R: RF) (phi:MinForm V):
   formula_aut (CA:=BuechiAbstractAutomaton R) phi = formula_aut (CA:=UPBuechiAbstractAutomaton) phi.
Proof.
  induction phi; simpl; auto.
Qed.

Properties of Minimal S1S using Büchi Automata

Now we use Büchi automata as abstract automata to obtain results for minimal S1S for AS and UP semantics. Most results are just instantiations of the translation. We further obtain that
  • AS and UP semantics agree for satisfiability,
  • UP satisfaction is decidable, and
  • for UP satisfiable formulas we can obtain a satisfing interpretation.

Lemma dec_min_S1S_satisfaction:
   RF -> forall (V:finType) (phi: MinForm V), dec (sat (Sem:=Sequence) phi).
Proof.
  intros Ramsey.
  intros V phi. apply (@min_s1S_dec_satisfaction _ _ (BuechiAbstractAutomaton Ramsey)).
Qed.

Lemma satisfaction_sat_xm (V: finType) (phi: MinForm V) sigma:
  RF -> sat_xm (satisfies (Sem:=Sequence) phi sigma).
Proof.
  intros R.
  apply (@min_s1s_satisfies_xm _ V (BuechiAbstractAutomaton R)).
Qed.

Lemma dec_min_S1S_up_satisfaction (V:finType) (phi: MinForm V):
  dec (sat (Sem:=UPSequence) phi).
Proof.
  apply (@min_s1S_dec_satisfaction _ _ UPBuechiAbstractAutomaton).
Qed.

Corollary minsat_agree_as_up (V: finType) phi:
  RF -> @sat Sequence V phi <-> @sat UPSequence V phi.
Proof.
  intros R.
  rewrite <-(@sat_iff_aut_non_empty Sequence V (BuechiAbstractAutomaton R)).
  rewrite <-(@sat_iff_aut_non_empty UPSequence V UPBuechiAbstractAutomaton ).
  rewrite (formula_nfa_equal R).
  split.
  - intros [x [y M]] % nonempty_iff_match.
    exists (mkUPSeq x y). now apply match_accepted.
  - intros [[x y] M].
    exists (x +++ omega_iter y). apply M.
Qed.

Lemma sat_up_obtain (V: finType) phi : @sat UPSequence V phi -> { sigma | @satisfies UPSequence V phi sigma}.
Proof.
  apply (@ min_s1S_dec_obtain UPSequence V UPBuechiAbstractAutomaton).
Qed.

Lemma dec_satisfaction_up (V: finType) sigma (phi: MinForm V) : dec (@satisfies UPSequence V phi sigma).
Proof.
  eapply (@dec_trans _ _ _ (@formula_aut_correct UPSequence V UPBuechiAbstractAutomaton phi _)).
Unshelve.
  destruct sigma as [x y]. apply dec_up_in_lang.
Qed.