ImpAlg.Lattices
Set Implicit Arguments.
Set Contextual Implicit.
Require Import Utf8.
Require Import Setoid.
Require Import Morphisms.
Require Export Relation_Definitions.
Require Import ImpAlg.Ens.
Set Contextual Implicit.
Require Import Utf8.
Require Import Setoid.
Require Import Morphisms.
Require Export Relation_Definitions.
Require Import ImpAlg.Ens.
Class Order {X:Set} :=
{
ord : X → X → Prop;
ord_refl : reflexive X ord;
ord_antisym : antisymmetric X ord;
ord_trans : transitive X ord
}.
Definition up_closed_set `{X:Set} (ord:X → X → Prop) A:= ∀ (a b:X), ord a b → A a → A b.
Definition anti_mon `{Ord:Order} (f:X → X):= ∀ (a b:X), ord a b → ord (f b) (f a).
Definition image_set `{X:Set} (f:X→X) (A:Ens):Ens := fun x => ∃ a, (A a ∧ x = f a).
Definition preimage `{X:Set} (f:X → X) (a:X) := (fun x=> a=f x).
Definition preimage_set `{X:Set} (f:X → X) A := (fun x=> exists a, A a ∧ a=f x).
Definition reverse `{X:Set} (ord:X → X → Prop) (a b:X):= ord b a.
Generalizable Variables X ord.
Infix "≤" := ord : ia_scope.
Global Open Scope ia_scope.
The reversed relation is also an order
Definition rev `{Ord:Order X}:= reverse ord.
Lemma rev_refl `{Ord:Order X}: reflexive X rev.
Proof.
intro x.
apply ord_refl.
Qed.
Lemma rev_antisym `{Ord:Order X}: antisymmetric X rev.
Proof.
intros x y H1 H2.
apply (ord_antisym H2 H1).
Qed.
Lemma rev_trans `{Ord:Order X}: transitive X rev.
Proof.
intros x y z H1 H2.
apply (ord_trans z y x H2 H1).
Qed.
Definition RevOrd `{Ord:Order X}:=@Build_Order X (reverse ord) (rev_refl) (rev_antisym) (rev_trans).
Lemma rev_refl `{Ord:Order X}: reflexive X rev.
Proof.
intro x.
apply ord_refl.
Qed.
Lemma rev_antisym `{Ord:Order X}: antisymmetric X rev.
Proof.
intros x y H1 H2.
apply (ord_antisym H2 H1).
Qed.
Lemma rev_trans `{Ord:Order X}: transitive X rev.
Proof.
intros x y z H1 H2.
apply (ord_trans z y x H2 H1).
Qed.
Definition RevOrd `{Ord:Order X}:=@Build_Order X (reverse ord) (rev_refl) (rev_antisym) (rev_trans).
If f is anti-monotonic with respect to an pre-order, and A is upwards-closed,
then the preimage of A through f is also upwards closed.
We will use this with the negation
Lemma pre_upclosed_rev `{Ord:Order X}: ∀ (A:X → Prop) f,
(anti_mon f) → @up_closed_set X ord A → (@up_closed_set X rev (preimage_set f A)).
Proof.
unfold RevOrd.
unfold up_closed_set.
unfold preimage_set.
intros A f Anti Clos a b Hab (na,(Aa,Ha));subst.
exists (f b);intuition.
apply (Clos (f a));now intuition.
Qed.
Global Instance ord_Reflexive `{Ord:Order X}: Reflexive ord:=ord_refl.
Global Instance ord_Transitive `{Ord:Order X}: Transitive ord:=ord_trans.
Global Instance ord_Antisymmetric `{Ord:Order X}: Antisymmetric X _ ord:=ord_antisym.
Lemma by_refl `{Ord:Order X}: ∀ (a b:X), a = b → a ≤ b.
Proof.
intros a b H; subst;reflexivity.
Qed.
Class Lattice `{Ord:Order X} :=
{
meet : X → X → X;
join : X → X → X;
meet_commutative: ∀ a b, meet a b = meet b a;
meet_associative: ∀ a b c, meet (meet a b) c = meet a (meet b c);
meet_absorptive: ∀ a b, meet a (join a b) = a;
meet_idempotent: ∀ a, meet a a = a ;
join_commutative: ∀ a b, join a b = join b a;
join_associative: ∀ a b c, join (join a b) c = join a (join b c);
join_absorptive: ∀ a b, join a (meet a b) = a;
join_idempotent: ∀ a, join a a = a;
consistent : ∀ a b, ord a b ↔ a = meet a b
}.
Generalizable Variables Ord meet join.
Infix "≤" := ord : ia_scope.
Infix "⋀" := meet (at level 68, left associativity): ia_scope.
Infix "⋁" := join (at level 68, left associativity): ia_scope.
Hint Resolve meet_commutative meet_associative meet_absorptive meet_idempotent consistent.
Hint Resolve join_commutative join_associative join_absorptive join_idempotent.
Exchanging join and meet gives a lattice for the reverse order .
Lemma meet_join `{L:Lattice}:
∀ (a b:X), a = a ⋀ b ↔ b = a ⋁ b.
Proof.
intros; split;intro H;rewrite H.
- rewrite meet_commutative,join_commutative,join_absorptive. reflexivity.
- rewrite meet_absorptive. reflexivity.
Qed.
Lemma join_consistent `{L:Lattice}:
∀ a b, a ≤ b ↔ b = a ⋁ b.
Proof.
intros.
split; intro H.
- apply meet_join. apply consistent. assumption.
- apply consistent. apply meet_join. assumption.
Qed.
Lemma rev_consistent `{L:Lattice}: ∀ a b, rev a b ↔ a = join a b.
Proof.
intros.
unfold rev,reverse.
split;intros.
- apply join_consistent in H.
now rewrite H at 1.
- apply join_consistent.
now rewrite H at 1.
Qed.
Definition RevLattice `{L:Lattice}:=
@Build_Lattice X (RevOrd) join meet join_commutative join_associative
join_absorptive (@join_idempotent X Ord L) meet_commutative meet_associative
meet_absorptive (@meet_idempotent X Ord L) (@rev_consistent X Ord L).
Simple tactic to automatize proofs by duality
Ltac dualityL t:= apply (t _ _ RevLattice).
Definition lb `{L:Lattice} (P:Ens) : X → Prop := fun x => forall y, P(y) -> x ≤ y.
Definition ub `{L:Lattice} (P:Ens) : X → Prop := fun x => forall y, P(y) -> y ≤ x.
Definition glb `{L:Lattice} (P:Ens) : X → Prop := fun x => lb P x ∧ ∀ y, lb P y → y ≤ x.
Definition lub `{L:Lattice} (P:Ens) : X → Prop := fun x => ub P x ∧ ∀ y, ub P y → x ≤ y.
Definition min `{L:Lattice} (P:Ens) : X → Prop := fun x => lb P x ∧ P x.
Definition sup `{L:Lattice} (P:Ens) : X → Prop := fun x => ub P x ∧ P x.
Transparent lb ub glb lub.
We prove that meet and join are indeed lower and upper bound
Lemma meet_lb_l `{L:Lattice} :
∀ a b : X, a ⋀ b ≤ a.
Proof.
intros a b.
apply consistent.
rewrite meet_associative.
rewrite (meet_commutative _ (b ⋀ a)).
rewrite meet_associative,meet_idempotent,meet_commutative.
reflexivity.
Qed.
Lemma meet_lb_r `{L:Lattice} :
∀ a b : X, a ⋀ b ≤ b.
Proof.
intros.
rewrite meet_commutative.
apply meet_lb_l.
Qed.
Theorem meet_glb `{L:Lattice} :
∀ a b : X, ∀ x, x ≤ a /\ x ≤ b ↔ x ≤ a ⋀ b.
Proof.
intros;split;intros.
- destruct H as (Ha,Hb).
apply consistent.
apply consistent in Ha.
apply consistent in Hb.
rewrite <- meet_associative.
rewrite <- Ha. exact Hb.
- split.
+ apply (ord_trans _ (a ⋀ b));auto.
apply meet_lb_l.
+ apply (ord_trans _ (a ⋀ b));auto.
apply meet_lb_r.
Qed.
Lemma join_ub_l `{L:Lattice} :
∀ a b : X, a ≤ a ⋁ b.
Proof.
dualityL @meet_lb_l.
Qed.
Lemma join_ub_r `{L:Lattice} :
∀ a b : X, b ≤ a ⋁ b.
Proof.
dualityL @meet_lb_r.
Qed.
Theorem join_lub `{L:Lattice} :
∀ a b : X, ∀ x, a ≤ x /\ b ≤ x ↔ a ⋁ b ≤ x.
Proof.
dualityL @meet_glb.
Qed.
∀ a b : X, a ⋀ b ≤ a.
Proof.
intros a b.
apply consistent.
rewrite meet_associative.
rewrite (meet_commutative _ (b ⋀ a)).
rewrite meet_associative,meet_idempotent,meet_commutative.
reflexivity.
Qed.
Lemma meet_lb_r `{L:Lattice} :
∀ a b : X, a ⋀ b ≤ b.
Proof.
intros.
rewrite meet_commutative.
apply meet_lb_l.
Qed.
Theorem meet_glb `{L:Lattice} :
∀ a b : X, ∀ x, x ≤ a /\ x ≤ b ↔ x ≤ a ⋀ b.
Proof.
intros;split;intros.
- destruct H as (Ha,Hb).
apply consistent.
apply consistent in Ha.
apply consistent in Hb.
rewrite <- meet_associative.
rewrite <- Ha. exact Hb.
- split.
+ apply (ord_trans _ (a ⋀ b));auto.
apply meet_lb_l.
+ apply (ord_trans _ (a ⋀ b));auto.
apply meet_lb_r.
Qed.
Lemma join_ub_l `{L:Lattice} :
∀ a b : X, a ≤ a ⋁ b.
Proof.
dualityL @meet_lb_l.
Qed.
Lemma join_ub_r `{L:Lattice} :
∀ a b : X, b ≤ a ⋁ b.
Proof.
dualityL @meet_lb_r.
Qed.
Theorem join_lub `{L:Lattice} :
∀ a b : X, ∀ x, a ≤ x /\ b ≤ x ↔ a ⋁ b ≤ x.
Proof.
dualityL @meet_glb.
Qed.
meet and join are monotonic
Lemma meet_mon_l `{L:Lattice}:
∀ a a' b, a≤a' → a⋀b ≤ a'⋀b.
Proof.
intros a a' b H.
apply meet_glb;split.
+ apply (ord_trans _ a _ (meet_lb_l a b) H).
+ apply meet_lb_r.
Qed.
Lemma meet_mon_r `{L:Lattice}:
∀ a a' b, a≤a' → b⋀a ≤ b⋀a'.
Proof.
intros a a' b H. do 2 rewrite (meet_commutative b _). apply meet_mon_l. auto.
Qed.
Lemma join_mon_l `{L:Lattice}:
∀ a a' b, a≤a' → a⋁b ≤ a'⋁b.
Proof.
intros a a' b.
dualityL @meet_mon_l.
Qed.
Lemma join_mon_r `{L:Lattice}:
∀ a a' b, a≤a' → b⋁a ≤ b⋁a'.
Proof.
intros a a'.
dualityL @meet_mon_r.
Qed.
We show that glb and lub, and thus arbitrary meet and join if they exist, are unique
Theorem glb_unique `{L:Lattice}:
∀ (P:X → Prop), ∀ x y, (glb P) x → (glb P) y → x=y.
Proof.
intros P x y Hx Hy.
unfold glb,lb in *.
destruct Hx as (Hxlb,Hxglb).
destruct Hy as (Hylb,Hyglb).
apply ord_antisym.
+ apply Hyglb.
intros y0 H0.
apply Hxlb,H0.
+ apply Hxglb.
intros x0 H0.
apply Hylb,H0.
Qed.
Theorem lub_unique `{L:Lattice}:
∀ (P: X → Prop), ∀ x y, (lub P) x → (lub P) y → x=y.
Proof.
dualityL @glb_unique.
Qed.
Completeness for meet implies completeness for join and vice-versa.
Definition meet_complete `{L:Lattice}:= ∀(P: X → Prop), ∃ m:X, glb P m.
Definition join_complete `{L:Lattice}:= ∀(P: X → Prop), ∃ m:X, lub P m.
Theorem meet_join_completeness `{L:Lattice}:
meet_complete → join_complete.
Proof.
intros H P; red in H.
specialize (H (ub P)); destruct H as [m [Hm Hlb]].
exists m; split.
+ intros x Hx; apply Hlb.
intros y Hy; apply Hy, Hx.
+ intros x Hx.
apply Hm; unfold ub; intros y Hy.
apply Hx, Hy.
Qed.
Theorem join_meet_completeness `{L:Lattice}:
join_complete → meet_complete.
Proof.
dualityL @meet_join_completeness.
Qed.
Greatest lower bound and lowest upper bound
correspond to expected intro/elim rules that
we use after to define them.
Lemma glb_elim_intro `{L:Lattice}:
∀ (A:Ens) m, glb A m <-> (∀ (y:X), (A y → m ≤ y)) ∧ (∀(y:X), (∀ x, A x → ord y x) → ord y m).
Proof.
intros A m.
split.
- intros (H1,H2);intuition.
- intros (Hl, Hgl);split;intuition.
Qed.
Lemma lub_elim_intro `{L:Lattice}:
∀ (A:Ens) m, lub A m <-> (∀ (y:X), (A y → y ≤ m)) ∧ (∀(y:X), (∀ x, A x → ord x y) → ord m y).
Proof.
dualityL @glb_elim_intro.
Qed.
Hint Resolve join_ub_r join_ub_l meet_lb_l meet_lb_r.
Class BoundedLattice `{L:Lattice} :=
{
bot : X;
top : X;
bot_min: ∀ a, bot ≤ a;
top_max: ∀ a, a ≤ top;
}.
Notation "⊥" := bot.
Notation "⊤" := top.
A reversed bounded lattice is a bounded lattice
Definition RevBoundedLattice `{BL:BoundedLattice}:=
@Build_BoundedLattice _ _ RevLattice top bot top_max bot_min.
Ltac dualityBL p:= apply (p _ _ _ RevBoundedLattice).
Properties of ⊥ and ⊤
Lemma meet_bot_l `{BL:BoundedLattice}:
∀ a, ⊥ ⋀ a = ⊥.
Proof.
intros.
apply (@ord_antisym _ _ (⊥ ⋀ a) ⊥ ).
apply meet_lb_l.
apply bot_min.
Qed.
Lemma meet_bot_r `{BL:BoundedLattice}:
∀ a, a ⋀ ⊥ = ⊥.
Proof.
intros.
apply ord_antisym.
apply meet_lb_r.
apply bot_min.
Qed.
Lemma join_bot_l `{BL:BoundedLattice}:
∀ a, ⊥ ⋁ a = a.
Proof.
intros.
apply ord_antisym.
- apply join_lub;split.
+ apply bot_min;auto.
+ apply ord_refl.
- apply join_ub_r.
Qed.
Lemma join_bot_r `{BL:BoundedLattice}:
∀ a, a ⋁ ⊥ = a.
Proof.
intros.
apply (ord_antisym).
- apply @join_lub;split.
+ apply ord_refl.
+ apply bot_min;auto.
- apply join_ub_l.
Qed.
Lemma join_top_l `{BL:BoundedLattice}:
∀ a, ⊤ ⋁ a = ⊤.
Proof.
dualityBL @meet_bot_l.
Qed.
Lemma join_top_r `{BL:BoundedLattice}:
∀ a, a ⋁ ⊤ = ⊤.
Proof.
dualityBL @meet_bot_r.
Qed.
Lemma meet_top_l `{BL:BoundedLattice}:
∀ a, ⊤ ⋀ a = a.
Proof.
dualityBL @join_bot_l.
Qed.
Lemma meet_top_r `{BL:BoundedLattice}:
∀ a, a ⋀ ⊤ = a.
Proof.
dualityBL @join_bot_r.
Qed.
Hint Resolve bot_min meet_bot_l meet_bot_r join_bot_l join_bot_r.
Hint Resolve top_max join_top_l join_top_r meet_top_l meet_top_r.
Class CompleteLattice `{L:Lattice} :=
{
meet_set: Ens → X;
join_set: Ens → X;
meet_elim : ∀ (A:Ens) y, A y → ord (meet_set A) y;
meet_intro : ∀ (A:Ens) y, (∀ x, A x → ord y x) → ord y (meet_set A);
join_elim: ∀ (A:Ens) y, A y → ord y (join_set A);
join_intro : ∀ (A:Ens) y, (∀ x, A x → ord x y) → ord (join_set A) y;
}.
Hint Resolve meet_elim meet_intro join_elim join_intro.
Notation "⊓":= meet_set.
Notation "⊔":= join_set.
A reversed complete lattice is a lattice
Definition RevCompleteLattice `{CL:CompleteLattice}:=
@Build_CompleteLattice _ _ RevLattice join_set meet_set join_elim join_intro meet_elim meet_intro.
Ltac dualityCL p:= apply (p _ _ _ RevCompleteLattice).
Complete lattices are bounded
Global Instance CBL `{CL:CompleteLattice}:BoundedLattice:=
{top:=(⊔ (λ x:X, True)); bot:=(⊓ (λ x:X, True))}.
Proof.
- intro a. apply meet_elim. apply I.
- intro a. apply join_elim. apply I.
Defined.
Lemma meet_emptyset `{CL:CompleteLattice}: ⊓ emptyset = ⊤.
Proof.
apply ord_antisym;[apply top_max|].
apply meet_intro. intros x H; contradict H.
Qed.
Lemma join_emptyset `{CL:CompleteLattice}: ⊔ emptyset = ⊥.
Proof.
apply ord_antisym;[|apply bot_min].
apply join_intro. intros x H; contradict H.
Qed.
{top:=(⊔ (λ x:X, True)); bot:=(⊓ (λ x:X, True))}.
Proof.
- intro a. apply meet_elim. apply I.
- intro a. apply join_elim. apply I.
Defined.
Lemma meet_emptyset `{CL:CompleteLattice}: ⊓ emptyset = ⊤.
Proof.
apply ord_antisym;[apply top_max|].
apply meet_intro. intros x H; contradict H.
Qed.
Lemma join_emptyset `{CL:CompleteLattice}: ⊔ emptyset = ⊥.
Proof.
apply ord_antisym;[|apply bot_min].
apply join_intro. intros x H; contradict H.
Qed.
meet_set is the glb, join_set the lub
Lemma meet_set_glb `{CL:CompleteLattice}:
∀ A, glb A (meet_set A).
Proof.
intro A.
apply glb_elim_intro.
split;auto.
Qed.
Lemma join_set_lub `{CL:CompleteLattice}:
∀ A, lub A (join_set A).
Proof.
dualityCL @meet_set_glb.
Qed.
We define meet and join of indexed families.
Definition meet_family `{CL:CompleteLattice} I (f:I → X):X := ⊓ (fun x => ∃ (i:I), x = f i).
Definition join_family `{CL:CompleteLattice} I (f:I → X):X := ⊔ (fun x => ∃ (i:I), x = f i).
Notation "∩ f" := (meet_family f) (at level 60).
Notation " '⋂[' a ']' p " := ( ⊓ (fun x => ∃ a, x= p)) (at level 60).
Definition inf `{CL:CompleteLattice} (f:X → X):= ⋂[a] ((f a)).
Lemma meet_elim_trans `{CL:CompleteLattice}:
∀ (A : Ens) (z: X), (exists y , A y ∧ y ≤ z) → ⊓ A ≤ z.
Proof.
intros A z (y,(Hy,Hyz)).
apply (@ord_trans X Ord _ _ _ (meet_elim A y Hy) Hyz).
Qed.
Lemma join_elim_trans `{CL:CompleteLattice}:
∀ (A : Ens) (y: X), (exists z , A z ∧ y ≤ z) → y ≤ ⊔ A.
Proof.
dualityCL @meet_elim_trans.
Qed.
Definition join_family `{CL:CompleteLattice} I (f:I → X):X := ⊔ (fun x => ∃ (i:I), x = f i).
Notation "∩ f" := (meet_family f) (at level 60).
Notation " '⋂[' a ']' p " := ( ⊓ (fun x => ∃ a, x= p)) (at level 60).
Definition inf `{CL:CompleteLattice} (f:X → X):= ⋂[a] ((f a)).
Lemma meet_elim_trans `{CL:CompleteLattice}:
∀ (A : Ens) (z: X), (exists y , A y ∧ y ≤ z) → ⊓ A ≤ z.
Proof.
intros A z (y,(Hy,Hyz)).
apply (@ord_trans X Ord _ _ _ (meet_elim A y Hy) Hyz).
Qed.
Lemma join_elim_trans `{CL:CompleteLattice}:
∀ (A : Ens) (y: X), (exists z , A z ∧ y ≤ z) → y ≤ ⊔ A.
Proof.
dualityCL @meet_elim_trans.
Qed.
Tactics
We give a bunch of simple tactics to automatize the resolution of inequation involving meets and joinsLtac later:=eapply ex_intro.
Ltac auto_refl:=repeat (
match goal with
| [|- _ ∧ _ ]=> split
| [|- _ = _ ]=> reflexivity
end).
Ltac auto_meet_elim_trans:=repeat (apply meet_elim_trans;later;split;[later;reflexivity|]);try reflexivity.
Ltac auto_meet_elim_risky:=repeat (apply meet_elim_trans;later;split;[later;auto_refl|]);repeat(reflexivity);repeat(assumption).
Ltac auto_meet_intro:= let H:=fresh "H" in let H1:=fresh "H" in apply meet_intro;
try(intros ?x (?a,H);rewrite H);try(intros ?x (?a,(H,H1));rewrite H).
Ltac auto_meet_leq:= repeat auto_meet_intro; auto_meet_elim_trans.
Ltac auto_join_elim_trans:=repeat (apply join_elim_trans;later;split;[later;reflexivity|]);try reflexivity.
Ltac auto_join_elim_risky:=repeat (apply join_elim_trans;later;split;[later;auto_refl|]);try reflexivity.
Ltac auto_join_intro:= let H:=fresh "H" in let H1:=fresh "H" in apply join_intro;
try(intros ?x (?a,H);rewrite H);try(intros ?x (?a,(H,H1));rewrite H).
Ltac auto_join_leq:= repeat auto_join_intro; auto_join_elim_trans.
Lemma inf_elim_trans `{CL:CompleteLattice}:
∀ (f:X → X) (z:X), (exists b, f b ≤ z) → inf f ≤ z.
Proof.
intros f z (b,Hb).
eapply ord_trans.
- apply meet_elim;exists b;reflexivity.
- assumption.
Qed.
Lemma inf_comm_aux `{CL:CompleteLattice}:
∀(f:X→X→X), ⋂[a] (⋂[b] (f a b)) ≤ ⋂[b] (⋂[a] (f a b)).
Proof.
intro f.
auto_meet_leq.
Qed.
Lemma inf_comm `{CL:CompleteLattice}:
∀(f:X→X→X), ⋂[a] (⋂[b] (f a b)) = ⋂[b] (⋂[a] (f a b)).
Proof.
intro f.
apply ord_antisym;apply (inf_comm_aux).
Qed.
Lemma meet_comm_aux `{CL:CompleteLattice}:
∀(P:X→X→Prop) (f:X→X→X),
⊓ (λ x,∃ a, x=⊓(λ y,∃ b, y=f a b ∧ P a b)) ≤ ⊓ (λ y,∃ b, y=⊓(λ x,∃ a, x = f a b ∧ P a b)) .
Proof.
intros P f.
auto_meet_leq.
now auto_meet_elim_risky.
Qed.
Lemma meet_comm `{CL:CompleteLattice}:
∀(P:X→X→Prop) (f:X→X→X),
⊓ (λ x,∃ a, x=⊓(λ y,∃ b, y=f a b ∧ P a b)) = ⊓ (λ y,∃ b, y=⊓(λ x,∃ a, x = f a b ∧ P a b)).
Proof.
intros P f.
apply ord_antisym;apply (meet_comm_aux).
Qed.
Lemma meet_fam_elim `{CL:CompleteLattice}:
∀ I (f:I → X) (i:I), (∩ f) ≤ f(i).
Proof.
intros.
unfold meet_family.
apply meet_elim.
exists i.
reflexivity.
Qed.
Lemma meet_fam_intro `{CL:CompleteLattice}:
∀I f y, (∀ (i:I), y ≤ f i) → y ≤ ∩ f.
Proof.
intros.
apply meet_intro.
intros.
destruct H0 as [i Hi];rewrite Hi; auto.
Qed.
Lemma double_meet `{CL:CompleteLattice}:
∀ P, ⊓(λ x1 : X,∃ a0 : X, x1 = ⊓ (P a0))
= ∩ (fun x => ⊓ (P x)).
Proof.
intros.
reflexivity.
Qed.
Lemma double_meet_elim `{CL:CompleteLattice}:
∀ (f:X → X → X) a b, ∩ (fun x => ⊓ (fun y => ∃ z, y= f x z)) ≤ f a b.
Proof.
intros f a b.
apply (ord_trans _ ( ⊓ (λ y : X, ∃ z, y = f a z))).
* apply (meet_fam_elim (fun (x:X) => ⊓ (λ y : X, ∃ z : X, y = f x z))).
* apply meet_elim.
exists b;reflexivity.
Qed.
If two sets have the same elements, their meet are equal
Lemma meet_subset `{CL:CompleteLattice}:
∀ A B, subset A B -> ⊓ B ≤ ⊓ A.
Proof.
intros A B H.
apply meet_intro. intros x Ax.
apply meet_elim;intuition.
Qed.
Lemma meet_same_set_le `{CL:CompleteLattice}:
∀ A B, same_set A B -> ⊓ A ≤ ⊓ B.
Proof.
intros A B H.
apply meet_intro.
intros x Hx.
apply meet_elim.
apply H; exact Hx.
Qed.
Lemma meet_same_set `{CL:CompleteLattice}:
∀ A B, same_set A B -> ⊓ A = ⊓ B.
Proof.
intros A B H.
apply ord_antisym;apply meet_same_set_le;auto.
apply same_set_sym;auto.
Qed.
Global Instance meet_set_Proper `{CompleteLattice}:
Proper ((@same_set X) ==> (eq)) (meet_set).
Proof.
intros A B HAB.
apply meet_same_set; intuition.
Qed.
If two sets have the same elements, their join are equal
Lemma join_subset `{CL:CompleteLattice}: ∀ A B, subset A B -> ⊔ A ≤ ⊔ B.
Proof.
dualityCL @meet_subset.
Qed.
Lemma join_same_set `{CL:CompleteLattice}: ∀ A B, same_set A B -> ⊔ A = ⊔ B.
Proof.
dualityCL @meet_same_set.
Qed.
Global Instance join_set_Proper `{CompleteLattice}:
Proper ((@same_set X) ==> (eq)) (join_set).
Proof.
dualityCL @meet_set_Proper.
Qed.