Tarski.v

From mathcomp Require Export fintype finset ssrbool ssreflect eqtype.


Module Type SIG.
  Parameter T : finType.
  Parameter A : {set T}.
  Parameter F : {set T} -> {set T}.
  Parameter mono : forall (X Y : {set T}), X \subset Y -> F X \subset F Y.
End SIG.

Module  Tarski (sig : SIG).
  Import sig.
  Definition C :=  [set S | F S \subset S].
  Definition D := [set S : {set T}| S \subset F S].
  Definition lfp := (\bigcap_(E in C) E).
  Definition gfp := (\bigcup_(E in D) E).
  Definition fps := [set S | S == F S].

  Lemma FXX :
    forall X, X \in C -> F X \subset X.
  Proof.
    move => X. rewrite in_set; auto.
  Qed.

  Lemma PX :
    forall X, X \in C -> lfp \subset X.
  Proof.
    move => X; rewrite in_set => H.
    apply /subsetP => x.
    move /bigcapP; apply.
    rewrite in_set; auto.
  Qed.

  Lemma FPX :
    forall X, X \in C -> F lfp \subset X.
  Proof.
    move => X H.
    apply /subsetP => x Hx.
    move : (FXX _ H).
    move /subsetP; apply.
    suff : F lfp \subset F X. {
      move /subsetP; auto.
    }
    apply mono.
    apply PX; auto.
  Qed.

  Lemma PC :
    lfp \in C.
  Proof.
    rewrite in_set.
    apply /subsetP => x Hx.
    apply /bigcapP => X HX.
    move : (FPX X HX).
    move /subsetP; apply; auto.
  Qed.

  Theorem tarski_lfp :
    (F lfp = lfp) /\ (forall X, X \in fps -> lfp \subset X).
  Proof.
    split.
    {
      apply /setP /subset_eqP /andP; split; apply /subsetP => x Hx.
      - move : (FPX _ PC).
        move /subsetP; apply; auto.
      - move /bigcapP : Hx; apply.
        rewrite in_set.
        apply mono.
        move : PC.
        rewrite in_set; auto.
    }
    {
     move => X.
     rewrite in_set => /eqP XFX.
     apply /subsetP => x.
     move /bigcapP; apply.
     rewrite in_set.
     rewrite <- XFX.
     apply /subsetP => y; auto.
    }
  Qed.

  Lemma XFX :
    forall X, X \in D -> X \subset F X.
  Proof.
    move => X. rewrite in_set; auto.
  Qed.

  Lemma XP :
    forall X, X \in D -> X \subset gfp.
  Proof.
    move => X; rewrite in_set => H.
    apply /subsetP => x Hx.
    apply /bigcupP.
    exists X; auto.
    rewrite in_set; auto.
  Qed.

  Lemma XFP :
    forall X, X \in D -> X \subset F gfp.
  Proof.
    move => X H.
    apply /subsetP => x Hx.
    suff : F X \subset F gfp. {
      move /subsetP; apply.
      move : (XFX X H).
      move /subsetP; auto.
    }
    apply mono.
    apply XP; auto.
  Qed.

  Lemma PD :
    gfp \in D.
  Proof.
    rewrite in_set.
    apply /subsetP => x.
    move /bigcupP  => [X HX Hx].
    move : (XFP X HX).
    move /subsetP; apply; auto.
  Qed.

  Theorem tarski_gfp :
    (F gfp = gfp) /\ (forall X, X \in fps -> X \subset gfp).
  Proof.
    split.
    {
      move : (XFX _ PD) => PFP.
      apply /setP /subset_eqP /andP; split; auto.
      apply /subsetP => x Hx.
      apply /bigcupP.
      exists (F gfp); auto.
      rewrite in_set.
      apply mono; auto.
    }
    {
     move => X.
     rewrite in_set => /eqP XFX.
     apply /subsetP => x Hx.
     apply /bigcupP.
     exists X; auto.
     rewrite in_set.
     rewrite <- XFX.
     apply /subsetP => y; auto.
    }
  Qed.

End Tarski.