semantics.ord.clat
Complete Lattices
Require Import base protype ordtype.
Module CLat.
Record mixin_of (T : ordType) := Mixin {
inf : forall I, (I -> T) -> T;
_ : forall I (F : I -> T), is_glb F (inf F)
}.
Section ClassDef.
Record class_of (T : Type) := Class {
base : Ord.class_of T;
mixin : mixin_of (Ord.Pack base T)
}.
Local Coercion base : class_of >-> Ord.class_of.
Structure type := Pack {sort; _ : class_of sort; _ : Type }.
Local Coercion sort : type >-> Sortclass.
Variable (T : Type) (cT : type).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack T c T.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).
Definition pack b0 (m0 : mixin_of (@Ord.Pack T b0 T)) :=
[find pt | Ord.sort pt ~ T | "is not an ordType"]
[find pe | Ord.class pt ~ pe]
[find m | m ~ m0 | "is not the right mixin"]
@Pack T (@Class T pe m) T.
Definition proType := @Pro.Pack cT xclass xT.
Definition ordType := @Ord.Pack cT xclass xT.
End ClassDef.
Module Exports.
Coercion base : class_of >-> Ord.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion proType : type >-> Pro.type.
Canonical proType.
Coercion ordType : type >-> Ord.type.
Canonical ordType.
Notation clat := type.
Notation CLatMixin := Mixin.
Notation CLat T m := (@pack T _ m _ id _ id _ id).
Notation "[ 'clatMixin' 'of' T ]" := (class _ : mixin_of T)
(at level 0, format "[ 'clatMixin' 'of' T ]") : form_scope.
Notation "[ 'clat' 'of' T 'for' C ]" := (@clone T C _ idfun)
(at level 0, format "[ 'clat' 'of' T 'for' C ]") : form_scope.
Notation "[ 'clat' 'of' T ]" := (@clone T _ _ id)
(at level 0, format "[ 'clat' 'of' T ]") : form_scope.
End Exports.
End CLat.
Export CLat.Exports.
Module CLat.
Record mixin_of (T : ordType) := Mixin {
inf : forall I, (I -> T) -> T;
_ : forall I (F : I -> T), is_glb F (inf F)
}.
Section ClassDef.
Record class_of (T : Type) := Class {
base : Ord.class_of T;
mixin : mixin_of (Ord.Pack base T)
}.
Local Coercion base : class_of >-> Ord.class_of.
Structure type := Pack {sort; _ : class_of sort; _ : Type }.
Local Coercion sort : type >-> Sortclass.
Variable (T : Type) (cT : type).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack T c T.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).
Definition pack b0 (m0 : mixin_of (@Ord.Pack T b0 T)) :=
[find pt | Ord.sort pt ~ T | "is not an ordType"]
[find pe | Ord.class pt ~ pe]
[find m | m ~ m0 | "is not the right mixin"]
@Pack T (@Class T pe m) T.
Definition proType := @Pro.Pack cT xclass xT.
Definition ordType := @Ord.Pack cT xclass xT.
End ClassDef.
Module Exports.
Coercion base : class_of >-> Ord.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion proType : type >-> Pro.type.
Canonical proType.
Coercion ordType : type >-> Ord.type.
Canonical ordType.
Notation clat := type.
Notation CLatMixin := Mixin.
Notation CLat T m := (@pack T _ m _ id _ id _ id).
Notation "[ 'clatMixin' 'of' T ]" := (class _ : mixin_of T)
(at level 0, format "[ 'clatMixin' 'of' T ]") : form_scope.
Notation "[ 'clat' 'of' T 'for' C ]" := (@clone T C _ idfun)
(at level 0, format "[ 'clat' 'of' T 'for' C ]") : form_scope.
Notation "[ 'clat' 'of' T ]" := (@clone T _ _ id)
(at level 0, format "[ 'clat' 'of' T ]") : form_scope.
End Exports.
End CLat.
Export CLat.Exports.
Definition inf {T : clat} {I : Type} (F : I -> T) : T :=
CLat.inf (CLat.class T) F.
Definition sup {T : clat} {I : Type} (F : I -> T) : T :=
inf (fun (p : { x : T | is_ub F x}) => sval p).
Definition bot {T : clat} : T := inf id.
Definition top {T : clat} : T := inf (fun b : False => match b with end).
Definition meet {T : clat} (x y : T) : T := inf (pairb x y).
Definition join {T : clat} (x y : T) : T := inf (fun (p : { z : T | (x ≤ z) /\ (y ≤ z) }) => sval p).
Definition supguard {T : clat} (P : Prop) (x : T) : T :=
sup (fun (_ : P) => x).
Definition infguard {T : clat} (P : Prop) (x : T) : T :=
inf (fun (_ : P) => x).
Notation "∀ x .. y , s" := (inf (fun x => .. (inf (fun y => s%ORD)) .. ))
(at level 98, x binder, y binder, right associativity,
format "'[' ∀ x .. y , '/ ' s ']'") : ord_scope.
Notation "∀ x .. y | p , s" := (inf (fun x => .. (inf (fun y => infguard p s%ORD)) .. ))
(at level 98, x binder, y binder, right associativity,
format "'[' ∀ x .. y | p , '/ ' s ']'") : ord_scope.
Notation "∃ x .. y , s" := (sup (fun x => .. (sup (fun y => s%ORD)) .. ))
(at level 98, x binder, y binder, right associativity,
format "'[' ∃ x .. y , '/ ' s ']'") : ord_scope.
Notation "∃ x .. y | p , s" := (sup (fun x => .. (sup (fun y => supguard p s%ORD)) .. ))
(at level 98, x binder, y binder, right associativity,
format "'[' ∃ x .. y | p , '/ ' s ']'") : ord_scope.
Notation "⊤" := top : ord_scope.
Notation "⊥" := bot : ord_scope.
Infix "∧" := meet (at level 80, right associativity) : ord_scope.
Infix "∨" := join (at level 85, right associativity) : ord_scope.
Definition inf_closed {A : clat} (P : A -> Prop) :=
forall I (F : I -> A), (forall i, P (F i)) -> P (inf F).
forall I (F : I -> A), (forall i, P (F i)) -> P (inf F).
Definition sup_closed {A : clat} (P : A -> Prop) :=
forall I (F : I -> A), (forall i, P (F i)) -> P (sup F).
Section Rules.
Variable (T : clat).
Implicit Types (x y z : T).
Lemma all_axiom I (F : I -> T) : is_glb F (inf F).
Proof. by case: T F => [?[?[]]]. Qed.
Lemma allI I (F : I -> T) x : (forall i, x ≤ F i) -> x ≤ inf F.
Proof. exact/glbP/all_axiom. Qed.
Lemma allE I (F : I -> T) x i : F i ≤ x -> inf F ≤ x.
Proof. move<-. exact/lbP/all_axiom. Qed.
Lemma allIc I (P : I -> Prop) (F : I -> T) x :
(forall i, P i -> x ≤ F i) -> x ≤ ∀ i | P i, F i.
Proof. move=> h. apply: allI => i. apply: allI. exact: h. Qed.
Lemma allEc I (P : I -> Prop) (F : I -> T) x i :
P i -> F i ≤ x -> ∀ i | P i, F i ≤ x.
Proof. move=> pi h. apply: allE (i) _. exact: allE pi h. Qed.
Lemma ex_axiom I (F : I -> T) : is_lub F (sup F).
Proof.
apply: mk_lub.
- move=> x. apply: allI => -[y /=]. exact.
- move=> y ub. exact: allE (exist _ y ub) le_refl.
Qed.
Lemma exE I (F : I -> T) x : (forall i, F i ≤ x) -> sup F ≤ x.
Proof. exact/lubP/ex_axiom. Qed.
Lemma exI I (F : I -> T) x i : x ≤ F i -> x ≤ sup F.
Proof. move->. exact/ubP/ex_axiom. Qed.
Lemma exEc I (P : I -> Prop) (F : I -> T) x :
(forall i, P i -> F i ≤ x) -> ∃ i | P i, F i ≤ x.
Proof. move=> h. apply: exE => i. apply: exE. exact: h. Qed.
Lemma exIc I (P : I -> Prop) (F : I -> T) x i :
P i -> x ≤ F i -> x ≤ ∃ i | P i, F i.
Proof. move=> pi h. apply: exI (i) _. exact: exI pi h. Qed.
Lemma botE x : ⊥ ≤ x.
Proof. exact: allE le_refl. Qed.
Lemma topI x : x ≤ ⊤.
Proof. exact: allI. Qed.
Lemma meet_axiom x y : is_glb (pairb x y) (x ∧ y).
Proof. exact: all_axiom. Qed.
Lemma meetI x y z : x ≤ y -> x ≤ z -> x ≤ y ∧ z.
Proof. move=> le_x_y le_x_z. by apply: allI => -[]/=. Qed.
Lemma meetEl x y z : x ≤ z -> x ∧ y ≤ z.
Proof. move=> le_x_z. exact: allE true _. Qed.
Lemma meetEr x y z : y ≤ z -> x ∧ y ≤ z.
Proof. move=> le_y_z. exact: allE false _. Qed.
Lemma join_axiom x y : is_lub (pairb x y) (x ∨ y).
Proof.
move=> z. split.
- move=> le_xy_z -[] /=; rewrite -le_xy_z; by apply: allI => -[w [/=]].
- move=> h. apply: allE (exist _ z _) _ => //=. split.
exact: (h true). exact: (h false).
Qed.
Lemma joinE x y z : x ≤ z -> y ≤ z -> x ∨ y ≤ z.
Proof. move=> le_x_z le_y_z. by apply/join_axiom => -[]/=. Qed.
Lemma joinIl x y z : x ≤ y -> x ≤ y ∨ z.
Proof. move->. by apply: allI => -[?[]] /=. Qed.
Lemma joinIr x y z : x ≤ z -> x ≤ y ∨ z.
Proof. move->. by apply: allI => -[?[]] /=. Qed.
End Rules.
Hint Resolve botE topI.
Ltac focus1p :=
match goal with
| [|- ?x ≤ ?x] => exact: le_refl
| [|- _ ≤ ⊤] => exact: topI
| [|- ⊥ ≤ _] => exact: botE
| [|- sup _ ≤ _] => apply: exE; intro
| [|- supguard _ _ ≤ _] => apply: exE; intro
| [|- _ ≤ inf _] => apply: allI; intro
| [|- _ ≤ infguard _ _] => apply: allI; intro
| [|- _ ≤ _ ∧ _] => apply: meetI
| [|- _ ∨ _ ≤ _] => apply: joinE
end.
Ltac focus := nointr (repeat focus1p).
Ltac focusn := done ||
match goal with
| [|- _ ∧ _ ≤ _] => (apply: meetEl; focusn) || (apply: meetEr; focusn)
| [|- _ ≤ _ ∨ _] => (apply: joinIl; focusn) || (apply: joinIr; focusn)
| [|- inf _ ≤ _] => apply: allE; focusn
| [|- infguard _ _ ≤ _] => apply: allE; focusn
| [|- _ ≤ sup _] => apply: exI; focusn
| [|- _ ≤ supguard _ _] => apply: exI; focusn
end.
Ltac cauto := try apply: le_eq; repeat focus1p; focusn.
Section JLatLaws.
Variable (T : clat).
Implicit Types (x y z : T).
Lemma joinxx : idempotent (@join T).
Proof. move=> x. cauto. Qed.
Lemma joinC : commutative (@join T).
Proof. move=> x y. cauto. Qed.
Lemma joinA : associative (@join T).
Proof. move=> x y z. cauto. Qed.
Lemma joinAC : right_commutative (@join T).
Proof. move=> x y z. cauto. Qed.
Lemma joinCA : left_commutative (@join T).
Proof. move=> x y z. cauto. Qed.
Lemma joinACA : interchange (@join T) (@join T).
Proof. move=> w x y z. cauto. Qed.
Lemma joinBx x : (⊥ ∨ x) = x.
Proof. cauto. Qed.
Lemma joinxB x : (x ∨ ⊥) = x.
Proof. cauto. Qed.
Lemma bot_eq x : x ≤ ⊥ -> x = ⊥.
Proof. move=> h. cauto. Qed.
Lemma le_joinP x y : (x ≤ y) <-> ((x ∨ y) = y).
Proof. split=> [h|<-]; cauto. Qed.
Lemma join_mono x1 x2 y1 y2 : x1 ≤ x2 -> y1 ≤ y2 -> x1 ∨ y1 ≤ x2 ∨ y2.
Proof. move=> h1 h2. cauto. Qed.
Global Instance join_proper : Proper (ord_op ++> ord_op ++> ord_op) (@join T).
Proof. move=> x1 x2 le1 y1 y2 le2. cauto. Qed.
Canonical join_monoid := Monoid.Law joinA joinBx joinxB.
Canonical join_comoid := Monoid.ComLaw joinC.
End JLatLaws.
Section MLatLaws.
Variable (T : clat).
Implicit Types (x y z : T).
Lemma meetxx : idempotent (@meet T).
Proof. move=> x. cauto. Qed.
Lemma meetC : commutative (@meet T).
Proof. move=> x y. cauto. Qed.
Lemma meetA : associative (@meet T).
Proof. move=> x y z. cauto. Qed.
Lemma meetAC : right_commutative (@meet T).
Proof. move=> x y z. cauto. Qed.
Lemma meetCA : left_commutative (@meet T).
Proof. move=> x y z. cauto. Qed.
Lemma meetACA : interchange (@meet T) (@meet T).
Proof. move=> w x y z. cauto. Qed.
Lemma meetTx x : (⊤ ∧ x) = x.
Proof. cauto. Qed.
Lemma meetxT x : (x ∧ ⊤) = x.
Proof. cauto. Qed.
Lemma top_eq x : ⊤ ≤ x -> x = ⊤.
Proof. move=> h. cauto. Qed.
Lemma le_meetP x y : (x ≤ y) <-> (x = (x ∧ y)).
Proof. split=> [h|->]; cauto. Qed.
Lemma meet_mono x1 x2 y1 y2 : x1 ≤ x2 -> y1 ≤ y2 -> x1 ∧ y1 ≤ x2 ∧ y2.
Proof. move=> h1 h2. cauto. Qed.
Global Instance meet_proper : Proper (ord_op ++> ord_op ++> ord_op) (@meet T).
Proof. move=> x1 x2 le1 y1 y2 le2. cauto. Qed.
Canonical meet_monoid := Monoid.Law meetA meetTx meetxT.
Canonical meet_comoid := Monoid.ComLaw meetC.
End MLatLaws.
Section LatLaws.
Variable (T : clat).
Implicit Types (x y z : T).
Lemma meetxK x y : (x ∧ (y ∨ x)) = x.
Proof. cauto. Qed.
Lemma meetKx x y : (x ∧ (x ∨ y)) = x.
Proof. cauto. Qed.
Lemma joinxK x y : (x ∨ (y ∧ x)) = x.
Proof. cauto. Qed.
Lemma joinKx x y : (x ∨ (x ∧ y)) = x.
Proof. cauto. Qed.
Lemma joinTx x : (⊤ ∨ x) = ⊤.
Proof. cauto. Qed.
Lemma joinxT x : (x ∨ ⊤) = ⊤.
Proof. cauto. Qed.
Lemma meetBx x : (⊥ ∧ x) = ⊥.
Proof. cauto. Qed.
Lemma meetxB x : (x ∧ ⊥) = ⊥.
Proof. cauto. Qed.
End LatLaws.
Section CLatLaws.
Variable (T : clat).
Lemma all_mono I (F G : I -> T) :
(forall i, F i ≤ G i) -> ∀ i, F i ≤ ∀ i, G i.
Proof. move=> h. cauto. Qed.
Lemma ex_mono I (F G : I -> T) :
(forall i, F i ≤ G i) -> ∃ i, F i ≤ ∃ i, G i.
Proof. move=> h. cauto. Qed.
End CLatLaws.
Section CLatDef.
Variable (T : clat).
Implicit Types (x y z : T).
Lemma top_def x : ⊤ ≤ x -> ⊤ = x.
Proof. move=> h. cauto. Qed.
Lemma bot_def x : x ≤ ⊥ -> ⊥ = x.
Proof. move=> h. cauto. Qed.
Lemma join_def x y z :
x ≤ z ->
y ≤ z ->
(forall w, x ≤ w -> y ≤ w -> z ≤ w) ->
(x ∨ y) = z.
Proof.
move=> h1 h2 h3. apply: le_eq. cauto. apply: h3; cauto.
Qed.
Lemma meet_def x y z :
z ≤ x ->
z ≤ y ->
(forall w, w ≤ x -> w ≤ y -> w ≤ z) ->
(x ∧ y) = z.
Proof.
move=> h1 h2 h3. apply: le_eq. apply: h3; cauto. cauto.
Qed.
Lemma ex_def I (F : I -> T) x :
(forall i, F i ≤ x) ->
(forall y, (forall i, F i ≤ y) -> x ≤ y) ->
sup F = x.
Proof.
move=> h1 h2. apply: le_eq. cauto. apply: h2 => i. cauto.
Qed.
Lemma all_def I (F : I -> T) x :
(forall i, x ≤ F i) ->
(forall y, (forall i, y ≤ F i) -> y ≤ x) ->
inf F = x.
Proof.
move=> h1 h2. apply: le_eq. apply: h2 => i. cauto. cauto.
Qed.
End CLatDef.
Section ReverseCLat.
Variable X : clat.
Definition rev_inf I (F : I -> X^r) : X^r := sup F.
Lemma rev_infP I (F : I -> X^r) : is_glb F (rev_inf F).
Proof.
apply: mk_glb.
- move=> i. rewrite rev_leE /rev_inf. by cauto.
- move=> /=x xP. rewrite rev_leE /rev_inf. focus=> i. exact: xP.
Qed.
Canonical reverse_clatMixin := CLatMixin rev_infP.
Canonical reverse_clat := Eval hnf in CLat X^r reverse_clatMixin.
End ReverseCLat.
Lemma rev_allE (X : clat) I (F : I -> X) :
@inf (reverse_clat X) I F = @sup X I F.
Proof. by []. Qed.
Lemma rev_allEc (X : clat) I (F : I -> X^r) (P : I -> Prop) :
(∀ i | P i, F i) = ∃ i | P i, (F i : X).
Proof. by []. Qed.
Lemma rev_exE (X : clat) I (F : I -> X) :
@sup (reverse_clat X) I F = @inf X I F.
Proof.
apply: ex_def. move=> i. rewrite rev_leE. cauto. move=> /= x xP. rewrite rev_leE. focus=> i. exact: xP.
Qed.
Lemma rev_exEc (X : clat) I (F : I -> X^r) (P : I -> Prop) :
(∃ i | P i, F i) = ∀ i | P i, (F i : X).
Proof.
rewrite rev_exE. f_equal. fext=> i. exact: rev_exE.
Qed.
forall I (F : I -> A), (forall i, P (F i)) -> P (sup F).
Section Rules.
Variable (T : clat).
Implicit Types (x y z : T).
Lemma all_axiom I (F : I -> T) : is_glb F (inf F).
Proof. by case: T F => [?[?[]]]. Qed.
Lemma allI I (F : I -> T) x : (forall i, x ≤ F i) -> x ≤ inf F.
Proof. exact/glbP/all_axiom. Qed.
Lemma allE I (F : I -> T) x i : F i ≤ x -> inf F ≤ x.
Proof. move<-. exact/lbP/all_axiom. Qed.
Lemma allIc I (P : I -> Prop) (F : I -> T) x :
(forall i, P i -> x ≤ F i) -> x ≤ ∀ i | P i, F i.
Proof. move=> h. apply: allI => i. apply: allI. exact: h. Qed.
Lemma allEc I (P : I -> Prop) (F : I -> T) x i :
P i -> F i ≤ x -> ∀ i | P i, F i ≤ x.
Proof. move=> pi h. apply: allE (i) _. exact: allE pi h. Qed.
Lemma ex_axiom I (F : I -> T) : is_lub F (sup F).
Proof.
apply: mk_lub.
- move=> x. apply: allI => -[y /=]. exact.
- move=> y ub. exact: allE (exist _ y ub) le_refl.
Qed.
Lemma exE I (F : I -> T) x : (forall i, F i ≤ x) -> sup F ≤ x.
Proof. exact/lubP/ex_axiom. Qed.
Lemma exI I (F : I -> T) x i : x ≤ F i -> x ≤ sup F.
Proof. move->. exact/ubP/ex_axiom. Qed.
Lemma exEc I (P : I -> Prop) (F : I -> T) x :
(forall i, P i -> F i ≤ x) -> ∃ i | P i, F i ≤ x.
Proof. move=> h. apply: exE => i. apply: exE. exact: h. Qed.
Lemma exIc I (P : I -> Prop) (F : I -> T) x i :
P i -> x ≤ F i -> x ≤ ∃ i | P i, F i.
Proof. move=> pi h. apply: exI (i) _. exact: exI pi h. Qed.
Lemma botE x : ⊥ ≤ x.
Proof. exact: allE le_refl. Qed.
Lemma topI x : x ≤ ⊤.
Proof. exact: allI. Qed.
Lemma meet_axiom x y : is_glb (pairb x y) (x ∧ y).
Proof. exact: all_axiom. Qed.
Lemma meetI x y z : x ≤ y -> x ≤ z -> x ≤ y ∧ z.
Proof. move=> le_x_y le_x_z. by apply: allI => -[]/=. Qed.
Lemma meetEl x y z : x ≤ z -> x ∧ y ≤ z.
Proof. move=> le_x_z. exact: allE true _. Qed.
Lemma meetEr x y z : y ≤ z -> x ∧ y ≤ z.
Proof. move=> le_y_z. exact: allE false _. Qed.
Lemma join_axiom x y : is_lub (pairb x y) (x ∨ y).
Proof.
move=> z. split.
- move=> le_xy_z -[] /=; rewrite -le_xy_z; by apply: allI => -[w [/=]].
- move=> h. apply: allE (exist _ z _) _ => //=. split.
exact: (h true). exact: (h false).
Qed.
Lemma joinE x y z : x ≤ z -> y ≤ z -> x ∨ y ≤ z.
Proof. move=> le_x_z le_y_z. by apply/join_axiom => -[]/=. Qed.
Lemma joinIl x y z : x ≤ y -> x ≤ y ∨ z.
Proof. move->. by apply: allI => -[?[]] /=. Qed.
Lemma joinIr x y z : x ≤ z -> x ≤ y ∨ z.
Proof. move->. by apply: allI => -[?[]] /=. Qed.
End Rules.
Hint Resolve botE topI.
Ltac focus1p :=
match goal with
| [|- ?x ≤ ?x] => exact: le_refl
| [|- _ ≤ ⊤] => exact: topI
| [|- ⊥ ≤ _] => exact: botE
| [|- sup _ ≤ _] => apply: exE; intro
| [|- supguard _ _ ≤ _] => apply: exE; intro
| [|- _ ≤ inf _] => apply: allI; intro
| [|- _ ≤ infguard _ _] => apply: allI; intro
| [|- _ ≤ _ ∧ _] => apply: meetI
| [|- _ ∨ _ ≤ _] => apply: joinE
end.
Ltac focus := nointr (repeat focus1p).
Ltac focusn := done ||
match goal with
| [|- _ ∧ _ ≤ _] => (apply: meetEl; focusn) || (apply: meetEr; focusn)
| [|- _ ≤ _ ∨ _] => (apply: joinIl; focusn) || (apply: joinIr; focusn)
| [|- inf _ ≤ _] => apply: allE; focusn
| [|- infguard _ _ ≤ _] => apply: allE; focusn
| [|- _ ≤ sup _] => apply: exI; focusn
| [|- _ ≤ supguard _ _] => apply: exI; focusn
end.
Ltac cauto := try apply: le_eq; repeat focus1p; focusn.
Section JLatLaws.
Variable (T : clat).
Implicit Types (x y z : T).
Lemma joinxx : idempotent (@join T).
Proof. move=> x. cauto. Qed.
Lemma joinC : commutative (@join T).
Proof. move=> x y. cauto. Qed.
Lemma joinA : associative (@join T).
Proof. move=> x y z. cauto. Qed.
Lemma joinAC : right_commutative (@join T).
Proof. move=> x y z. cauto. Qed.
Lemma joinCA : left_commutative (@join T).
Proof. move=> x y z. cauto. Qed.
Lemma joinACA : interchange (@join T) (@join T).
Proof. move=> w x y z. cauto. Qed.
Lemma joinBx x : (⊥ ∨ x) = x.
Proof. cauto. Qed.
Lemma joinxB x : (x ∨ ⊥) = x.
Proof. cauto. Qed.
Lemma bot_eq x : x ≤ ⊥ -> x = ⊥.
Proof. move=> h. cauto. Qed.
Lemma le_joinP x y : (x ≤ y) <-> ((x ∨ y) = y).
Proof. split=> [h|<-]; cauto. Qed.
Lemma join_mono x1 x2 y1 y2 : x1 ≤ x2 -> y1 ≤ y2 -> x1 ∨ y1 ≤ x2 ∨ y2.
Proof. move=> h1 h2. cauto. Qed.
Global Instance join_proper : Proper (ord_op ++> ord_op ++> ord_op) (@join T).
Proof. move=> x1 x2 le1 y1 y2 le2. cauto. Qed.
Canonical join_monoid := Monoid.Law joinA joinBx joinxB.
Canonical join_comoid := Monoid.ComLaw joinC.
End JLatLaws.
Section MLatLaws.
Variable (T : clat).
Implicit Types (x y z : T).
Lemma meetxx : idempotent (@meet T).
Proof. move=> x. cauto. Qed.
Lemma meetC : commutative (@meet T).
Proof. move=> x y. cauto. Qed.
Lemma meetA : associative (@meet T).
Proof. move=> x y z. cauto. Qed.
Lemma meetAC : right_commutative (@meet T).
Proof. move=> x y z. cauto. Qed.
Lemma meetCA : left_commutative (@meet T).
Proof. move=> x y z. cauto. Qed.
Lemma meetACA : interchange (@meet T) (@meet T).
Proof. move=> w x y z. cauto. Qed.
Lemma meetTx x : (⊤ ∧ x) = x.
Proof. cauto. Qed.
Lemma meetxT x : (x ∧ ⊤) = x.
Proof. cauto. Qed.
Lemma top_eq x : ⊤ ≤ x -> x = ⊤.
Proof. move=> h. cauto. Qed.
Lemma le_meetP x y : (x ≤ y) <-> (x = (x ∧ y)).
Proof. split=> [h|->]; cauto. Qed.
Lemma meet_mono x1 x2 y1 y2 : x1 ≤ x2 -> y1 ≤ y2 -> x1 ∧ y1 ≤ x2 ∧ y2.
Proof. move=> h1 h2. cauto. Qed.
Global Instance meet_proper : Proper (ord_op ++> ord_op ++> ord_op) (@meet T).
Proof. move=> x1 x2 le1 y1 y2 le2. cauto. Qed.
Canonical meet_monoid := Monoid.Law meetA meetTx meetxT.
Canonical meet_comoid := Monoid.ComLaw meetC.
End MLatLaws.
Section LatLaws.
Variable (T : clat).
Implicit Types (x y z : T).
Lemma meetxK x y : (x ∧ (y ∨ x)) = x.
Proof. cauto. Qed.
Lemma meetKx x y : (x ∧ (x ∨ y)) = x.
Proof. cauto. Qed.
Lemma joinxK x y : (x ∨ (y ∧ x)) = x.
Proof. cauto. Qed.
Lemma joinKx x y : (x ∨ (x ∧ y)) = x.
Proof. cauto. Qed.
Lemma joinTx x : (⊤ ∨ x) = ⊤.
Proof. cauto. Qed.
Lemma joinxT x : (x ∨ ⊤) = ⊤.
Proof. cauto. Qed.
Lemma meetBx x : (⊥ ∧ x) = ⊥.
Proof. cauto. Qed.
Lemma meetxB x : (x ∧ ⊥) = ⊥.
Proof. cauto. Qed.
End LatLaws.
Section CLatLaws.
Variable (T : clat).
Lemma all_mono I (F G : I -> T) :
(forall i, F i ≤ G i) -> ∀ i, F i ≤ ∀ i, G i.
Proof. move=> h. cauto. Qed.
Lemma ex_mono I (F G : I -> T) :
(forall i, F i ≤ G i) -> ∃ i, F i ≤ ∃ i, G i.
Proof. move=> h. cauto. Qed.
End CLatLaws.
Section CLatDef.
Variable (T : clat).
Implicit Types (x y z : T).
Lemma top_def x : ⊤ ≤ x -> ⊤ = x.
Proof. move=> h. cauto. Qed.
Lemma bot_def x : x ≤ ⊥ -> ⊥ = x.
Proof. move=> h. cauto. Qed.
Lemma join_def x y z :
x ≤ z ->
y ≤ z ->
(forall w, x ≤ w -> y ≤ w -> z ≤ w) ->
(x ∨ y) = z.
Proof.
move=> h1 h2 h3. apply: le_eq. cauto. apply: h3; cauto.
Qed.
Lemma meet_def x y z :
z ≤ x ->
z ≤ y ->
(forall w, w ≤ x -> w ≤ y -> w ≤ z) ->
(x ∧ y) = z.
Proof.
move=> h1 h2 h3. apply: le_eq. apply: h3; cauto. cauto.
Qed.
Lemma ex_def I (F : I -> T) x :
(forall i, F i ≤ x) ->
(forall y, (forall i, F i ≤ y) -> x ≤ y) ->
sup F = x.
Proof.
move=> h1 h2. apply: le_eq. cauto. apply: h2 => i. cauto.
Qed.
Lemma all_def I (F : I -> T) x :
(forall i, x ≤ F i) ->
(forall y, (forall i, y ≤ F i) -> y ≤ x) ->
inf F = x.
Proof.
move=> h1 h2. apply: le_eq. apply: h2 => i. cauto. cauto.
Qed.
End CLatDef.
Section ReverseCLat.
Variable X : clat.
Definition rev_inf I (F : I -> X^r) : X^r := sup F.
Lemma rev_infP I (F : I -> X^r) : is_glb F (rev_inf F).
Proof.
apply: mk_glb.
- move=> i. rewrite rev_leE /rev_inf. by cauto.
- move=> /=x xP. rewrite rev_leE /rev_inf. focus=> i. exact: xP.
Qed.
Canonical reverse_clatMixin := CLatMixin rev_infP.
Canonical reverse_clat := Eval hnf in CLat X^r reverse_clatMixin.
End ReverseCLat.
Lemma rev_allE (X : clat) I (F : I -> X) :
@inf (reverse_clat X) I F = @sup X I F.
Proof. by []. Qed.
Lemma rev_allEc (X : clat) I (F : I -> X^r) (P : I -> Prop) :
(∀ i | P i, F i) = ∃ i | P i, (F i : X).
Proof. by []. Qed.
Lemma rev_exE (X : clat) I (F : I -> X) :
@sup (reverse_clat X) I F = @inf X I F.
Proof.
apply: ex_def. move=> i. rewrite rev_leE. cauto. move=> /= x xP. rewrite rev_leE. focus=> i. exact: xP.
Qed.
Lemma rev_exEc (X : clat) I (F : I -> X^r) (P : I -> Prop) :
(∃ i | P i, F i) = ∀ i | P i, (F i : X).
Proof.
rewrite rev_exE. f_equal. fext=> i. exact: rev_exE.
Qed.