Library preord


Require Import Setoid.
Require Import Coq.Program.Basics.

Require Import basics.
Require Import categories.

Delimit Scope preord_scope with preord.
Open Scope preord_scope.

Preordered types and monotone functions.

A preorder is a type equipped with a transitive, reflexive relation. Unlike standard domain theory, we will be concentrating on preorders rather than partial orders as the basis of order theory.
As compared to partial orders, preorders lack the axiom of antisymmetry. Instead, we work (almost) always up to the equivalence relation induced by the preorder. On a preorder, we automatically define a setoid by setting x y iff x y /\ y x. Thus, we "recover" antisymmetry by convention.
Module Preord.
  Record mixin_of (T:Type) :=
    Mixin
    { ord : T -> T -> Prop
    ; refl : forall x, ord x x
    ; trans : forall {x y z},
             ord x y -> ord y z -> ord x z
    }.
  Structure type : Type :=
    Pack { carrier :> Type ; mixin : mixin_of carrier }.

  Definition ord_op T := ord _ (mixin T).

  Record hom (X Y:type) := Hom
    { map :> carrier X -> carrier Y
    ; axiom : forall (a b:carrier X), ord_op X a b -> ord_op Y (map a) (map b)
    }.

  Program Definition ident (X:type) : hom X X := Hom X X (fun x => x) _.
  Program Definition compose (X Y Z:type) (g:hom Y Z) (f:hom X Y)
    := Hom X Z (fun x => g (f x)) _.

  Definition comp_mixin := Comp.Mixin type hom ident compose.

  Definition eq (X:type) (a b:X) := ord_op X a b /\ ord_op X b a.

  Definition hom_ord (X Y:type) (f g:hom X Y) := forall x, ord_op Y (f x) (g x).
  Definition hom_eq (X Y:type) (f g:hom X Y) := forall x, eq Y (f x) (g x).

  Program Definition ord_mixin X Y := Mixin (hom X Y) (hom_ord X Y) _ _.

  Program Definition eq_mixin X Y := Eq.Mixin (hom X Y) (hom_eq X Y) _ _ _.

  Lemma cat_axioms : Category.axioms type hom eq_mixin comp_mixin.

  Program Definition ord_eq (T:type) : Eq.mixin_of T :=
    Eq.Mixin T (eq T) _ _ _.
End Preord.
Notation preord := Preord.type.

Notation "x ≤ y" := (@Preord.ord_op _ x y) : preord_scope.
Notation "y ≥ x" := (@Preord.ord_op _ x y) (only parsing) : preord_scope.
Notation "x ≰ y" := (~ (@Preord.ord_op _ x y)) : preord_scope.
Notation "y ≱ x" := (~ (@Preord.ord_op _ x y)) (only parsing) : preord_scope.

Here we set up the category PREORD of preorders with montone functions and the canonical structure magic that makes notation work.
Coercion Preord.carrier : Preord.type >-> Sortclass.
Coercion Preord.map : Preord.hom >-> Funclass.

Canonical Structure hom_order X Y := Preord.Pack (Preord.hom X Y) (Preord.ord_mixin X Y).
Canonical Structure Preord_Eq (X:preord) : Eq.type :=
  Eq.Pack (Preord.carrier X) (Preord.ord_eq X).

Canonical Structure PREORD :=
  Category preord Preord.hom _ _ Preord.cat_axioms.

Canonical Structure preord_hom_eq (A B:preord):=
  Eq.Pack (Preord.hom A B) (Preord.eq_mixin A B).
Canonical Structure preord_comp :=
  Comp.Pack preord Preord.hom Preord.comp_mixin.

The preorder axioms and their relation to equality.
Lemma ord_refl : forall (T:preord) (x:T), x x.

Lemma ord_trans : forall (T:preord) (x y z:T), x y -> y z -> x z.

Lemma ord_antisym : forall (T:preord) (x y:T), x y -> y x -> x y.

Lemma eq_ord : forall (T:preord) (x y:T), x y -> x y.

Lemma eq_ord' : forall (T:preord) (x y:T), x y -> y x.

Set up setoid rewriting
Add Parametric Relation (A:preord) : (Preord.carrier A) (@Preord.ord_op A)
  reflexivity proved by (ord_refl A)
  transitivity proved by (ord_trans A)
    as ord_rel.

Add Parametric Morphism (A:preord) :
  (@Preord.ord_op A)
    with signature (Preord.ord_op A) -->
                   (Preord.ord_op A) ++>
                   impl
     as ord_morphism.

