Library HF

Require Export List.
Require Export Omega.

Module Type DecHerFinZF.

Parameter hf : Type.
Parameter IN : hf -> hf -> Prop.
Definition nIN (x y:hf) : Prop := ~IN x y.
Infix "∈" := IN (at level 70).
Infix "∉" := nIN (at level 70).

Definition Subq (X Y:hf) : Prop := forall z, z X -> z Y.
Infix "⊆" := Subq (at level 70).

Parameter INb : hf -> hf -> bool.
Axiom IN_ref : forall x y, x y <-> INb x y = true.

Axiom set_ext : forall X Y, X Y -> Y X -> X = Y.

Axiom eps_ind : forall (P:hf -> Prop), (forall X, (forall x, x X -> P x) -> P X) -> forall X, P X.

Parameter empty : hf.
Notation "∅" := empty.
Axiom emptyE : forall (x:hf), x .

Parameter upair : hf -> hf -> hf.
Notation "{ x , y }" := (upair x y).
Axiom upairAx : forall (x y z:hf), z {x,y} <-> z = x \/ z = y.

Parameter union : hf -> hf.
Notation "⋃" := union (at level 40).
Axiom unionAx : forall (x z:hf), z x <-> exists y, y x /\ z y.

Parameter power : hf -> hf.
Notation "℘" := power.
Axiom powerAx : forall (X:hf), forall Y:hf, Y X <-> Y X.

Parameter repl : hf -> (hf -> hf) -> hf.
Notation "{ f | x ⋳ X }" := (repl X (fun x:hf => f)).
Axiom replAx : forall X f z, z {f x|x X} <-> exists x, x X /\ z = f x.

Parameter sep : hf -> (hf -> bool) -> hf.
Notation "{ x ⋳ X | P }" := (sep X (fun x:hf => P)).
Axiom sepAx : forall X P z, z {x X|P x} <-> z X /\ P z = true.

End DecHerFinZF.

Module AckermannCoding1937 : DecHerFinZF.

Definition hf := nat.

Fixpoint mod2 (x:nat) : bool :=
match x with
| O => false
| S O => true
| S (S x') => mod2 x'
end.

Fixpoint div2 (x:nat) : nat :=
match x with
| O => O
| S O => O
| S (S x') => S (div2 x')
end.

Fixpoint mul2 (x:nat) : nat :=
match x with
| O => O
| S x' => S (S (mul2 x'))
end.

Lemma mod2S x : mod2 (S x) <> mod2 x.

Lemma S_even_odd x : mod2 x = false -> mod2 (S x) = true.

Lemma S_odd_even x : mod2 x = true -> mod2 (S x) = false.

Lemma mod2mul2 x : mod2 (mul2 x) = false.

Lemma mod2Smul2 x : mod2 (S (mul2 x)) = true.

Lemma div2mul2 x : div2 (mul2 x) = x.

Lemma div2Smul2 x : div2 (S (mul2 x)) = x.

Lemma mod2div2S x : (mod2 x = true -> div2 (S x) = S (div2 x)) /\ (mod2 x = false -> div2 (S x) = div2 x).

Lemma mod2tdiv2S x : mod2 x = true -> div2 (S x) = S (div2 x).

Lemma mod2fdiv2S x : mod2 x = false -> div2 (S x) = div2 x.

Lemma mul2div2_evenodd x : (mod2 x = false /\ mul2 (div2 x) = x) \/ (mod2 x = true /\ S (mul2 (div2 x)) = x).

Lemma mul2div2_even x : mod2 x = false -> mul2 (div2 x) = x.

Lemma mul2div2_odd x : mod2 x = true -> S (mul2 (div2 x)) = x.

Lemma div2mod2_eq x y : div2 x = div2 y -> mod2 x = mod2 y -> x = y.

Lemma complete_induction (P:nat -> Prop) :
(forall x, (forall y, y < x -> P y) -> P x) ->
(forall x, P x).

Lemma div2SSlt x : div2 (S x) < S x /\ div2 (S (S x)) < S (S x).

Lemma div2Slt x : div2 (S x) < S x.

Lemma div2_induction (P:nat -> Prop) :
P 0 -> (forall x, P (div2 x) -> P x) ->
forall x, P x.

Fixpoint INb (x y:hf) : bool :=
match x with
| O => mod2 y
| S x' => INb x' (div2 y)
end.

Lemma div2INb x y : INb x (div2 y) = INb (S x) y.

Definition empty : hf := 0.

Lemma emptyEq : forall x, INb x empty = false.

Lemma INb_leq x y : INb x y = true -> x < y.

