Isabelle中通过双射证明有限自然数集合族基数的咨询

你的证明思路完全有效，这是有限集合计数的经典双射法：只要在待计数集合和基数已知的集合之间构造出双射，就能直接得到待计数集合的基数。

你遇到的归纳不适用问题的根源 #

你当前的辅助引理都把参数x固定为Suc 0（也就是1），但set_to_bitmap递归的时候x是递增的，递归步的参数不符合引理的前提条件，自然没法用自带的归纳规则推进。解决方法是先推广所有辅助引理，去掉x=1的硬绑定，先证明更通用的结论，再代入x=1得到你需要的特定版本：

• 先定义通用区间合法集合：valid_set_range xs low high ≡ ∀a∈xs. low ≤ a ∧ a ≤ high，你原来的valid_set xs n等价于valid_set_range xs 1 n
• 把所有引理的前提替换为通用区间条件，比如长度引理的通用版本为：

  lemma length_set_to_bitmap_general:
    "valid_set_range xs x (x + n - 1) ⟹ length (set_to_bitmap xs x n) = n"
  

  这个引理直接对n做自然数归纳即可，不需要用set_to_bitmap.induct，归纳步拆开Suc n的定义后，递归调用的参数Suc x和n刚好匹配归纳假设的条件，证明非常顺畅。

剩余引理的证明思路 #

• 两个恒等引理（bitmap_to_set_to_bitmap_id、set_to_bitmap_to_set_id）是证明双射的核心，同样先推广为通用区间版本，对n做归纳即可。只要证完这两个引理，不需要单独证明单射和满射，即可直接得到两个集合之间存在双射。
• 基数推导直接用Isabelle标准库的bij_betw相关引理：bij_betw f A B ⟹ card A = card B，其中：
  • 映射f为λxs. set_to_bitmap xs 1 n
  • 定义域A = {xs. valid_set xs n}
  • 陪域B = {ps. valid_bitmap ps n}
• 陪域的基数card B = 2 ^^ n是标准结论，直接调用列表计数的库引理即可，不需要自行证明。

同类参考 #

你要证明的本质就是集合{1..n}的幂集基数为2^n，属于Isabelle标准库的基础结论，在Finite_Set、Power等理论模块中有大量同类双射证明可以参考，你的位映射构造就是幂集和二进制位列表的标准对应实现。

内容的提问来源于stack exchange，提问作者Eva