semantics.tower.llat
Require Import base ord.
Module LLat.
Record mixin_of (T : clat) := Mixin {
lt : T -> T -> Prop;
_ : forall x y z, lt x y -> (y ≤ z) -> lt x z;
_ : forall x y z, (x ≤ y) -> lt y z -> lt x z;
_ : forall I (F : I -> T) x,
lt (inf F) x -> exists i, lt (F i) x
}.
Section ClassDef.
Record class_of (T : Type) := Class {
base : CLat.class_of T;
mixin : mixin_of (CLat.Pack base T)
}.
Local Coercion base : class_of >-> CLat.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 (@CLat.Pack T b0 T)) :=
[find pt | CLat.sort pt ~ T | "is not a clat"]
[find pe | CLat.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.
Definition clat := @CLat.Pack cT xclass xT.
End ClassDef.
Module Exports.
Coercion base : class_of >-> CLat.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.
Coercion clat : type >-> CLat.type.
Canonical clat.
Notation llat := type.
Notation LLatMixin := Mixin.
Notation LLat T m := (@pack T _ m _ id _ id _ id).
Notation "[ 'llatMixin' 'of' T ]" := (class _ : mixin_of T)
(at level 0, format "[ 'llatMixin' 'of' T ]") : form_scope.
Notation "[ 'llat' 'of' T 'for' C ]" := (@clone T C _ idfun)
(at level 0, format "[ 'llat' 'of' T 'for' C ]") : form_scope.
Notation "[ 'llat' 'of' T ]" := (@clone T _ _ id)
(at level 0, format "[ 'llat' 'of' T ]") : form_scope.
End Exports.
End LLat.
Export LLat.Exports.
Definition ord_l_op (T : llat) (x y : T) := LLat.lt (LLat.class T) x y.
Notation "x ⊏ y" := (ord_l_op x%ORD y%ORD)
(at level 99, y at next level, no associativity) : ord_scope.
Notation "x ⊏ y :> T" := ((x:T) ⊏ (y:T))
(at level 99, y at next level, no associativity) : ord_scope.
Section LLatLemmas.
Variable (T : llat).
Implicit Types (x y z : T).
Lemma lt_left x y z : (x ⊏ y) -> (y ≤ z) -> x ⊏ z.
Proof. by case: T x y z => ?[?[]]. Qed.
Lemma lt_right x y z : (x ≤ y) -> (y ⊏ z) -> x ⊏ z.
Proof. by case: T x y z => ?[?[]]. Qed.
Lemma lt_inf I (F : I -> T) x : (inf F ⊏ x) -> exists i, F i ⊏ x.
Proof. case: T F x => ?[?[*]]; by eauto. Qed.
End LLatLemmas.
Class lmonotone {T : llat} (f : T -> T) : Prop := {
lmonotone_to_monotone :> monotone f;
lmonoP : forall x y, (f x ⊏ f y) -> x ⊏ y
}.
Module LLat.
Record mixin_of (T : clat) := Mixin {
lt : T -> T -> Prop;
_ : forall x y z, lt x y -> (y ≤ z) -> lt x z;
_ : forall x y z, (x ≤ y) -> lt y z -> lt x z;
_ : forall I (F : I -> T) x,
lt (inf F) x -> exists i, lt (F i) x
}.
Section ClassDef.
Record class_of (T : Type) := Class {
base : CLat.class_of T;
mixin : mixin_of (CLat.Pack base T)
}.
Local Coercion base : class_of >-> CLat.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 (@CLat.Pack T b0 T)) :=
[find pt | CLat.sort pt ~ T | "is not a clat"]
[find pe | CLat.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.
Definition clat := @CLat.Pack cT xclass xT.
End ClassDef.
Module Exports.
Coercion base : class_of >-> CLat.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.
Coercion clat : type >-> CLat.type.
Canonical clat.
Notation llat := type.
Notation LLatMixin := Mixin.
Notation LLat T m := (@pack T _ m _ id _ id _ id).
Notation "[ 'llatMixin' 'of' T ]" := (class _ : mixin_of T)
(at level 0, format "[ 'llatMixin' 'of' T ]") : form_scope.
Notation "[ 'llat' 'of' T 'for' C ]" := (@clone T C _ idfun)
(at level 0, format "[ 'llat' 'of' T 'for' C ]") : form_scope.
Notation "[ 'llat' 'of' T ]" := (@clone T _ _ id)
(at level 0, format "[ 'llat' 'of' T ]") : form_scope.
End Exports.
End LLat.
Export LLat.Exports.
Definition ord_l_op (T : llat) (x y : T) := LLat.lt (LLat.class T) x y.
Notation "x ⊏ y" := (ord_l_op x%ORD y%ORD)
(at level 99, y at next level, no associativity) : ord_scope.
Notation "x ⊏ y :> T" := ((x:T) ⊏ (y:T))
(at level 99, y at next level, no associativity) : ord_scope.
Section LLatLemmas.
Variable (T : llat).
Implicit Types (x y z : T).
Lemma lt_left x y z : (x ⊏ y) -> (y ≤ z) -> x ⊏ z.
Proof. by case: T x y z => ?[?[]]. Qed.
Lemma lt_right x y z : (x ≤ y) -> (y ⊏ z) -> x ⊏ z.
Proof. by case: T x y z => ?[?[]]. Qed.
Lemma lt_inf I (F : I -> T) x : (inf F ⊏ x) -> exists i, F i ⊏ x.
Proof. case: T F x => ?[?[*]]; by eauto. Qed.
End LLatLemmas.
Class lmonotone {T : llat} (f : T -> T) : Prop := {
lmonotone_to_monotone :> monotone f;
lmonoP : forall x y, (f x ⊏ f y) -> x ⊏ y
}.
Reserved Notation "x ^+" (at level 3, left associativity, format "x ^+").
Reserved Notation "x ^-" (at level 3, left associativity, format "x ^-").
Record lprop := mk_lprop { chuL : Prop; chuR : Prop; _ : chuL -> chuR -> False }.
Arguments mk_lprop l r p : rename, clear implicits.
Notation "p ^+" := (chuL p).
Notation "p ^-" := (chuR p).
Section Chu.
Implicit Types (p q r : lprop).
Implicit Types (x y z : Prop).
Lemma chuP p : p^+ -> p^- -> False.
Proof. by case: p. Qed.
Definition chu_le p q := (chuL p ≤ chuL q) /\ (chuR q ≤ chuR p).
Lemma chu_le_refl : reflexive chu_le.
Proof. by split. Qed.
Lemma chu_le_trans : transitive chu_le.
Proof. move=> p q r [h1 h2] [h3 h4]. split. by rewrite h1. by rewrite h4. Qed.
Canonical chu_proMixin := ProMixin chu_le_refl chu_le_trans.
Canonical lprop_proType := Eval hnf in ProType lprop chu_proMixin.
Lemma chu_eq p q : chuL p = chuL q -> chuR p = chuR q -> p = q.
Proof.
move: p q => [l1 r1 h1] [l2 r2 h2] /= e1 e2. destruct e1, e2.
f_equal. exact: pi.
Qed.
Lemma chu_le_eq p q : p ≤ q -> q ≤ p -> p = q.
Proof.
move=> [l1 r1] [l2 r2]. apply: chu_eq; exact: le_eq.
Qed.
Canonical chu_ordMixin := OrdMixin chu_le_eq.
Canonical lprop_ordType := Eval hnf in OrdType lprop chu_ordMixin.
Program Definition chu_inf T (F : T -> lprop) := mk_lprop (inf (chuL \o F)) (sup (chuR \o F)) _.
Next Obligation.
rewrite prop_exE in H0. case: H0 => y /=. apply: chuP. exact: H.
Qed.
Lemma chu_infP T (F : T -> lprop) : is_glb F (chu_inf F).
Proof.
move=> x /=. split. move=> [/=h1 h2] i. split. rewrite h1. exact: allE (i) _.
rewrite -h2. exact: exI (i) _. move=> h. split=> /=. apply: allI => i /=.
by case: (h i). apply: exE => i /=. by case: (h i).
Qed.
Canonical chu_clatMixin := CLatMixin chu_infP.
Canonical lprop_clat := Eval hnf in CLat lprop chu_clatMixin.
Definition chu_lt (A B : lprop) : Prop :=
chuR A /\ chuL B.
Lemma chu_lt_left p q r :
chu_lt p q -> (q ≤ r) -> chu_lt p r.
Proof.
move=> [na pb] [bc _]. split=> //. exact: bc.
Qed.
Lemma chu_lt_right p q r :
(p ≤ q) -> chu_lt q r -> chu_lt p r.
Proof.
move=> [_ ba] [nb pc]. split=> //. exact: ba.
Qed.
Lemma chu_lt_inf I (F : I -> lprop) p :
chu_lt (inf F) p -> exists i, chu_lt (F i) p.
Proof.
move=> [/=]. rewrite prop_exE /= => -[i nfi] pa. exists i. by split.
Qed.
Canonical chu_llatMixin := LLatMixin chu_lt_left chu_lt_right chu_lt_inf.
Canonical chu_llat := Eval hnf in LLat lprop chu_llatMixin.
End Chu.
Section IProdLLat.
Variables (T : Type) (F : T -> llat).
Implicit Types (f g h : iprod F) (x : T).
Definition iprod_lt f g := exists x, f x ⊏ g x.
Lemma iprod_lt_left f g h :
iprod_lt f g -> (g ≤ h) -> iprod_lt f h.
Proof.
move=> -[x lt_fx_gx] le_g_h. exists x. exact: lt_left (le_g_h x).
Qed.
Lemma iprod_lt_right f g h :
(f ≤ g) -> iprod_lt g h -> iprod_lt f h.
Proof.
move=> le_f_g [x lt_gx_hx]. exists x. exact: lt_right (le_f_g x) _.
Qed.
Lemma iprod_lt_inf I (P : I -> iprod F) f :
iprod_lt (inf P) f -> exists i, iprod_lt (P i) f.
Proof.
case=> x /lt_inf[i lt_Px_fx]. exists i. exists x. exact: lt_Px_fx.
Qed.
Canonical iprod_llatMixin := LLatMixin iprod_lt_left iprod_lt_right iprod_lt_inf.
Canonical iprod_llat := Eval hnf in LLat (iprod F) iprod_llatMixin.
End IProdLLat.
Variables (T : Type) (F : T -> llat).
Implicit Types (f g h : iprod F) (x : T).
Definition iprod_lt f g := exists x, f x ⊏ g x.
Lemma iprod_lt_left f g h :
iprod_lt f g -> (g ≤ h) -> iprod_lt f h.
Proof.
move=> -[x lt_fx_gx] le_g_h. exists x. exact: lt_left (le_g_h x).
Qed.
Lemma iprod_lt_right f g h :
(f ≤ g) -> iprod_lt g h -> iprod_lt f h.
Proof.
move=> le_f_g [x lt_gx_hx]. exists x. exact: lt_right (le_f_g x) _.
Qed.
Lemma iprod_lt_inf I (P : I -> iprod F) f :
iprod_lt (inf P) f -> exists i, iprod_lt (P i) f.
Proof.
case=> x /lt_inf[i lt_Px_fx]. exists i. exists x. exact: lt_Px_fx.
Qed.
Canonical iprod_llatMixin := LLatMixin iprod_lt_left iprod_lt_right iprod_lt_inf.
Canonical iprod_llat := Eval hnf in LLat (iprod F) iprod_llatMixin.
End IProdLLat.