Add Parametric Morphism (A:preord) :
  (@Preord.ord_op A)
    with signature (eq_op (Preord_Eq A)) ==>
                   (eq_op (Preord_Eq A)) ==>
                   iff
     as ord_eq_morphism.

Add Parametric Morphism (A B:preord) :
  (@Preord.map A B)
   with signature (Preord.ord_op (hom_order A B)) ++>
                  (Preord.ord_op A) ++>
                  (Preord.ord_op B)
    as preord_map_morphism.

Add Parametric Morphism (A B:preord) :
  (@Preord.map A B)
   with signature (eq_op (Preord_Eq (hom_order A B))) ==>
                  (eq_op (Preord_Eq A)) ==>
                  (eq_op (Preord_Eq B))
    as preord_map_eq_morphism.

This lemma is handy for using an equality in the context to prove a goal by transitivity on both sides.
Lemma use_ord (A:preord) (a b c d:A) :
  b c -> a b -> c d -> a d.

PREORD is a concrete category.
Program Definition PREORD_concrete : concrete PREORD :=
  Concrete PREORD
  Preord.carrier
  (fun X => Eq.mixin (Preord_Eq X))
  Preord.map _ _.

Canonical Structure PREORD_concrete.

Monotone functions respect equality and order.
Lemma preord_eq : forall (X Y:preord) (f:X Y) (x y:X), x y -> f x f y.

Lemma preord_ord : forall (X Y:preord) (f:X Y) (x y:X), x y -> f x f y.

Hint Resolve ord_refl ord_trans ord_antisym preord_ord preord_eq eq_ord eq_ord'.

Add Parametric Morphism (X Y:preord) :
  (@hommap PREORD PREORD_concrete X Y)
  with signature (eq_op (CAT_EQ PREORD X Y)) ==>
                 (eq_op (Preord_Eq X)) ==>
                 (eq_op (Preord_Eq Y))
  as preord_apply_eq_morphism.

Add Parametric Morphism (X Y:preord) :
  (@hommap PREORD PREORD_concrete X Y)
  with signature (eq_op (CAT_EQ PREORD X Y)) ++>
                 (eq_op (Preord_Eq X)) ++>
                 (Preord.ord_op Y)
  as preord_apply_eqord_morphism.

Add Parametric Morphism (X Y:preord) :
  (@hommap PREORD PREORD_concrete X Y)
  with signature (fun (x y:hom PREORD X Y) => Preord.ord_op (hom_order X Y) x y) ==>
                 (Preord.ord_op X) ==>
                 (Preord.ord_op Y)
  as preord_apply_ord_morphism.

PREORD is termianted.

Program Definition unitpo := Preord.Pack unit (Preord.Mixin _ (fun _ _ => True) _ _).
Canonical Structure unitpo.

Program Definition preord_terminate (A:preord) : A unitpo :=
  Preord.Hom A unitpo (fun x => tt) _.

Program Definition preord_terminated_mixin :=
  Terminated.Mixin
     preord Preord.hom
     Preord.eq_mixin
     unitpo preord_terminate
     _.

Canonical Structure preord_terminated :=
  Terminated
     preord Preord.hom
     Preord.eq_mixin
     Preord.comp_mixin
     Preord.cat_axioms
     preord_terminated_mixin.

PREORD is initialized.
Program Definition emptypo :=
  Preord.Pack False (Preord.Mixin _ (fun _ _ => False) _ _).
Canonical Structure emptypo.

Program Definition preord_initiate (A:preord) : emptypo A :=
  Preord.Hom emptypo A (fun x => False_rect _ x) _.

Program Definition preord_initialized_mixin :=
  Initialized.Mixin
     preord Preord.hom
     Preord.eq_mixin
     emptypo preord_initiate
     _.

Canonical Structure preord_initialized :=
  Initialized
     preord Preord.hom
     Preord.eq_mixin
     Preord.comp_mixin
     Preord.cat_axioms
     preord_initialized_mixin.

The preorder on products, defined pointwise.
Definition prod_ord (A B:preord) (x y:A*B):=
  (fst x) (fst y) /\ (snd x) (snd y).

Program Definition prod_preord (A B:preord) : preord :=
  Preord.Pack (A*B) (Preord.Mixin _ (prod_ord A B) _ _).

Canonical Structure prod_preord.

