时间戳

首页 > 解决方案 > 如何在 Coq 中定义这种依赖类型的树结构？

coq - 如何在 Coq 中定义这种依赖类型的树结构？

问题描述

我想定义一种相当简单的树，但我不知道该怎么做。

首先，定义一个具有自然数值的标准二叉树，除了我们不允许空树：

Inductive nat_btree : Type :=
| leaf : nat -> nat_btree
| unary : nat_btree -> nat -> nat_btree
| binary : nat_btree -> nat_btree -> nat -> nat_btree.

现在，我想做的是定义一个我们称之为 special_nat_btree 的数据类型，它是一个 nat_btree，条件是每个节点都是：

  1. 一个值为 n 且没有子节点的节点（即叶子）
  2. 值为 n+1 的节点和值为 n 的单个子节点
  3. 一个值为 n^2 的节点，恰好有两个子节点，每个子节点的值为 n

因此，例如，我们可以有以下内容：

1
|
2     2   3
 \   /    |
   4      4
    \    /
      16
       |
      17

但我真的不知道正确的语法，甚至不知道在 Coq 中实现它的最佳方法。我最初的想法是要求证明子树中的“根值”与我们正在尝试构建的内容相匹配。因此，例如，上面的“一元”构造函数将变为：

unary : forall (t : special_nat_btree) (n : nat),
    special_nat_btree -> nat -> (n = S (root_val t)) -> 
    special_nat_btree

除了上述语法可能已经错误之外，这种方法还需要定义一个“root_val”函数，该函数将与 special_nat_btree 相互递归。填写我的推理，我得到以下信息（这不会编译）：

Inductive special_nat_btree : Type :=
  | leaf : nat -> special_nat_btree
  | unary : forall (t : special_nat_btree) (n : nat),
      special_nat_btree -> nat -> (n = S (root_val t)) -> 
      special_nat_btree
  | binary : forall (t_1 t_2 : special_nat_btree) (n : nat),
      special_nat_btree -> special_nat_btree -> nat ->
      (root_val t_1 = root_val t_2) ->
      (n = (root_val t_1) * (root_val t_1)) -> special_nat_btree
with
root_val (t : special_nat_btree) : nat :=
  match t with
  | leaf n => n
  | unary t' n p => n
  | binary t_1 t_2 n p_1 p_2 => n
  end.

而且，呃，我很确定我已经偏离了轨道。那么我应该如何处理呢？或者，如果我的想法没有完全偏离，那么完成我想要做的事情的正确语法是什么？

标签： coq

解决方案

这个索引类型怎么样

(* [btree n]: tree with root value [n]. *)
Inductive btree : nat -> Type :=
| leaf : forall n, btree n
| unary : forall n, btree n -> btree (S n)
| binary : forall n, btree n -> btree n -> btree (n * n)
.

然后使用 sigma 表示不确定值的树：

Definition tree : Type := { n : nat & btree n }.

例如：

Example foo : tree := existT _ _
  (unary _ (binary _ (binary _ (unary _ (leaf 1))
                               (leaf 2))
                     (unary _ (leaf 3)))).

树中的_in 实际上不是您描述的节点的值，而是实际值（nin btree n）是根据这些字段的内容计算出来的（因此将它们放在上面就不会那么混乱）：unary x _是一个节点valuex+1和它的孩子有 value x。

推荐阅读