Library HF

Require Export Setoid Morphisms.
Require Import List.
Require Import Bool.

Lemma in_map_inv : forall (A B:Set) (f:A->B) x l,
  In x (map f l) -> exists2 y, In y l & x = f y.


Inductive hf : Set := HF (elts : list hf).

Definition hf_elts (x:hf) := let (lx) := x in lx.

Lemma hf_elts_ext : forall x, HF (hf_elts x) = x.

Lemma hf_ind2 : forall P : hf -> Prop,
  (forall l, (forall x, In x l -> P x) -> P (HF l)) ->
  forall x, P x.


Definition forall_elt P x :=
  fold_right (fun y b => P y && b) true (hf_elts x).

Definition exists_elt P x :=
  negb (forall_elt (fun x => negb (P x)) x).

Lemma forall_elt_case :
  forall P x,
  forall_elt P x = true /\ (forall y, In y (hf_elts x) -> P y = true) \/
  forall_elt P x = false /\ (exists2 y, In y (hf_elts x) & P y = false).

Lemma forall_elt_true_intro :
  forall P x,
  (forall y, In y (hf_elts x) -> P y = true) ->
  forall_elt P x = true.

Lemma forall_elt_false_intro :
  forall P y x,
  In y (hf_elts x) ->
  P y = false ->
  forall_elt P x = false.

Lemma forall_elt_true_elim :
  forall P y x,
  forall_elt P x = true ->
  In y (hf_elts x) ->
  P y = true.

Lemma forall_elt_false_elim :
  forall P x,
  forall_elt P x = false ->
  exists2 y, In y (hf_elts x) & P y = false.

Lemma exists_elt_true_intro :
  forall P y x,
  In y (hf_elts x) ->
  P y = true ->
  exists_elt P x = true.

Lemma exists_elt_true_elim :
  forall P x,
  exists_elt P x = true ->
  exists2 y, In y (hf_elts x) & P y = true.


Fixpoint eq_hf (x y: hf) {struct x} : bool :=
  forall_elt (fun x1 => exists_elt (fun y1 => eq_hf x1 y1) y) x &&
  forall_elt (fun y1 => exists_elt (fun x1 => eq_hf x1 y1) x) y.

Definition Eq_hf x y := eq_hf x y = true.

Lemma eq_hf_intro :
  forall x y,
  (forall x', In x' (hf_elts x) ->
   exists2 y', In y' (hf_elts y) & Eq_hf x' y') ->
  (forall y', In y' (hf_elts y) ->
   exists2 x', In x' (hf_elts x) & Eq_hf x' y') ->
  Eq_hf x y.

Lemma eq_hf_elim1 :
  forall x' x y,
  Eq_hf x y ->
  In x' (hf_elts x) ->
  exists2 y', In y' (hf_elts y) & Eq_hf x' y'.

Lemma eq_hf_elim2 :
  forall y' x y,
  Eq_hf x y ->
  In y' (hf_elts y) ->
  exists2 x', In x' (hf_elts x) & Eq_hf x' y'.

Instance eq_hf_refl : Reflexive Eq_hf.
Qed.

Instance eq_hf_sym : Symmetric Eq_hf.
Qed.

Instance eq_hf_trans : Transitive Eq_hf.
Qed.

Instance eq_hf_equiv : Equivalence Eq_hf.
Instance eq_hf_morph : Proper (Eq_hf ==> Eq_hf ==> @eq bool) eq_hf.
Qed.


Definition in_hf (x y: hf) : bool := exists_elt (fun y1 => eq_hf x y1) y.

Definition In_hf x y := in_hf x y = true.

Lemma in_hf_intro : forall x x' y,
  Eq_hf x x' ->
  In x' (hf_elts y) ->
  In_hf x y.

Lemma in_hf_elim : forall x y,
  In_hf x y ->
  exists2 x', In x' (hf_elts y) & Eq_hf x x'.

Lemma in_hf_reg_l: forall a a' b,
  Eq_hf a a' -> In_hf a b -> In_hf a' b.

Lemma in_hf_reg_r :
  forall a x y,
  Eq_hf x y ->
  In_hf a x ->
  In_hf a y.

Instance In_hf_morph : Proper (Eq_hf ==> Eq_hf ==> iff) In_hf.

Qed.