Fixpoint adj (x:nat) (y:nat) : nat :=
match x with
| O => if (mod2 y) then y else S y
| S x' => if (mod2 y) then S (mul2 (adj x' (div2 y))) else mul2 (adj x' (div2 y))
end.


Lemma INbdiv2adj x y : div2 (adj (S x) y) = adj x (div2 y).

Lemma adjEq : forall z x y, INb z (adj x y) = true <-> z = x \/ INb z y = true.
Lemma adjINb x y : INb x y = true -> adj x y = y.

Fixpoint list2hf (l:list nat) : nat :=
match l with
| nil => 0
| cons x r => adj x (list2hf r)
end.

Lemma INb_list2hf (l:list nat) : forall z, In z l <-> INb z (list2hf l) = true.

Lemma nat_remove_In_iff (x y:nat) l : In x (remove eq_nat_dec y l) <-> x <> y /\ In x l.

Definition tmin m n := m - (m - n).

Fixpoint hf2list (x:nat) : list nat :=
match x with
| O => nil
| S x' => if mod2 x then (0::(map S (hf2list (tmin x' (div2 x))))) else (map S (hf2list (tmin x' (div2 x))))
end.

Lemma tmindiv2 x : tmin x (div2 (S x)) = div2 (S x) /\ tmin (S x) (div2 (S (S x))) = div2 (S (S x)).


Lemma hf2list_eq (x:nat) : (mod2 x = true /\ hf2list x = (0::(map S (hf2list (div2 x))))) \/ (mod2 x = false /\ hf2list x = (map S (hf2list (div2 x)))).

Lemma hf2list_t_eq (x:nat) : mod2 x = true -> hf2list x = (0::(map S (hf2list (div2 x)))).

Lemma hf2list_f_eq (x:nat) : mod2 x = false -> hf2list x = (map S (hf2list (div2 x))).

Lemma list2hf_mapS_even l : mod2 (list2hf (map S l)) = false.

Lemma list2hf_mapS (l:list nat) : list2hf (map S l) = mul2 (list2hf l).

Lemma list2hf_hf2list (x:nat) : list2hf (hf2list x) = x.

Lemma INb_hf2list z y : INb z y = true <-> In z (hf2list y).

Definition equi (l1 l2:list nat) := incl l1 l2 /\ incl l2 l1.

Lemma hf2list_list2hf (l:list nat) : equi (hf2list (list2hf l)) l.

Lemma empty_or_nonempty y : y = 0 \/ exists x, INb x y = true.

Lemma INb_ext (x y:hf) : (forall z, INb z x = true <-> INb z y = true) -> x = y.

Definition IN (x y:hf) : Prop := INb x y = true.
Definition nIN (x y:hf) : Prop := ~IN x y.

Infix "∈" := IN (at level 70).
Infix "∉" := nIN (at level 70).

Definition Subq (X Y:hf) : Prop := forall z, z X -> z Y.
Infix "⊆" := Subq (at level 70).

Lemma IN_ref : forall x y, x y <-> INb x y = true.

Lemma set_ext : forall X Y, X Y -> Y X -> X = Y.

Lemma eps_ind (P:hf -> Prop) : (forall X, (forall x, x X -> P x) -> P X) -> forall X, P X.

Notation "∅" := empty.

Lemma emptyE (x:hf) : x .

Definition upair (x y:hf) : hf := list2hf (x::y::nil).

Notation "{ x , y }" := (upair x y).

Lemma upairAx (x y z:hf) : z {x,y} <-> z = x \/ z = y.

Definition union (x:hf) : hf := list2hf (flat_map hf2list (hf2list x)).

Notation "⋃" := union (at level 40).

Lemma unionAx (x z:hf) : z x <-> exists y, y x /\ z y.

Definition repl (X:hf) (f:hf -> hf) : hf := list2hf (map f (hf2list X)).

Notation "{ f | x ⋳ X }" := (repl X (fun x:hf => f)).

Lemma replAx X f z : z {f x|x X} <-> exists x, x X /\ z = f x.

Definition sep (X:hf) (P:hf -> bool) : hf := list2hf (filter P (hf2list X)).

Notation "{ x ⋳ X | P }" := (sep X (fun x:hf => P)).

Lemma sepAx X P z : z {x X|P x} <-> z X /\ P z = true.

Fixpoint powerl (l:list hf) : list hf :=
match l with
| (x::r) => powerl r ++ map (adj x) (powerl r)
| nil => cons 0 nil
end.

Definition power (X:hf) : hf := list2hf (powerl (hf2list X)).

Notation "℘" := power.

Lemma powerl_lem (l:list hf) : forall Y:hf, Y list2hf l <-> In Y (powerl l).

Lemma powerAx (X:hf) : forall Y:hf, Y X <-> Y X.

End AckermannCoding1937.