0

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

这是我的 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 时，我遇到了类似的问题。在归纳步骤上也有问题。

4

2 回答 2

2

你的证明开始没有问题。如果用 简化第二个子目标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.
于 2022-03-04T08:52:55.660 回答
0

如果您可以阅读 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.
于 2022-03-03T22:52:36.487 回答