The Coq mailing list

["Yevgeniy Makarov" <emakarov AT gmail.com>]

Hi,

> Inductive tree (A:Type): Type :=
> tree_node : A -> forest A -> tree A
> with forest (A:Type):Type:=
> |nochild: forest A
> |addchild: tree A->forest A->forest A.
>
> 1 here what's A stands for? means the node's type is Type? can I change 
> Type to
> nat?

A is the type of things that are stored in the tree, i.e., the type of
tree labels. A itself has sort Type, which means that A can be
basically any type (nat, list, ~ A /\ B, etc.).

> 2 how to present in a tree T,  node1 is the father of node 2 ,node 3..,or 
> node2
> is
> the son of the only father node 1.

Here is an example of a tree:

Definition t := tree_node nat 0 (addchild nat (tree_node nat 1
(nochild nat)) (nochild nat)).

The type of the labels (A above) is nat. The tree has two nodes: one
has label 0, its son has label 1.

This seems a little verbose, so in the beginning (before declaring
tree) you can say

Set Implicit Arguments.

and then after defining tree

Implicit Arguments nochild [A].

Then the same example can be written as

Definition t := tree_node 0 (addchild (tree_node 1 nochild) nochild).

> 3 how to define direction graph structure? and how to present in a graph 
> G,and
> how
> to define the relation between faher and son.

Data in Coq is represented using inductive types. You can read a
tutorial on inductive types on the Coq documentation web page.

Yevgeniy