我正在使用 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 点的问题？ 谢谢
【问题讨论】：
标签： functional-programming subset agda set-theory proof-of-correctness
顺便说一句，我已经使用我提出的策略解决了我的问题。为了定义计算子集数量的函数，我使用标准 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
【讨论】：