Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Erasable Red/Black Trees in Coq

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Erasable Red/Black Trees in Coq


Chronological Thread 
  • 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.







Archive powered by MHonArc 2.6.18.

Top of Page