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 : ∀ x dom F,
  eq_hf_fun dom F F ->
  x ∈ dom ->
  couple x (F x) ∈ lam dom F.

Lemma lam_elim : ∀ p dom F,
  eq_hf_fun dom F F ->
  p ∈ lam dom F ->
  exists2 x, x ∈ dom & p == couple x (F x).

Lemma lam_ext :
  ∀ 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 : ∀ 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: ∀ f x y,
  couple x y ∈ f ->
  (∀ p, p ∈ f -> fst p == x -> p == couple x y) ->
  app f x == y.

Lemma beta_eq :
  ∀ dom F x,
  eq_hf_fun dom F F ->
  x ∈ 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 : ∀ dom y a,
  eq_hf_fun dom (fun y' => func_cons y a y')
    (fun y' => func_cons y a y').

Lemma df_morph2 : ∀ 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: ∀ f x y F Y,
  f ∈ F ->
  y ∈ Y ->
  func_cons f x y ∈ func_map_image F x Y.

Lemma func_map_image_elim : ∀ g x F Y,
  g ∈ func_map_image F x Y ->
  exists2 f, f ∈ F &
  exists2 y, y ∈ 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 :
  ∀ f X Y,
  eq_hf_fun X f f ->
  eq_hf_fun X Y Y ->
  (∀ x, x ∈ X -> f x ∈ Y x) ->
  lam X f ∈ dep_func X Y.

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

Lemma dep_func_total : ∀ f x X Y,
  f ∈ dep_func X Y ->
  x ∈ X ->
  exists2 p, fst p == x & p ∈ f.

Lemma dep_func_elim : ∀ f x X Y,
  eq_hf_fun X Y Y ->
  f ∈ dep_func X Y ->
  x ∈ X ->
  app f x ∈ Y x.

Lemma dep_func_eta: ∀ f X Y,
  f ∈ dep_func X Y ->
  f == lam X (fun x => app f x).

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