在 AGDA 中计算自然数的子集

Posted 2023-02-25

【中文标题】在 AGDA 中计算自然数的子集

【英文标题】：Computing the subsets of natural numbers in AGDA

【发布时间】：2019-12-23 23:12:40

【问题描述】：

我正在使用 AGDA 做一些经典的数学证明。我想证明一组基数 n 的子集数等于 2^n（即 pow (2, n)）。为此，我的策略如下：

1) 编写一个函数 sub n，给定每个自然数，它返回小于或等于 n 的所有可能的自然数子集的列表。

2) 编写两个函数“length”和“pow”，分别计算列表的长度和2^n

3) 将 3 个函数放在一起证明这个陈述。

但是，我在解决第 1 点时遇到了麻烦）。我的想法是让函数返回一个“list Nat”类型的列表，但是我在实现递归时遇到了一些问题。基本上，我对归纳步骤的想法是将“n”的每个子集关联到两个新子集：自身和添加“n+1”的子集。

您认为这是一种有效的策略吗？此外，我该如何解决第 1 点的问题？ 谢谢

【参考方案1】：

顺便说一句，我已经使用我提出的策略解决了我的问题。为了定义计算子集数量的函数，我使用标准 map 函数和一个附加的辅助函数 add-to-list：

add-to-list : ℕ → List ℕ  → List ℕ 
add-to-list n x  = n  ∷ x


subℕ : ℕ → List ( List ℕ )
subℕ zero = [ 0 ] ∷ []
subℕ (suc x) = subℕ x ++ ( map ( add-to-list  x ) ( subℕ x ) )

然后，我证明以下两个基本引理：

l-aux : ∀ A : Set   x y : List A  → ( length ( x ++ y ) )≡( ( length x ) + ( length  y ))
l-aux A [] y = refl
l-aux A x ∷ x₁ y rewrite l-aux A  x₁ y = refl

l-aux-1 : ∀ A : Set   x : List A   f : A → A  → ( length ( map f x ) ) ≡ ( length x )
l-aux-1 A [] f = refl
l-aux-1 A x ∷ x₁ f rewrite l-aux-1 A  x₁ f = refl

证明被简化为基本递归：

number-of-subsets : ∀ ( n : ℕ ) → ( length ( subℕ n ) ) ≡ ( pow 2 n )
number-of-subsets zero = refl
number-of-subsets (suc n ) rewrite l-aux List ℕ subℕ n  map ( add-to-list n ) (subℕ n) | l-aux-1 List ℕ subℕ n add-to-list n  |  number-of-subsets n | +0 (pow 2 n )  = refl