coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Suneel Sarswat <suneel.sarswat AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: [Coq-Club] OCaml extraction and proof obligations
- Date: Sat, 23 Jan 2021 00:14:03 +0530
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=suneel.sarswat AT gmail.com; spf=Pass smtp.mailfrom=suneel.sarswat AT gmail.com; spf=None smtp.helo=postmaster AT mail-ej1-f47.google.com
- Ironport-phdr: 9a23:cFip3hayLgHlvL8OIvYKolr/LSx+4OfEezUN459isYplN5qZrsq5bnLW6fgltlLVR4KTs6sC17OH9fm+EjxZqdbZ6TZeKcMKD0dEwewt3CUYSPafDkP6KPO4JwcbJ+9lEGFfwnegLEJOE9z/bVCB6le77DoVBwmtfVEtfre9FYHdldm42P6v8JPPfQpImCC9YbRvJxmqsAndrMYbjZZmJ6or1xfEo3REdudLyWh1IV6fgwvw6t2/8ZJ+8Slcoe4t+9JFXa7nY6k2ULtUASg8PWso/sPrrx7DTQWO5nsYTGoblwdDDhbG4h/nQJr/qzP2ueVh1iaUO832Vq00Vi+576h3Uh/oiTwIOCA//WrKl8F/lqNboBampxxi347ZZZyeOfRicq/Be94RWGxMVdtTWSNcGIOxd4QAAeoPM+hbsofzuUcBoACkCgWwHu7i0CNEimP00KA8zu8vERvG3AslH98WrXrUsdP1O7kMXuCx0aLG0C/Mb+lN2Tbz8ofIbg0qrPaXXbJtd8re11cgFwffglWLs4PlJSiV1+oXvGiH9OdgWuevhHQmqwF1uDSg2sAsiozQi48T11vL+jl3zpwvKt2kVE50f8SkEJ1IuiyEKYd7Xt4uTmJstSs7yLAKpZ61cSgUxJklyRPSZf+Kf5WH7BzjSuucPSp0iXZrdr+9hxi/9Uatx+zyWMWp31tHqDdOnNfLtnAIzRPT686HR+Nj8UauxTaPzRrc5f1YIUA1kqrbLYQtzaA/l5oPq0TDGTP5l1/zjK+ScEUr4PSo6+XhYrX6vpOcKpd0hR/4MqQogMCwH/k3MhUWU2if5+uzz6fv/UziQLhMk/Y4kbHZvYjEKcgHoqO1GQxY34Y55xqhEjur084UkHYFIV9DZRmJlZLmO0vUL/D9Ffq/g0qjkDNsx/3eO73uGJTNLnzanLj/f7Zx9ldQyAQ8wN1d/Z5UBbYBIPX8Wk/1qtPUFAM2Mwuxw+r/CdV90J0RWX6XD6OHLK/ftUWE6+EvLuWWeoMZpTXwJ+Iq6vPslXM5nEUSfait3ZsZcnC4GfFmLl2CYXrxhNcOD3kFvg4kQOzxklKCSyVTZnioUKIg/Tw7B4emAp3CRoCpmrCOwCC7HphOamBcFl+MCWvod5mDW/oUdC2SJdZhniUYWrilVo8uzgqjtBT6yrpiNurb4DcUtZPl1Nhv5u3cjws+9TJuD5fV72bYRGZt22gMWjV+iKt4uAl2zkqJ+al+mf1RU9JJsaBnSAA/YKXByeF3D5jJUxjaYd6VAAK9X9OrDDV3Vdsr2MAHf25yHtyjilbI2C/8UOxdrKCCGJFhqvGU5HP2Pcsoky+bhplktEEvR450DUPjhqN78FKOVYvAkkHcmqTzMKpAg2jC82CMyWfIt0ZdAlYpDff1GEsHb06TluzXo1vYRub3W7siOwpFj8WFL/kSM4y7vRB9XP7mfe/mTSe0kma0CwyPw+rVPoXvcmQZmi7aDRpdng==
Dear Members,
I am not sure if this question is properly posed.
I have a coq program and its proof.
Now I want to run and test the extracted OCaml code on real data.
The coq project is completed using natural numbers since the real problem only involves natural numbers.
In the real data sets the numbers can be as large as millions.
In the extracted OCaml code the nat, bool and the list has symbolic representation besides it is doing unary operations for add, mult, leb, eqb, sub.
In order to use the OCaml code I used the library Coq.extraction.ExtrOcamlNatInt but it has a disclaimer
"trying to obtain efficient certified programs by extracting nat into int is definitively *not* a good idea:"
Can I call my program certified? Is there a better solution?
Besides this, the above library does not convert eqb and leb for some reason?? So, I am doing it like this
Extract Constant Nat.eqb => "( = )".
Extract Constant Nat.leb => "( <= )".
Extract Constant Nat.leb => "( <= )".
Is this correct? What are the proof obligations, if any?
I looked possible at solution on net and found a sulution mentioned on https://softwarefoundations.cis.upenn.edu/vfa-current/Extract.html.
For this, I need to convert my entire project (10k+ lines) from nat to int! Is there a quick fix?
Thanks in advance,
Suneel
- [Coq-Club] OCaml extraction and proof obligations, Suneel Sarswat, 01/22/2021
- Re: [Coq-Club] OCaml extraction and proof obligations, Frédéric Besson, 01/22/2021
- Re: [Coq-Club] OCaml extraction and proof obligations, Suneel Sarswat, 01/22/2021
- Re: [Coq-Club] OCaml extraction and proof obligations, Frédéric Besson, 01/22/2021
- Re: [Coq-Club] OCaml extraction and proof obligations, Suneel Sarswat, 01/22/2021
- Re: [Coq-Club] OCaml extraction and proof obligations, Frédéric Besson, 01/22/2021
Archive powered by MHonArc 2.6.19+.