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.