# Library CompleteLattice

Require Export Utf8.

Module Equiv.
Class t (A:Type) : Type := Make {
eq : AAProp;
refl : x, eq x x;
sym : x y, eq x yeq y x;
trans : x y z, eq x yeq y zeq x z
}.
End Equiv.
Local Notation "x == y" := (Equiv.eq x y) (at level 40).

Module Poset.
Class t A : Type := Make {
eq :> Equiv.t A;
order : AAProp;
refl : x y, x==yorder x y;
antisym : x y, order x yorder y xx==y;
trans : x y z, order x yorder y zorder x z
}.
End Poset.
Notation "x ⊑ y" := (Poset.order x y) (at level 40).

Class subset A `{Equiv.t A} : Type := SubSet
{ carrier : AProp;
subset_comp_eq : x y:A, x==ycarrier xcarrier y}.
Coercion carrier : subset >-> Funclass.

Module CompleteLattice.
Class t (A:Type) : Type := Make
{ porder :> Poset.t A;
join : subset AA;
join_bound : x:A, f:subset A, f xx join f;
join_lub : f:subset A, z, ( x:A, f xx z) → join f z
}.
Definition subset_meet A {L:t A} (S:subset A) : subset A.
Defined.
Definition meet {A} {L:t A} (S:subset A) : A := join (subset_meet A S).

Lemma meet_bound : A (L:t A),
x:A, f:subset A, f x(meet f) x.

Lemma meet_glb : A (L:t A),
f:subset A, z, ( x, f xz x) → z meet f.
End CompleteLattice.

Hint Resolve @Equiv.refl @Equiv.sym @Equiv.trans
@Poset.refl @Poset.antisym @Poset.trans
@CompleteLattice.join_bound @CompleteLattice.join_lub
@CompleteLattice.meet_bound @CompleteLattice.meet_glb.

Instance ProductEquiv {A B} (Ea : Equiv.t A) (Eb : Equiv.t B) : Equiv.t (A × B).
Defined.

Instance ProductPoset {A B} (Pa: Poset.t A) (Pb: Poset.t B) : Poset.t (A × B).
Defined.

Definition left_subset {A B} (Ea:Equiv.t A) (Eb:Equiv.t B) (f:subset (A×B)) : subset A.
Defined.

Definition right_subset {A B} (Ea:Equiv.t A) (Eb:Equiv.t B) (f:subset (A×B)) : subset B.
Defined.

Instance ProductCompleteLattice {A B} (La: CompleteLattice.t A) (Lb: CompleteLattice.t B) : CompleteLattice.t (A × B).
Defined.

Notation "'℘' A" := (AProp) (at level 10).

Instance PowerSetEquiv A : Equiv.t ( A).
Defined.

Instance PowerSetPoset A : Poset.t ( A).
Defined.

Instance PowerSetCompleteLattice A : CompleteLattice.t ( A).
Defined.

Instance PointwiseEquiv {A L} `(Equiv.t L) : Equiv.t (AL).
Defined.

Instance PointwisePoset A {L} `(Poset.t L) : Poset.t (AL).
Defined.

Definition proj {L A} `{CompleteLattice.t L} `(Q:subset (AL)) (x:A) : subset L.
Defined.

Instance PointwiseCompleteLattice A {L} `(CompleteLattice.t L) : CompleteLattice.t (AL).
Defined.

Class monotone A `{Poset.t A} B `{Poset.t B} (f: A B) : Prop :=
mon_prop : a1 a2, a1 a2f a1 f a2.

Instance PointwiseMonotoneEquiv A B `(Poset.t A) `(Poset.t B) : Equiv.t { f | monotone A B f } :=
{| eq F1 F2 := x y, x == y proj1_sig F1 x == proj1_sig F2 y |}.

Instance PointwiseMonotonePoset A B `(Poset.t A) `(Poset.t B) : Poset.t { f | monotone A B f } :=
{| order F1 F2 := x, proj1_sig F1 x proj1_sig F2 x |}.

