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.