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

【问题标题】：Define polymorphic inductive type tree in coq在 coq 中定义多态归纳类型树
【发布时间】：2021-03-07 01:39:08
【问题描述】：

为了证明我定义的树高是 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.

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

【问题讨论】：

我认为您的 height 函数是错误的 - 我不完全确定您要计算什么（不幸的是，它看起来会返回 1 + 1 + the height of the first leaf of the root，这不是整棵树的高度）。

标签： coq

【解决方案1】：

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

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

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

【讨论】：

【解决方案2】：

Fixpoint height {X: Type} (t: tree X) : nat :=
  match t with
  | emp_tr _ => 0
  | node_tr _ l => let fix height_list (ltrees: list (tree X)) :=  
               match ltrees with
               | [] => 0
               | htr :: ttr => max (height htr) (height_list ttr)
               end
               in 1 + height_list l
  end.

用 let 求解。

【讨论】：