CODEWITHSUNDEEP
coq
Morgan Sinclaire
Morgan Sinclaire

Reputation: 27

How to define this dependently-typed tree structure in Coq?

I’d like to define a rather simple kind of tree, but I’m not sure how to do it.

First, define a standard binary tree with natural number values, except we disallow empty trees:

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

Now, what I’d like to do is define a datatype we’ll call special_nat_btree which is a nat_btree with the condition that every node is either:

  1. A node with value n, and no children (i.e. a leaf)
  2. A node with value n+1, and a single child of value n
  3. A node with value n^2, and exactly two children, each of value n

So for instance we could have the following:

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

But I really don’t know the right syntax or even the best approach to implementing this in Coq. My initial thinking was to demand a proof that the “root values” in the subtree(s) match what we’re trying to construct. So for instance the “unary” constructor above would become something like:

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

Besides the above syntax probably being wrong already, this approach also requires defining a “root_val” function that would be in a mutual recursion with special_nat_btree. Filling out my reasoning, I get the following (this will not compile):

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.

And, uh, I’m pretty sure I’m way off track with this. So how should I approach this? Or, if my thinking isn't completely off, what's the correct syntax to accomplish what I'm trying to do?

Upvotes: 2

Views: 451

Answers (1)

Li-yao Xia
Li-yao Xia

Reputation: 33399

How about this indexed type

(* [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)
.

Then use a sigma to represent trees of indeterminate value:

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

For example:

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

The _ in the tree are actually not the values of the nodes as you describe, but instead the actual values (n in btree n) are computed from the contents of those fields (and so it's less confusing to just leave them off above): unary x _ is a node with value x+1 and its child has value x.

Upvotes: 4

Related Questions