PREORD is a cartesian category.
Program Definition pi1 {A B:preord} : prod_preord A B A :=
  Preord.Hom (prod_preord A B) A (fun x => fst x) _.

Program Definition pi2 {A B:preord} : prod_preord A B B :=
  Preord.Hom (prod_preord A B) B (fun x => snd x) _.

Program Definition mk_pair {C A B:preord} (f:C A) (g:C B) : C prod_preord A B :=
  Preord.Hom C (prod_preord A B) (fun c => (f c, g c)) _.

Program Definition preord_cartesian_mixin
  := Cartesian.Mixin
      Preord.type Preord.hom
      Preord.eq_mixin
      Preord.comp_mixin
      prod_preord (@pi1) (@pi2) (@mk_pair) _.

Canonical Structure preord_cartesian : cartesian :=
  Cartesian Preord.type Preord.hom
      Preord.eq_mixin
      Preord.comp_mixin
      Preord.cat_axioms
      preord_terminated_mixin
      preord_cartesian_mixin.

Further, PREORD is a cartesian closed category.
Program Definition preord_curry (C A B:preord) (f:C×A B) : C hom_order A B :=
  Preord.Hom C (hom_order A B) (fun c => Preord.Hom A B (fun a => f (c,a)) _) _.

Program Definition preord_apply (A B:preord) : (hom_order A B × A) B :=
  Preord.Hom (hom_order A B × A) B (fun fx => fst fx (snd fx)) _.

Program Definition preord_ccc_mixin
   := CartesianClosed.Mixin
       Preord.type Preord.hom
       Preord.eq_mixin
       Preord.comp_mixin
       Preord.cat_axioms
       preord_terminated_mixin
       preord_cartesian_mixin
       hom_order preord_curry preord_apply
       _.

Canonical Structure preord_ccc : cartesian_closed :=
  CartesianClosed
       Preord.type Preord.hom
       Preord.eq_mixin
       Preord.comp_mixin
       Preord.cat_axioms
       preord_cartesian_mixin
       preord_terminated_mixin
       preord_ccc_mixin.

The preorder on sums, defined in the standard way.
Definition sum_ord (A B:preord) (x y:A+B):=
  match x, y with
  | inl x', inl y' => x' y'
  | inr x', inr y' => x' y'
  | _, _ => False
  end.

Program Definition sum_preord (A B:preord) : preord :=
  Preord.Pack (A+B) (Preord.Mixin _ (sum_ord A B) _ _).

Canonical Structure sum_preord.

Preorders with an ord_dec structure have a decidable order relation.
Record ord_dec (A:preord) :=
  OrdDec
  { orddec :> forall x y:A, {x y}+{x y} }.


Preorders with decidable ordering also have decidable equality.
Canonical Structure PREORD_EQ_DEC (A:preord) (OD:ord_dec A) :=
  EqDec (Preord_Eq A) (fun (x y:A) =>
      match @orddec A OD x y with
      | left H1 =>
          match @orddec A OD y x with
          | left H2 => left _ (conj H1 H2)
          | right H => right _ (fun HEQ => H (proj2 HEQ))
          end
      | right H => right (fun HEQ => H (proj1 HEQ))
      end).

The "lift" preorder, which adjoins a new bottom element. The lift construction gives rise to an endofunctor on PREORD.
Definition lift_ord (A:preord) (x:option A) (y:option A) : Prop :=
   match x with None => True | Some x' =>
     match y with None => False | Some y' => x' y' end end.

Program Definition lift_mixin (A:preord) : Preord.mixin_of (option A) :=
  Preord.Mixin (option A) (lift_ord A) _ _.

Canonical Structure lift (A:preord) : preord :=
  Preord.Pack (option A) (lift_mixin A).

Program Definition liftup (A:preord) : A lift A :=
  Preord.Hom A (lift A) (@Some A) _.

Program Definition lift_map {A B:preord} (f:A B) : lift A lift B :=
  Preord.Hom (lift A) (lift B) (option_map (Preord.map A B f)) _.

Lemma lift_map_id (A:preord) : lift_map id(A) id(lift A).

Lemma lift_map_compose (A B C:preord) (g:B C) (f:A B) :
  lift_map (g f) lift_map g lift_map f.

Lemma lift_map_eq (A B:preord) (f f':A B) : f f' -> lift_map f lift_map f'.

Program Definition liftF : functor PREORD PREORD :=
  (Functor PREORD PREORD lift (@lift_map) _ _ _).