3

有一组一些结构。我试图证明集合的基数等于某个数字。完整的理论太长，无法在此处发布。所以这里是一个简化的，只是为了展示这个想法。

让对象（我需要计算）是包含从 1 到 n 的自然数的集合。证明思路如下。我定义了一个函数，它将集合转换为 0 和 1 的列表。这是函数及其逆：

fun set_to_bitmap :: "nat set ⇒ nat ⇒ nat ⇒ nat list" where
  "set_to_bitmap xs x 0 = []"
| "set_to_bitmap xs x (Suc n) =
    (if x ∈ xs then Suc 0 else 0) # set_to_bitmap xs (Suc x) n"

fun bitmap_to_set :: "nat list ⇒ nat ⇒ nat set" where
  "bitmap_to_set [] n = {}"
| "bitmap_to_set (x#xs) n =
    (if x = Suc 0 then {n} else {}) ∪ bitmap_to_set xs (Suc n)"

value "set_to_bitmap {1,3,7,8} 1 8"
value "bitmap_to_set (set_to_bitmap {1,3,7,8} 1 8) 1"

然后我打算证明 1) 一些长度为 n 的 0/1 列表等于2^^n，2) 函数是双射，3) 所以原始集合的基数2^^n也是。

这里有一些辅助定义和引理，看起来很有用：

definition "valid_set xs n ≡ (∀a. a ∈ xs ⟶ 0 < a ∧ a ≤ n)"
definition "valid_bitmap ps n ≡ length ps = n ∧ set ps ⊆ {0, Suc 0}"

lemma length_set_to_bitmap:
  "valid_set xs n ⟹
   x = Suc 0 ⟹
   length (set_to_bitmap xs x n) = n"
  apply (induct xs x n rule: set_to_bitmap.induct)
  apply simp
  sorry

lemma bitmap_members:
  "valid_set xs n ⟹
   x = Suc 0 ⟹
   set_to_bitmap xs x n = ps ⟹
   set ps ⊆ {0, Suc 0}"
  apply (induct xs x n arbitrary: ps rule: set_to_bitmap.induct)
  apply simp
  sorry

lemma valid_set_to_valid_bitmap:
  "valid_set xs n ⟹
   x = Suc 0 ⟹
   set_to_bitmap xs x n = ps ⟹
   valid_bitmap ps n"
  unfolding valid_bitmap_def
  using bitmap_members length_set_to_bitmap by auto

lemma valid_bitmap_to_valid_set:
  "valid_bitmap ps n ⟹
   x = Suc 0 ⟹
   bitmap_to_set ps x = xs ⟹
   valid_set xs n"
  sorry

lemma set_to_bitmap_inj:
  "valid_set xs n ⟹
   valid_set xy n ⟹
   x = Suc 0 ⟹
   set_to_bitmap xs x n = ps ⟹
   set_to_bitmap ys x n = qs ⟹
   ps = qs ⟹
   xs = ys"
  sorry

lemma set_to_bitmap_surj:
  "valid_bitmap ps n ⟹
   x = Suc 0 ⟹
   ∃xs. set_to_bitmap xs x n = ps"
  sorry

lemma bitmap_to_set_to_bitmap_id:
  "valid_set xs n ⟹
   x = Suc 0 ⟹
   bitmap_to_set (set_to_bitmap xs x n) x = xs"
  sorry

lemma set_to_bitmap_to_set_id:
  "valid_bitmap ps n ⟹
   x = Suc 0 ⟹
   set_to_bitmap (bitmap_to_set ps x) x n = ps"
  sorry

这是最后一个引理：

lemma valid_set_size:
  "card {xs. valid_set xs n} = 2 ^^ n"

这种方法看起来有效吗？有没有这样的证明的例子？你能提出一个关于如何证明引理的想法吗？我被卡住了，因为归纳set_to_bitmap.induct似乎在这里不适用。

4

1 回答 1

4

原则上，这种方法确实有效：如果你有一个f从一个集合A到一个集合B的函数和一个反函数，你可以证明bij_betw f A B（阅读：是一个从tof的双射），然后暗示。ABcard A = card B

但是，我有一些评论：

  1. 如果无论如何只能有 0 或 1，则应该使用bool列表而不是列表。nat

  2. 使用现有的库函数通常比自己定义新函数要好。您的两个函数可以使用如下库函数定义：

    set_to_bitmap :: nat ⇒ nat ⇒ nat set ⇒ bool list
set_to_bitmap x n A = map (λi. i ∈ A) [x..<x+n]

bitmap_to_set :: nat ⇒ bool list ⇒ nat set
bitmap_to_set n xs = (λi. i + n) ` {i. i < length xs ∧ xs ! i}```

  3. 旁注：我会为集合使用大写字母，而不是类似xs（通常用于列表）。

  4. 也许这是因为你简化了你的问题，但在它现在的形式下， is和is valid_set A nsimple 是一样的。库的结果很容易显示其基数：A ⊆ {1..n}{A. valid_set A n}Pow {1..n}

    lemma "card (Pow {1..(n::nat)}) = 2 ^ n"
  by (simp add: card_Pow)`

至于您最初的问题：您的前几个引理是可证明的，但是要进行归纳，您必须首先摆脱一些不需要的假设。这x = Suc 0是最糟糕的——如果你有一个假设，你就无法使用归纳，因为一旦你做了一个归纳步骤，你就会增加x1，所以你将无法应用你的归纳假设。您的前三个引理的以下版本很容易通过：

lemma length_set_to_bitmap:
  "length (set_to_bitmap xs x n) = n"
  by (induct xs x n rule: set_to_bitmap.induct) auto

lemma bitmap_members:
  "set (set_to_bitmap xs x n) ⊆ {0, Suc 0}"
  by (induct xs x n rule: set_to_bitmap.induct) auto

lemma valid_set_to_valid_bitmap: "valid_bitmap (set_to_bitmap xs x n) n"
  unfolding valid_bitmap_def
  using bitmap_members length_set_to_bitmap by auto

我还建议不要添加“缩写”之类ps = set_to_bitmap xs x n的假设。它不会破坏任何东西，但它往往会使事情不必要地复杂化。

下一个引理有点棘手。由于您的递归定义，您必须首先概括引理（valid_bitmap要求集合在 from 1to范围内n，但是一旦您进行了一个归纳步骤，它必须是 from 2to n）。以下作品：

lemma valid_bitmap_to_valid_set_aux:
  "bitmap_to_set ps x ⊆ {x..<x + length ps}"
  by (induction ps x rule: bitmap_to_set.induct)
     (auto simp: valid_bitmap_def valid_set_def)

lemma valid_bitmap_to_valid_set:
  "valid_bitmap ps n ⟹ valid_set (bitmap_to_set ps 1) n"
  using valid_bitmap_to_valid_set_aux unfolding valid_bitmap_def valid_set_def
  by force

内射性和满射性（这是您的最终目标）应该遵循两者是反函数的事实。证明这可能通过归纳是可行的，但需要一些概括和辅助引理。如果您坚持使用我上面概述的库函数的非递归定义，应该会更容易。

于 2021-11-06T14:29:28.950 回答