nat.zfp

(**
  ZFCert で自然数定義してみた
*)

(* フォン・ノイマン式の自然数の構成。
   0 := 空集合、succ(n) := n ∪ {n} = n ∪ singleton(n)。 *)

(* 0 は空集合公理からそのまま得られる。 *)
Choose zero Hzero from empty_set.

(* succ の定義には対 {n} を作る必要があるので、対公理から積み上げる。 *)
Choose pair Hpair from pairing.

theorem exists_singleton : forall x, exists p, forall y, (y in p <-> y = x).
intro x.
specialize pairing x x as H.
resolution.
qed.

Choose singleton Hsingleton from exists_singleton.

theorem exists_cup : forall x, forall y, exists u, forall z, (z in u <-> z in x or z in y).
intro x.
intro y.
specialize union pair(x,y) as H.
obtain u Hu from H.
use u.
intro z.
specialize Hu z as Huz.
cases Huz.
split.
  intro Hzinu.
  rule cut Hex : exists y', z in y' and y' in pair(x,y).
    apply Huz_forward.
    exact Hzinu.
  obtain y' Hy' from Hex.
  cases Hy'.
  rule cut Hy'eq : y' = x or y' = y.
    specialize Hpair x y y' as Hp.
    cases Hp.
    apply Hp_forward.
    exact Hy'_right.
  cases Hy'eq.
  left.
  rewrite <- Hy'eq_left.
  exact Hy'_left.
  right.
  rewrite <- Hy'eq_right.
  exact Hy'_left.
  intro Hor.
  cases Hor.
  apply Huz_backward.
  use x.
  split.
    exact Hor_left.
    specialize Hpair x y x as Hp.
    cases Hp.
    apply Hp_backward.
    left.
    refl.
    apply Huz_backward.
    use y.
    specialize Hpair x y y as Hp.
    cases Hp.
    split.
      exact Hor_right.
      apply Hp_backward.
      right.
      refl.
qed.

Choose cup Hcup from exists_cup.

(* succ(x) := x ∪ singleton(x) *)
theorem exists_succ : forall x, exists u, forall z, (z in u <-> z in x or z in singleton(x)).
intro x.
specialize exists_cup x singleton(x) as Hc.
exact Hc.
qed.

Choose succ Hsucc from exists_succ.

(* 等号の両辺を所属関係に代入するための補助補題。
   equal_elim は名前付き項（単純な変数）にしか使えないので、
   succ(x) のような複合項を扱えるように一般形をあらかじめ証明しておく。 *)
theorem eq_subst_mem : forall a, forall b, forall y, (a = b -> (y in a -> y in b)).
intro a.
intro b.
intro y.
intro Heq.
intro Hy.
rule equal_elim a b z : y in z.
exact Heq.
exact Hy.
qed.

(* ペアノの公理のうち一番簡単な「0 はどの数の後者でもない」。
   succ(x) は必ず x を要素に持つが、zero は要素を持たないので、
   succ(x) = zero とすると矛盾する。 *)
theorem succ_never_zero : forall x, not (succ(x) = zero).
intro x.
intro Heq.
specialize Hsucc x as Hsx.
specialize Hsx x as Hsxx.
cases Hsxx.
rule cut Hxin : x in succ(x).
  apply Hsxx_backward.
  right.
  specialize Hsingleton x as Hsi.
  specialize Hsi x as Hsix.
  cases Hsix.
  apply Hsix_backward.
  refl.
specialize eq_subst_mem succ(x) zero x as Hsub.
rule cut Hxinzero : x in zero.
  apply Hsub.
  exact Heq.
  exact Hxin.
specialize Hzero x as Hnx.
contradiction.
qed.


(* x は必ず自分自身の後者に含まれる。単射性の証明で使う補題。 *)
theorem mem_succ_self : forall x, x in succ(x).
intro x.
specialize Hsucc x as Hsx.
specialize Hsx x as Hsxx.
cases Hsxx.
apply Hsxx_backward.
right.
specialize Hsingleton x as Hsi.
specialize Hsi x as Hsix.
cases Hsix.
apply Hsix_backward.
refl.
qed.

(* 等号の対称性。 *)
theorem eq_sym : forall a, forall b, (a = b -> b = a).
intro a.
intro b.
intro Heq.
rule equal_elim a b z : z = a.
exact Heq.
refl.
qed.

