Library ZFnats
Natural numbers
Definition zero := empty.
Definition succ n := n ∪ singl n.
Instance succ_morph : morph1 succ.
Definition pred := union.
Instance pred_morph : morph1 pred.
Qed.
Lemma discr : ∀ k, ~ succ k == zero.
Definition lt := in_set.
Definition le m n := lt m (succ n).
Infix "<" := lt.
Infix "<=" := le.
Instance lt_morph : Proper (eq_set ==> eq_set ==> iff) lt.
Qed.
Instance le_morph : Proper (eq_set ==> eq_set ==> iff) le.
Lemma le_case : ∀ m n, m <= n -> m == n \/ m < n.
Lemma succ_intro1 : ∀ x n, x == n -> x < succ n.
Lemma succ_intro2 : ∀ x n, x < n -> x < succ n.
Lemma lt_is_le : ∀ x y, x < y -> x <= y.
Lemma le_refl : ∀ n, n <= n.
Hint Resolve lt_is_le le_refl.
Definition is_nat n : Prop :=
∀ nat:set,
zero ∈ nat ->
(∀ k, k ∈ nat -> succ k ∈ nat) ->
n ∈ nat.
Lemma is_nat_zero : is_nat zero.
Lemma is_nat_succ : ∀ n, is_nat n -> is_nat (succ n).
Definition N := subset infinite is_nat.
Lemma zero_typ: zero ∈ N.
Lemma succ_typ: ∀ n, n ∈ N -> succ n ∈ N.
Lemma N_ind : ∀ (P: set->Prop),
(∀ n n', n ∈ N -> n == n' -> P n -> P n') ->
P zero ->
(∀ n, n ∈ N -> P n -> P (succ n)) ->
∀ n, n ∈ N -> P n.
Lemma lt_trans : ∀ m n p, p ∈ N -> m < n -> n < p -> m < p.
Lemma pred_succ_eq : ∀ n, n ∈ N -> pred (succ n) == n.
Lemma pred_typ : ∀ n, n ∈ N -> pred n ∈ N.
Lemma succ_inj : ∀ m n, m ∈ N -> n ∈ N -> succ m == succ n -> m == n.
max
Definition max := union2.
Instance max_morph : morph2 max.
Qed.
Lemma lt_0_succ : ∀ n, n ∈ N -> zero < succ n.
Lemma lt_mono : ∀ m n, m ∈ N -> n ∈ N ->
m < n -> succ m < succ n.
Lemma le_total : ∀ m, m ∈ N -> ∀ n, n ∈ N ->
m < n \/ m == n \/ n < m.
Lemma max_sym : ∀ m n, max m n == max n m.
Lemma max_eq : ∀ m n, m == n -> max m n == m.
Lemma max_lt : ∀ m n, n ∈ N -> m < n -> max m n == n.
Lemma max_typ : ∀ m n, m ∈ N -> n ∈ N -> max m n ∈ N.
Fixpoint nat2set (n:nat) : set :=
match n with
| 0 => zero
| S k => succ (nat2set k)
end.
Lemma nat2set_typ : ∀ n, nat2set n ∈ N.
Lemma nat2set_inj : ∀ n m, nat2set n == nat2set m -> n = m.
Lemma nat2set_reflect : ∀ x, x ∈ N -> exists n, x == nat2set n.
Recursor (as in G""odel's T)
Definition NREC f g n y :=
∀ P,
Proper (eq_set ==> eq_set ==> iff) P ->
P zero f -> (∀ m x, m ∈ N -> P m x -> P (succ m) (g m x)) -> P n y.
Lemma NREC_inv : ∀ f g n y,
morph2 g ->
NREC f g n y ->
NREC f g n y /\
(n == zero -> y == f) /\
(∀ m, m ∈ N -> n == succ m -> exists2 z, NREC f g m z & y == g m z).
Require Import ZFrepl.
Lemma NREC_choice_0 : ∀ f g, uchoice_pred (NREC f g zero).
Lemma NREC_choice : ∀ f g n,
n ∈ N ->
morph2 g ->
uchoice_pred (NREC f g n).
Recursor at the level of sets
Definition natrec f g n := uchoice (NREC f g n).
Global Instance natrec_morph' :
Proper (eq ==> eq ==> eq_set ==> eq_set) natrec.
Qed.
Instance natrec_morph :
Proper (eq_set ==> (eq_set ==> eq_set ==> eq_set) ==> eq_set ==> eq_set) natrec.
Qed.
Lemma natrec_def : ∀ f g n,
morph2 g -> n ∈ N -> NREC f g n (natrec f g n).
Lemma natrec_0 : ∀ f g, natrec f g zero == f.
Lemma natrec_S : ∀ f g n, morph2 g -> n ∈ N ->
natrec f g (succ n) == g n (natrec f g n).
Lemma natrec_typ P f g n :
morph1 P ->
morph2 g ->
n ∈ N ->
f ∈ P zero ->
(∀ k h, k ∈ N -> h ∈ P k -> g k h ∈ P (succ k)) ->
natrec f g n ∈ P n.