Instance in_hf_morph : Proper (Eq_hf ==> Eq_hf ==> @eq _) in_hf.
Qed.

Lemma In_hf_head : forall x y l,
  Eq_hf x y ->
  In_hf x (HF (y::l)).

Lemma In_hf_tail : forall x y l,
  In_hf x (HF l) ->
  In_hf x (HF (y::l)).

Lemma In_hf_elim : forall x y l,
  In_hf x (HF (y::l)) ->
  Eq_hf x y \/ In_hf x (HF l).

Lemma In_app_left : forall x l1 l2,
  In_hf x (HF l1) ->
  In_hf x (HF (l1 ++ l2)).

Lemma In_app_right : forall x l1 l2,
  In_hf x (HF l2) ->
  In_hf x (HF (l1 ++ l2)).

Lemma In_app_elim : forall x l1 l2,
  In_hf x (HF (l1 ++ l2)) ->
  In_hf x (HF l1) \/ In_hf x (HF l2).

Definition incl_hf x y :=
  forall_elt (fun x1 => in_hf x1 y) x.

Definition Incl_hf x y := forall a, In_hf a x -> In_hf a y.

Instance incl_hf_morph : Proper (Eq_hf ==> Eq_hf ==> iff) Incl_hf.
Qed.

Lemma incl_hf_sound : forall x y,
  incl_hf x y = true -> Incl_hf x y.

Lemma incl_hf_complete : forall x y,
  Incl_hf x y -> incl_hf x y = true.

Lemma Eq_hf_intro : forall x y,
  Incl_hf x y -> Incl_hf y x -> Eq_hf x y.

Lemma Eq_hf_cons : forall x1 x2 l1 l2,
  Eq_hf x1 x2 ->
  Eq_hf (HF l1) (HF l2) ->
  Eq_hf (HF (x1::l1)) (HF (x2::l2)).

