Library CompleteLattice
Require Export Utf8.
Module Equiv.
Class t (A:Type) : Type := Make {
eq : A → A → Prop;
refl : ∀ x, eq x x;
sym : ∀ x y, eq x y → eq y x;
trans : ∀ x y z, eq x y → eq y z → eq 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 : A → A → Prop;
refl : ∀ x y, x==y → order x y;
antisym : ∀ x y, order x y → order y x → x==y;
trans : ∀ x y z, order x y → order y z → order x z
}.
End Poset.
Notation "x ⊑ y" := (Poset.order x y) (at level 40).
Class subset A `{Equiv.t A} : Type := SubSet
{ carrier : A → Prop;
subset_comp_eq : ∀ x y:A, x==y → carrier x → carrier y}.
Coercion carrier : subset >-> Funclass.
Module CompleteLattice.
Class t (A:Type) : Type := Make
{ porder :> Poset.t A;
join : subset A → A;
join_bound : ∀x:A, ∀f:subset A, f x → x ⊑ join f;
join_lub : ∀f:subset A, ∀z, (∀ x:A, f x → x ⊑ 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 x → z ⊑ 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" := (A → Prop) (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 (A→L).
Defined.
Instance PointwisePoset A {L} `(Poset.t L) : Poset.t (A→L).
Defined.
Definition proj {L A} `{CompleteLattice.t L} `(Q:subset (A→L)) (x:A) : subset L.
Defined.
Instance PointwiseCompleteLattice A {L} `(CompleteLattice.t L) : CompleteLattice.t (A→L).
Defined.
Class monotone A `{Poset.t A} B `{Poset.t B} (f: A → B) : Prop :=
mon_prop : ∀ a1 a2, a1 ⊑ a2 → f 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 : A → A → A;
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 ⊑ z → y ⊑ 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 : A → A → A;
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 ⊑ x → z ⊑ y → z ⊑ (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 (A→B) _.
Defined.
Instance PointwiseTop (A:Type) B PB (top:@Top.t B PB) : @Top.t (A→B) _.
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 (A→B) := 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 == x → lfp F ⊑ x.
Lemma lfp_postfixpoint : f (lfp F) ⊑ lfp F.
Lemma lfp_least_postfixpoint : ∀x, f x ⊑ x → lfp F ⊑ x.
End f.
Lemma lfp_monotone : ∀ f1 f2 : L → L,
∀ F1: monotone _ _ f1,
∀ F2: monotone _ _ f2,
f1 ⊑ f2 → lfp F1 ⊑ lfp F2.
End Knaster_Tarski.
Module Equiv.
Class t (A:Type) : Type := Make {
eq : A → A → Prop;
refl : ∀ x, eq x x;
sym : ∀ x y, eq x y → eq y x;
trans : ∀ x y z, eq x y → eq y z → eq 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 : A → A → Prop;
refl : ∀ x y, x==y → order x y;
antisym : ∀ x y, order x y → order y x → x==y;
trans : ∀ x y z, order x y → order y z → order x z
}.
End Poset.
Notation "x ⊑ y" := (Poset.order x y) (at level 40).
Class subset A `{Equiv.t A} : Type := SubSet
{ carrier : A → Prop;
subset_comp_eq : ∀ x y:A, x==y → carrier x → carrier y}.
Coercion carrier : subset >-> Funclass.
Module CompleteLattice.
Class t (A:Type) : Type := Make
{ porder :> Poset.t A;
join : subset A → A;
join_bound : ∀x:A, ∀f:subset A, f x → x ⊑ join f;
join_lub : ∀f:subset A, ∀z, (∀ x:A, f x → x ⊑ 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 x → z ⊑ 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" := (A → Prop) (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 (A→L).
Defined.
Instance PointwisePoset A {L} `(Poset.t L) : Poset.t (A→L).
Defined.
Definition proj {L A} `{CompleteLattice.t L} `(Q:subset (A→L)) (x:A) : subset L.
Defined.
Instance PointwiseCompleteLattice A {L} `(CompleteLattice.t L) : CompleteLattice.t (A→L).
Defined.
Class monotone A `{Poset.t A} B `{Poset.t B} (f: A → B) : Prop :=
mon_prop : ∀ a1 a2, a1 ⊑ a2 → f 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 : A → A → A;
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 ⊑ z → y ⊑ 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 : A → A → A;
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 ⊑ x → z ⊑ y → z ⊑ (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 (A→B) _.
Defined.
Instance PointwiseTop (A:Type) B PB (top:@Top.t B PB) : @Top.t (A→B) _.
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 (A→B) := 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 == x → lfp F ⊑ x.
Lemma lfp_postfixpoint : f (lfp F) ⊑ lfp F.
Lemma lfp_least_postfixpoint : ∀x, f x ⊑ x → lfp F ⊑ x.
End f.
Lemma lfp_monotone : ∀ f1 f2 : L → L,
∀ F1: monotone _ _ f1,
∀ F2: monotone _ _ f2,
f1 ⊑ f2 → lfp F1 ⊑ lfp F2.
End Knaster_Tarski.