Set Implicit Arguments.

Require Import Utils.

Require Import Sequences.
Require Import MinimalS1S.
Require Import FinSets.

Require Import FiniteSemigroups.
Require Import RamseyanFactorizations.
Require Import UPSequences.

Full S1S

Full S1S has both, first and second order variables, and is this parameterized by two finite types. We give a reduction to minimal S1S that preserves satisfaction and satisfiability. We close with classical reasoning in S1S (more connectives, de Morgan laws, ...) if we assume that satisfaction satisfies XM.

Inductive Form (FVar SVar: finType):=
 | Le : FVar -> FVar -> Form FVar SVar
 | Mem : FVar -> SVar -> Form FVar SVar
 | And : Form FVar SVar -> Form FVar SVar -> Form FVar SVar
 | Neg : Form FVar SVar -> Form FVar SVar
 | FEx : FVar -> Form FVar SVar -> Form FVar SVar
 | SEx : SVar -> Form FVar SVar -> Form FVar SVar.

Ltac s1s_induction phi := induction phi as [x y| x X |phi Hs psi Ht |phi Hs |x phi Hs| X phi Hs ].

Notation "x '<2' y" := (@Le _ _ x y) (at level 40).
Notation "x 'el2' y" := (Mem x y) (at level 40).
Notation "phi '/\2' psi" := (And phi psi) (at level 43, right associativity).
Notation "'~2' phi" := (Neg phi) (at level 41).
Notation "'ex1' x , phi" := (FEx x phi) (at level 44).
Notation "'ex2' X , phi" := (SEx X phi) (at level 44).