Lemma Eq_hf_split : forall l1 l1' l2 l2',
  Eq_hf (HF l1) (HF l1') ->
  Eq_hf (HF l2) (HF l2') ->
  Eq_hf (HF(l1++l2)) (HF(l1'++l2')).

Lemma hf_size_ind : forall (P:hf->Type) x,
  P (HF nil) ->
  (forall x' y,
   In_hf x' x ->
   Incl_hf y x ->
   P y -> P (HF(x'::hf_elts y))) ->
  P x.


Lemma cancel_repeat : forall a l,
  In_hf a (HF l) -> Eq_hf (HF(a::l)) (HF l).

Definition cons_hf x l := if in_hf x (HF l) then l else x :: l.

Lemma cons_hf_cons :
  forall x l, Eq_hf (HF(cons_hf x l)) (HF(cons x l)).

Lemma In_hf_head_hf : forall x y l,
  Eq_hf x y ->
  In_hf x (HF (cons_hf y l)).

Lemma In_hf_tail_hf : forall x y l,
  In_hf x (HF l) ->
  In_hf x (HF (cons_hf y l)).

Lemma In_hf_elim_hf : forall x y l,
  In_hf x (HF (cons_hf y l)) ->
  Eq_hf x y \/ In_hf x (HF l).

Lemma Eq_hf_cons_hf : forall x1 x2 l1 l2,
  Eq_hf x1 x2 ->
  Eq_hf (HF l1) (HF l2) ->
  Eq_hf (HF (cons_hf x1 l1)) (HF (cons_hf x2 l2)).

Fixpoint app_hf (l1 l2:list hf) {struct l1} : list hf :=
  match l1 with
    nil => l2
  | cons x l' => cons_hf x (app_hf l' l2)
  end.

Lemma In_app_hf_left : forall x l1 l2,
  In_hf x (HF l1) ->
  In_hf x (HF (app_hf l1 l2)).

Lemma In_app_hf_right : forall x l1 l2,
  In_hf x (HF l2) ->
  In_hf x (HF (app_hf l1 l2)).

Lemma In_app_hf_elim : forall x l1 l2,
  In_hf x (HF (app_hf l1 l2)) ->
  In_hf x (HF l1) \/ In_hf x (HF l2).

Definition fold_set (X:Type) (f:hf->X->X) (x:hf) (acc:X) : X :=
  let fix F (l:list hf) : X :=
    match l with
      nil => acc
    | cons x l' => if in_hf x (HF l') then F l' else f x (F l')
    end in
  F (hf_elts x).

Lemma fold_set_unfold : forall X f x l acc,
  fold_set X f (HF(x::l)) acc =
  if in_hf x (HF l) then fold_set X f (HF l) acc
  else f x (fold_set X f (HF l) acc).

Lemma fold_set_ind : forall X (P:hf->X->Prop) f x acc,
  P (HF nil) acc ->
  (forall x' y acc, In_hf x' x -> In_hf x' y -> P y acc ->
   P (HF(x'::hf_elts y)) acc) ->
  (forall x' y acc, In_hf x' x -> ~ In_hf x' y -> P y acc ->
   P (HF(x'::hf_elts y)) (f x' acc)) ->
  P x (fold_set X f x acc).

Fixpoint canonical (x:hf) : hf :=
  HF (fold_set _ (fun y cl => canonical y :: cl) x nil).

Lemma canonical_correct : forall x, Eq_hf (canonical x) x.

Hint Resolve In_hf_head In_hf_head_hf In_hf_head_hf In_hf_tail_hf.


Notation "{ l }" := (HF l) (at level 0, l at level 99).

Notation EMPTY := {nil}.
Notation ONE := {EMPTY::nil}.
Notation TWO := {EMPTY::ONE::nil}.

Infix ":::" := cons_hf (at level 60, right associativity).
Infix "+++" := app_hf (at level 60, right associativity).

Notation "x \in y" := (In_hf x y) (at level 60).
Notation "x == y" := (Eq_hf x y) (at level 70).

Notation morph1 := (Proper (Eq_hf ==> Eq_hf)).
Notation morph2 := (Proper (Eq_hf ==> Eq_hf ==> Eq_hf)).
Notation morph3 := (Proper (Eq_hf ==> Eq_hf ==> Eq_hf ==> Eq_hf)).


Definition empty := HF nil.
Definition singl x := HF (x:::nil).
Definition pair x y := HF (x:::y:::nil).

Definition union (x:hf) :=
  HF (fold_set _ (fun y l => hf_elts y+++l) x nil).

Definition power (x:hf) :=
  HF (fold_set _
          (fun y pow p => pow p ++ pow (y::p)) x
          (fun p => HF (rev p) :: nil) nil).

Definition subset (x:hf) (P:hf->bool) :=
  HF (fold_set _ (fun y l => if P y then y :: l else l) x nil).

Definition repl (x:hf) (f:hf->hf) :=
  HF (map f (hf_elts x)).

Instance singl_morph : morph1 singl.

Instance pair_morph : morph2 pair.

Definition eq_hf_fun (x:hf) (f1 f2:hf->hf) :=
  forall y1 y2, y1 \in x -> y1 == y2 -> f1 y1 == f2 y2.

Lemma eq_hf_fun_sym : forall x f1 f2,
  eq_hf_fun x f1 f2 -> eq_hf_fun x f2 f1.

Lemma eq_hf_fun_trans : forall x f1 f2 f3,
   eq_hf_fun x f1 f2 -> eq_hf_fun x f2 f3 -> eq_hf_fun x f1 f3.

Lemma eq_hf_fun_left : forall x f1 f2,
  eq_hf_fun x f1 f2 -> eq_hf_fun x f1 f1.

Definition hf_pred_morph x P :=
  forall y1 y2, y1 \in x -> y1 == y2 -> P y1 = true -> P y2 = true.

Definition eq_hf_pred (x:hf) (f1 f2:hf->bool) :=
  forall y1 y2, y1 \in x -> y1 == y2 -> f1 y1 = f2 y2.


Lemma empty_elim : forall x, ~ x \in empty.

Lemma empty_ext : forall a, (forall x, ~ x \in a) -> a == empty.

Lemma singl_intro : forall x y, x == y -> x \in singl y.

Lemma singl_elim : forall x a, x \in singl a -> x == a.

Lemma singl_ext :
  forall y x,
  x \in y ->
  (forall z, z \in y -> z == x) ->
  y == singl x.

Lemma pair_elim : forall x a b,
  x \in pair a b -> x == a \/ x == b.

Lemma pair_intro1 : forall x a b, x == a -> x \in pair a b.

Lemma pair_intro2 : forall x a b, x == b -> x \in pair a b.

Lemma union_intro : forall x y z, x \in y -> y \in z -> x \in union z.

Lemma union_elim : forall x z, x \in union z -> exists2 y, x \in y & y \in z.

Lemma union_ext :
  forall u z,
  (forall x y, x \in y -> y \in z -> x \in u) ->
  (forall x, x \in u -> exists2 y, x \in y & y \in z) ->
  u == union z.

Instance union_morph : morph1 union.

Qed.

Lemma union_singl : forall x, union (singl x) == x.


Lemma power_intro :
  forall x y, Incl_hf x y -> x \in power y.

Lemma power_elim : forall x y z, x \in power y -> z \in x -> z \in y.

Lemma power_ext :
  forall p a,
  (forall x, (forall y, y \in x -> y \in a) -> x \in p) ->
  (forall x y, x \in p -> y \in x -> y \in a) ->
  p == power a.

Lemma power_morph : morph1 power.

Lemma subset_intro_gen : forall a (P:hf->bool) x,
  x \in a -> (forall x', x==x' -> P x' = true) -> x \in subset a P.

Lemma subset_intro : forall a (P:hf->bool) x,
  hf_pred_morph a P ->
  x \in a -> P x = true -> x \in subset a P.

Lemma subset_elim1 : forall a (P:hf->bool) x, x \in subset a P -> x \in a.

Lemma subset_elim2_gen : forall a (P:hf->bool) x,
  x \in subset a P ->
  exists2 x', x==x' & P x' = true.

Lemma subset_elim2 : forall a (P:hf->bool) x,
  hf_pred_morph a P ->
  x \in subset a P ->
  P x = true.

Lemma subset_ext :
  forall s a (P:hf->bool),
  hf_pred_morph a P ->
  (forall x, x \in a -> P x = true -> x \in s) ->
  (forall x, x \in s -> x \in a) ->
  (forall x, x \in s -> P x = true) ->
  s == subset a P.

Lemma subset_morph_ext : forall x1 x2 y1 y2,
  x1 == x2 -> eq_hf_pred x1 y1 y2 -> subset x1 y1 == subset x2 y2.

Lemma subset_empty1 : forall P, subset empty P == empty.

Lemma subset_singl : forall x a (P:hf->bool),
  x \in a ->
  P x = true ->
  (forall x', x' \in a -> (x==x' <-> P x' = true)) ->
  subset a P == singl x.


Lemma repl_intro : forall a f y x,
  eq_hf_fun a f f ->
  y \in a -> x == f y -> x \in repl a f.

Lemma repl_elim : forall a f x,
  eq_hf_fun a f f ->
  x \in repl a f -> exists2 y, y \in a & x == f y.

Lemma repl_ext : forall x a f,
  eq_hf_fun a f f ->
  (forall y, y \in a -> f y \in x) ->
  (forall y, y \in x -> exists2 z, z \in a & y == f z) ->
  x == repl a f.

Lemma repl_morph :
  forall x1 x2 f1 f2,
  x1 == x2 ->
  eq_hf_fun x1 f1 f2 ->
  repl x1 f1 == repl x2 f2.

Definition hf_false := empty.
Definition hf_true := singl hf_false.
Definition hf_bool := pair hf_false hf_true.

Definition couple x y := pair (singl x) (pair x y).
Definition fst p := union (subset (union p) (fun x => in_hf (singl x) p)).
Definition snd p :=
  union (subset (union p) (fun y => eq_hf (pair (fst p) y) (union p))).

Lemma union_couple_eq : forall a b, union (couple a b) == pair a b.

Instance couple_morph : morph2 couple.
Qed.

Instance fst_morph : morph1 fst.

Qed.

Lemma fst_def : forall x y, fst (couple x y) == x.

Instance snd_morph : morph1 snd.

Qed.

Lemma snd_def : forall x y, snd (couple x y) == y.

Lemma snd_ext : forall p x y,
 p == couple x y ->
 y == snd p.




Lemma raw_choose_elt : forall x, {y | In y (hf_elts x)}+{x==empty}.

Lemma choose_elt : forall x, {y | y \in x}+{x==empty}.

Lemma regularity_ax: forall a a0, a0 \in a ->
    exists2 b, b \in a & ~(exists2 c, c \in a & c \in b).