Module Join.
Class t {A} `(Poset.t A) : Type := Make {
op : AAA;
join_bound1 : x y:A, x op x y;
join_bound2 : x y:A, y op x y;
join_least_upper_bound : x y z:A, x zy z(op x y) z
}.
End Join.
Notation "x ⊔ y" := (Join.op x y) (at level 40).

Module Meet.
Class t {A} `(Poset.t A) : Type := Make {
op : AAA;
meet_bound1 : x y:A, op x y x;
meet_bound2 : x y:A, op x y y;
meet_greatest_lower_bound : x y z:A, z xz yz (op x y)
}.
End Meet.
Notation "x ⊓ y" := (Meet.op x y) (at level 40).

Module Bot.
Class t {A} `(Poset.t A) : Type := Make {
elem : A;
prop : x : A, elem x
}.
End Bot.
Notation "⊥" := (Bot.elem) (at level 40).

Module Top.
Class t {A} `(Poset.t A) : Type := Make {
elem : A;
prop : x : A, x elem
}.
End Top.
Notation "⊤" := (Top.elem) (at level 40).

Module Lattice.
Class t (A:Type) : Type := Make
{ porder :> Poset.t A;
join :> Join.t porder;
meet :> Meet.t porder;
bot :> Bot.t porder;
top :> Top.t porder
}.
End Lattice.
Hint Resolve
@Join.join_bound1 @Join.join_bound2 @Join.join_least_upper_bound
@Meet.meet_bound1 @Meet.meet_bound2 @Meet.meet_greatest_lower_bound
@Bot.prop @Top.prop.

Definition empty {L} `{CL:CompleteLattice.t L} : subset L.
Defined.

Definition bottom {L} `{CL:CompleteLattice.t L} : L := CompleteLattice.join empty.

Lemma bottom_is_bottom : L `{CL:CompleteLattice.t L}, x:L, bottom x.

Definition top {L} `{CL:CompleteLattice.t L} : L := CompleteLattice.meet empty.

Lemma top_is_top : L `{CL:CompleteLattice.t L}, x:L, x top.

Instance PowerSetBot (A:Type) : Bot.t (PowerSetPoset A).
Defined.

Instance PowerSetTop (A:Type) : Top.t (PowerSetPoset A).
Defined.

Instance PowerSetJoin (A:Type) : Join.t (PowerSetPoset A).
Defined.

Instance PowerSetMeet (A:Type) : Meet.t (PowerSetPoset A).
Defined.

Instance PowerSetLattice (A:Type) : Lattice.t ( A) := Lattice.Make _ _ _ _ _ _.

Instance PointwiseBot (A:Type) B PB (Bot:@Bot.t B PB) : @Bot.t (AB) _.
Defined.

Instance PointwiseTop (A:Type) B PB (top:@Top.t B PB) : @Top.t (AB) _.
Defined.

Instance PointwiseJoin (A:Type) B PB `(J:@Join.t B PB) : Join.t (PointwisePoset A PB).
Defined.

Instance PointwiseMeet (A:Type) B PB `(J:@Meet.t B PB) : Meet.t (PointwisePoset A PB).
Defined.

Instance PointwiseLattice (A:Type) B (L:Lattice.t B) : Lattice.t (AB) := Lattice.Make _ _ _ _ _ _.

Instance ProductLattice A B `{Lattice.t A} `{Lattice.t B} : Lattice.t (A×B).
Defined.

Definition PostFix {L P} f `(F:@monotone L P L P f) : subset L.
Defined.

Section Knaster_Tarski.

Definition lfp {L} `{CompleteLattice.t L} {f} (F:monotone L L f) : L :=
CompleteLattice.meet (PostFix f F).

Variable L : Type.
Variable CL : CompleteLattice.t L.

Section f.
Variable (f: L L) (F: monotone L L f).

Lemma lfp_fixpoint : f (lfp F) == lfp F.

Lemma lfp_least_fixpoint : x, f x == xlfp F x.

Lemma lfp_postfixpoint : f (lfp F) lfp F.

Lemma lfp_least_postfixpoint : x, f x xlfp F x.

End f.

Lemma lfp_monotone : f1 f2 : L L,
F1: monotone _ _ f1,
F2: monotone _ _ f2,
f1 f2lfp F1 lfp F2.

End Knaster_Tarski.