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

Section ReducablityOfFirstOrderVariables.

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 "<>" := (ItoM0 i j) (at level 60).

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

 Lemma ItoM0Svar I J X : <> (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 : <> |= (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: <> |= phi <-> <> [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: <> |= phi <-> <> [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 <-> <> |= [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 # 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.