0

我想在 HOL 中证明非负整数是有根据的。一个人怎么能做到？

Definition int_lt_def:
  int_lt = λ(x:int). λ(y:int). (0≤x)/\(x<y)
End

Theorem WF_int_lt:
  WF int_lt
Proof
  simp [relationTheory.WF_DEF] >>
  gen_tac >>
  simp [int_lt_def] >>
  cheat
QED

我知道，自然数和非负数之间存在双射。

这种双射以两种方式保持顺序。

归纳原理适用于自然数。

从归纳原则遵循最小数原则。

如果我有正数的归纳原理，那么我可以重复证明并证明非负整数的最小数原理。

因此，我认为主要问题浓缩为以下问题：

如何证明非负数的归纳原理？

原则：

∀P. (∀x. (∀y. 0 ≤ y ∧ y < x ⇒ P y) ⇒ P x) ⇒ ∀x. P x
4

0 回答 0