证明二叉树的性质

Question

作为我自己的练习，我正在尝试定义和证明二叉树的一些属性。

这是我的 btree 定义：

Inductive tree : Type :=
| Leaf
| Node (x : nat) (t1 : tree) (t2 : tree).

第一个属性我想证明的是btree的高度至少是log2(n+1) 其中n是节点的数量。所以我简单地定义了 countNodes：

Fixpoint countNodes (t : tree) :=
  match t with
  | Leaf => 0
  | Node _ t1 t2 => 1 + (countNodes t1) + (countNodes t2)
  end.

和heightTree：

Fixpoint heightTree (t : tree) :=
  match t with
  | Leaf => 0
  | Node _ t1 t2 => 1 + (max (heightTree t1) (heightTree t2))
  end.

现在，这是我的（不完整的）定理。任何人都可以向我提供有关如何完成此归纳的提示吗？似乎我应该有 2 个基本案例（Leaf 和 Node _ Leaf Leaf），我该怎么做？

Theorem height_of_tree_is_at_least_log2_Sn : forall t : tree,
    log2 (1 + (countNodes t)) <= heightTree t.
Proof.
  intros.
  induction t.
  - simpl. rewrite Nat.log2_1. apply le_n.
  -

剩余目标：

1 goal (ID 26)
  
  x : nat
  t1, t2 : tree
  IHt1 : log2 (1 + countNodes t1) <= heightTree t1
  IHt2 : log2 (1 + countNodes t2) <= heightTree t2
  ============================
  log2 (1 + countNodes (Node x t1 t2)) <= heightTree (Node x t1 t2)

PS: 我在尝试证明任何节点的度数只能为0、1或2时遇到了类似的问题。归纳步骤也有问题。

Answer 1

如果您可以阅读 Mathcomp/SSReflect，请看一下这个引理：

https://github.com/clayrat/fav-ssr/blob/trunk/src/bintree.v#L102-L108

你的定理可以推导出来：

Corollary log_h_geq t : log2n (size1_tree t) <= height t.
Proof.
rewrite -(exp2nK (height t)); apply: leq_log2n.
by exact: exp_h_geq.
Qed.

Answer 2

你的proof start没有问题。如果您将第二个 sub-goal 简化为 simpl in *，您将获得：

1 goal (ID 47)
  
  x : nat
  t1, t2 : tree
  IHt1 : Nat.log2 (S (countNodes t1)) <= heightTree t1
  IHt2 : Nat.log2 (S (countNodes t2)) <= heightTree t2
  ============================
  Nat.log2 (S (S (countNodes t1 + countNodes t2))) <=
  S (Init.Nat.max (heightTree t1) (heightTree t2))

为了使内容更具可读性，您将引用树的表达式替换为变量（例如 remember）：

1 goal (ID 59)
  
  x : nat
  t1, t2 : tree
  n1, n2, p1, p2 : nat
  IH1 : Nat.log2 (S n1) <= p1
  IH2 : Nat.log2 (S n2) <= p2
  ============================
  Nat.log2 (S (S (n1 + n2))) <= S (Init.Nat.max p1 p2)

现在是 log2 和 max 的目标。 log2 上的许多属性都在标准库中。 lia 策略对于处理 max.

非常有帮助

关于你关于节点度数的问题：你如何使你的陈述正式化？是不是如下?

Fixpoint Forallsubtree (P : tree -> Prop) t :=
  match t with
    Leaf => P t
  | Node x t1 t2 => P t /\ Forallsubtree P t1 /\ Forallsubtree P t2
  end.

Definition root_degree (t: tree) :=
  match t with Leaf => 0 | Node _ _ _ => 2 end. 

Goal forall t,
  Forallsubtree (fun t =>  0 <= root_degree t <= 2) t.  
induction t; cbn; auto.    
Qed.

证明二叉树的性质

Proving Binary Tree Properties

binary-tree

computer-science

coq

proof-general