时间戳

首页 > 解决方案 > 在 coq 中定义多态归纳类型树

coq - 在 coq 中定义多态归纳类型树

问题描述

我坚持练习证明我定义的树高是 3。我在网上找到了二叉树 coq 代码，但我定义的树不是二叉树。该节点包含任意数量。

树图附： 树

下面是我的树代码：

Inductive tree (X:Type) : Type :=
  | empty : tree X
  | branch : X -> list (tree X) -> tree X.

Arguments tree {X}.
Arguments empty {X}.
Arguments branch {X}.

Definition mytree :=
  branch 1 [ branch 5 [ branch 2 [empty] ] ;  branch 8 [empty] ;
          branch 7 [ branch 3 [empty];branch 4 [empty] ] ].

Fixpoint height {X: Type} (node: @tree X) : nat :=
  match node with
  | empty => 0
  | branch _ l => S (match l with 
                        | [] => 0
                        | h::t => S (height h)
                       end)
  end.

下面是单元测试。我试图证明我的树高是 3（如图所示）

Example test_height:
  height mytree = 3.
Proof.
  simpl.

在我简化之后，它显示： 6 = 3: 1 子目标 ______________________________________(1/1) 6 = 3

我猜我之前定义的 BC 一个或多个函数是错误的。但我不确定是哪一个，为什么他们错了？任何人都可以帮助或给我一些提示吗？太感谢了

PS：还有一个关于练习的提示：

提示：您可能需要使用 let 表达式定义相互递归的函数。

它给出了 let 表达式的工作原理如下： • 命名递归函数（需要关键字修复）：

Definition a := let fix f (x:nat) := match x with
| O => O
| S y => f y
end
in f 2.

但我不确定如何在我的练习中使用这个让。

标签： coq

解决方案

您错误地定义了高度函数。您应该通过伪代码定义高度

height empty = 0
height (branch _ children) = 1 + max [height child | child in children]

如果孩子为空，则最大值应返回 0。一旦你正确定义了高度函数，你应该能够使用反身性来证明这个命题。

推荐阅读