二叉树结构归纳法：sumLeaves t = sumNodes t +1的归纳步骤求解

函数定义 #

data Tree a = Leaf a | Node a (Tree a) (Tree a)

sumLeaves :: Tree a -> Integer
sumLeaves (Leaf x) = 1 
sumLeaves (Node _ lt rt) = sumLeaves lt + sumLeaves rt 

sumNodes :: Tree a -> Integer
sumNodes (Leaf x) = 0 
sumNodes (Node _ lt rt) = 1 + sumNodes lt + sumNodes rt 

任务 #

通过结构归纳法证明：对于所有有限树 t :: Tree a，等式 sumLeaves t = sumNodes t + 1 成立。

已完成内容 #

要证：sumLeaves t = sumNodes t + 1

I.A.（基例）：t = Leaf 0（任意Leaf实例均可）

sumLeaves (Leaf 0) = 1
sumNodes (Leaf 0) + 1 = 0 + 1 = 1

因此 1 = 1，基例成立。

I.V.（归纳假设）：假设该陈述对任意子树lt和rt成立，即
sumLeaves lt = sumNodes lt + 1
sumLeaves rt = sumNodes rt + 1

问题 #

I.S.（归纳步骤）该如何推导？我在这最后一步遇到了困难，请求帮助。

归纳步骤（I.S.）推导 #

要证明当t是Node _ lt rt形式的树时，等式sumLeaves t = sumNodes t + 1成立，按以下步骤推导：

1. 先根据sumLeaves的定义展开：
   sumLeaves (Node _ lt rt) = sumLeaves lt + sumLeaves rt
2. 代入归纳假设（sumLeaves lt = sumNodes lt + 1、sumLeaves rt = sumNodes rt + 1）：
   sumLeaves (Node _ lt rt) = (sumNodes lt + 1) + (sumNodes rt + 1)
3. 合并右边的常数项：
   = sumNodes lt + sumNodes rt + 2
4. 再看等式右边的sumNodes t + 1，先展开sumNodes的定义：
   sumNodes (Node _ lt rt) = 1 + sumNodes lt + sumNodes rt
5. 给这个结果加1：
   sumNodes (Node _ lt rt) + 1 = (1 + sumNodes lt + sumNodes rt) + 1 = sumNodes lt + sumNodes rt + 2
6. 对比步骤3和步骤5的结果，两者完全一致，因此：
   sumLeaves (Node _ lt rt) = sumNodes (Node _ lt rt) + 1

结合已证明的基例，通过结构归纳法可得出结论：所有有限树t :: Tree a都满足sumLeaves t = sumNodes t + 1。

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