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) :=
    { 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.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) ++>
     as ord_morphism.

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

Add Parametric Morphism (A B:preord) :
  ( 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) :
  ( 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
  (fun X => Eq.mixin (Preord_Eq X)) _ _.

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 :=
     preord Preord.hom
     unitpo preord_terminate

Canonical Structure preord_terminated :=
     preord Preord.hom

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 :=
     preord Preord.hom
     emptypo preord_initiate

Canonical Structure preord_initialized :=
     preord Preord.hom

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
      prod_preord (@pi1) (@pi2) (@mk_pair) _.

Canonical Structure preord_cartesian : cartesian :=
  Cartesian Preord.type Preord.hom

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
       hom_order preord_curry preord_apply

Canonical Structure preord_ccc : cartesian_closed :=
       Preord.type Preord.hom

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

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 :> 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))
      | right H => right (fun HEQ => H (proj1 HEQ))

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 ( 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) _ _ _).