Library directed

Require Import basics.
Require Import preord.
Require Import categories.
Require Import sets.
Require Import finsets.
Require Import effective.

Conditionally-inhabited sets and h-directed sets.

A finite set is conditionally-inhabited for hf whenever hf is false; or when hf is true, the set is inhabited.
This very odd little definition is the key to providing a uniform presentation of pointed and unpointed domains.
Definition inh {A:preord} (hf:bool) (X:finset A) :=
  if hf then exists x, x X else True.

Lemma inh_dec A hf (X:finset A) : { inh hf X } + {~inh hf X}.

Lemma inh_image A B hf (X:finset A) (f:A B) :
  inh hf X <-> inh hf (image f X).

Lemma inh_sub A hf (X Y:finset A) :
  X Y -> inh hf X -> inh hf Y.

Lemma inh_eq A hf (X Y:finset A) :
  X Y -> inh hf X -> inh hf Y.

Lemma elem_inh A hf (X:finset A) x : x X -> inh hf X.

Hint Resolve inh_sub elem_inh.

A subset of the image of a function is equal to the image of some subset of the set X.
Lemma finset_sub_image (A B:preord) (T:set.theory)
  (f:A B) (X:set T A) (M:finset B) :
  M image f X ->
  exists M', M image f M' /\ M' X.

A directed preorder is an effective preorder where every finite set has an upper bound (that may be found constructively).
Record directed_preord :=
  { dir_preord :> preord
  ; dir_effective : effective_order dir_preord
  ; choose_ub_set : forall M:finset dir_preord, { k | upper_bound k M }

Lemma choose_ub (I:directed_preord) (i j:I) :
  { k | i k /\ j k }.

A set X is h-directed when every h-inhabited finite subset has an upper bound in X.
Definition directed {T:set.theory} {A:preord} (hf:bool) (X:set T A) :=
  forall (M:finset A) (Hinh:inh hf M),
    M X -> exists x, upper_bound x M /\ x X.

To prove a set X is directed, it suffices (and is necessary) that every pair of elements in X has an upper bound in X; and that X is inhabited when b = false.
Lemma prove_directed (T:set.theory) (A:preord) (b:bool) (X:set T A) :
  (if b then True else exists x, x X) ->
  (forall x y, x X -> y X -> exists z, x z /\ y z /\ z X) ->
  directed b X.

Directeness forms a set color.
Program Definition directed_hf_cl (hf:bool) : color :=
  Color (fun SL A X => @directed SL A hf X) _ _ _ _.

Definition semidirected_cl := directed_hf_cl true.
Definition directed_cl := directed_hf_cl false.

The preorder of natural numbers with their arithmetic ordering is an effective, directed preorder.
Require Import Arith.
Require Import NArith.

Program Definition nat_ord := Preord.Pack nat (Preord.Mixin nat le _ _).
Solve Obligations using eauto with arith.

Program Definition nat_eff : effective_order nat_ord :=
  EffectiveOrder nat_ord le_dec (fun x => Some (N.to_nat x)) _.

Program Definition nat_dirord : directed_preord :=
  DirPreord nat_ord nat_eff _.