# Library HFrelation

Require Import List.
Require Export HF.

Definition lam (x:hf) (f:hf->hf) :=
repl x (fun x => couple x (f x)).

Lemma lam_intro : forall x dom F,
eq_hf_fun dom F F ->
x \in dom ->
couple x (F x) \in lam dom F.

Lemma lam_elim : forall p dom F,
eq_hf_fun dom F F ->
p \in lam dom F ->
exists2 x, x \in dom & p == couple x (F x).

Lemma lam_ext :
forall x1 x2 f1 f2,
x1 == x2 ->
eq_hf_fun x1 f1 f2 ->
lam x1 f1 == lam x2 f2.

Definition image f := repl f snd.
Definition domain f := repl f fst.

Instance domain_morph : morph1 domain.
Qed.

Instance image_morph : morph1 image.
Qed.

Lemma lam_domain : forall x F,
eq_hf_fun x F F ->
domain (lam x F) == x.

Definition app (x y: hf) :=
snd (union (subset x (fun p => eq_hf (fst p) y))).

Instance app_morph : morph2 app.
Qed.

Lemma app_def: forall f x y,
couple x y \in f ->
(forall p, p \in f -> fst p == x -> p == couple x y) ->
app f x == y.

Lemma beta_eq :
forall dom F x,
eq_hf_fun dom F F ->
x \in dom ->
app (lam dom F) x == F x.

Definition func_cons f x y :=
HF(couple x y::hf_elts f).

Instance func_cons_morph : morph3 func_cons.
Qed.

Definition func_map_image F x Y :=
union (repl F (fun f => repl Y (fun y' => func_cons f x y'))).

Lemma df_morph1 : forall dom y a,
eq_hf_fun dom (fun y' => func_cons y a y')
(fun y' => func_cons y a y').

Lemma df_morph2 : forall F a y,
eq_hf_fun F (fun f => repl y (fun y' => func_cons f a y'))
(fun f => repl y (fun y' => func_cons f a y')).

Lemma func_map_image_intro: forall f x y F Y,
f \in F ->
y \in Y ->
func_cons f x y \in func_map_image F x Y.

Lemma func_map_image_elim : forall g x F Y,
g \in func_map_image F x Y ->
exists2 f, f \in F &
exists2 y, y \in Y & g == func_cons f x y.

Definition func (x y: hf) :=
fold_set hf
(fun x' fs => func_map_image fs x' y)
x (singl empty).

Definition dep_func (x:hf) (y:hf->hf) :=
fold_set hf
(fun x' fs => func_map_image fs x' (y x'))
x (singl empty).

Lemma dep_func_intro :
forall f X Y,
eq_hf_fun X f f ->
eq_hf_fun X Y Y ->
(forall x, x \in X -> f x \in Y x) ->
lam X f \in dep_func X Y.

Lemma dep_func_elim0 : forall f p X Y,
f \in dep_func X Y ->
p \in f ->
(exists2 x, x \in X &
exists2 y, y \in Y x &
p == couple x y) /\
(forall p', p' \in f -> fst p == fst p' -> p == p').

Lemma dep_func_total : forall f x X Y,
f \in dep_func X Y ->
x \in X ->
exists2 p, fst p == x & p \in f.

Lemma dep_func_elim : forall f x X Y,
eq_hf_fun X Y Y ->
f \in dep_func X Y ->
x \in X ->
app f x \in Y x.

Lemma dep_func_eta: forall f X Y,
f \in dep_func X Y ->
f == lam X (fun x => app f x).

Lemma dep_func_ext : forall x1 x2 y1 y2,
x1 == x2 ->
eq_hf_fun x1 y1 y2 ->
dep_func x1 y1 == dep_func x2 y2.