coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jonathan <jonikelee AT gmail.com>
- To: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>, Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Erasable Red/Black Trees in Coq
- Date: Wed, 23 Apr 2014 11:42:30 -0400
Thank you! I will try this out. I'm a bit reluctant about -impredicative-set, but erasability is already incompatible with certain things - certainly with indefinite description (which would unerase erasable terms). Also, I anticipate that I need both this associativity up to conversion and real backtracking of tactics over evars (which I've been told is in the trunk, but haven't figured out how to use yet) to get the full benefit.
-- Jonathan
On 04/23/2014 07:37 AM, Arnaud Spiwack wrote:
Actually… in the case of list I found a solution. It uses the
-impredicative-set flag of Coq: the impredicative encoding of lists have
associativity of append/empty up to conversion (this requires eta, but it's
already available in Coq v8.4).
Here is the relevant definitions. Since this type (kind of) isomorphic to
lists you should be able to reason on sorted lists quite nicely.
Definition IList (A:Type) :=
forall R:Set, (A->R->R) -> R -> R
.
Definition empty {A} : IList A :=
fun R c e => e
.
Definition single {A} (x:A) : IList A :=
fun R c e => c x e
.
Definition app {A} (l r:IList A) : IList A :=
fun R c e => l R c (r R c e)
.
Notation "l ++ r" := (app l r).
Remark app_empty_neutral_r : forall A (l:IList A), l++empty = l.
Proof.
intros **.
reflexivity.
Qed.
Remark app_empty_neutral_l : forall A (l:IList A), empty++l = l.
Proof.
intros **.
reflexivity.
Qed.
Remark app_associative : forall A (l r q:IList A), (l++r)++q = l++(r++q).
Proof.
intros **.
reflexivity.
Qed.
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, (continued)
- 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, 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, Jonathan, 04/24/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Jonathan, 04/26/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, AUGER Cédric, 04/26/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Arnaud Spiwack, 04/28/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Jason Gross, 04/28/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.