# 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.

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.

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.

(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 :=

DirPreord

{ 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 }.

DirPreord

{ 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.

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.

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

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

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