伊莎贝尔结构证明

Question

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

让对象（我需要数）是包含从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 的归纳似乎不适用于这里。

Answer 1

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

不过，我有几点意见：

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

通常使用现有的库函数比自己定义新函数更好。您的两个函数可以使用这样的库函数来定义：

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}```

旁注：我会使用大写字母来表示集合，而不是 xs（通常用于列表）之类的东西。
也许这是因为你简化了你的问题，但在目前的形式中，valid_set A n 与 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 是最糟糕的一个——如果你把它作为一个假设，你就无法使用归纳法，因为一旦你做了一个归纳步骤，你就将 x 增加 1，所以你赢了'能够应用你的归纳假设。您的前三个引理的以下版本很容易通过：

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 要求集合在 1 到 n 的范围内，但是一旦你进行了一个归纳步骤，它就必须从 2 到 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

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

伊莎贝尔结构证明

Isabelle structure proof

functional-programming

isabelle

hol