Full S1S is parameterized by the semantics (AS and UP) as minimal S1S, too.
Section FullS1S.

  Context {Sem: AbstractSequence}.

  Notation NatSet := (Seq finType_bool).
  Definition memSet (sigma: NatSet) (n: nat) := sigma n = true.

  Notation "n 'elS' sigma" := (memSet sigma n) (at level 20).

  Global Instance memSetProper : Proper (@seq_equiv _ _ ==> eq ==> iff) memSet.
  Proof.
    intros sigma tau E n m <-. unfold memSet. now rewrite E.
  Qed.

  Definition subset (sigma tau : NatSet) := forall n, n elS sigma -> n elS tau.

  Global Instance subset_proper : Proper (@seq_equiv _ _ ==> @seq_equiv _ _ ==> iff) subset.
  Proof.
    intros sigma sigma' Es tau tau' Et. split; intros H n.
    - rewrite <-Es, <-Et. apply H.
    - rewrite Es, Et. apply H.
  Qed.

  Reserved Notation " I # J |== s" (at level 50).
  Notation "i '[' x ':=' n ']'" := (fun v => if (decision(v = x)) then n else i v) (at level 10).

  Fixpoint satisfies (FVar SVar: finType) (I:FVar -> nat)(J:SVar -> NatSet) (phi:Form FVar SVar) : Prop := match phi with
    | x <2 y => I x < I y
    | x el2 X => (I x) elS (J X)
    | phi /\2 psi => I # J |== phi /\ I # J |== psi
    | ~2 phi => ~ (I # J |== phi)
    | ex1 x, phi => exists n, (I [x := n]) # J |== phi
    | ex2 X, phi => exists M, I # (J [X := M]) |== phi
  end where " I # J |== phi" := (satisfies I J phi).


We show coincidence for full S1S.
  Section Coincidence.
    Variable (FVar SVar: finType).
    Implicit Types (I : FVar -> nat) (J : SVar -> NatSet) (N M : NatSet)(x y : FVar).
    Implicit Types (phi psi : Form FVar SVar).


    Definition sat phi := exists I J, I # J |== phi.

    Fixpoint free_fvars phi : list FVar := match phi with
      | x <2 y => [x;y]
      | x el2 X => [x]
      | phi /\2 psi => free_fvars phi ++ free_fvars psi
      | ~2 phi => free_fvars phi
      | ex1 x, phi => rem (free_fvars phi) x
      | ex2 X, phi => free_fvars phi
    end.

    Fixpoint free_svars phi : list SVar := match phi with
      | x <2 y => nil
      | x el2 X => [X]
      | phi /\2 psi => free_svars phi ++ free_svars psi
      | ~2 phi => free_svars phi
      | ex1 x, phi => free_svars phi
      | ex2 X, phi => rem (free_svars phi) X
    end.

    Lemma s1s_coincidence I J I' J' phi: (forall x, x el free_fvars phi -> I x = I' x) ->
                                      (forall X, X el free_svars phi -> J X == J' X) ->
                                      (I # J |== phi -> I' # J' |== phi).
    Proof.
      revert I J I' J'. s1s_induction phi; intros I J I' J' FE SE Sat; cbn in Sat; cbn; cbn in FE, SE.
      - repeat rewrite <-FE; cbn; auto.
      - rewrite <-FE, <- SE; cbn; auto.
      - split; [apply (Hs I J)| apply (Ht I J)] ; auto; apply Sat.
      - intros Sat'. apply Sat. apply (Hs I' J'); cbn; auto; intros z Z; symmetry; auto.
      - destruct Sat as [n Sat]. exists n. apply (Hs (I[x := n]) J); cbn; auto.
        intros y Fy. destruct decision; auto.
      - destruct Sat as [M Sat]. exists M. apply (Hs I (J[X := M])); cbn; auto.
        intros Y SY. destruct decision. reflexivity. now apply SE, in_rem_iff.
    Qed.

    Lemma s1s_coincidence' I J I' J' phi: (I # J |== phi -> (forall x, x el free_fvars phi -> I x = I' x) ->
                                      (forall X, X el free_svars phi -> J X == J' X) ->
                                      I' # J' |== phi).
    Proof.
      intros Sat EF ES. apply (s1s_coincidence EF ES Sat).
    Qed.

    Lemma s1s_coincidence_bi I J I' J' phi: (forall x, x el free_fvars phi -> I x = I' x) ->
                                      (forall X, X el free_svars phi -> J X == J' X) ->
                                      (I # J |== phi <-> I' # J' |== phi).
    Proof.
      intros F1 F2. split.
      - now apply s1s_coincidence.
      - apply s1s_coincidence; intros x Fx; symmetry; auto.
    Qed.
  End Coincidence.


Reduction from Full S1S to Minimal S1S

We first define a satisfaction relation for minimal S1S using functions as interpretation. Then we can do the reduction from full S1S to minimal S1S in two steps: first convert formulas, then convert interpretations.

Singleton Sets

For the first step we need to assume a const operation to build singleton sets.

  Context {C: WithConst Sem}.

  Fixpoint singletonSet (n: nat) := match n with
     | 0 => true ::: (const false)
     | S n => false ::: singletonSet n
  end.

  Lemma singletonSetCorrect1 n : n elS (singletonSet n).
  Proof.
    induction n; unfold memSet; cbn.
    - now rewrite nth_first.
    - rewrite nth_step. apply IHn.
  Qed.

  Lemma singletonSetCorrect2 n m : m elS (singletonSet n) -> n = m.
  Proof.
    revert m. induction n; intros m; unfold memSet; cbn; intros H.
    - destruct m; auto. exfalso. now rewrite nth_step, const_nth in H.
    - destruct m.
      + exfalso. now rewrite nth_first in H.
      + f_equal. apply IHn. now rewrite nth_step in H.
  Qed.

  Lemma sing_equiv n m : n = m <-> singletonSet n == singletonSet m.
  Proof.
    split.
    - intros E. subst n. reflexivity.
    - intros E. apply singletonSetCorrect2.
      rewrite E. apply singletonSetCorrect1.
  Qed.

  Lemma singleton_iff M n : n elS M /\ (forall m, m elS M -> n = m) <-> M == singletonSet n.
  Proof.
    split.
    - intros [H1 H2] m.
      decide (n = m) as [<-|D].
      + now rewrite H1, singletonSetCorrect1.
      + pose proof (@singletonSetCorrect2 n m) as H. unfold memSet in *.
        specialize (H2 m). cbn in *. destruct (M m).
        * exfalso. auto.
        * destruct ((singletonSet n) m) in *; auto.
    - intros H. split.
      + rewrite H. apply singletonSetCorrect1.
      + intros m. rewrite H. apply singletonSetCorrect2.
  Qed.


  Definition is_singleton M := exists n, M == singletonSet n.

  Lemma singleton_is_singleton n: is_singleton(singletonSet n).
  Proof. now exists n. Qed.

  Global Instance is_singleton_proper : Proper (@seq_equiv _ _ ==> iff) is_singleton.
  Proof.
    intros M N E. split; intros [n P]; exists n; [rewrite <-E | rewrite E]; assumption.
  Qed.

  Lemma dec_singleton_sets m M: is_singleton M -> dec (M == singletonSet m).
  Proof.
    intros Sing. decide (m elS M) as[H|H].
    - left. destruct Sing as [n Sing']. rewrite Sing' in *. now apply sing_equiv, singletonSetCorrect2.
    - right. intros Sing'. apply H.
      destruct Sing as [n Sing]. rewrite Sing in *.
      apply sing_equiv in Sing'. subst m. apply singletonSetCorrect1.
  Qed.

Reduction to Minimal S1S using Interpretations as Functions


  Reserved Notation "K |= phi" (at level 50).
  Fixpoint satisfies_fun (Var: finType) (phi:MinForm Var) (K: Var -> NatSet) : Prop := match phi with
    | X <0 Y => exists m n, m < n /\ m elS (K X) /\ n elS (K Y)
    | X <<=0 Y => subset (K X) (K Y)
    | phi /\0 psi => K |= phi /\ K |= psi
    | ~0 phi => ~ (K |= phi)
    | ex0 X, phi => exists tau, K [X := tau] |= phi
  end where "K |= phi" := (satisfies_fun phi K ).

  Lemma satisfies_fun_extensional (Var: finType) (phi: MinForm Var) (K1 K2 : Var -> NatSet) :
     (forall X, K1 X == K2 X) -> K1 |= phi -> K2 |= phi.
  Proof.
    revert K1 K2. min_s1s_ind phi; intros K1 K2 E; simpl.
    - intros [n [m [L [M1 M2]]]]. exists n, m. repeat split; auto; now rewrite <-E.
    - intros H n. rewrite <-!E. apply H.
    - intros [H1 H2]. split. apply (IHphi K1); auto. apply (IHpsi K1); auto.
    - intros N S. apply N. now apply (IHphi K2).
    - intros [tau H]. exists tau. eapply IHphi. 2: apply H.
      intros Y. destruct decision; trivial_decision. reflexivity. apply E.
  Qed.

  Lemma satisfies_fun_extensional_bi (Var: finType) (phi: MinForm Var) (K1 K2 : Var -> NatSet) :
     (forall X, K1 X == K2 X) -> K1 |= phi <-> K2 |= phi.
  Proof.
    intros E. split; apply satisfies_fun_extensional; auto. intros X. now symmetry.
  Qed.



  Section ReduceFullS1S_to_MinS1S.
    Variables (FVar SVar: finType).
    Definition Var := (FVar (+) SVar) (+) finType_unit.

Conversion of Variables

    Notation toV1 x := ((inl (inl x)) : Var).
    Notation toV2 X := ((inl (inr X) : Var)).

    Implicit Types (I: FVar -> nat)( J: SVar ->NatSet) (K : Var -> NatSet).

  Definition ItoM0 I J: Var -> NatSet := fun z => match z with
                                                   | inl (inl x) => singletonSet (I x)
                                                   | inl (inr X) => J X
                                                   | inr _ => singletonSet 0 end.

  Notation "<< i , j >>" := (ItoM0 i j) (at level 60).

  Implicit Types (x y : FVar) (X Y : SVar) (V : Var).


  Definition Sing x : MinForm Var := (ex0 (inr tt), (toV1 x) <0 (inr tt)) /\0 ~0 (toV1 x) <0 (toV1 x).

  Arguments Sing x : simpl never.

  Lemma sing_correct K x : K |= Sing x <-> is_singleton (K (toV1 x)).
  Proof.
    split.
    - intros [[sigma [n [m [L [M1 M2]]]]] N]. trivial_decision. exists n.
      apply singleton_iff. split; auto.
      intros k M. decide (n = k); auto.
      exfalso. apply N. decide (n < k); [exists n,k | exists k, n]; repeat split; auto.
    - intros [n E]. split.
      + exists (singletonSet (S n)), n, (S n). trivial_decision. rewrite E.
        repeat split; auto using singletonSetCorrect1.
      + intros [k [m [L [M1 M2]]]]. enough (k = m) by omega.
        rewrite E in M1, M2. apply singletonSetCorrect2 in M1. apply singletonSetCorrect2 in M2. congruence.
  Qed.

Conversion of Formulas

  Definition free_sings' l phi_0 := fold_right (fun x phi => Sing x /\0 phi) phi_0 l.
  Definition free_sings phi_0 := free_sings' (elem FVar) phi_0.

  Lemma free_sings'_correct K l phi_0 : K |= free_sings' l phi_0 <-> K |= phi_0 /\ (forall x, x el l -> is_singleton (K (toV1 x))).
  Proof.
    induction l as [| x l]; split.
    - simpl. intros H. split; auto. intros x F. now exfalso.
    - simpl. now intros [H _].
    - intros [H1 H2]. split.
      + now apply IHl.
      + intros y [H3 | H3].
        * subst y. now apply sing_correct.
        * now apply IHl.
    - intros [H1 H2]. split.
      + apply sing_correct, H2. auto.
      + apply IHl. split; auto.
  Qed.

  Lemma free_sings_correct K phi_0 : K |= free_sings phi_0 <-> K |= phi_0 /\ (forall x, is_singleton (K (toV1 x))).
  Proof.
    unfold free_sings. split.
    - intros [H1 H2] % free_sings'_correct. split; auto.
    - intros [H1 H2]. apply free_sings'_correct; split; auto.
  Qed.

  Fixpoint toMinMSO' phi := match phi with
    | x <2 y => (toV1 x) <0 (toV1 y)
    | x el2 X => (toV1 x) <<=0 (toV2 X)
    | phi /\2 psi => [phi] /\0 [psi]
    | ~2 phi => (~0 [phi])
    | ex1 x, phi => ex0 (toV1 x), (Sing x) /\0 [phi]
    | ex2 X, phi => ex0 (toV2 X), [phi]
  end where "[ x ]" := (toMinMSO' x).

  Definition toMinMSO phi:= free_sings (toMinMSO' phi).

  Lemma toMinMSO_correct K phi: K |= toMinMSO phi <-> K |= [phi] /\ forall x, is_singleton (K (toV1 x)).
  Proof.
    unfold toMinMSO. apply free_sings_correct.
  Qed.


  Lemma update_first_order I J x n phi: <<I [x := n],J>> |= phi <-> <<I,J>> [toV1 x := singletonSet n] |= phi .
  Proof.
    apply satisfies_fun_extensional_bi.
    intros X. simpl. destruct decision.
    - subst X. cbn. trivial_decision. reflexivity.
    - destruct X as [[ X|X]|]; try reflexivity.
      cbn in *. now rewrite decision_false by congruence.
  Qed.

  Lemma update_second_order I J X M phi: <<I,J [X := M]>> |= phi <-> <<I,J>> [toV2 X := M] |= phi .
  Proof.
    apply satisfies_fun_extensional_bi. intros Y.
    destruct decision.
    - subst Y. cbn. now trivial_decision.
    - destruct Y as [[ Y|Y]|]; try reflexivity.
      cbn in *. now trivial_decision.
  Qed.

  Arguments decision _ : simpl never.

 Lemma to_min_s1s_correct I J phi: I # J |== phi <-> <<I,J>> |= [phi].
 Proof.
    revert J I.
    s1s_induction phi; intros J I; cbn.
    - split.
      + intros Sat. exists (I x), (I y). repeat split; auto using singletonSetCorrect1.
      + intros [i [j [L [LX % singletonSetCorrect2 LY % singletonSetCorrect2]]]]. now subst i j.
    - split.
      + intros Sat n A % singletonSetCorrect2. now subst n.
      + intros Incl. apply Incl, singletonSetCorrect1.
    - now rewrite Hs, Ht.
    - now rewrite Hs.
    - split.
      + intros [n Sat]. exists (singletonSet n). split.
        * apply sing_correct. trivial_decision. apply singleton_is_singleton.
        * apply update_first_order. now apply Hs.
      + intros [M [[n P] % sing_correct Sat]].
        exists n. apply Hs, update_first_order.
        eapply satisfies_fun_extensional. 2: apply Sat.
        trivial_decision.
        intros X. destruct decision; trivial_decision; auto. reflexivity.
    - split.
      + intros [M Sat]. exists M.
        now apply update_second_order, Hs.
      + intros [M Sat]. exists M. now apply Hs, update_second_order.
  Qed.

  Definition all_sings K := (forall x, is_singleton (K (toV1 x))).

  Definition ItoM1 K : all_sings K -> (FVar -> nat).
  Proof.
    intros F x. specialize (F x).
    apply cc_nat in F.
    - destruct F as [n _]. exact n.
    - intros n. now apply dec_singleton_sets.
  Defined.
  Arguments ItoM1 K H : clear implicits.

  Definition ItoM2 K : SVar -> NatSet := fun X =>K (toV2 X).

  Notation "<| I , H />" := (ItoM1 I H) (at level 40).
  Notation "<\ I |>" := (ItoM2 I) (at level 40).

  Lemma ItoM1_agree' K (H: all_sings K) n x: K (toV1 x) == singletonSet n -> ItoM1 K H x = n.
  Proof.
    intros E. unfold ItoM1. destruct cc_nat as [m Q].
    rewrite E in Q. now apply sing_equiv.
  Qed.

  Lemma ItoM1_agree K_1 K_2 (H1: all_sings K_1) (H2: all_sings K_2) x: K_1 (toV1 x) == K_2 (toV1 x) -> ItoM1 K_1 H1 x = ItoM1 K_2 H2 x.
  Proof.
    destruct (H2 x) as [n Q]. rewrite Q. intros H.
    eapply ItoM1_agree' in H. eapply ItoM1_agree' in Q.
    now rewrite Q, H.
  Qed.

  Lemma ItoM2_agree' K X: ItoM2 K X = K (toV2 X).
  Proof.
    reflexivity.
  Qed.

  Lemma ItoM2_agree K_1 K_2 X: K_1 (toV2 X) == K_2 (toV2 X) -> ItoM2 K_1 X == ItoM2 K_2 X.
  Proof.
    intros E. apply E.
  Qed.

  Lemma to_min_s1s_complete K phi (H:forall x, is_singleton (K (toV1 x))) : K |= [phi] <-> <| K ,H /> # <\ K |> |== phi.
  Proof with trivial_decision; try easy.
    revert K H. s1s_induction phi; intros K H; cbn.
    - split.
      + intros [i [j [L [Si Sj]]]].
        erewrite 2ItoM1_agree'.
        * apply L.
        * destruct (H y) as [n Q]. rewrite Q in *.
          now apply sing_equiv, singletonSetCorrect2.
        * destruct (H x) as [n Q]. rewrite Q in *.
          now apply sing_equiv, singletonSetCorrect2.
      + intros L.
        destruct (H y) as [n Qy]. destruct (H x) as [m Qx].
        exists m, n. rewrite Qy, Qx. repeat split; auto using singletonSetCorrect1.
        erewrite 2ItoM1_agree' in L. now apply L. assumption. assumption.
    - destruct (H x) as [n Q]. rewrite Q. split; intros Sub.
      + erewrite ItoM1_agree'. 2: apply Q.
        apply Sub, singletonSetCorrect1.
      + intros m P % singletonSetCorrect2. subst m.
        erewrite ItoM1_agree' in Sub. 2: apply Q. apply Sub.
    - now rewrite Hs, Ht.
    - now rewrite Hs.
    - split.
      + intros [M [[n H1] %sing_correct H2]]...
        exists n. eapply s1s_coincidence. 3: apply Hs. 3: apply H2.
        * intros y H3. destruct decision; auto.
          -- subst y. apply ItoM1_agree'...
          -- apply ItoM1_agree...
        * intros Y H3. apply ItoM2_agree. symmetry...
      + intros [n H1]. exists (singletonSet n). split.
        * eapply sing_correct. trivial_decision. apply singleton_is_singleton.
        * eapply Hs. eapply s1s_coincidence.
          3: apply H1.
          -- intros y H3. cbn. destruct decision as [D|D].
             ++ symmetry. apply ItoM1_agree'. subst y...
             ++ apply ItoM1_agree...
          -- intros Y H3. apply ItoM2_agree...
    - cbn. split.
      + intros [M H1]. exists M. eapply s1s_coincidence.
        3: apply Hs. 3: apply H1.
        -- intros x H3. apply ItoM1_agree. symmetry...
        -- intros Y H3. cbn. destruct decision.
           ++ subst Y. rewrite ItoM2_agree'...
           ++ apply ItoM2_agree...
      + intros [M H1]. exists M. rewrite Hs. eapply s1s_coincidence.
        3: apply H1.
        -- intros x H3. apply ItoM1_agree...
        -- intros Y H3. simpl. destruct decision.
           ++ subst Y. symmetry. rewrite ItoM2_agree'...
           ++ apply ItoM2_agree...
    Unshelve.
    * intros y. simpl. destruct decision.
      ** rewrite H1. apply singleton_is_singleton.
      ** apply H.
    * intros y. destruct decision.
      ** apply singleton_is_singleton.
      ** apply H.
    * intros x. simpl...
    * intros x. simpl...
  Qed.

   End ReduceFullS1S_to_MinS1S.



Reduction to Minimal S1S using Interpretations as Sequences

Now we need to convert between interpretations as functions Var -> NatSet and interpretations as seqs for minimal S1S. This is done by zipping resp. projecting.

  Context {ZM : WithZipMap Sem}.

  Section ConvertInterpretations.


     Variable (V: finType).
     Notation B := finType_bool.

     Implicit Types (K : V -> NatSet)(sigma: Seq (finSet V)).


     Lemma update_equiv_apart X K tau : equiv_apart X (bigzip (K [X := tau])) (bigzip K).
     Proof.
       intros n Y D. symmetry. repeat (setoid_rewrite bigzip_correct). now rewrite decision_false by assumption.
     Qed.
     Lemma update_equiv_apart' X sigma tau : equiv_apart X (bigzip ((bigpi sigma) [X := tau])) sigma.
     Proof.
       intros n Y D. setoid_rewrite bigzip_correct. now rewrite decision_false, bigpi_correct by assumption.
     Qed.

     Lemma equiv_apart_update X K tau: equiv_apart X tau (bigzip K) -> bigzip (K [X := bigpi tau X]) == tau.
     Proof.
       intros H n. apply vector_eq. intros Y. rewrite bigzip_correct. destruct decision.
       + rewrite bigpi_correct. now subst Y.
       + specialize (H n Y). setoid_rewrite bigzip_correct in H. symmetry. now apply H.
     Qed.

     Lemma equiv_apart_update' X sigma tau: equiv_apart X tau sigma -> forall Y, (bigpi sigma) [X := bigpi tau X] Y == (bigpi tau) Y.
     Proof.
       intros H Y n. destruct decision.
       - now subst Y.
       - rewrite !bigpi_correct. symmetry. now apply H.
     Qed.

     Lemma function_implies_seq K phi: satisfies_fun phi K <-> MinimalS1S.satisfies phi (bigzip K).
     Proof.
       revert K. min_s1s_ind phi; intros K; cbn.
       - unfold set_mem. split; intros [n [m [L [M1 M2]]]]; exists n, m; split; auto.
         + repeat (setoid_rewrite bigzip_correct). split; auto.
         + setoid_rewrite bigzip_correct in M1. now setoid_rewrite bigzip_correct in M2.
       - unfold set_mem. split; intros H n.
         + repeat (setoid_rewrite bigzip_correct). apply H.
         + specialize (H n). now repeat (setoid_rewrite bigzip_correct in H).
       - now rewrite IHphi, IHpsi.
       - now rewrite IHphi.
       - split; intros [tau Sat].
         + exists (bigzip (K [X:=tau])). split. now apply IHphi.
           apply update_equiv_apart.
         + exists (bigpi tau X). apply IHphi. now rewrite equiv_apart_update.
    Qed.

    Lemma seq_implies_function sigma phi: MinimalS1S.satisfies phi sigma <-> satisfies_fun phi (bigpi sigma).
    Proof.
      revert sigma. min_s1s_ind phi; intros sigma; cbn.
      - unfold memSet. split; intros [n [m [L [M1 M2]]]]; exists n, m; split; auto.
         + rewrite !bigpi_correct. split; auto.
         + now rewrite bigpi_correct in M1, M2.
       - unfold set_mem. split; intros H n; specialize (H n); unfold memSet in *.
         + rewrite !bigpi_correct. apply H.
         + now rewrite !bigpi_correct in H.
       - now rewrite IHphi, IHpsi.
       - now rewrite IHphi.
       - split; intros [tau Sat].
         + exists (bigpi tau X). eapply satisfies_fun_extensional.
           * intros Y. symmetry. now apply equiv_apart_update'.
           * apply IHphi, Sat.
         + exists (bigzip ((bigpi sigma) [X := tau])). split.
           * apply IHphi. eapply satisfies_fun_extensional. 2: apply Sat.
             intros Y. now rewrite bigpi_bigzip_inv.
           * apply update_equiv_apart'.
     Qed.

   End ConvertInterpretations.


We now put both reductions together to translate full S1S to minimal S1S.

   Lemma full_s1s_to_min_s1s_correct (FVar SVar : finType) (phi: Form FVar SVar) I J : I # J |== phi <-> MinimalS1S.satisfies (toMinMSO' phi) (bigzip (ItoM0 I J)) .
   Proof.
     rewrite seq_implies_function.
     erewrite satisfies_fun_extensional_bi.
     - apply to_min_s1s_correct.
     - intros X. now rewrite <-bigpi_bigzip_inv.
   Qed.

   Lemma full_s1s_to_min_s1s_complete (FVar SVar : finType) (phi: Form FVar SVar) sigma
                                       (H : forall x, is_singleton( bigpi sigma (inl (inl x)) )) :
                    MinimalS1S.satisfies (toMinMSO' phi) sigma <-> (ItoM1 H) # (ItoM2 (bigpi sigma)) |== phi.
   Proof.
     rewrite seq_implies_function.
     rewrite to_min_s1s_complete.
     reflexivity.
   Qed.

   Lemma min_sat_iff_full_sat (FVar SVar: finType) (phi: Form FVar SVar) : MinimalS1S.sat (toMinMSO phi) <-> sat phi.
   Proof.
     split.
     - intros [sigma [Sat Free] % seq_implies_function % toMinMSO_correct].
       exists (ItoM1 Free) , (ItoM2 (bigpi sigma)).
       now apply full_s1s_to_min_s1s_complete, seq_implies_function.
     - intros [I [J Sat]].
       exists (bigzip (ItoM0 I J)). apply seq_implies_function, toMinMSO_correct. split.
       + erewrite satisfies_fun_extensional_bi.
         * apply to_min_s1s_correct, Sat.
         * intros x. now rewrite <-bigpi_bigzip_inv.
       + intros x. rewrite <-bigpi_bigzip_inv. apply singleton_is_singleton.
   Qed.

   Lemma dec_min_sat_implies_dec_full_sat (FVar SVar: finType) (phi: Form FVar SVar) : (dec (MinimalS1S.sat (toMinMSO phi))) -> (dec (sat phi)).
   Proof.
     intros. apply (dec_trans H), min_sat_iff_full_sat.
   Qed.

  Lemma min_sat_xm_implies_full_sat_xm: (forall (V: finType) (phi: MinForm V) sigma, (sat_xm (MinimalS1S.satisfies phi sigma))) ->
      (forall (FVar SVar: finType) (phi: Form FVar SVar) I J , sat_xm (I # J |== phi)).
  Proof.
    intros H FVar SVar phi I J.
    now rewrite full_s1s_to_min_s1s_correct.
  Qed.

  Definition FX := forall V_1 V_2 (phi: Form V_1 V_2) I J, sat_xm (I # J |== phi).

End FullS1S.

Notation "i '[' x ':=' n ']'" := (fun v => if (decision(v = x)) then n else i v) (at level 10).
Notation " I # J |== phi" := (satisfies I J phi) (at level 50).
Notation "n 'elS' sigma" := (memSet sigma n) (at level 20).

Results for Full S1S

Results for full S1S are obtained from minimal S1S using the previous reduction.

Section ResultsFullS1S.

We start with AS semantics ...
  Section ASSemantics.

    Existing Instance Sequence.

    Lemma full_s1s_satisfies_xm: RF ->
       forall FVar SVar (phi: Form FVar SVar) I J ,
         sat_xm (I # J |== phi).
    Proof.
      intros Ramsey.
      apply min_sat_xm_implies_full_sat_xm.
      intros V phi sigma.
      now apply satisfaction_sat_xm.
    Qed.

    Lemma full_s1s_dec: RF ->
       forall FVar SVar (phi: Form FVar SVar),
         dec (sat phi).
    Proof.
      intros Ramsey *. now apply dec_min_sat_implies_dec_full_sat, dec_min_S1S_satisfaction.
    Qed.

    Corollary RF_implies_FX: RF -> FX.
    Proof.
      intros Rf. unfold FX.
      now apply full_s1s_satisfies_xm.
    Qed.

  End ASSemantics.

... an continue with UP semantics.
  Section UPSemantics.

    Existing Instance UPSequence.

    Lemma full_s1s_dec_up_satisfies FVar SVar (phi: Form FVar SVar) I J: dec (I # J |== phi).
    Proof.
      pose proof ( to_min_s1s_correct I J phi) as H.
      symmetry in H.
      eapply (@ dec_trans _ _ _ H).
    Unshelve.
      pose proof (function_implies_seq (ItoM0 I J) (toMinMSO' phi) ) as H2.
      symmetry in H2.
      eapply (@ dec_trans _ _ _ H2).
    Unshelve.
      apply dec_satisfaction_up.
    Qed.

    Lemma full_s1s_dec_up_satisfaction FVar SVar (phi: Form FVar SVar) : dec (sat phi).
    Proof.
      apply dec_min_sat_implies_dec_full_sat, dec_min_S1S_up_satisfaction.
    Qed.

    Lemma full_s1s_up_sat_obtain FVar SVar (phi: Form FVar SVar) : sat phi -> { I : FVar -> nat & {J | I # J |== phi}}.
    Proof.
      intros [sigma [Sat Free] % seq_implies_function% toMinMSO_correct] %min_sat_iff_full_sat % sat_up_obtain.
      exists (ItoM1 Free), (ItoM2 (bigpi sigma)).
      now apply to_min_s1s_complete.
    Qed.

    Lemma full_s1s_up_sat_if_as_sat FVar SVar (phi: Form FVar SVar) :
           RF -> (sat (Sem:= Sequence) phi <-> sat (Sem := UPSequence) phi).
    Proof.
      intros Rf.
      rewrite <-!min_sat_iff_full_sat.
      now apply minsat_agree_as_up.
    Qed.

  End UPSemantics.

End ResultsFullS1S.

Derived Connectives and Formulas for S1S

We define more connectives for full S1S. We begin with connectives and formulas that can be verified constructively and later switch to classical reasoning. The connectives are used in the encoding of RP later.
We want to use a variable type for first order variables, that provides at least three distinct variables.

Class finTypeCardAtLeast3:= mkFinTypeCardAtLeast3{
    V: finType;
    x1 :V;
    x2: V;
    x3 : V;
    D1: x1 <> x2;
    D2: x2 <> x3;
    D3: x1 <> x3}.
Coercion V : finTypeCardAtLeast3 >-> finType.

Section MoreConnectives1.

  Context {Sem: AbstractSequence}.
  Context {C: WithConst Sem}.

  Notation NatSet := (Seq finType_bool).

  Context {V_1 :finTypeCardAtLeast3}{V_2: finType}.
  Hint Resolve D1 D2 D3.
  Implicit Types (x y : V_1)(X Y: V_2) (I: V_1 -> nat) (J: V_2 -> NatSet).

Identity lemmas for precise rewriting.

  Lemma el_correct x X I J : I # J |== x el2 X <-> I x elS J X.
  Proof. split; auto. Qed.

  Lemma le_correct x y I J : I # J |== x <2 y <-> I x < I y.
  Proof. split; auto. Qed.

  Lemma and_correct phi psi I J : I # J |== phi /\2 psi <-> I # J |== phi /\ I # J |== psi.
  Proof. split; auto. Qed.

  Lemma ex1_correct phi I J x : I # J |== ex1 x, phi <-> exists n, I [x := n] # J |== phi.
  Proof. reflexivity. Qed.

  Lemma neg_correct phi I J : I # J |== ~2 phi <-> ~ I # J |== phi.
  Proof. reflexivity. Qed.

Top, bottom, and other simple formulas

  Definition top : Form V_1 V_2 := ex1 x1, ex1 x2, x1 <2 x2.
  Lemma top_correct I J : I # J|== top.
  Proof.
    exists 0, 1. simpl. trivial_decision. omega.
  Qed.

  Definition bot : Form V_1 V_2 := ex1 x1, x1 <2 x1.
  Lemma bot_correct I J : ~ I # J |== bot.
  Proof.
    intros [x Sat]. simpl in Sat. trivial_decision. omega.
  Qed.

  Definition Leq x y : Form V_1 V_2 := ~2 (y <2 x).

  Lemma leq_correct x y I J : I # J |== Leq x y <-> I x <= I y.
  Proof.
    cbn. omega.
  Qed.

   Definition fresh x y :=
     if (decision (x1 = x))
     then if (decision (x1 = y))
          then x2
          else if (decision (x2 = y))
              then x3
              else x2
     else if (decision (x1 = y))
          then if (decision (x2 = x))
               then x3
               else x2
          else x1.

  Lemma fresh_correct x y : fresh x y <> x /\ fresh x y <> y.
  Proof.
    pose proof D1. pose proof D2. pose proof D3.
    unfold fresh. repeat destruct decision; split; congruence.
  Qed.

  Definition IsSucc x y : Form V_1 V_2 := x <2 y /\2 ~2 (ex1 (fresh x y), x <2 (fresh x y) /\2 (fresh x y) <2 y).
  Lemma isSuccCorrect I J x y: I # J |== IsSucc x y <-> S(I x) = I y.
  Proof.
    pose proof (fresh_correct x y) as [H1 H2].
    split; unfold IsSucc.
    - intros [SatL SatN]. decide (S (I x) = I y); auto.
      exfalso. apply SatN. exists (S (I x)). split; simpl in *; trivial_decision; omega.
    - intros . split.
      + simpl. rewrite <-H. omega.
      + intros [z [Sat1 Sat2]]. simpl in Sat1, Sat2. trivial_decision. omega.
  Qed.

  Definition IsSuccMem x X : Form V_1 V_2 := ex1 (fresh x x), (IsSucc x (fresh x x)) /\2 (fresh x x) el2 X.
  Lemma isSuccMemCorrect I J x X : I # J |== IsSuccMem x X <-> S(I x) elS (J X).
  Proof.
    pose proof (fresh_correct x x) as [H _].
    unfold IsSuccMem. split.
    - intros [y [Succ%isSuccCorrect Mem]]. cbn in *. trivial_decision. now subst y.
    - intros Mem. exists (S (I x)). split.
      + apply isSuccCorrect. now trivial_decision.
      + simpl. now trivial_decision.
  Qed.

Conjunction and existential quantification for multiple formulas/variables.

  Definition bigAnd (F: list (Form V_1 V_2)) := fold_right (@And _ _) top F.
  Lemma bigAndCorrect I J F : I # J |== bigAnd F <-> (forall phi, phi el F -> I # J|== phi).
  Proof.
    split; unfold bigAnd.
    - intros Sat phi E. induction F.
      + now exfalso.
      + destruct E as [<-|E]; simpl in Sat; tauto.
    - intros Sat. induction F.
      + apply top_correct.
      + simpl. split; auto.
  Qed.

  Definition finBigAnd (F:finType) (f: F -> Form V_1 V_2) (P : F -> Prop) {D: forall (a:F), dec (P a)} : Form V_1 V_2 := bigAnd (List.map f (FinTypes.External.filter (DecPred P) (elem F))).
  Arguments finBigAnd {F} f P {D}.

  Lemma finBigAndCorrect I J (F:finType) (f:F -> Form V_1 V_2) (P : F -> Prop) {D: forall (a:F), dec (P a)} : (I # J|== finBigAnd f P) <-> forall a, P a -> I # J |== f a.
  Proof.
    unfold finBigAnd. rewrite bigAndCorrect. split.
    - intros H a Q. apply H, in_map_iff. exists a. split; auto. now apply in_filter_iff.
    - intros H phi [x [<- [_ Q]% in_filter_iff]] % in_map_iff. auto.
  Qed.

  Definition bigEx2 (vars : list V_2) (phi: Form V_1 V_2) : Form V_1 V_2 := fold_right (fun X phi => ex2 X, phi) phi vars.
  Fixpoint bigUpdate2 (vars : list V_2) (f : V_2 -> NatSet) J := match vars with
       | [] => J
       | X::vars => (bigUpdate2 vars f J) [X := f X] end.

  Definition bigUpdate2_correct vars f J X : bigUpdate2 vars f J X = if (decision (X el vars)) then f X else J X.
  Proof with trivial_decision.
    induction vars; cbn ...
    - reflexivity.
    - destruct (decision (a = X \/ X el vars)) as [[<-|D]|D]; cbn; trivial_decision; auto.
      destruct decision as [<- |D']; auto.
  Qed.

  Lemma bigUpdate2_unchanged vars vals J: forall X, ~ X el vars -> (J X) = (bigUpdate2 vars vals J) X.
  Proof.
    intros X N. rewrite bigUpdate2_correct. now trivial_decision.
  Qed.

  Lemma bigUpdate2_update vars vals J X M: ~ X el vars -> (forall Y, (bigUpdate2 vars vals J) [X := M] Y == bigUpdate2 vars vals (J [X := M]) Y).
  Proof.
    intros N Y. rewrite !bigUpdate2_correct. destruct decision as [<-|D].
    - now trivial_decision.
    - reflexivity.
  Qed.

  Lemma bigEx2_correct I J vars phi : dupfree vars -> ( I # J |== bigEx2 vars phi <-> exists (f : V_2-> NatSet), I # (bigUpdate2 vars f J) |== phi).
  Proof.
    intros D. unfold bigEx2. split.
    - revert J. induction D as [| X vars]; intros J Sat.
      + now exists (fun _ => singletonSet 0).
      + destruct Sat as [M Sat]. destruct (IHD (J [X := M]) Sat) as [f Sat']. exists (f [X := M]).
        apply (s1s_coincidence' Sat'); auto.
        intros Y F. rewrite !bigUpdate2_correct. cbn. symmetry. now destruct decision as [[D'|D']|D']; trivial_decision.
    - revert J. induction D as [| X A]; intros J [f Sat]; auto.
       cbn. exists (f X). apply IHD. exists f.
       eapply s1s_coincidence_bi. 3: apply Sat. auto. intros Y _.
       now rewrite <-bigUpdate2_update by assumption.
  Qed.

  Arguments finType_cc {X} {p} {D}.

  Definition finBigEx2 (X:finType) (v: X -> V_2) (phi: Form V_1 V_2) : Form V_1 V_2 := bigEx2 (List.map v (elem X)) phi.
  Definition finBigUpdate2 (X:finType) (v: X -> V_2) (V: X -> NatSet) J := bigUpdate2 (List.map v (elem X))
       (fun Y => match (decision (exists (x:X), v x = Y)) with
                 |left D => V (proj1_sig (finType_cc D))
                 | right _ => singletonSet 0 end ) J.

  Lemma finBigUpdate2_unchanged (X:finType) (v: X -> V_2) (V: X -> NatSet) J Y : (forall (x:X), v x <> Y) -> (finBigUpdate2 v V J) Y = J Y.
  Proof.
    intros N. unfold finBigUpdate2. rewrite <-bigUpdate2_unchanged; auto.
    intros M. apply in_map_iff in M. firstorder.
  Qed.

  Lemma finBigUpdate2_changed (X:finType) (v: X -> V_2) (V: X -> NatSet) J (x:X) : injective v -> finBigUpdate2 v V J (v x) = (V x).
  Proof.
    intros Inj. unfold finBigUpdate2. rewrite bigUpdate2_correct. destruct decision as [D|D].
    - destruct decision as [D'|D'].
      + destruct finType_cc as [y E]. cbn. apply Inj in E. now subst y.
      + exfalso. apply D'. now exists x.
    - exfalso. apply D, in_map_iff. now exists x.
  Qed.

  Lemma finBigEx2_correct (X:finType) (v: X -> V_2) (phi:Form V_1 V_2) I J : injective v -> (I # J|== finBigEx2 v phi <-> exists (V: X -> NatSet), I # (finBigUpdate2 v V J) |== phi).
  Proof.
    intros Inj; unfold finBigEx2, finBigUpdate2.
    rewrite bigEx2_correct. split.
    - intros [f Sat]. exists (fun (x:X) => f (v x)).
      apply (s1s_coincidence' Sat); auto.
      intros Y F. rewrite !bigUpdate2_correct. destruct decision as [D'|D'].
        * destruct decision as [D|D].
          -- now destruct finType_cc as [y <-].
          -- exfalso. apply D. apply in_map_iff in D'. firstorder.
        * reflexivity.
    - intros [V Sat]. eauto.
    - apply dupfree_map; auto. apply dupfree_elements.
  Qed.

End MoreConnectives1.

Notation " 'AND' { x | P } S " := (finBigAnd (P:=(fun x => P)) (fun x => S) ) (at level 60).
Notation "x '<=2' y" := (Leq x y) (at level 40).

Classical Reasoning given FX

We now assume FX to e.g. show de Morgan laws and to define universal quantification.
Ltac s1s_contra_xm XM D := match goal with
   | H:_ |- ?I # ?J |== ?phi =>
      destruct (XM I J phi) as [D|D]; auto; exfalso
end.

Section MoreConnectives2.

  Context {V_1: finTypeCardAtLeast3}{V_2: finType}.

  Definition FAll x (phi:Form V_1 V_2) := ~2 ex1 x, ~2 phi.
  Definition SAll X (phi:Form V_1 V_2) := ~2 ex2 X, ~2 phi.
  Definition Or (phi psi: Form V_1 V_2) := ~2 (~2 phi /\2 ~2 psi).
  Definition s1s_impl (phi psi: Form V_1 V_2) := Or (~2 phi) psi.

  Definition bigOr (F: list (Form V_1 V_2)) := fold_right Or bot F.
  Definition finBigOr (F:finType) (f: F -> Form V_1 V_2) (P : F -> Prop) {D: forall (a:F), dec (P a)}: Form V_1 V_2 := bigOr (List.map f (FinTypes.External.filter (DecPred P) (elem F))).

End MoreConnectives2.

Arguments finBigOr {V_1} {V_2} {F} f P {D}.

Notation "'all1' x , y" := (FAll x y) (at level 44).
Notation "'all2' x , y" := (SAll x y) (at level 44).
Notation "x '\/2' y" := (Or x y) (at level 41, right associativity).
Notation "phi '==>2' psi " := (s1s_impl phi psi) (at level 45, right associativity).

Notation " 'OR' { x | P } S " := (finBigOr (fun x => S) (fun x => P) ) (at level 60).

Section ClassicalReasoning.

  Context{AS:AbstractSequence}.
  Context {V_1: finTypeCardAtLeast3}{V_2: finType}.
  Implicit Types (phi: Form V_1 V_2).
  Context{satisfies_xm : forall I J phi, sat_xm (I # J |== phi)}.

  Ltac s1s_contra D := s1s_contra_xm satisfies_xm D.

  Lemma or_correct I J phi psi: (I # J |== phi \/2 psi) <-> (I # J |== phi \/ I # J |== psi).
  Proof.
    unfold Or. cbn. now apply deMorgan_and.
  Qed.

  Lemma s1s_DM_neg_and I J phi psi : (I # J |== ~2 (phi /\2 psi)) <-> (I # J |== ~2 phi \/2 ~2 psi).
  Proof.
    unfold Or. cbn. now rewrite <-!double_negation; auto.
  Qed.

  Lemma impl_correct I J phi psi : I # J |== phi ==>2 psi <-> (I # J |== phi -> I # J |== psi).
  Proof.
    unfold s1s_impl. cbn. rewrite <-double_negation; auto. firstorder.
  Qed.

  Lemma bigOrCorrect I J F : I # J |== bigOr F <-> (exists phi, phi el F /\ I # J |== phi).
  Proof.
    split; unfold bigOr.
    - intros B. induction F.
      + exfalso. now apply (bot_correct (I:=I)(J:=J)).
      + apply or_correct in B. destruct B as [B|B].
        * exists a; auto.
        * destruct (IHF B) as [phi [P Q]]. exists phi. split; auto.
    - intros [s [P Q]]. induction F.
      + now exfalso.
      + destruct P as [<- | P]; apply or_correct; [left|right]; auto.
  Qed.

  Lemma finBigOrCorrect I J (F:finType) (f:F -> Form V_1 V_2) (P : F -> Prop) {D: forall (a:F), dec (P a)} : (I # J |== (finBigOr f P ) ) <-> exists a, (I # J |== f a) /\ P a.
  Proof.
    unfold finBigOr. rewrite bigOrCorrect. split.
    - intros [phi [[a [<- [_ M2]%in_filter_iff]]%in_map_iff Sat]]. now exists a.
    - intros [x [Sat Q1]]. exists (f x). split; auto. apply in_map_iff.
      exists x. split; auto. now apply in_filter_iff.
  Qed.

  Lemma all1_correct I J x phi : I # J |== all1 x, phi <-> forall k, (I [x := k]) # J |== phi.
  Proof.
    cbn. rewrite deMorgan_all. apply iff_all. intros n. now rewrite <-double_negation.
  Qed.

  Lemma all2_correct I J X phi : I # J |== all2 X, phi <-> forall N, I # (J [X := N]) |== phi.
  Proof.
    cbn. rewrite deMorgan_all. apply iff_all. intros beta. now rewrite <-double_negation.
  Qed.

  Lemma s1s_DM_forall_neg I J phi x : (I # J |== ~2 all1 x, phi) <-> (I # J |== ex1 x, ~2 phi).
  Proof.
    unfold FAll. rewrite !neg_correct. now rewrite <-double_negation.
  Qed.

  Lemma s1s_DM_exist_neg I J phi x : (I # J |== ~2(ex1 x, phi)) <-> (I # J |== all1 x, ~2 phi).
  Proof.
    unfold FAll. cbn. apply iff_neg, iff_ex. intros n. now rewrite <-double_negation.
  Qed.

End ClassicalReasoning.