二叉树归纳示例

Question

我已经将这个归纳问题作为练习，而且我已经几个月没有使用归纳了，所以我不知道如何解决这个问题。这是示例：

"Prove by induction: In a non-empty binary tree, the number of nodes is equal to the number of links between the nodes plus one".

我对如何启动它有一个基本的想法，比如基本情况是 1 个节点和 0 个链接。但是，我不确定如何在我的解决方案中表示 "links"。非常感谢任何帮助。

Answer 1

我将从归纳定义一个非空二叉树开始。

Inductive nonemptyTree :=
    | Endpoint 
    | Single (l : nonemptyTree)
    | Double (l : nonemptyTree) (r : nonemptyTree).

这看起来比普通的二叉树复杂一点，但清楚地区分不同的结构并删除典型的 "Nil" 构造函数有助于证明。

从那里，您需要定义 "links" 和 "nodes" 是什么以及如何在给定树的情况下计算它们。鉴于 nonemptyTree 定义，这很容易。

Fixpoint links (t : nonemptyTree) : nat :=
    match t with
    | Endpoint => 0
    | Single l => 1 + links l
    | Double l r => 2 + links l + links r
    end.

Fixpoint nodes (t : nonemptyTree ) : nat :=
    match t with
    | Endpoint => 1
    | Single l => 1 + nodes l
    | Double l r => 1 + nodes l + nodes r
    end.

到那时，我们只需要证明对于所有树t，nodes t = links t + 1。只有三种情况需要考虑，而您已经得到了第一种情况（基本情况）。

二叉树归纳示例

Binary Tree Induction Example

binary-tree

induction