Set Implicit Arguments.

Require Import Coq.Init.Nat.
Require Import Coq.Arith.Even.
Require Import Coq.Arith.Div2.

Require Import BasicDefs.
Require Import FinType.
Require Import Seqs.
Open Scope list_scope.
Close Scope string_scope.

Monadic Second Order Logic on the Successor Relation

MSO is defined on the following representation of decidable sets. This representation is later instantiated with Admissible Classes.
Class NatSetClass:= mkNatSet {
  NatSet : Type;
  memSet : nat -> NatSet -> Prop;
  decMemSet : (forall n M, dec (memSet n M));
  singletonSet: nat -> NatSet;
  singletonSetCorrect1: forall n, memSet n (singletonSet n);
  singletonSetCorrect2: forall n y, memSet y (singletonSet n) -> n = y
}.

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

Definition setEquiv {natSet:NatSetClass} (M N : NatSet) := forall n, n elS M <-> n elS N.
Notation "N =~= M" := (setEquiv N M) (at level 65).

Section Sets.
  Context{natSet:NatSetClass}.

  Global Instance decMemSetInstance n M: dec (n elS M).
  Proof.
    apply decMemSet.
  Qed.

  Global Instance set_equiv_Equivalence : Equivalence (setEquiv ).
  Proof.
    constructor.
    - now intros E.
    - intros w_1 w_2 E n. symmetry. apply E.
    - intros w_1 w_2 w_3 E_1 E_2 n. split; intros E'. now apply E_2, E_1. now apply E_1, E_2.
  Qed.

  Global Instance memSet_proper: Proper (eq ==> setEquiv ==> iff) memSet.
  Proof.
    intros n m <- N M E. split; intros I; now apply E.
  Qed.

  Definition subset (M N : NatSet) := forall n, n elS M -> n elS N.

  Global Instance subset_proper : Proper (setEquiv ==> setEquiv ==> iff) subset.
  Proof.
    intros M M' ME N N' NE. split; intros Sub.
    - intros n. rewrite <-NE, <-ME. apply Sub.
    - intros n. rewrite NE, ME. apply Sub.
  Qed.

  Lemma sing_equiv n m : n = m <-> singletonSet n =~= singletonSet m.
  Proof.
    split.
    - intros E. subst n. reflexivity.
    - intros E. specialize (E n). destruct E as [E _].
      assert (n elS singletonSet n) as H by apply singletonSetCorrect1.
      specialize (E H). now apply singletonSetCorrect2 in E.
  Qed.

End Sets.

Definition of MSO and MSO_0


Notation "i '[' x ':=' n ']'" := (fun v => if (decision(v = x)) then n else i v) (at level 10).

Definition SVar := nat.
Definition FVar := nat.

  Inductive FormMin :=
    | MLe : SVar -> SVar -> FormMin
    | MIncl: SVar -> SVar -> FormMin
    | MAnd : FormMin -> FormMin -> FormMin
    | MNeg : FormMin -> FormMin
    | MEx : SVar -> FormMin -> FormMin.

  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).

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

Notation "x '<2' y" := (Le x y) (at level 40).
Notation "x 'el2' y" := (Mem x y) (at level 40).
Notation "x '<<=2' y" := (Incl 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).

  Fixpoint free_vars (phi : FormMin) : list SVar := match phi with
    |X <0 Y => [X;Y]
    |X <<=0 Y => [X;Y]
    |phi /\0 psi => (free_vars phi) ++ (free_vars psi)
    |~0 phi => free_vars phi
    |ex0 X, phi => rem (X:=EqType SVar) (free_vars phi) X
  end.

  Lemma free_vars_and_incl phi psi: free_vars phi <<= free_vars (phi /\0 psi) /\ free_vars psi <<= free_vars (phi /\0 psi).
  Proof.
    simpl. auto.
  Qed.


Section MSO.
  Context{natSet:NatSetClass}.

Semantics of MSO_0

  Definition setless M N := (exists m n, m elS M /\ n elS N /\ m < n).


  Definition SInter := (SVar -> NatSet).

  Reserved Notation "J |= phi" (at level 50).
  Fixpoint msatisfies (J:SInter) (phi:FormMin) : Prop := match phi with
    | X <0 Y => setless (J X) (J Y)
    | X <<=0 Y => subset (J X) (J Y)
    | phi /\0 psi => J |= phi /\ J |= psi
    | ~0 phi => ~ (J |= phi)
    | ex0 X, phi => exists M, J [ X := M ] |= phi
  end where "J |= phi" := (msatisfies J phi).

  Lemma coincidence (I_1 I_2 :SInter) phi: (forall X, X el free_vars phi -> I_1 X =~= I_2 X) -> I_1 |= phi -> I_2 |= phi.
  Proof.
    revert I_1 I_2. induction phi as [X Y| X Y| phi Hs psi Ht | phi Hs | X phi Hs]; intros I_1 I_2 A Sat.
    - destruct Sat as [n [m P]]. exists n, m. repeat rewrite <-A by (simpl; tauto). tauto.
    - intros n. repeat rewrite <-A by (simpl;auto). apply Sat.
    - destruct Sat. split; [apply (Hs I_1 I_2) | apply (Ht I_1 I_2)]; cbn in A; eauto.
    - intros Sat'. apply Sat. apply (Hs I_2 I_1); auto. intros X F. symmetry. apply A, F.
    - destruct Sat as [M Sat]. exists M. apply (Hs (I_1 [X := M] ) (I_2 [X:=M])); auto.
      intros Y F. destruct decision as [<- |D]. reflexivity. apply A. cbn. now apply in_rem_iff.
  Qed.

  Lemma msatisfies_extensional I I' phi: (I === I') -> I |= phi <-> I' |= phi.
  Proof.
    intros E. split; apply coincidence; intros X F; [ | symmetry]; now rewrite E.
  Qed.

  Lemma msatisfies_set_extensional I M N V phi: M =~= N -> (I [V := M]) |= phi <-> (I [V := N]) |= phi.
  Proof.
    intros E. split; apply coincidence; intros X F; decide (X = V); auto; try reflexivity. now symmetry.
  Qed.

  Definition MNotEmpty(X:SVar) := ex0 (X + 1), X <0 (X+1).
  Definition MSingleton (X:SVar) := (MNotEmpty X) /\0 ~0 X <0 X.

  Lemma not_empty_correct I X : I |= (MNotEmpty X) <-> exists n, n elS (I X).
  Proof.
    split.
    - intros [M [x [y P]]]. trivial_decision. now exists x.
    - intros [x P]. exists (singletonSet (x+1)), x, (x+1). trivial_decision. repeat split.
      + assumption.
      + apply singletonSetCorrect1.
      + omega.
  Qed.

  Lemma singleton_correct I X n : (setEquiv (I X) (singletonSet n)) -> I |= (MSingleton X).
  Proof.
    intros Sing. split.
    - apply not_empty_correct. exists n. rewrite Sing. apply singletonSetCorrect1.
    - intros [x [y [Ex [Ey L]]]]. rewrite Sing in Ex, Ey.
      apply singletonSetCorrect2 in Ex. apply singletonSetCorrect2 in Ey. omega.
  Qed.

  Lemma singleton_correct2 I X: I |= (MSingleton X) -> exists x, setEquiv (I X) (singletonSet x).
  Proof.
    intros [NotEmpty Sing].
    apply not_empty_correct in NotEmpty. destruct NotEmpty as [x P]. exists x.
    intros y. split.
    - intros Q. decide (y = x) as [D|D].
      + subst y. apply singletonSetCorrect1.
      + destruct Sing. decide (x < y).
        * exists x, y; repeat split; oauto.
        * exists y, x; repeat split; oauto.
    - intros Q. apply singletonSetCorrect2 in Q. now subst y.
  Qed.

