Fixpoint.v

Require Import Ensembles.
From mathcomp Require Import ssreflect.

Arguments Singleton {U}.
Arguments Union {U}.
Arguments Setminus {U}.
Arguments Included {U}.
Arguments Couple {U}.
Arguments Empty_set {U}.


Variable T : Set.

Definition rel := T -> T -> Prop.

Definition po (R : rel) :=
  (forall x, R x x) /\
  (forall x y z, R x y -> R y z -> R x z) /\
  (forall x y , R x y -> R y x -> x = y)
  .
Arguments In {U}.



Definition ub {R : rel} {H : po R} X b :=
  forall a, In X a -> R a b.


Definition lb {R : rel} {H : po R} X a :=
  forall b, In X b -> R a b.


Definition lub {R H} X b :=
  (@ub R H X b) /\
  forall b', @ub R H X b' -> R b b'.


Definition glb {R H} X a :=
  (@lb R H X a) /\
  forall a', @lb R H X a' -> R a' a.

Lemma lub_uniq {R H} X :
  forall x y, @lub R H X x -> @lub R H X y -> x = y.
Proof.
  move =>  y z [uby Hy] [ubz Hz].
  inversion H as [Hrel [Htra Hcomp]].
  apply Hcomp; [apply Hy | apply Hz]; auto.
Qed.


Lemma glb_uniq {R H} X :
  forall x y, @glb R H X x -> @glb R H X y -> x = y.
Proof.
  move =>  y z [uby Hy] [ubz Hz].
  inversion H as [Hrel [Htra Hcomp]].
  apply Hcomp; [apply Hz | apply Hy]; auto.
Qed.

Axiom Lub : forall R (HR : po R), Ensemble T -> T.

Axiom LUB : forall R HR X, @lub R HR X (Lub R HR X).

Axiom Glb : forall R (HR : po R), Ensemble T -> T.

Axiom GLB : forall R HR X, @glb R HR X (Glb R HR X).

Definition map f (L : Ensemble T) :=
  forall a, In L a -> In L (f a).


Definition complat R H L :=
  forall X, Included X L -> exists x y, @lub R H X x /\ @glb R H X y.

Definition mono R HR L (HL : complat R HR L)  f (Hf : map f L) :=
  forall x y, R x y -> R (f x) (f y).

Definition direct R HR L (HL: complat R HR L) X (HX : Included X L) :=
  forall x y, In X x -> In X y -> exists z, In X z /\ R x z /\ R y z.

Definition Map {T} ( f: T -> T) x := exists y, f y = x.



Definition continuous R HR L (HL : complat R HR L)  f (Hf : map f L) :=
  forall X (HX : Included X L), direct R HR L HL X HX ->
  f(Lub R HR X) = Lub R HR (fun x => exists y, In X y /\ f y = x).

Definition lfp R HR L (HL : complat R HR L) f (Hf : map f L) a :=
  f a = a /\
  forall b, In L b -> f b = b -> R a b.

Definition gfp R HR L (HL : complat R HR L) f (Hf : map f L) b :=
  f b = b /\
  forall a, In L a -> f a = a -> R a b.

Lemma weak_tarski_lfp R HR L HL f Hf (Hmono : mono R HR L HL f Hf)  :
  let G := fun x => R (f x) x in
  let g := Glb R HR G in
  lfp R HR L HL f Hf g.
Proof.
  move => G g.
  move : (GLB R HR G).
  inversion HR as [Hr [Ht Hc]].
  move => [H1 H2].
  split.
  {
    have fbb : R (f g) g. {
      apply H2 => b Hb.
      apply Ht with (f b); auto.
    }
    apply Hc; auto.
    apply H1.
    apply Hmono; auto.
  }
  {
    move => b Hb Hfb.
    apply H1.
    unfold G, In.
    rewrite Hfb.
    apply Hr.
  }
Qed.

Lemma GG_lfp R HR L HL f Hf (Hmono : mono R HR L HL f Hf) :
  let G := fun x => R (f x) x in
  let g := Glb R HR G in
  let G' := fun x => (f x) = x in
  let g' := Glb R HR G' in
  g' = g.
Proof.
  move => G g G' g'.
  move : (GLB R HR G) => [HG1 HG2].
  move : (GLB R HR G') => [HG'1 HG2'].
  inversion HR as [Hr [Ht Hc]].
  unfold lb in *.
  have GG' : Included G' G. {
    unfold Included.
    unfold In, G', G => x ->; auto.
  }
  apply Hc.
  {
    apply HG'1.
    unfold G', In.
    have fgg : R (f g) g. {
      apply HG2.
      unfold G, In => b Hb.
      apply Ht with (f b); auto.
    }
    apply Hc; auto.
    apply HG1.
    unfold G, In.
    apply Hmono; auto.
  }
  {
    apply HG2' => b fbb.
    apply HG1.
    apply GG'; auto.
  }
Qed.



Lemma weak_tarski_gfp R HR L HL f Hf (Hmono : mono R HR L HL f Hf)  :
  let G := fun x => R x (f x) in
  let g := Lub R HR G in
  gfp R HR L HL f Hf g.
Proof.
  move => G g.
  move : (LUB R HR G).
  inversion HR as [Hr [Ht Hc]].
  move => [H1 H2].
  split.
  {
    have fbb : R g (f g). {
      apply H2 => b Hb.
      rewrite /G /In in Hb.
      apply Ht with (f b); auto.
    }
    apply Hc; auto.
    apply H1.
    apply Hmono; auto.
  }
  {
    move => b Hb Hfb.
    apply H1.
    unfold G, In.
    rewrite Hfb.
    apply Hr.
  }
Qed.

Lemma GG_gfp R HR L HL f Hf (Hmono : mono R HR L HL f Hf) :
  let G := fun x => R x (f x) in
  let g := Lub R HR G in
  let G' := fun x => (f x) = x in
  let g' := Lub R HR G' in
  g' = g.
Proof.
  move => G g G' g'.
  move : (LUB R HR G) => [HG1 HG2].
  move : (LUB R HR G') => [HG1' HG2'].
  inversion HR as [Hr [Ht Hc]].
  unfold lb in *.
  have GG' : Included G' G. {
    unfold Included.
    unfold In, G', G => x ->; auto.
  }
  apply Hc.
  {
    apply HG1.
    apply HG2' => b Hb.
    move : (HG1' _ Hb) => Hg'.
    rewrite <- Hb.
    apply Hmono; auto.
  }
  {
    apply HG1'.
    unfold G', In.
    have Hg : R g (f g). {
      apply HG2 => b Hb.
      move : (HG1 _ Hb) => Hg.
      unfold G, In in Hb.
      apply Ht with (f b); auto.
    }
    apply Hc; auto.
    apply HG1.
    unfold G, In.
    apply Hmono; auto.
  }
Qed.