(* m ∈ n かつ n ∈ m は起こりえない（2要素の循環所属の禁止）。
   正則性（foundation）公理を対 {m, n} に適用して示す。 *)
theorem no_two_cycle : forall m, forall n, (m in n -> (n in m -> false)).
intro m.
intro n.
intro Hmn.
intro Hnm.
rule cut Hnonempty : exists a, a in pair(m,n).
  use m.
  specialize Hpair m n m as Hpmm.
  cases Hpmm.
  apply Hpmm_backward.
  left.
  refl.
specialize foundation pair(m,n) as Hf.
apply Hf in Hnonempty as Hy.
obtain y Hy2 from Hy.
cases Hy2.
specialize Hpair m n y as Hpy.
cases Hpy.
rule cut Hyeq : y = m or y = n.
  apply Hpy_forward.
  exact Hy2_left.
cases Hyeq.
  specialize eq_sym y m as Es1.
  apply Es1 in Hyeq_left as Hmy.
  specialize eq_subst_mem m y n as Esub1.
  rule cut Hniny : n in y.
    apply Esub1.
    exact Hmy.
    exact Hnm.
  specialize Hy2_right n as Hspec1.
  apply Hspec1.
  exact Hniny.
  specialize Hpair m n n as Hpnn.
  cases Hpnn.
  apply Hpnn_backward.
  right.
  refl.
  specialize eq_sym y n as Es2.
  apply Es2 in Hyeq_right as Hny.
  specialize eq_subst_mem n y m as Esub2.
  rule cut Hminy : m in y.
    apply Esub2.
    exact Hny.
    exact Hmn.
  specialize Hy2_right m as Hspec2.
  apply Hspec2.
  exact Hminy.
  specialize Hpair m n m as Hpmm2.
  cases Hpmm2.
  apply Hpmm2_backward.
  left.
  refl.
qed.

(* ペアノの公理「succ の単射性」: succ(m) = succ(n) ならば m = n。 *)
theorem succ_injective : forall m, forall n, (succ(m) = succ(n) -> m = n).
intro m.
intro n.
intro Heq.
specialize mem_succ_self m as Hmm.
specialize eq_subst_mem succ(m) succ(n) m as Esub1.
rule cut Hmsn : m in succ(n).
  apply Esub1.
  exact Heq.
  exact Hmm.
specialize Hsucc n as Hsn1.
specialize Hsn1 m as Hsnm.
cases Hsnm.
rule cut Hmor : m in n or m in singleton(n).
  apply Hsnm_forward.
  exact Hmsn.
cases Hmor.
  rule cut Hswap : succ(n) = succ(m).
    specialize eq_sym succ(m) succ(n) as Es.
    apply Es.
    exact Heq.
  specialize mem_succ_self n as Hnn.
  specialize eq_subst_mem succ(n) succ(m) n as Esub2.
  rule cut Hnsm : n in succ(m).
    apply Esub2.
    exact Hswap.
    exact Hnn.
  specialize Hsucc m as Hsm1.
  specialize Hsm1 n as Hsmn.
  cases Hsmn.
  rule cut Hnor : n in m or n in singleton(m).
    apply Hsmn_forward.
    exact Hnsm.
  cases Hnor.
    rule cut Hfalse : false.
      specialize no_two_cycle m n as Hcyc.
      apply Hcyc.
      exact Hmor_left.
      exact Hnor_left.
    contradiction.
    specialize Hsingleton m as Hsim.
    specialize Hsim n as Hsimn.
    cases Hsimn.
    rule cut Hnm_eq : n = m.
      apply Hsimn_forward.
      exact Hnor_right.
    specialize eq_sym n m as Esf.
    apply Esf.
    exact Hnm_eq.
  specialize Hsingleton n as Hsin.
  specialize Hsin m as Hsinm.
  cases Hsinm.
  apply Hsinm_forward.
  exact Hmor_right.
qed.

(* ここから帰納法の原理。無限公理が与える帰納的集合 inf の中で、
   「zero と succ で閉じた最小の部分集合」として nat を分出公理で
   切り出し、それが望みの帰納法の原理そのものになることを示す。 *)

(* 空集合はちょうど一つしかない、という事実。inf 内部の証人が
   zero そのものであることを示すのに使う。 *)
