0

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

基本上，我有一个自然数的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，我也无法证明。似乎只有其中一个（包括and ）足以证明其余部分，但我无法证明其中任何一个。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
4

1 回答 1

0

经过user9716869的一些提示后，很明显我的主要问题是arbitrary对induction. 使用(induction _ arbitrary: _)and (cases _)（详见参考手册），证明非常简单。

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

注意：在这些证明中，我们使用了一个关于归纳类型的隐式引理，它们的内射性（这意味着(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
于 2021-05-12T17:59:01.623 回答