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.
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.