coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Inductive Records, example needed.

From: Cedric Auger <sedrikov AT gmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Inductive Records, example needed.
Date: Mon, 7 Sep 2015 01:55:51 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=sedrikov AT gmail.com; spf=Pass smtp.mailfrom=sedrikov AT gmail.com; spf=None smtp.helo=postmaster AT mail-io0-f172.google.com
Ironport-phdr: 9a23:mL306x8VTeKymv9uRHKM819IXTAuvvDOBiVQ1KB91uIcTK2v8tzYMVDF4r011RmSDdmds6MP0ruM+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuStKU15X8jrHos7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JsKWqLjOq88ULZwDTI8Mmlz6teh/U3IShLK7X8BWE0XlABJCk7L9kepcI32t37Ru+Zn2SLSFND5QKp8DS+v471qSxj2oCgCPj89tmrQj5oj3+pgvBu9qkknkMbva4aPOa8mcw==

2015-09-04 23:09 GMT+02:00 Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>:

Hello,

I tried to make Recursive Records, but I can't find any example. There's no hint in the Coq manual.

The best I could do was "

Inductive R := { head: nat; tail: R }.", but with without a Nil it has no use.
(For example, R -> False is trivial theorem. That means that no instance of this type could possibly exist. :( )

​In inductive context, yes, but there is also the coinductive one.

Otherwise, you can also try:​

​​
Inductive R := { head: nat; tail: option R }.​

Or trees:

​
Inductive R := { index:Type; chidren : index -> R }.

(leaves have index=emptySet)

Thanks in advance,
Ilmars

[Coq-Club] Inductive Records, example needed., Ilmārs Cīrulis, 09/04/2015
- Re: [Coq-Club] Inductive Records, example needed., Cedric Auger, 09/07/2015
  - Re: [Coq-Club] Inductive Records, example needed., Ilmārs Cīrulis, 09/09/2015