Ord.preorder
Require Import base.
Module Pro.
Record mixin_of (T : Type) := Mixin {
rel : T -> T -> Prop;
_ : reflexive rel;
_ : transitive rel
}.
Notation class_of := mixin_of.
Section ClassDef.
Structure type := Pack {sort; _ : class_of sort; _ : Type }.
Local Coercion sort : type >-> Sortclass.
Variable (T : Type) (cT : type).
Definition class := let: Pack _ c _ := cT return class_of cT in c.
Definition pack c := @Pack T c T.
Definition clone c of phant_id class c := @Pack T c T.
End ClassDef.
Module Exports.
Coercion sort : type >-> Sortclass.
Notation proType := type.
Notation ProMixin := Mixin.
Notation ProType T m := (@pack T m).
Notation "[ 'proMixin' 'of' T ]" := (class _ : mixin_of T)
(at level 0, format "[ 'proMixin' 'of' T ]") : form_scope.
Notation "[ 'proType' 'of' T 'for' C ]" := (@clone T C _ idfun)
(at level 0, format "[ 'proType' 'of' T 'for' C ]") : form_scope.
Notation "[ 'proType' 'of' T ]" := (@clone T _ _ id)
(at level 0, format "[ 'proType' 'of' T ]") : form_scope.
End Exports.
End Pro.
Export Pro.Exports.
Definition ord_op T := Pro.rel (Pro.class T).
Arguments ord_op {T} x y.
Delimit Scope ord_scope with ORD.
Open Scope ord_scope.
Notation "x <= y" := (ord_op x y) : ord_scope.
Notation "x <= y :> T" := ((x:T) <= (y:T)) : ord_scope.
Notation "x <= y <= z" := (x <= y /\ y <= z) : ord_scope.
Notation "x >= y" := (y <= x) (only parsing) : ord_scope.
Notation "x >= y >= z" := (z <= y <= x)
(at level 70, y at next level, only parsing) : ord_scope.
Module Pro.
Record mixin_of (T : Type) := Mixin {
rel : T -> T -> Prop;
_ : reflexive rel;
_ : transitive rel
}.
Notation class_of := mixin_of.
Section ClassDef.
Structure type := Pack {sort; _ : class_of sort; _ : Type }.
Local Coercion sort : type >-> Sortclass.
Variable (T : Type) (cT : type).
Definition class := let: Pack _ c _ := cT return class_of cT in c.
Definition pack c := @Pack T c T.
Definition clone c of phant_id class c := @Pack T c T.
End ClassDef.
Module Exports.
Coercion sort : type >-> Sortclass.
Notation proType := type.
Notation ProMixin := Mixin.
Notation ProType T m := (@pack T m).
Notation "[ 'proMixin' 'of' T ]" := (class _ : mixin_of T)
(at level 0, format "[ 'proMixin' 'of' T ]") : form_scope.
Notation "[ 'proType' 'of' T 'for' C ]" := (@clone T C _ idfun)
(at level 0, format "[ 'proType' 'of' T 'for' C ]") : form_scope.
Notation "[ 'proType' 'of' T ]" := (@clone T _ _ id)
(at level 0, format "[ 'proType' 'of' T ]") : form_scope.
End Exports.
End Pro.
Export Pro.Exports.
Definition ord_op T := Pro.rel (Pro.class T).
Arguments ord_op {T} x y.
Delimit Scope ord_scope with ORD.
Open Scope ord_scope.
Notation "x <= y" := (ord_op x y) : ord_scope.
Notation "x <= y :> T" := ((x:T) <= (y:T)) : ord_scope.
Notation "x <= y <= z" := (x <= y /\ y <= z) : ord_scope.
Notation "x >= y" := (y <= x) (only parsing) : ord_scope.
Notation "x >= y >= z" := (z <= y <= x)
(at level 70, y at next level, only parsing) : ord_scope.
Section PreorderLemmas.
Variable (T : proType).
Implicit Types (x y z : T).
Lemma le_refl x : x <= x.
Proof. by case: T x => ?[]. Qed.
Lemma le_trans x y z : x <= y -> y <= z -> x <= z.
Proof. by case: T x y z => ?[]. Qed.
End PreorderLemmas.
Arguments le_refl {T x}.
Arguments le_trans {T x} y {z} le_x_y le_y_z.
Hint Resolve le_refl.
Instance ord_op_rew (T : proType) : Coq.Classes.RelationClasses.RewriteRelation (@ord_op T).
Instance ord_op_refl (T : proType) : Coq.Classes.RelationClasses.Reflexive (@ord_op T) := @le_refl T.
Instance ord_op_trans (T : proType) : Coq.Classes.RelationClasses.Transitive (@ord_op T) := @le_trans T.
Instance ord_op_preord (T : proType) : Coq.Classes.RelationClasses.PreOrder (@ord_op T).
Proof. constructor; exact _. Qed.
This is a situation where typeclasses uses the coq apply and it doesn't
play nice with canonical structures.
Section SubtypePreorder.
Variable (T : Type) (X : proType) (f : T -> X).
Implicit Types (x y z : T).
Definition induced_le x y := f x <= f y.
Lemma induced_le_refl x : induced_le x x. exact: le_refl. Qed.
Lemma induced_le_trans : transitive induced_le. move=> x y z. exact: le_trans. Qed.
Canonical induced_proMixin := ProMixin induced_le_refl induced_le_trans.
Definition induced_proType := Eval hnf in ProType T induced_proMixin.
End SubtypePreorder.
Arguments induced_proType T {X} f.
Definition reverse R : Type := R.
Section ReversePreorder.
Variable (T : proType).
Implicit Types (x y : reverse T).
Definition rev_le x y := (y <= x).
Lemma reverse_le_refl x : rev_le x x. exact: le_refl. Qed.
Lemma reverse_le_trans x y z : rev_le x y -> rev_le y z -> rev_le x z.
Proof. move=> le_y_x le_z_y. exact: le_trans le_z_y le_y_x. Qed.
Canonical reverse_proMixin := ProMixin reverse_le_refl reverse_le_trans.
Canonical reverse_proType := Eval hnf in ProType (reverse T) reverse_proMixin.
End ReversePreorder.
Notation "T ^r" := (reverse T) (at level 2, format "T ^r") : type_scope.
Lemma rev_leE (T : proType) x y : (x <= y :> T^r) = (y <= x :> T). by []. Qed.
Section NatPreorder.
Implicit Types (m n k : nat).
Definition nat_le m n : Prop := (m <= n)%N.
Lemma nat_le_refl m : nat_le m m. exact: leqnn. Qed.
Lemma nat_le_trans m n k : nat_le m n -> nat_le n k -> nat_le m k.
Proof. exact: leq_trans. Qed.
Canonical nat_proMixin := ProMixin nat_le_refl nat_le_trans.
Canonical nat_proType := Eval hnf in ProType nat nat_proMixin.
End NatPreorder.
Lemma nat_leE (m n : nat) : (m <= n) = (m <= n)%N.
Proof. by []. Qed.
Section PropPreorder.
Implicit Types (P Q R : Prop).
Definition prop_le P Q := P -> Q.
Lemma prop_le_refl P : prop_le P P. by []. Qed.
Lemma prop_le_trans P Q R : prop_le P Q -> prop_le Q R -> prop_le P R.
Proof. rewrite/prop_le. tauto. Qed.
Canonical prop_proMixin := ProMixin prop_le_refl prop_le_trans.
Canonical prop_proType := Eval hnf in ProType Prop prop_proMixin.
End PropPreorder.
Instance prop_impl_subrelation : subrelation (@ord_op prop_proType) Basics.impl.
Proof. by []. Qed.
Instance impl_prop_subrelation : subrelation Basics.impl (@ord_op prop_proType).
Proof. by []. Qed.
Lemma prop_leE (P Q : Prop) : (P <= Q) = (P -> Q).
Proof. by []. Qed.
Section PairPreorder.
Variable (X Y : proType).
Implicit Types (p q r : X * Y).
Definition pair_le p q := p.1 <= q.1 /\ p.2 <= q.2.
Lemma pair_le_refl p : pair_le p p.
Proof. by []. Qed.
Lemma pair_le_trans p q r : pair_le p q -> pair_le q r -> pair_le p r.
Proof.
move: p q r => [a1 b1] [a2 b2] [a3 b3] [/=r1 s1] [/=r2 s2]. split=> /=.
exact: le_trans r1 r2. exact: le_trans s1 s2.
Qed.
Canonical pair_proMixin := ProMixin pair_le_refl pair_le_trans.
Canonical pair_proType := Eval hnf in ProType (X * Y) pair_proMixin.
End PairPreorder.
Lemma pair_leE (X Y : proType) (p q : X * Y) :
(p <= q) = (p.1 <= q.1 /\ p.2 <= q.2).
Proof. by []. Qed.
Section IProdPreorder.
Variables (T : Type) (F : T -> proType).
Implicit Types (f g h : iprod F).
Definition iprod_le f g := forall x, f x <= g x.
Lemma iprod_le_refl f : iprod_le f f.
Proof. by []. Qed.
Lemma iprod_le_trans f g h : iprod_le f g -> iprod_le g h -> iprod_le f h.
Proof. move=> h1 h2 x. exact: le_trans (h1 x) (h2 x). Qed.
Canonical iprod_proMixin := ProMixin iprod_le_refl iprod_le_trans.
Canonical iprod_proType := Eval hnf in ProType (iprod F) iprod_proMixin.
End IProdPreorder.
Arguments iprod_le {T F} f g /.
Lemma iprod_leE (T : Type) (F : T -> proType) (f g : forall x, F x) :
(f <= g :> iprod _) = (forall x, f x <= g x).
Proof. by []. Qed.
Canonical prod_proType (T : Type) (X : proType) :=
Eval hnf in ProType (T -> X) (@iprod_proMixin T (fun _ => X)).
Lemma prod_leE (T : Type) (X : proType) (f g : T -> X) :
(f <= g) = (forall x, f x <= g x).
Proof. by []. Qed.
Allow using f <= g to rewrite applications e.g. in f x <= g x.
(*Instance prod_le_pointwise {T : Type} {X : proType} :
subrelation (@ord_op (prod_proType T X)) (eq ++> ord_op)*)
Global Instance prod_pointwise_subrelation (T : Type) (X : proType) :
subrelation (@ord_op (prod_proType T X)) (pointwise_relation T ord_op).
Proof. by []. Qed.
subrelation (@ord_op (prod_proType T X)) (eq ++> ord_op)*)
Global Instance prod_pointwise_subrelation (T : Type) (X : proType) :
subrelation (@ord_op (prod_proType T X)) (pointwise_relation T ord_op).
Proof. by []. Qed.
Definition monotone {X Y : proType} (f : X -> Y) :=
forall x y : X, x <= y -> f x <= f y.
Existing Class monotone.
Type of monotone functions
Section MFun.
Variable (X Y : proType).
Structure mfun_type := mk_mfun_type {
monofun :> X -> Y;
_ : monotone monofun
}.
Definition mfun_of of phant (X -> Y) := mfun_type.
Identity Coercion type_of_mfun : mfun_of >-> mfun_type.
End MFun.
Notation "{ 'mono' fT }" := (mfun_of (Phant fT))
(at level 0, format "{ 'mono' '[hv' fT ']' }") : type_scope.
Definition mfun {X Y : proType} (f : X -> Y) {fP : monotone f} :
{mono X -> Y} := mk_mfun_type fP.
Arguments mfun {X Y} f {fP} : rename.
Instance mfun_is_monotone {X Y : proType} (f : {mono X -> Y}) : monotone f.
Proof. by case: f. Qed.
Lemma mono {X Y : proType} (f : X -> Y) {fP : monotone f} (x y : X) :
x <= y -> f x <= f y.
Proof. exact: fP. Qed.
Instance monotone_proper {X Y : proType} (f : X -> Y) {fP : monotone f} :
Proper (ord_op ++> ord_op) f.
Proof. exact: mono. Qed.
Instance mfun_proper {X Y : proType} (f : {mono X -> Y}) :
Proper (ord_op ++> ord_op) f.
Proof. exact: mono. Qed.
Lemma mfun_eq (X Y : proType) (f g : {mono X -> Y}) :
f = g :> (X -> Y) -> f = g.
Proof.
move: f g => [f fm] [g gm] /=. destruct 1. f_equal. exact: pi.
Qed.
Variable (X Y : proType).
Structure mfun_type := mk_mfun_type {
monofun :> X -> Y;
_ : monotone monofun
}.
Definition mfun_of of phant (X -> Y) := mfun_type.
Identity Coercion type_of_mfun : mfun_of >-> mfun_type.
End MFun.
Notation "{ 'mono' fT }" := (mfun_of (Phant fT))
(at level 0, format "{ 'mono' '[hv' fT ']' }") : type_scope.
Definition mfun {X Y : proType} (f : X -> Y) {fP : monotone f} :
{mono X -> Y} := mk_mfun_type fP.
Arguments mfun {X Y} f {fP} : rename.
Instance mfun_is_monotone {X Y : proType} (f : {mono X -> Y}) : monotone f.
Proof. by case: f. Qed.
Lemma mono {X Y : proType} (f : X -> Y) {fP : monotone f} (x y : X) :
x <= y -> f x <= f y.
Proof. exact: fP. Qed.
Instance monotone_proper {X Y : proType} (f : X -> Y) {fP : monotone f} :
Proper (ord_op ++> ord_op) f.
Proof. exact: mono. Qed.
Instance mfun_proper {X Y : proType} (f : {mono X -> Y}) :
Proper (ord_op ++> ord_op) f.
Proof. exact: mono. Qed.
Lemma mfun_eq (X Y : proType) (f g : {mono X -> Y}) :
f = g :> (X -> Y) -> f = g.
Proof.
move: f g => [f fm] [g gm] /=. destruct 1. f_equal. exact: pi.
Qed.
Order on monotone functions
Canonical mfun_proType (X Y : proType) :=
Eval hnf in induced_proType {mono X -> Y} (@monofun _ _).
Lemma mfun_leE (X Y : proType) (f g : {mono X -> Y}) :
(f <= g) = (forall x, f x <= g x).
Proof. by []. Qed.
The coercion transforms between the different orders.
Instance monofun_proper {X Y : proType} :
Proper (@ord_op (mfun_proType X Y) ++> ord_op) (@monofun X Y).
Proof. by []. Qed.
Instance monotone_reverse {X Y : proType} (f : X -> Y) {fP : monotone f} :
@monotone (reverse_proType X) (reverse_proType Y) f := fun x y => fP y x.
Proper (@ord_op (mfun_proType X Y) ++> ord_op) (@monofun X Y).
Proof. by []. Qed.
Instance monotone_reverse {X Y : proType} (f : X -> Y) {fP : monotone f} :
@monotone (reverse_proType X) (reverse_proType Y) f := fun x y => fP y x.
Section LubPreorder.
Variables (T : Type) (X : proType) (f : T -> X).
Definition is_ub x := forall i, f i <= x.
Definition is_lub x := forall y, (x <= y) <-> is_ub y.
Lemma ubP x i : is_ub x -> f i <= x. exact. Qed.
Lemma lub_ub x : is_lub x -> is_ub x.
Proof. move=> lub i. by apply lub. Qed.
Coercion lub_ub : is_lub >-> is_ub.
Lemma lubP x y : is_lub x -> is_ub y -> x <= y.
Proof. by move=> lub /lub. Qed.
Lemma lubE x y : is_lub x -> (x <= y) = is_ub y.
Proof. move=> h. apply: pext; by apply h. Qed.
Lemma mk_lub x :
is_ub x -> (forall y, is_ub y -> x <= y) -> is_lub x.
Proof.
move=> h1 h2 y; split; last by exact: h2. move=> le_x_y i.
apply: le_trans le_x_y. exact: h1.
Qed.
End LubPreorder.
Lemma ub_anti {T} {X : proType} (f g : T -> X) x :
f <= g -> is_ub g x -> is_ub f x.
Proof.
move=> le_f_g h i. apply: le_trans (h i). exact: le_f_g.
Qed.
Lemma lub_mono {T} {X : proType} (f g : T -> X) x y :
is_lub f x -> is_lub g y -> f <= g -> x <= y.
Proof.
move=> lubf lubg le_f_g. apply: lubP lubf _. exact: ub_anti lubg.
Qed.
Section GlbPreorder.
Variables (T : Type) (X : proType) (f : T -> X).
Definition is_lb x := forall i, x <= f i.
Definition is_glb x := forall y, (y <= x) <-> is_lb y.
Let Y := [proType of X^r].
Lemma lbP x i : is_lb x -> x <= f i. exact: (@ubP T Y). Qed.
Lemma glb_lb x : is_glb x -> is_lb x. exact: (@lub_ub T Y). Qed.
Coercion glb_lb : is_glb >-> is_lb.
Lemma glbP x y : is_glb x -> is_lb y -> y <= x. exact: (@lubP T Y). Qed.
Lemma glbE x y : is_glb x -> (y <= x) = is_lb y. exact: (@lubE T Y). Qed.
Lemma mk_glb x : is_lb x -> (forall y, is_lb y -> y <= x) -> is_glb x.
Proof. exact: (@mk_lub T Y). Qed.
End GlbPreorder.
Lemma lb_mono {T} {X : proType} (f g : T -> X) x :
f <= g -> is_lb f x -> is_lb g x.
Proof. exact: (@ub_anti T [proType of X^r]). Qed.
Lemma glb_anti {T} {X : proType} (f g : T -> X) x y :
is_glb f x -> is_glb g y -> g <= f -> y <= x.
Proof. exact: (@lub_mono T [proType of X^r]). Qed.