证明 Isabelle 中 naturals 的递归 "less than" 定义的基本属性

Question

我试图重新创建自然数的简化版本，用于学习目的（因为它涉及归纳定义、递归函数等...）。然而，在那个过程中，我陷入了一些我认为非常微不足道的事情。

基本上，我有一个自然数“natt”的定义和一个“<”关系的定义：

datatype natt = Zero | Succ natt

primrec natt_less :: "natt ⇒ natt ⇒ bool" (infixl "<" 75) where
  "natt_less n Zero = False"
| "natt_less n (Succ m') = (case n of Zero ⇒ True | Succ n' ⇒ natt_less n' m')"

从这些，我试图证明 < 关系的 3 个基本属性：

非自反性：~ (a < a)
非对称：a < b ⟹ ~ (b < a)
传递性：a < b ⟹ b < c ⟹ a < c

我能够证明第一个，但不能证明其他的。更让我吃惊的是，有一些子引理可以帮助解决这些问题，例如 Succ a < b ⟹ a < b、a < b ⟹ a < Succ b 或 a < b ∨ a = b ∨ b < a，它们看起来更微不足道，但尽管如此即使在多次次尝试之后，我也无法证明。似乎只有其中一个（包括2.和3.）足以证明其余部分，但我无法证明其中的任何。

我主要尝试使用归纳法。加上我自己定义的事实，有两种可能性——我的定义是错误的，没有所需的属性，或者我遗漏了一些 method/argument。所以，我有两个问题：

我的定义有误吗（即它没有准确表示 < 并且缺少所需的属性）？如果是这样，我该如何解决？
如果不是，我如何证明这些看似微不足道的性质？

对于上下文，我目前的尝试是通过归纳法，我可以证明基本情况，但总是卡在归纳法中，不知道去哪里进行假设，例如在这个例子中：

lemma less_Succ_1: "Succ a < b ⟹ a < b"
proof (induction b)
  case Zero
  assume "Succ a < Zero"
  then have "False" by simp
  then show ?case by simp
next 
  case (Succ b)
  assume "(Succ a < b ⟹ a < b)" "Succ a < Succ b"
  then show "a < Succ b" oops

Answer 1

根据 user9716869 的一些提示，很明显我的主要问题是对 induction 中的 arbitrary 选项缺乏了解。使用 (induction _ arbitrary: _) 和 (cases _)（详见 reference manual），证明非常简单。

由于这些是出于教育目的，下面的证明并不是为了简洁，而是为了让每一步都非常清楚。如果需要更多的自动化，其中的大部分可以大大减少，有些可以在一行中完成（我在引理下方留下评论）。

注意：在这些证明中，我们使用了关于归纳类型的隐式引理，它们的单射性（这意味着 (Succ a = Succ b) ≡ (a = b) 和 Zero ≠ Succ a）。此外，根据定义 (Succ a < Succ b) ≡ (a < b)。

首先，我们证明了 2 个有用的引理：

a < b ⟹ b ≠ Zero
b ≠ Zero ⟷ (∃ b'. b = Succ b')

lemma greater_not_Zero [simp]: "a < b ⟹ b ≠ Zero"
  (*by clarsimp*)
proof
  assume "a < b" "b = Zero"
  then have "a < Zero" by simp
  then show "False" by simp
qed

lemma not_Zero_is_Succ: "b ≠ Zero ⟷ (∃ b'. b = Succ b')"
  (*by (standard, cases b) auto*)
proof
  show "b ≠ Zero ⟹ ∃ b'. b = Succ b'"
  proof (cases b)
    case Zero
    assume ‹b ≠ Zero› 
    moreover note ‹b = Zero›
    ultimately show "∃b'. b = Succ b'" by contradiction
  next
    case (Succ b')
    assume ‹b ≠ Zero› 
    note ‹b = Succ b'› 
    then show "∃b'. b = Succ b'" by simp
  qed
next
  assume "∃ b'. b = Succ b'"
  then obtain b'::natt where "b = Succ b'" by clarsimp
  then show "b ≠ Zero" by simp
qed

有了这些，我们可以证明 3 个主要陈述：

非自反性：~ (a < a)
非对称性：a < b ⟹ ~ (b < a)
传递性：a < b ⟹ b < c ⟹ a < c

lemma less_not_refl [simp]: "¬ a < a"
  (*by (induction a) auto*)
proof (induction a)
  case Zero
  show "¬ Zero < Zero" by simp
next
  case (Succ a)
  note IH = ‹¬ a < a›
  show "¬ Succ a < Succ a" 
  proof
    assume "Succ a < Succ a"
    then have "a < a" by simp
    then show "False" using IH by contradiction
  qed
qed

lemma less_not_sym: "a < b ⟹ ¬ b < a"
proof (induction a arbitrary: b)
  case Zero
  then show "¬ b < Zero" by simp
next
  case (Succ a)
  note IH = ‹⋀b. a < b ⟹ ¬ b < a› 
    and IH_prems = ‹Succ a < b›
  show "¬ b < Succ a"
  proof
    assume asm:"b < Succ a"

    have "b ≠ Zero" using IH_prems by simp
    then obtain b'::natt where eq: "b = Succ (b')" 
      using not_Zero_is_Succ by clarsimp
    then have "b' < a" using asm by simp
    then have "¬ a < b'" using IH by clarsimp
    moreover have "a < b'" using IH_prems eq by simp
    ultimately show "False" by contradiction
  qed
qed

lemma less_trans [trans]: "a < b ⟹ b < c ⟹ a < c"
proof (induction c arbitrary: a b)
  case Zero
  note ‹b < Zero›
  then have "False" by simp
  then show ?case by simp
next 
  case (Succ c)
  note IH = ‹⋀a b. a < b ⟹ b < c ⟹ a < c› 
    and IH_prems = ‹a < b› ‹b < Succ c›
  show "a < Succ c"
  proof (cases a)
    case Zero
    note ‹a = Zero›
    then show "a < Succ c" by simp 
  next 
    case (Succ a')
    note cs_prem = ‹a = Succ a'›

    have "b ≠ Zero" using IH_prems by simp
    then obtain b' where b_eq: "b = Succ b'" 
      using not_Zero_is_Succ by clarsimp
    then have "a' < b'" using IH_prems cs_prem b_eq by simp
    moreover have "b' < c" using IH_prems b_eq by simp
    ultimately have "a' < c" using IH by simp
    then show "a < Succ c" using cs_prem by simp
  qed
qed

证明 Isabelle 中 naturals 的递归 "less than" 定义的基本属性

Proving basic properties of recursive "less than" definition for naturals in Isabelle

proof

isabelle

isar