证明 Isabelle 中自然数递归“小于”定义的基本性质

如何解决证明 Isabelle 中自然数递归“小于”定义的基本性质

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

基本上，我有自然数“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 个基本属性：

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

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

我主要尝试使用归纳法。加上我自己定义的事实，有两种可能性 - 我的定义是错误的，并且没有所需的属性，或者我缺少一些方法/参数。所以，我有两个问题：

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

---

就上下文而言，我目前的尝试是通过归纳法，我可以证明基本情况，但总是陷入归纳情况，不知道从哪里开始假设，例如在此示例中：

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

解决方法

经过 user9716869 的一些提示后，很明显我的主要问题是对 arbitrary 中的 induction 选项缺乏了解。使用 (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