theorem empty_unique : forall a, forall b, ((forall z, not (z in a)) -> (forall z, not (z in b)) -> a = b).
intro a.
intro b.
intro H1.
intro H2.
apply extensionality.
intro z.
split.
intro Hz.
specialize H1 z as Hz1.
contradiction.
intro Hz.
specialize H2 z as Hz2.
contradiction.
qed.

(* 要素の側を等号で置き換えるための補助補題（eq_subst_mem の左辺版）。 *)
theorem eq_subst_mem_left : forall a, forall b, forall s, (a = b -> (a in s -> b in s)).
intro a.
intro b.
intro s.
intro Heq.
intro Ha.
rule equal_elim a b z : z in s.
exact Heq.
exact Ha.
qed.

Choose inf Hinf from infinity.

(* 無限公理の内部の空要素は zero と一致する。 *)
theorem zero_in_inf : zero in inf.
cases Hinf.
obtain e He from Hinf_left.
cases He.
rule cut Heez : e = zero.
  specialize empty_unique e zero as Heu.
  apply Heu.
  exact He_left.
  exact Hzero.
specialize eq_subst_mem_left e zero inf as Esub.
apply Esub.
exact Heez.
exact He_right.
qed.

(* 無限公理の内部の後者的な要素は succ(x) と一致する。 *)
theorem inf_closed_succ : forall x, (x in inf -> succ(x) in inf).
intro x.
intro Hxinf.
cases Hinf.
specialize Hinf_right x as Hspec.
rule cut Hex : exists s, (s in inf and forall z, (z in s <-> (z in x or z = x))).
  apply Hspec.
  exact Hxinf.
obtain s Hs from Hex.
cases Hs.
rule cut Heq_s : s = succ(x).
  specialize extensionality s succ(x) as Hext.
  apply Hext.
  intro z.
  split.
    intro Hzs.
    specialize Hs_right z as Hzspec.
    cases Hzspec.
    rule cut Hzor : z in x or z = x.
      apply Hzspec_forward.
      exact Hzs.
    specialize Hsucc x as Hsx.
    specialize Hsx z as Hsxz.
    cases Hsxz.
    apply Hsxz_backward.
    cases Hzor.
      left.
      exact Hzor_left.
      right.
      specialize Hsingleton x as Hsix.
      specialize Hsix z as Hsixz.
      cases Hsixz.
      apply Hsixz_backward.
      exact Hzor_right.
    intro Hzsuccx.
    specialize Hsucc x as Hsx2.
    specialize Hsx2 z as Hsxz2.
    cases Hsxz2.
    rule cut Hzor2 : z in x or z in singleton(x).
      apply Hsxz2_forward.
      exact Hzsuccx.
    specialize Hs_right z as Hzspec2.
    cases Hzspec2.
    apply Hzspec2_backward.
    cases Hzor2.
      left.
      exact Hzor2_left.
      right.
      specialize Hsingleton x as Hsix2.
      specialize Hsix2 z as Hsixz2.
      cases Hsixz2.
      apply Hsixz2_forward.
      exact Hzor2_right.
specialize eq_subst_mem_left s succ(x) inf as Esub2.
apply Esub2.
exact Heq_s.
exact Hs_left.
qed.

(* nat := inf の部分集合のうち、zero と succ で閉じたすべての部分集合に
   含まれるもの。これが「最小の帰納的集合」＝自然数全体になる。
   alias は Choose で導入した定数（inf, zero, succ）を自由変数として
   参照できないため、ここでは論理式をそのまま書き下している。 *)
theorem exists_nat : exists b, forall x, (x in b <-> (x in inf and forall j, (((forall w, (w in j -> w in inf)) and (zero in j and forall n, (n in j -> succ(n) in j))) -> x in j))).
separation Nat inf x : forall j, (((forall w, (w in j -> w in inf)) and (zero in j and forall n, (n in j -> succ(n) in j))) -> x in j).
exact Nat.
qed.

Choose nat Hnat from exists_nat.

theorem zero_in_nat : zero in nat.
specialize Hnat zero as Hz.
cases Hz.
apply Hz_backward.
split.
  exact zero_in_inf.
  intro j.
  intro Hj.
  cases Hj.
  cases Hj_right.
  exact Hj_right_left.
qed.

