coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Proving bounds on data structures in Coq?

From: Siddharth Bhat <siddu.druid AT gmail.com>
To: Coq-Club Club <coq-club AT inria.fr>
Subject: [Coq-Club] Proving bounds on data structures in Coq?
Date: Thu, 18 Oct 2018 19:49:43 +0530
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=siddu.druid AT gmail.com; spf=Pass smtp.mailfrom=siddu.druid AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi1-f178.google.com
Ironport-phdr: 9a23:kGtXUhLo+Eis1mdV6NmcpTZWNBhigK39O0sv0rFitYgRLP/xwZ3uMQTl6Ol3ixeRBMOHs60C07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffwdFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QKsqUjq+8ahkVB7oiD8GNzEn9mHXltdwh79frB64uhBz35LYbISTOfFjfK3SYMkaSHJOUchRWSJPAZ6yYZUTAOcaJ+lUs5PwqkESoReiBwShAv7kxD9Shn/x2K03y/kvEQDb0wM9H9IBqm7UrMn1NKwPTO21zLPHzSneZP5Rwjf96ZXHfQ08of2WQL1wa9fRyUgyGA7egVWQrJbqPzKR1ugXr2eb6O9gWPuphmU6qA9xuiCiytkwhoTNnI4YyVDJ+T9kzIs0J9C0UlN3bNynHZZWqiqULZF5Qtk4TGFtoCs6yqMJuZq8fCUSzZQo3R/fa/ief4iP4xLvSf+dITlliH9ne7+znRmy8U+nyu3zUsm7zkxGoTZCktnJrnwN1hrT5dabSvZl4EutxTKC2xrQ5+xEO0w4iKvWJpw7zrItlJceslzPHirsl0X3iK+WeF8k+u+t6+n/ebXmp4KTOJJpig3kL6sugNG/AeUlPQUVUGib/P6z1Lzn/UHjXLpKifg2nrHDsJ/GPcQburK5AwhN34k/7Ba/Fi6q38gcnXkaN11IYwmHjojsO1HWOv/0F/a/g1K2kDdq3f/KJLPhAo+eZkTExZzmZPNW71NWgCE30NoXs5lTE/QKJO/5ck73rt3RSBEjZV+a2eHiXe582o8eUHiTAuezMKrO+QuT5+4jPq+AfpIUtB7yLvEk47jlinpvygxVRrWgwZZCMCPwJf9hOUjMJCO02o5QQ1dPhRI3SanRsHPHVDdSY3ioWKdlv2M0DYunCcHIQYX/2eXdjhf+JYVfYyV9Mn7JCW3hLtzWVPIFaSbUKchkwGRdCOqRDrQ53BTrjzfUjrpqKu2OpH8dvJPnkd90vqjdzE5iszNzCMuZ3ieGSGQmxm4=

Hello,

I was interested in implementing data structures from Okasaki's "purely functional data structures", but I'm not sure how to actually prove theorems about the amortized analysis -- in terms of the banker's method / physicist's method, while still being able to extract such a data structure out to Haskell code.

So, TL;DR:

How do I define data structures in Coq such that it is:

1. Extractable to code

2. Allows reasoning to prove bounds using Okasaki's methods?

Thanks,

~Siddharth

Sending this from my phone, please excuse any typos!

[Coq-Club] Proving bounds on data structures in Coq?, Siddharth Bhat, 10/18/2018
- Re: [Coq-Club] Proving bounds on data structures in Coq?, Xuanrui Qi, 10/18/2018
  - Re: [Coq-Club] Proving bounds on data structures in Coq?, Robby Findler, 10/18/2018
    - Re: [Coq-Club] Proving bounds on data structures in Coq?, Siddharth Bhat, 10/18/2018
      - Re: [Coq-Club] Proving bounds on data structures in Coq?, mukesh tiwari, 10/19/2018