Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] question for help

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] question for help


chronological Thread 
  • From: "Yevgeniy Makarov" <emakarov AT gmail.com>
  • To: judy AT mail.ccnu.edu.cn
  • Cc: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] question for help
  • Date: Tue, 25 Sep 2007 17:58:25 +0200
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=beta; h=received:message-id:date:from:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references; b=JcWbGjTdFntRByYNmdF8k9XM4nnPoWzShiQ9vnktqZocdW6ZauU3zT+7dpbedYKrWg/QhWCCmP5i11gJz91p6kVnXgVPyJS3BG8hlYKpVLfj+Rg9RmArT8R4UVg6MZAdwAAZqkabiC4lMyW0J4JmoSoS/l94eYMV6UusUGd63yg=
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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





Archive powered by MhonArc 2.6.16.

Top of Page