Пример индукции бинарного дерева

Question

Мне дали эту проблему индукции как практику, и я не работал с индукцией в течение нескольких месяцев, поэтому я заблудился о том, как подойти к этой проблеме. Вот пример:

«Доказать по индукции: в непустом бинарном дереве количество узлов равно количеству связей между узлами плюс один».

У меня есть базовое представление о том, как его запустить, например, как базовый вариант - 1 узел с 0 ссылками. Однако я не уверен, как представить «ссылки» в моем решении. Любая помощь с благодарностью.

Answer 1

Я бы начал с индуктивного определения непустого двоичного дерева.

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

Это выглядит немного сложнее, чем обычное двоичное дерево, но с четким разграничением различных образований и удалением типичного конструктора "Nil", помогающего в доказательстве.

Оттуда вы захотите определить, что такое «ссылки» и «узлы» и как их вычислять по дереву. Это довольно легко, учитывая определение 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. Осталось рассмотреть только три случая, и вы уже получили первый (базовый вариант).