theorem nat_closed_succ : forall n, (n in nat -> succ(n) in nat).
intro n.
intro Hnnat.
specialize Hnat n as Hn.
cases Hn.
rule cut Hconj : n in inf and forall j, (((forall w, (w in j -> w in inf)) and (zero in j and forall n, (n in j -> succ(n) in j))) -> n in j).
  apply Hn_forward.
  exact Hnnat.
cases Hconj.
specialize Hnat succ(n) as Hsn.
cases Hsn.
apply Hsn_backward.
split.
  specialize inf_closed_succ n as Hic.
  apply Hic.
  exact Hconj_left.
  intro j.
  intro Hj.
  cases Hj.
  cases Hj_right.
  specialize Hconj_right j as Hcj.
  rule cut Hnj : n in j.
    apply Hcj.
    split.
      exact Hj_left.
      exact Hj_right.
  specialize Hj_right_right n as Hnjs.
  apply Hnjs.
  exact Hnj.
qed.

(* ペアノの公理「帰納法の原理」: nat は zero と succ で閉じたどの
   部分集合よりも小さい。任意の性質 P について、P(zero) と
   (n が自然数で P(n) ならば P(succ(n))) が言えれば、分出公理で
   {x in inf : P(x)} を作ってこの定理に渡すことで、nat の要素すべてが
   P を満たすことが導ける（下の nat_is_zero_or_succ が具体例）。 *)
theorem nat_induction : forall x, (x in nat -> forall j, (((forall w, (w in j -> w in inf)) and (zero in j and forall n, (n in j -> succ(n) in j))) -> x in j)).
intro x.
intro Hxnat.
specialize Hnat x as Hx.
cases Hx.
rule cut Hconj : x in inf and forall j, (((forall w, (w in j -> w in inf)) and (zero in j and forall n, (n in j -> succ(n) in j))) -> x in j).
  apply Hx_forward.
  exact Hxnat.
cases Hconj.
exact Hconj_right.
qed.

(* nat_induction の使用例: すべての自然数は zero か、
   何かの後者である。P(x) := (x = zero or exists k, x = succ(k)) を
   分出公理で inf から切り出し、それが帰納的であることを示してから
   nat_induction に渡す。 *)
theorem exists_predSet : exists b, forall x, (x in b <-> (x in inf and (x = zero or exists k, x = succ(k)))).
separation PredSet inf x : x = zero or exists k, x = succ(k).
exact PredSet.
qed.

Choose predSet HpredSet from exists_predSet.

theorem predSet_subset_inf : forall w, (w in predSet -> w in inf).
intro w.
intro Hw.
specialize HpredSet w as Hwp.
cases Hwp.
rule cut Hconj : w in inf and (w = zero or exists k, w = succ(k)).
  apply Hwp_forward.
  exact Hw.
cases Hconj.
exact Hconj_left.
qed.

theorem predSet_inductive : zero in predSet and forall n, (n in predSet -> succ(n) in predSet).
split.
  specialize HpredSet zero as Hz2.
  cases Hz2.
  apply Hz2_backward.
  split.
    exact zero_in_inf.
    left.
    refl.
  intro n.
  intro Hn.
  specialize HpredSet n as Hnp.
  cases Hnp.
  rule cut Hconj2 : n in inf and (n = zero or exists k, n = succ(k)).
    apply Hnp_forward.
    exact Hn.
  cases Hconj2.
  specialize HpredSet succ(n) as Hsp.
  cases Hsp.
  apply Hsp_backward.
  split.
    specialize inf_closed_succ n as Hic2.
    apply Hic2.
    exact Hconj2_left.
    right.
    use n.
    refl.
qed.

theorem nat_is_zero_or_succ : forall n, (n in nat -> (n = zero or exists k, n = succ(k))).
intro n.
intro Hnnat.
specialize nat_induction n as Hni.
rule cut Hall : forall j, (((forall w, (w in j -> w in inf)) and (zero in j and forall m, (m in j -> succ(m) in j))) -> n in j).
  apply Hni.
  exact Hnnat.
specialize Hall predSet as Hp.
rule cut Hnpred : n in predSet.
  apply Hp.
  split.
    exact predSet_subset_inf.
    exact predSet_inductive.
specialize HpredSet n as Hnp2.
cases Hnp2.
rule cut Hconj3 : n in inf and (n = zero or exists k, n = succ(k)).
  apply Hnp2_forward.
  exact Hnpred.
cases Hconj3.
exact Hconj3_right.
qed.