Tarski.v

Require Import Ensembles.

Notation sets := Ensemble.
Notation "∅" := Empty_set.
Notation "x ∈ X" := (In _ X x)(at level 50).
Notation "A ∩ B" := (Intersection _ A B)(at level 40).
Notation "A ∪ B" := (Union _ A B)(at level 40).
Notation "A ⊂ B" := (Included _ A B)(at level 30).
Notation "A // B" := (Setminus _ A B)(at level 40).
Notation "¬ A" := (Complement _ A)(at level 40).
Notation "[ S => P ]" := (fun S => P).
Notation extension := Extensionality_Ensembles.

Variable U : Type.
Definition setU := sets U.

Definition monotone (F : setU -> setU ) := 
    forall X Y, X ⊂ Y -> F X ⊂ F Y.

Definition mu F : setU :=
    fun x => forall X, (F X) ⊂ X -> x ∈ X.

Definition nu F : setU :=
    fun x => exists X, X ⊂ F X /\ x ∈ X.

Theorem mu_min : forall F X, 
    monotone F -> F X ⊂ X -> mu F ⊂ X.
Proof.
    unfold Included; intros.
    unfold mu in *.
    apply H1; intro; intros.
    apply H0; auto.
Qed.

Theorem mu_fixpoint F : 
    monotone F -> F (mu F) = mu F.
Proof.
    intros.
    apply extension; split; unfold Included; intros.
    +   unfold mu; unfold In; intros.        
        specialize (mu_min _ _ H H1); intro.
        specialize (H _ _ H2).
        apply H1; apply H; auto.
    +   unfold mu in H0.
        apply H0.
        apply H; unfold Included; intros.        
        unfold mu, In; intros.
        specialize (mu_min F X H H2); intro.
        specialize (H _ _ H3).
        apply H2; apply H; auto.
Qed.

Theorem nu_max : forall F X,
    monotone F -> X ⊂ F X -> X ⊂ nu F.
Proof.
    unfold Included; intros.
    unfold nu; exists X; auto.
Qed.

Theorem nu_fixpoint F : 
    monotone F -> F (nu F) = nu F.
Proof.
    intros.
    assert (forall X, X ⊂ F X -> X ⊂ nu F).
    {   
        intros; apply nu_max; auto. 
    }
    assert (nu F ⊂ F (nu F)).
    {
        unfold Included; intros.
        inversion H1 as [X [HX Hx]].
        specialize (nu_max _ _ H HX); intro.
        specialize (H _ _ H2).
        eauto.
    }  
    apply extension; split; unfold Included; intros.
    +   generalize (H _ _ H1); intro.
        apply H0 in H3.
        apply H3; auto.
    +   apply H1; auto.
Qed.    








Theorem reduction_lemma P F :
    monotone F -> P ⊂ nu F <-> P ⊂ (F (nu [ S => P ∪ F S])).
Proof.
    intro Hm.
    split; unfold Included; intros.    
    +   assert (P ∪ F (nu F) = nu F).
        {
            apply extension; split; unfold Included; intros.
            +   inversion H1; subst; eauto.
                rewrite <- (nu_fixpoint _ Hm); auto.
            +   apply Union_intror.
                rewrite (nu_fixpoint _ Hm); auto.
        }

        assert (nu F ⊂ (P ∪ F (nu F))).
        {
            unfold Included; intros.
            rewrite <- H1 in H2; auto.
        }

       assert (nu F ⊂ F (nu [S => P ∪ F S])).
       {
           rewrite <- (nu_fixpoint _ Hm).
           apply Hm.
           unfold Included; intros.
           induction H3 as [X [HF Hx]].
           exists X; split; auto.
           intro; intro; apply Union_intror; apply HF; auto.
       }
        eauto.
    +   apply H in H0.
        assert (monotone [S => P ∪ F S]).
        {
            intro; unfold Included; intros.
            induction H2; [apply Union_introl| apply Union_intror]; auto.
            apply (Hm _ _ H1); auto.
        }

        generalize (nu_fixpoint _ H1); intro.
        assert (nu [S => P ∪ F S] = F (nu [S => P ∪ F S])).
        {
            apply extension; split; unfold Included, In, nu in *; intros.
            +   assert ([x => exists X : sets U, X ⊂ (P ∪ F X) /\ x ∈ X] x0) by auto.
                rewrite <- H2 in H4.
                induction H4; auto.
            +   assert ((P ∪ F [x => exists X : sets U, X ⊂ (P ∪ F X) /\ x ∈ X] )x0).
                { apply Union_intror; auto. }
                rewrite H2 in H4; auto.
        }
        assert (nu [S => P ∪ F S] ⊂ nu F).
        {
            apply nu_max; auto.
            unfold Included; intros.
            rewrite <- H3; auto.
        }
        apply H4; rewrite H3; auto.
Qed.