The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

Precisely, that's not the way to go with such a large inductive. What
you want to do instead is write conversions [code] and [chr] to and
from binary integers, which are functions that are linear in size,
prove that they form a partial bijection (these proofs are linear as
well) and define character equality as:

Definition char_eqb (c c' : char) := code c == code c'.

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...

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).

Stéphane

2011/3/3 AUGER Cedric 
<Cedric.Auger AT lri.fr>:
> Le Thu, 3 Mar 2011 09:39:02 +0100,
> Stéphane Lescuyer 
>Â <stephane.lescuyer AT inria.fr>
>  a écrit :
>
> And as the first function to define would be equality, ie.
>
> match x, y with
> | TAB, TAB => true
> | CR, CR => true
> …
> | _, _ => false
> end.
>
> By diagonalizing, you'll need to have a 256×256 system.
>
>> Indeed, you are right, so in a way the situation isn't too bad.
>> Another matching pattern which looks simple but would be quadratic is
>> the following:
>>
>> match c1, c2 with
>> | TAB, _ => true
>> | _, CR => true
>> | _, _ => false
>> end
>>
>> I guess that's up to people to avoid stuff like that, except for some
>> basic necessary functions (equality test and maybe comparison).
>>
>> Even with 'only' 512 cases or so, what bothers me is that because
>> underscore patterns are only syntactic, the right-hand side expression
>> will end up being duplicated and typechecked 500+ times in the term.
>>
>> S.
>>
>> On Wed, Mar 2, 2011 at 11:55 PM, Brandon Moore
>>Â <brandon_m_moore AT yahoo.com>
>>  wrote:
>> >
>> >
>> >> From: Stéphane Lescuyer 
>>Â >>Â <stephane.lescuyer AT inria.fr>
>> >
>> >>
>> >> ...
>> >>
>> >> The other thing I would be worried about is '_' patterns,  where
>> >> writing something like:
>> >>
>> >> match c1, c2 with
>> >> | TAB, CR =>  true
>> >> | _, _ => false
>> >> end
>> >>
>> >> would look harmless while actually  expanding to a 256*256
>> >> matching tree.
>> >
>> > A minor point, but I think that expands to a 256+256 matching tree.
>> > I would expect all but the TAB branch of the outer match to not
>> > decompose the second argument. It seems that's how it actually
>> > works, at least with a smaller example. Perhaps something with
>> > dependent types might see the pathological case.
>> >
>> > Example:
>> >
>> > Inductive foo : Set := A | B | C | D | E .
>> >
>> > Definition bar : foo -> foo -> bool := fun x y =>
>> >  match x, y with
>> >  | A, B => true
>> >  | _, _ => false
>> >  end.
>> >
>> > Print bar.
>> >
>> > produces
>> >
>> > bar =
>> > fun x y : foo =>
>> > match x with
>> > | A =>
>> >    match y with
>> >    | A => false
>> >    | B => true
>> >    | C => false
>> >    | D => false
>> >    | E => false
>> >    end
>> > | B => false
>> > | C => false
>> > | D => false
>> > | E => false
>> > end
>> >     : foo -> foo -> bool
>> >
>> >
>> >
>> >
>> >
>>
>>
>>
>
>



-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06