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: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
  • To: Coq Club <coq-club AT inria.fr>
  • Cc: jonikelee AT gmail.com
  • Subject: Re: [Coq-Club] Erasable Red/Black Trees in Coq
  • Date: Wed, 23 Apr 2014 09:18:14 +0200

On 23 April 2014 11:17, AUGER Cédric <sedrikov AT gmail.com> wrote:
If you can decide of some property, then you have a form of irrelevance.
Any function to the 'bool' type can be converted in a function to
'Prop' by composition with 'conv (fun x => if x then True else False) :
bool -> Prop'. And for any boolean 'b', a term of type 'conv b' is
"irrelevant" (there is only a single habitant to that type).

That is mainly the main reason why we have UIP on decidable equalities.

This is, however, not sufficient for the trick I mentioned which needs conversion-level irrelevance. Which, indeed, isn't implemented in the current Coq. So, unfortunately, there is no conversion-level associativity yet in Coq. But we can hope the future makes it available.



Archive powered by MHonArc 2.6.18.

Top of Page