coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Anomaly: uncaught exception Invalid_argument "String.create". Please report.

From: Yoriyuki Yamagata <yoriyuki.yamagata AT aist.go.jp>
To: coq-club AT inria.fr
Subject: [Coq-Club] Anomaly: uncaught exception Invalid_argument "String.create". Please report.
Date: Mon, 20 Dec 2010 18:51:52 +0900
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:from:date:x-google-sender-auth:message-id :subject:to:content-type; b=Hetm7x0dAzvYg7DssfLpUxa4doBiUA1nFPyuGwFkK7f8vM+sQpQQBXHDkZSYXTuIji fQxqVYQYnYS6DJTbQ/1ygKFAZ/rE2RUcnl53tcudoTPsfmd/GASaJE6a/4kGjw44BbqN 6zrVu0fQ31xNFW07x/PLbSu+T9CSvttDCHDyA=

Hi, list.

I'm a completely beginner of Coq, and try to learn it by implementing AVL-tree. I complete a definition (with a correctness proof) of the balancing function, but unfortunately "Defined" command takes a long time then gives me a message "Anomaly: uncaught exception Invalid_argument "String.create". Please report." and fails.

I guess that Coq try to allocate a too large string, but what is the cause of it and is there a way to avoid it? I may use Qed but then I suppose that we cannot reason about the function later(?). Also, I use omega tactic a lot in the proof. Could this cause the problem?
I can manually prove the equations but it would be very tedious.

I attach my proof. (I know that my proof is really badly written.)
--
Yoriyuki　Yamagata
yoriyuki.yamagata AT aist.go.jp
http://staff.aist.go.jp/yoriyuki.yamagata/

Attachment: avlTree.v
Description: Binary data

[Coq-Club] Anomaly: uncaught exception Invalid_argument "String.create". Please report., Yoriyuki Yamagata
- Re: [Coq-Club] Anomaly: uncaught exception Invalid_argument "String.create". Please report., Pierre Courtieu
  - Re: [Coq-Club] Anomaly: uncaught exception Invalid_argument "String.create". Please report., Yoriyuki Yamagata