functional-programming - 伊莎贝尔结构证明

Question

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

让对象(我需要计数)是包含从 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

原则上，这种方法确实有效:如果你有一个函数 f 从集合 A 到集合 B 和一个它的反函数，你可以证明 bij_betw f A B(阅读:f 是从 A 到 B 的双射)，然后这意味着 card 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. 也许这是因为您简化了问题，但在目前的形式中，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 by 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

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