coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Erasable Red/Black Trees in Coq
- Date: Tue, 22 Apr 2014 10:04:54 +0200
Dear Jonathan,
This is a nice example. Note that this precise idea has been explored before (see for instance http://www.pps.univ-paris-diderot.fr/~letouzey/download/Letouzey_Spitters_05.pdf ).Another tool is Pierre-Yves Strub CoqMT [ http://pierre-yves.strub.nu/coqmt/ ], which allows to plug in decision procedures inside the conversion of Coq (the current prototype has Presburger's arithmetic if I'm not mistaken).
Both proof irrelevance and CoqMT are considered for integration with Coq (CoqMT will most likely be first).
/Arnaud Spiwack
On 21 April 2014 21:02, Jonathan <jonikelee AT gmail.com> wrote:
To all,
If you're interested in a way to get full erasability in Coq, or yet another encoding of Red/Black trees in Coq, have a look at:
https://github.com/jonleivent/mindless-coding
Erasability is accomplished by adding a single injectivity axiom to a single wrapper Prop type (Erasable). The readme explains things, and the Coq file is fairly well commented.
Any comments and/or criticisms are welcome!
-- Jonathan
- [Coq-Club] Erasable Red/Black Trees in Coq, Jonathan, 04/21/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Gabriel Scherer, 04/22/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Cedric Auger, 04/22/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Jonathan, 04/22/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Arnaud Spiwack, 04/22/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Jonathan, 04/22/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Arnaud Spiwack, 04/22/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Jonathan, 04/23/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, AUGER Cédric, 04/23/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Arnaud Spiwack, 04/23/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Arnaud Spiwack, 04/23/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Jonathan, 04/23/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Arnaud Spiwack, 04/24/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Jonathan, 04/24/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Arnaud Spiwack, 04/24/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Arnaud Spiwack, 04/23/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, AUGER Cédric, 04/23/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Jonathan, 04/23/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Arnaud Spiwack, 04/22/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Jonathan, 04/22/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Gabriel Scherer, 04/22/2014
Archive powered by MHonArc 2.6.18.