Semantics of MSO


  Definition FInter := (FVar -> nat).

  Implicit Types (I : FInter) (J : SInter) (N M : NatSet)(x y : FVar)(X Y : SVar).


Reserved Notation " I # J |== s" (at level 50).

Fixpoint satisfies (I:FInter)(J:SInter) (phi:Form) : Prop := match phi with
  | x <2 y => I x < I y
  | x el2 X => (I x) elS (J X)
  | X <<=2 Y => subset (J X) (J Y)
  | 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).

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

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

Definition mso_equiv (phi psi:Form) := forall I J, I # J |== phi <-> I # J |== psi.

Fixpoint free_fvars (phi:Form) : list FVar := match phi with
  | x <2 y => [x;y]
  | x el2 X => [x]
  | X <<=2 Y => nil
  | 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:Form) : list SVar := match phi with
  | x <2 y => nil
  | x el2 X => [X]
  | X <<=2 Y => [X;Y]
  | 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 mso_coincidence I J I' J' phi: (forall (x:SVar), x el free_fvars phi -> I x = I' x) ->
                                      (forall (X:SVar), X el free_svars phi -> J X =~= J' X) ->
                                      (I # J |== phi -> I' # J' |== phi).
Proof.
  revert I J I' J'. mso_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.
  - repeat rewrite <-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. now apply FE, in_rem_iff.
  - 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 mso_coincidence' I J I' J' phi: (I # J |== phi -> (forall (x:SVar), x el free_fvars phi -> I x = I' x) ->
                                      (forall (X:SVar), X el free_svars phi -> J X =~= J' X) ->
                                      I' # J' |== phi).
Proof.
  intros Sat EF ES. apply (mso_coincidence EF ES Sat).
Qed.

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

Definition SInterExtensional J J' := forall X, J X =~= J' X.
Notation "J =~~= K" := (SInterExtensional J K) (at level 65).

Global Instance SInter_ext_equiv: Equivalence SInterExtensional.
Proof.
  constructor.
  - intros J X. reflexivity.
  - intros J J' E X. now rewrite (E X).
  - intros J1 J2 J3 E1 E2 X. rewrite (E1 X). now rewrite <-(E2 X).
Qed.

Global Instance update_proper: Proper (SInterExtensional ==> eq ==> setEquiv ==> SInterExtensional) (fun J X M => J [X := M]).
Proof.
  intros J J' EJ X X' <- M M' EM Y. destruct decision; auto.
Qed.

Global Instance f_weak_coincidence: Proper (@seq_equal nat ==> SInterExtensional ==> eq ==> iff) satisfies .
Proof.
  intros I I' E1 J J' E2 phi s' <-. split; apply mso_coincidence; intros X _; cbn; auto. symmetry. apply E2.
Qed.

Reduction from MSO to MSO_0

Conversion of Variables

  Definition toV1 x :SVar := x+x.
  Definition toV2 x :SVar := S(x+x).

  Lemma toV1Double x : toV1 x = double x.
  Proof. reflexivity.
  Qed.

  Lemma toV2Double x : toV2 x = S(double x).
  Proof. reflexivity.
  Qed.

  Lemma toV1_even x : even (toV1 x).
  Proof.
    unfold toV1. apply even_equiv. exists x. omega.
  Qed.

  Lemma toV2_not_even x : ~even (toV2 x).
  Proof.
    unfold toV2. intros D. apply even_equiv in D. destruct D as [y D]. omega.
  Qed.

  Lemma fromToSVar X : div2 (toV2 X) = X.
  Proof.
    unfold toV2. rewrite_eq (S (X + X) = S ( 2 * X)). apply div2_double_plus_one.
  Qed.

  Lemma fromToFVar x : div2 (toV1 x) = x.
  Proof.
    unfold toV1. rewrite_eq (x + x = 2 * x). apply div2_double.
  Qed.

  Lemma divToV1 x: even x -> (toV1 (div2 x)) = x.
  Proof.
    intros E. unfold toV1. now rewrite (even_double x E) at 3.
  Qed.

  Lemma divToV2 x: ~even x -> (toV2 (div2 x)) = x.
  Proof.
    intros E. unfold toV2. rewrite (odd_double x) at 3. reflexivity.
    apply odd_equiv. destruct(Nat.Even_or_Odd x);auto. exfalso. now apply E, even_equiv.
  Qed.

  Lemma toV1Injective x y : x =y <-> toV1 x = toV1 y.
  Proof.
    split. now intros <-. unfold toV1. unfold FVar in *. omega.
  Qed.

  Lemma toV1Different x y : x <> y <-> toV1 x <> toV1 y.
  Proof.
    split; intros D E; apply D. now apply toV1Injective. now apply toV1Injective in E.
  Qed.

  Lemma toV2Injective x y : x =y <-> toV2 x = toV2 y.
  Proof.
    split. now intros <-. unfold toV2. unfold FVar in *. omega.
  Qed.

  Lemma toV2Different x y : x <> y <-> toV2 x <> toV2 y.
  Proof.
    split; intros D E; apply D. now apply toV2Injective. now apply toV2Injective in E.
  Qed.

  Instance dec_even n : dec (even n).
  Proof.
    destruct (even_odd_dec n) as [D|D].
    - now left.
    - right. intros E. apply even_equiv in E. apply odd_equiv in D.
      destruct D as [x D]. destruct E as [y E].
      omega.
  Defined.

  Definition ItoM0 I J: SInter := fun n => if (decision (even n))
                                                          then singletonSet(I (div2 n))
                                                          else J (div2 n).
  Notation "<< i , j >>" := (ItoM0 i j) (at level 60).

  Lemma ItoM0Fvar I J x : <<I,J>> (toV1 x) = singletonSet (I x).
  Proof.
    unfold ItoM0. rewrite decision_true by apply toV1_even. now rewrite fromToFVar.
  Qed.

  Lemma ItoM0Svar I J X : <<I,J>> (toV2 X) = (J X).
  Proof.
    unfold ItoM0. rewrite decision_false by apply toV2_not_even. now rewrite fromToSVar.
  Qed.

  Lemma first_order_var_singleton I J x : <<I,J>> |= (MSingleton (toV1 x)).
  Proof.
    apply (singleton_correct (n := I x)(X := toV1 x)).
    now rewrite ItoM0Fvar.
  Qed.

  Lemma second_order_var_singleton J x n : J [toV1 x := singletonSet n] |= (MSingleton (toV1 x)).
  Proof.
    apply (singleton_correct (n:=n) (X:=toV1 x)).
    now rewrite decision_true by reflexivity.
  Qed.

Conversion of Formulas

  Fixpoint free_sings' (l: list FVar) (phi:FormMin):= match l with
    | [] => phi
    | x::l => MSingleton (toV1 x) /\0 (free_sings' l phi)
  end.

  Lemma free_sings'_correct J l phi : J |= free_sings' l phi <-> J |= phi /\ forall x, x el l -> J |= MSingleton (toV1 x).
  Proof.
    split.
    - intros F. induction l.
      + cbn in F. split; auto. now intros.
      + destruct F as [S F]. split.
        * now apply IHl.
        * intros x [L|L].
          -- now subst x.
          -- now apply IHl.
    - intros [Sat A]. induction l.
      + apply Sat.
      + split.
        * apply A. auto.
        * apply IHl. auto.
  Qed.

  Definition free_sings (s':Form) (phi:FormMin) := free_sings' (free_fvars s') phi.


  Notation list_are_sings l I := (forall x, x el l -> I |= MSingleton (toV1 x)).
  Notation free_are_sings I phi := (list_are_sings (free_fvars phi) I ).

  Lemma free_sings_correct J s' phi: J |= free_sings s' phi <-> J |= phi /\ free_are_sings J s'.
  Proof.
    unfold free_sings. apply free_sings'_correct.
  Qed.

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

  Lemma singleton_interpretation I J x n phi: <<I [x := n],J>> |= phi <-> <<I,J>> [toV1 x := singletonSet n] |= phi .
  Proof.
    apply msatisfies_extensional.
    intros k. unfold ItoM0.
    decide (even k) as [E|E]; decide (k = toV1 x) as [D|D]; trivial_decision.
    - subst k. rewrite fromToFVar. simpl. now trivial_decision.
    - simpl. decide (Nat.div2 k = x) as [D'|D'].
      + exfalso. subst x. rewrite toV1Double in D. rewrite <-(even_double k)in D by auto. tauto.
      + now rewrite !decision_false by auto.
   - exfalso. subst k. apply E. apply toV1_even.
   - reflexivity.
  Qed.

  Lemma second_order_interpretation I J X M phi: <<I,J [X := M]>> |= phi <-> <<I,J>> [toV2 X := M] |= phi .
  Proof.
    apply msatisfies_extensional.
    intros k. unfold ItoM0.
    decide (even k) as [E|E]; decide (k = toV2 X) as [D|D]; trivial_decision.
    - exfalso. subst k. apply (toV2_not_even E).
    - reflexivity.
    - subst k. rewrite fromToSVar. simpl. now trivial_decision.
    - simpl. decide (Nat.div2 k = X) as [D'|D'].
      + exfalso. subst X. rewrite toV2Double in D. rewrite <-odd_double in D. tauto. now destruct (even_or_odd k).
      + now trivial_decision.
  Qed.

 Lemma to_min_mso_correct I J phi : I # J |== phi <-> <<I,J>> |= [phi].
  Proof.
    revert J I.
    induction phi as [x y| x X| X Y |phi Hs psi Ht |phi Hs |x phi Hs| X phi Hs ]; intros J I.
    - split.
      + intros Sat. split; unfold ItoM0.
        * exists (I x), (I y); repeat rewrite decision_true by apply toV1_even. repeat split.
          -- rewrite fromToFVar. apply singletonSetCorrect1.
          -- rewrite fromToFVar. apply singletonSetCorrect1.
          -- apply Sat.
        * split; apply first_order_var_singleton.
      + intros [[i [j [LX [LY L]]]] _].
        rewrite ItoM0Fvar in LX, LY.
        apply singletonSetCorrect2 in LX. apply singletonSetCorrect2 in LY.
        subst i. now subst j.
    - split.
      + intros Sat. split.
        * intros n A. rewrite ItoM0Fvar in A. apply singletonSetCorrect2 in A.
          rewrite ItoM0Svar. simpl in Sat. now subst n.
        * apply first_order_var_singleton.
      + intros [Incl _].
        specialize (Incl (I x)). rewrite ItoM0Fvar,ItoM0Svar in Incl.
        apply Incl. apply singletonSetCorrect1.
    - split.
      + intros Sub. simpl. unfold ItoM0. repeat rewrite decision_false by apply toV2_not_even. repeat rewrite fromToSVar. apply Sub.
      + intros Sub. simpl. simpl in *. unfold ItoM0 in *. repeat rewrite decision_false in Sub by apply toV2_not_even. rewrite !fromToSVar in Sub. apply Sub.
    - split; intros Sat; (split; [apply Hs | apply Ht]); apply Sat.
    - split.
      + intros Sat. simpl. apply free_sings_correct. split.
        * intros Sat'. now apply Sat, Hs.
        * auto using first_order_var_singleton.
      + intros [Sat _] % free_sings_correct Sat'. now apply Sat, Hs.
    - split.
      + intros [n Sat]. exists (singletonSet n). split.
        * apply second_order_var_singleton.
        * apply singleton_interpretation. now apply Hs.
      + intros [M [Sing Sat]]. apply singleton_correct2 in Sing.
        destruct Sing as [n P].
        exists n. apply Hs. trivial_decision.
        apply singleton_interpretation.
        apply msatisfies_set_extensional with (M:=M); auto.
    - split.
      + intros [M Sat]. exists M.
        now apply second_order_interpretation, Hs.
      + intros [M Sat]. exists M. apply Hs. now apply second_order_interpretation.
  Qed.

  Lemma free_vars_singleton (I:SInter) (Y Z:SVar) M : Z <> Y -> forall X, X el free_vars (MSingleton Y) -> (I[Z := M]) X =~= I X.
  Proof.
    intros ZY X F. cbn in F. trivial_decision. cbn. destruct decision.
    - subst X. apply in_app_iff in F. destruct F as [[F|F]|[F|[F|F]]]; exfalso; oauto.
    - reflexivity.
  Qed.

  Lemma to_min_mso_sings phi : forall J, J |= [phi] -> free_are_sings J phi.
  Proof.
    intros I Sat. intros z F. revert I Sat.
    mso_induction phi; cbn in F; intros I Sat.
    - destruct F as [F|[F|F]]; try (now exfalso); subst z; apply Sat.
    - destruct F as [F|F]; try (now exfalso). subst z. apply Sat.
    - now exfalso.
    - apply in_app_iff in F. destruct F; [apply Hs | apply Ht]; auto; apply Sat.
    - cbn in Sat. apply free_sings_correct in Sat. apply Sat, F.
    - destruct Sat as [n [_ Sat]]. apply (in_rem_iff z) in F. destruct F as [F N]. specialize (Hs F ( I [toV1 x := n]) Sat).
      apply (coincidence (I_1 := I [toV1 x := n])); auto. apply free_vars_singleton. unfold toV1. omega.
    - destruct Sat as [M Sat]. specialize (Hs F (I [toV2 X := M]) Sat).
      apply (coincidence (I_1 := I [toV2 X := M])); auto. apply free_vars_singleton. unfold toV2, toV1. omega.
  Qed.

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

Conversion of MSO_0 to MSO interpretations

  Definition ItoM1 l J : list_are_sings l J -> FInter.
  Proof.
    intros F.
    intros x. decide (x el l) as [D|D].
      + specialize (F x D). apply singleton_correct2 in F. apply cc_nat in F.
        * destruct F as [n _]. exact n.
        * intros n. now apply dec_singleton_sets.
      + exact 0.
  Defined.
  Definition ItoM2 J : SInter := fun X =>J (toV2 X).

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

  Lemma fromMinMSOInter_svar J X : J (toV2 X) =~= <\ J |> X.
  Proof.
    unfold ItoM2. cbn. reflexivity.
  Qed.

  Lemma fromMinMSOInter_fvar l J x (F: list_are_sings l J): x el l -> J (toV1 x) =~= singletonSet (<| F /> x).
  Proof.
    intros Fx. unfold ItoM1. cbn. destruct decision as [D|D].
    - now destruct cc_nat.
    - now exfalso.
  Qed.

  Lemma ItoM2_fvar_update J x n : <\ J |> =~~= <\ J [toV1 x := n] |>.
  Proof.
    intros X. unfold ItoM2. unfold toV2, toV1. now rewrite decision_false by comega.
  Qed.

  Ltac destruct_sig F v:= match type of F with
      | sig _ => destruct F as [v F]
      | _ => id
      end.

  Ltac prove_sings F:= match goal with
      | |-sig ?F' => match type of F' with
                   | ?H -> ?J =>
                            (assert H as F by now apply to_min_mso_sings); exists F end
      | _ => id
  end.

  Lemma sat_fromMinMSO l1 l2 J (F1: list_are_sings l1 J) (F2: list_are_sings l2 J) phi :
        free_fvars phi <<= l1 -> free_fvars phi <<= l2 ->
        <| F1 /> # <\ J |> |== phi -> <| F2 /> # <\ J |> |== phi.
  Proof.
    intros Sub1 Sub2 Sat.
    apply (mso_coincidence (I := ItoM1 F1)(J:=ItoM2 J)); auto.
    - intros x Fx. apply sing_equiv. now rewrite <-!fromMinMSOInter_fvar by auto.
    - intros X FX. reflexivity.
  Qed.

  Lemma sat_fromMinMSO_update x n N l1 l2 J (F: list_are_sings l1 J) (F': list_are_sings l2 (J [toV1 x := N]) ) phi :
      rem (free_fvars phi) x <<= l1 -> free_fvars phi <<= l2 -> N =~= singletonSet n ->
      <| F /> [x := n] # <\ J |> |== phi <-> <| F' /> # <\J [toV1 x := N] |> |== phi.
  Proof.
    intros Sub1 Sub2 Sing. apply mso_coincidence_bi.
    - intros y Fy. apply sing_equiv. destruct decision as [<-|D].
      + rewrite <-Sing, <-fromMinMSOInter_fvar by auto. now trivial_decision.
      + rewrite <-!fromMinMSOInter_fvar by auto. now rewrite decision_false by now apply toV1Different in D.
    - intros X FX. now rewrite <-(ItoM2_fvar_update J x N X).
  Qed.

  Lemma sat_fromMinMSO_s_update X N l1 l2 J (F: list_are_sings l1 J) (F': list_are_sings l2 (J [toV2 X := N]) ) phi :
      free_fvars phi <<= l1 -> free_fvars phi <<= l2 ->
      <| F /> # <\ J |> [X := N] |== phi <-> <| F' /> # <\ J [toV2 X := N] |> |== phi.
  Proof.
    intros Sub1 Sub2. apply mso_coincidence_bi.
    - intros y Fy. apply sing_equiv. rewrite <-!fromMinMSOInter_fvar by auto. unfold toV1, toV2. now rewrite decision_false by comega.
    - intros Y FY. rewrite <-(fromMinMSOInter_svar (J [toV2 X := N]) Y). destruct decision as [<-|D].
      + trivial_decision. reflexivity.
      + rewrite decision_false by now apply toV2Different in D. now rewrite <-fromMinMSOInter_svar.
  Qed.

  Lemma freeVarInSingleton X x: X el free_vars (MSingleton (toV1 x)) -> X = toV1 x.
  Proof.
    intros F. cbn in F. trivial_decision. destruct F as [FY|[FY|[FY|FY]]]; unfold toV1; try (now subst X; cbn). now exfalso.
  Qed.

  Lemma supdate_preserves_singleton J l x X M : list_are_sings l J -> x el l -> J [toV2 X := M] |= MSingleton (toV1 x).
  Proof.
    intros Sing Fl.
    apply (coincidence (I_1 := J)).
    - intros Y FY. rewrite decision_false. reflexivity. apply freeVarInSingleton in FY. subst Y. unfold toV1, toV2. comega.
    - apply Sing, Fl.
  Qed.

  Lemma fupfate_preserves_singleton J l x y n M : list_are_sings (rem l x) J -> y el l -> M =~= singletonSet n -> J [toV1 x := M] |= MSingleton (toV1 y).
  Proof.
    intros Sing yl SingM. decide (y = x) as [<-|D].
    - apply singleton_correct with (n:=n). now trivial_decision.
    - apply (coincidence (I_1:=J)).
      + intros X FX. rewrite decision_false. reflexivity. apply freeVarInSingleton in FX. subst X. now apply toV1Different in D.
      + apply Sing. apply in_rem_iff. auto.
  Qed.

  Lemma to_min_mso_complete J phi : {F: free_are_sings J phi | <| F /> # <\ J |> |== phi} <-> J |= [phi].
  Proof.
    revert J.
    mso_induction phi; intros J ; split; intros Sat; try (destruct_sig Sat F + prove_sings F).
            - split.
              + exists (<| F /> x), (<| F /> y). repeat split; auto;
                rewrite (fromMinMSOInter_fvar F); try (cbn; auto); apply singletonSetCorrect1.
              + split; apply F; cbn; auto.
            - red. destruct Sat as [[n [m [Sn [Sm l]]]] _].
              rewrite (fromMinMSOInter_fvar F) in Sn by (cbn;auto). rewrite (fromMinMSOInter_fvar F) in Sm by (cbn;auto).
              apply singletonSetCorrect2 in Sn. apply singletonSetCorrect2 in Sm. now rewrite Sm, Sn.
            - split.
              + red in Sat. red. rewrite (fromMinMSOInter_fvar F) by (cbn;auto).
                intros n P. apply singletonSetCorrect2 in P. now subst n.
              + split; apply F; cbn; auto.
            - red. destruct Sat as [Sub Sing]. red in Sub.
              rewrite (fromMinMSOInter_fvar F) in Sub by (cbn;auto).
              apply Sub, singletonSetCorrect1.
            - red in Sat. red. red. now rewrite (fromMinMSOInter_svar J Y), (fromMinMSOInter_svar J X).
            - red in Sat. red in Sat. red. now rewrite <-(fromMinMSOInter_svar J Y), <-(fromMinMSOInter_svar J X).
            - split.
              + apply Hs. assert (free_are_sings J phi) as F'. { intros x Fx. apply F. cbn. auto. }
          exists F'. apply (sat_fromMinMSO (l2:= free_fvars phi) (l1:= free_fvars (phi /\2 psi)) (F1:=F)); cbn; auto. apply Sat.
              + apply Ht. assert (free_are_sings J psi) as F'. { intros x Fx. apply F. cbn. auto. }
          exists F'. apply (sat_fromMinMSO (l2:= free_fvars psi) (l1:= free_fvars (phi /\2 psi)) (F1:=F)); cbn; auto. apply Sat.
            - destruct Sat as [SatS SatT].
        specialize (Hs J). specialize (Ht J).
        destruct Hs as [_ Hs]. destruct (Hs SatS) as [Fs SatS']. destruct Ht as [_ Ht]. destruct (Ht SatT) as [Ft SatT']. split.
        + apply (sat_fromMinMSO (l1:= free_fvars phi)(l2:=free_fvars (phi /\2 psi))(F1:=Fs)); cbn; auto.
        + apply (sat_fromMinMSO (l1:= free_fvars psi)(l2:=free_fvars (phi /\2 psi))(F1:=Ft)); cbn; auto.
      - red. red. rewrite free_sings_correct. split; auto.
        intros Sat'. apply Sat. specialize (Hs J). destruct Hs as [_ Hs]. destruct (Hs Sat') as [F' SatS].
        apply (sat_fromMinMSO (l1:= free_fvars phi) (l2:= free_fvars (~2 phi)) (F1:=F')); cbn; auto.
      - intros Sat'. red in Sat. red in Sat. rewrite free_sings_correct in Sat. destruct Sat as [Sat _].
        apply Sat, Hs. assert (free_are_sings J phi) as F'. { intros x Fx. apply F. cbn; auto. }
        exists F'. apply (sat_fromMinMSO (l1:= free_fvars phi) (l2:= free_fvars (~2 phi)) (F1:=F)); cbn; auto.
      - destruct Sat as [n Sat]. exists (singletonSet n). split.
        + apply second_order_var_singleton.
        + apply Hs. assert (free_are_sings (J [toV1 x := singletonSet n]) phi) as F'.
          {intros y Fy. apply (fupfate_preserves_singleton (l:= free_fvars phi) (J:=J)(n:=n)); cbn; auto. reflexivity. }
          exists F'. apply (sat_fromMinMSO_update F F' (n:=n)) ; cbn;auto; reflexivity.
      - destruct Sat as [N [Sing Sat]]. apply singleton_correct2 in Sing. destruct Sing as [n Sing]. trivial_decision.
        exists n. specialize (Hs (J [toV1 x := N])). destruct Hs as [_ Hs]. destruct (Hs Sat) as [F' SatS'].
        apply (sat_fromMinMSO_update F F'); cbn; auto.
      - destruct Sat as [M Sat]. exists M. apply Hs.
        assert (free_are_sings (J [toV2 X := M]) phi) as F'. { intros x Fx. apply (supdate_preserves_singleton (l:= free_fvars (ex2 X, phi)) (J:=J)); cbn; auto. }
        exists F'. apply (sat_fromMinMSO_s_update F F'); cbn; auto.
      - destruct Sat as [M Sat]. exists M.
        specialize (Hs (J [toV2 X := M])). destruct Hs as [_ Hs]. destruct (Hs Sat) as [F' SatS].
        apply (sat_fromMinMSO_s_update F F'); cbn; auto.
  Qed.

  Lemma mso_xm_satisfies: (forall J phi, J |= phi \/ ~ J |= phi) -> forall I J phi, I # J |== phi \/ ~(I # J |== phi).
  Proof.
    intros xm_satisfies J I phi.
    destruct (xm_satisfies (<<J,I>>) ([phi])) as [Sat | NSat].
    - left. now apply to_min_mso_correct.
    - right. intros Sat. now apply NSat, to_min_mso_correct.
  Qed.

  Definition minsat (phi: FormMin) := exists J, J |= phi.

  Lemma sat_iff_minsat phi : sat phi <-> minsat ([phi]).
  Proof.
    split.
    - intros [I [J Sat % to_min_mso_correct]]. now exists (<<I,J>>).
    - intros [I [F Sat] % to_min_mso_complete]. now exists (<|F/>), (<\I|>).
  Qed.

End ReducablityOfFirstOrderVariables.

Derived Connectives and Formulas for MSO


Section SyntacticSugarFirstOrder.

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

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

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

  Lemma leq_correct x y I J : I # J |== Leq x y <-> I x <= I y.
  Proof.
    split; unfold Leq.
    - intros H; cbn in H; omega.
    - intros Leq. cbn. omega.
  Qed.

  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.

  Definition bigAnd (F: list Form) := 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 B phi E. induction F.
      + now exfalso.
      + destruct E as [<-|E]; simpl in B; tauto.
    - intros B. induction F.
      + apply top_correct.
      + simpl. split; auto.
  Qed.

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

  Lemma finBigAndCorrect I J (F:finType) (f:F -> Form) (P : F -> Prop) {D: forall (a:F), dec (P a)} : (I # J|== finBigAnd f P) <-> forall a, P a -> I # J |== f a.
  Proof.
    split; unfold finBigAnd.
    - intros Sat x Q. rewrite bigAndCorrect in Sat. apply Sat. apply in_map_iff. exists x. split; auto. apply in_filter_iff; split; auto.
    - intros Sat. rewrite bigAndCorrect. intros phi In. apply in_map_iff in In. destruct In as [x [Q1 Q2]]. subst phi. apply Sat. now apply in_filter_iff in Q2.
  Qed.


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

  Definition bigUpdate2Spec vars f J X : bigUpdate2 vars f J X = if (decision (X el vars)) then f X else J X.
  Proof.
    induction vars.
    - cbn. now trivial_decision.
    - destruct (decision (X el a::vars)) as [[->|D] |D].
      + cbn. now trivial_decision.
      + trivial_decision. decide (X = a) as [<-|D'].
        * cbn. now trivial_decision.
        * cbn. trivial_decision. now rewrite <-IHvars.
      + cbn. trivial_decision. destruct decision as [<-|D'].
        * exfalso. auto.
        * now rewrite <-IHvars.
  Qed.

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

  Lemma bigUpdate2_update vars vals J X M: ~ X el vars -> (bigUpdate2 vars vals J) [X := M] =~~= bigUpdate2 vars vals (J [X := M]) .
  Proof.
    intros N Y. rewrite !bigUpdate2Spec. 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 : SVar-> NatSet), I # (bigUpdate2 vars f J) |== phi).
  Proof.
    intros D. unfold bigEx2. split.
    - revert J. induction D as [| X vars]; intros J Sat.
      + simpl in Sat. exists (fun _ => singletonSet 0). now cbn.
      + destruct Sat as [M Sat]. destruct (IHD (J [X := M]) Sat) as [f Sat']. exists (f [X := M]).
        cbn. trivial_decision. apply (mso_coincidence' Sat'); auto.
        intros Y F. rewrite !bigUpdate2Spec. destruct decision; destruct decision as [<- |D']; try reflexivity. now exfalso.
    - revert J. induction D as [| X A]; intros J [f Sat].
      + assumption.
      + cbn. exists (f X). cbn in Sat. apply IHD. exists f. now rewrite <-bigUpdate2_update by assumption.
  Qed.

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

  Definition finBigEx2 (X:finType) (v: X -> SVar) (phi: Form) : Form := bigEx2 (map v (elem X)) phi.
  Definition finBigUpdate2 (X:finType) (v: X -> SVar) (V: X -> NatSet) J := bigUpdate2 (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 -> SVar) (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.
    - reflexivity.
    - intros M. apply in_map_iff in M. firstorder.
  Qed.

  Lemma finBigUpdate2_changed (X:finType) (v: X -> SVar) (V: X -> NatSet) J (x:X) : injective v -> finBigUpdate2 v V J (v x) = (V x).
  Proof.
    intros Inj. unfold finBigUpdate2. rewrite bigUpdate2Spec. 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 -> SVar) (phi:Form) 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. split.
    - intros Sat. rewrite bigEx2_correct in Sat.
      + destruct Sat as [f Sat]. exists (fun (x:X) => f (v x)). apply (mso_coincidence' Sat); auto.
        intros Y F. rewrite !bigUpdate2Spec. 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.
      + apply dupfree_map; auto. apply dupfree_elements.
    - intros [V Sat]. apply bigEx2_correct.
      + apply dupfree_injective_map; auto. apply dupfree_elements.
      + exists (fun Y => match (decision (exists (x:X), v x = Y)) with
                 |left D => V (proj1_sig (finType_cc D))
                 | right _ => singletonSet 0 end ). apply Sat.
  Qed.

  Definition IsSucc x y : Form := x <2 y /\2 ~2 (ex1 (x+y+1), x <2 (x+y+1) /\2 (x+y+1) <2 y).
  Lemma isSuccCorrect I J x y: I # J |== IsSucc x y <-> S(I x) = I y.
  Proof.
    split; unfold IsSucc.
    - intros [SatL SatN]. decide (S (I x) = I y).
      + assumption.
      + 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 := ex1 (x+1), (IsSucc x (x+1)) /\2 (x+1) el2 X.
  Lemma isSuccMemCorrect I J x X : I # J |== IsSuccMem x X <-> S(I x) elS (J X).
  Proof.
    split; unfold IsSuccMem.
    - intros [y [Succ Mem]]. apply isSuccCorrect in Succ. simpl in Mem, Succ. trivial_decision. now subst y.
    - intros Mem. exists (S (I x)). split.
      + apply isSuccCorrect. now trivial_decision.
      + simpl. now trivial_decision.
  Qed.

  Definition ZeroEl (X:SVar) : Form := ex1 0, 0 el2 X /\2 ~2 ex1 1, 1 <2 0.

  Lemma zeroElCorrect I J X : I # J|== ZeroEl X <-> 0 elS (J X).
  Proof.
    split; unfold ZeroEl.
    - intros [z [E N]]. simpl in *. trivial_decision. decide (z = 0).
      + now subst z.
      + exfalso. apply N. exists 0. trivial_decision. omega.
    - intros E. exists 0. split.
      + simpl. now trivial_decision.
      + intros [z P]. simpl in *. trivial_decision. omega.
  Qed.

End SyntacticSugarFirstOrder.

End MSO.

Notation "N =~= M" := (setEquiv N M) (at level 65).
Notation "i '[' x ':=' n ']'" := (fun v:SVar => if (decision(v = x)) then n else i v) (at level 10).

Notation " I # J |== phi" := (satisfies I J phi) (at level 50).
Notation "I |= phi" := (msatisfies I phi) (at level 50).

Notation " 'AND' { x | P } S " := (finBigAnd (P:=(fun x => P)) (fun x => S) ) (at level 60).
Notation " 'AND' { ( a , b ) | P } S " := (finBigAnd (P:=(fun z => match z with (a,b) => P end)) (fun z => match z with (a,b) => S end) ) (at level 60).

Notation "x '<=2' y" := (Leq x y) (at level 40).

Notation "J =~~= K" := (SInterExtensional J K) (at level 65).

More Connectives and Lemmas assumming Classical Behavior of MSO

Ltac mso_contra_xm XM D := match goal with
   | H:_ |- ?I # ?J |== ?phi =>
      destruct (XM I J phi) as [D|D]; auto; exfalso
end.

Definition FAll (x:FVar)(phi:Form) := ~2 ex1 x, ~2 phi.
Notation "'all1' x , y" := (FAll x y) (at level 44).
Definition SAll (X:SVar)(phi:Form) := ~2 ex2 X, ~2 phi.
Notation "'all2' x , y" := (SAll x y) (at level 44).
Definition Or (phi psi: Form) := ~2 (~2 phi /\2 ~2 psi).
Notation "x '\/2' y" := (Or x y) (at level 41, right associativity).
Definition mso_impl phi psi := ~2 phi \/2 psi.
Notation "phi '==>2' psi " := (mso_impl phi psi) (at level 45, right associativity).

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

Notation " 'OR' { x | P } S " := (finBigOr (fun x => S) (fun x => P) ) (at level 60).
Notation " 'OR' { ( a , b , c ) | P } S " := (finBigOr (fun z => match z with (a,b,c) => S end) (fun z => match z with (a,b,c) => P end) ) (at level 60).

Section ClassicalReasoning.



  Context{natSet:NatSetClass}.
  Context{satisfies_xm : forall I J phi, logic_dec (I # J |== phi)}.

  Ltac mso_contra D := mso_contra_xm satisfies_xm D.



  Lemma mso_DN phi: mso_equiv phi (~2 (~2 phi)).
  Proof.
    intros I J. split.
    - intros Sat NSat. auto.
    - intros NNSat. mso_contra D. auto.
  Qed.

  Lemma or_correct I J phi psi: (I # J |== phi \/2 psi) <-> (I # J |== phi \/ I # J |== psi).
  Proof.
    split; unfold Or.
    - intros NA. destruct (satisfies_xm I J phi).
      + now left.
      + right. mso_contra D. apply NA. split; auto.
    - intros [Phi | Psi] [NPhi NPsi]; auto.
  Qed.

  Lemma mso_DM_neg_or phi psi : mso_equiv (~2 (phi \/2 psi)) (~2 phi /\2 ~2 psi).
  Proof.
    intros I J. split.
    - unfold Or. intros NOr. now apply mso_DN.
    - unfold Or. intros And. now apply mso_DN in And.
  Qed.

  Lemma mso_DM_neg_and phi psi : mso_equiv (~2 (phi /\2 psi)) (~2 phi \/2 ~2 psi).
  Proof.
    intros I J. split; unfold Or.
    - intros Nand. intros [NNPhi NNPsi].
      apply Nand. split; now apply mso_DN.
    - intros OrN [Phi Psi]. apply OrN. split; now apply mso_DN.
  Qed.

  Corollary mso_DM_neg_and' phi psi I J : ~(I # J |== (phi /\2 psi)) <-> I # J |== (~2 phi \/2 ~2 psi).
  Proof. apply mso_DM_neg_and. Qed.


  Lemma impl_correct I J phi psi : I # J |== phi ==>2 psi <-> (I # J |== phi -> I # J |== psi).
  Proof.
    split; unfold mso_impl.
    - intros [NPhi| Psi] % or_correct Phi; auto. now exfalso.
    - intros Impl. apply or_correct. destruct (satisfies_xm I J phi) as [Phi |NPhi].
      + right. now apply Impl.
      + now left.
  Qed.

  Lemma mso_DM_impl phi psi : mso_equiv (~2 (phi ==>2 psi)) (phi /\2 ~2 psi).
  Proof.
    intros I J. split; unfold mso_impl.
    - now intros [Psi%mso_DN NPhi] %mso_DM_neg_or.
    - intros [Phi%mso_DN NPhi]. now apply mso_DM_neg_or.
  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) (P : F -> Prop) {D: forall (a:F), dec (P a)} : (I # J |== (finBigOr f P ) ) <-> exists a, (I # J |== f a) /\ P a.
  Proof.
    split; unfold finBigOr.
    - intros Sat. apply bigOrCorrect in Sat. destruct Sat as [phi [Q1 Q2]]. apply in_map_iff in Q1. destruct Q1 as [x [Q1 R]]. exists x. subst phi. split; auto. apply in_filter_iff in R. apply R.
    - intros [x [Sat Q1]]. apply bigOrCorrect. exists (f x). split; auto. apply in_map_iff. exists x. split; auto. now apply in_filter_iff.
  Qed.

  Lemma mso_DM_finBigOR (X:finType) (P: X -> Prop) (decP: forall x, dec (P x)) (phi: X -> Form): mso_equiv (~2 OR {x | P x} (phi x)) (AND {x | P x} (~2 (phi x))).
  Proof.
    intros I J. split.
    - intros NOr. apply finBigAndCorrect. intros x Px. destruct (satisfies_xm I J (phi x)); auto.
      exfalso. apply NOr. fold satisfies. apply finBigOrCorrect. now exists x.
    - intros AndN [x [Sat Px]]%finBigOrCorrect. rewrite finBigAndCorrect in AndN.
      apply (AndN x); auto.
  Qed.

  Corollary mso_DM_finBigOR' (X:finType) (P: X -> Prop) (decP: forall x, dec (P x)) (phi: X -> Form) I J: ~(I # J |== ( OR {x | P x} (phi x))) <-> I # J |== (AND {x | P x} (~2 (phi x))).
  Proof. apply mso_DM_finBigOR.
  Qed.

   Lemma mso_DM_finBigAND (X:finType) (P: X -> Prop) (decP: forall x, dec (P x)) (phi: X -> Form): mso_equiv (~2 AND {x | P x} (phi x)) (OR {x | P x} (~2 (phi x))).
  Proof.
    intros I J. split.
    - intros NAnd. mso_contra D. apply mso_DM_finBigOR' in D.
      apply NAnd. fold satisfies. apply finBigAndCorrect.
      intros a Q. rewrite finBigAndCorrect in D. specialize (D a Q).
      now apply mso_DN in D.
    - intros [x [NPhi Q]] % finBigOrCorrect And.
      rewrite finBigAndCorrect in And. now specialize (And x Q).
  Qed.

  Corollary mso_DM_finBigAND' (X:finType) (P: X -> Prop) (decP: forall x, dec (P x)) (phi: X -> Form) I J: ~(I # J |== ( AND {x | P x} (phi x))) <-> I # J |== (OR {x | P x} (~2 (phi x))).
  Proof. apply mso_DM_finBigAND.
  Qed.

  Lemma mso_DM_ex1 I J phi x : (I # J |== ~2 ex1 x, ~2 phi ) <-> forall n, I[x := n] # J |== phi.
  Proof.
    split.
    - intros NA n. mso_contra D. apply NA. exists n. apply D.
    - intros A [n NE]. apply NE, A.
  Qed.
  Lemma mso_DM_ex2 I J phi X : (I # J |== ~2 ex2 X, ~2 phi ) <-> forall N, I # J[X := N] |== phi.
  Proof.
    split.
    - intros NA N. mso_contra D. apply NA. exists N. apply D.
    - intros A [N NE]. apply NE, A.
  Qed.

  Lemma all1_correct I J x phi : I # J |== all1 x, phi <-> forall k, (I [x := k]) # J |== phi.
  Proof.
    apply mso_DM_ex1.
  Qed.

  Lemma all2_correct I J X phi : I # J |== all2 X, phi <-> forall N, I # (J [X := N]) |== phi.
  Proof.
    apply mso_DM_ex2.
  Qed.

  Lemma mso_DM_forall_neg phi x : mso_equiv (~2 all1 x, phi) (ex1 x, ~2 phi).
  Proof.
    intros I J. split.
    - intros NA. mso_contra D.
      apply NA, D.
    - intros [n NSat] ASat. apply NSat, mso_DM_ex1 , ASat.
  Qed.

  Lemma mso_DM_forall_neg' I J phi x : ~ ( I # J |== all1 x, phi) <-> (I # J |== ex1 x, ~2 phi).
  Proof.
    apply mso_DM_forall_neg.
  Qed.


  Lemma mso_DM_exist_neg phi x : mso_equiv (~2(ex1 x, phi)) (all1 x, ~2 phi).
  Proof.
    intros I J. split.
    - intros NA. apply all1_correct. intros n.
      mso_contra D. apply NA. apply mso_DN in D. now exists n.
    - intros AN [n Sat]. rewrite all1_correct in AN. now apply (AN n).
  Qed.

  Lemma mso_DM_exist_neg' phi x I J: ~ I # J |== ex1 x, phi <-> I # J |== all1 x, ~2 phi.
  Proof.
     apply mso_DM_exist_neg.
  Qed.

  Lemma equiv_unsat phi psi : mso_equiv phi psi <-> ~ sat ((phi /\2 ~2 psi) \/2 ((~2 phi) /\2 psi)).
  Proof.
   split.
   - intros E [I [J [[Sat1 Sat2]|[Sat1 Sat2]] %or_correct]].
     + apply Sat2, E, Sat1.
     + apply Sat1, E, Sat2.
   - intros NSat I. split; intros Sat.
     + mso_contra D. apply NSat. exists I, J. apply or_correct. left. split; auto.
     + mso_contra D. apply NSat. exists I, J. apply or_correct. right. split; auto.
  Qed.

End ClassicalReasoning.