coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Ascii module

From: Brandon Moore <brandon_m_moore AT yahoo.com>
To: St�phane Lescuyer <stephane.lescuyer AT inria.fr>, AUGER Cedric <Cedric.Auger AT lri.fr>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Ascii module
Date: Fri, 4 Mar 2011 09:30:55 -0800 (PST)
Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=s1024; d=yahoo.com; h=Message-ID:X-YMail-OSG:Received:X-Mailer:References:Date:From:Subject:To:Cc:In-Reply-To:MIME-Version:Content-Type:Content-Transfer-Encoding; b=Bzrk1I0CUHSXUg6/TbsGfbbb9FnJUl72spuPFXqmNNHG6v4ZpUXZ0OyCcZXwJ6pnuqAVqUJ2jsdwmNL1SPg+26Rh2BBtKjiLVa3QlMvb2f8ZGK1OMA+/EIuy+5n61m8TYc5LeWMq6A187DZJMUiiRjGobHHH+PA3y6v4SBKUhZM=;

It seems like this should work quite well.

> Otherwise, if boolean equality is defined with a quadratic match,  the
> definition works OK but the proof that [char_eqb c c' -> c = c']  is
> *extremely* large (9minutes to typecheck, 1million+ nodes in the
> term).  For the total comparison function, things would be even worse
> because the  strict order transitivity proof would be cubic in the
> number of  constructors...

How do you measure nodes in a term?

> By the way, the loss of efficiency due to the conversion  is absolutely
> marginal (only starts to make a visible difference after  5000
> comparisons or so).

It is said that machine integers are used to implement reductions involving

Numbers.Cyclic.Int31

Would using that further reduce overhead?

Brandon

Re: [Coq-Club] Ascii module, (continued)