The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Fri, 4 Mar 2011 11:26:52 +0100,
Stéphane Lescuyer 
<stephane.lescuyer AT inria.fr>
 a écrit :

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

Maybe even better: write conversion between [ascii] and [chr] to and
from ascii, and prove these proofs form a total bijection;
it is almost what I proposed in my Char module (but didn't used
"Coercion").

Note that doing this, your "match x, y with TAB, CR => … | _, _ => …"
won't have a 256+256 branching, but a lot less.

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

what does take so many nodes?
256×256=65.536 which is 15 times smaller than 1million+,
so you have more than 15 nodes for a branch!

> 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

Some very cool stuff would be to better support for meta-things;
For example, if we could do something like:

Definition pair: positive → positive → positive :=
 λ π₁ π₂· 2^π₁×(2×π₂+1).

Meta convert (i : mutual_inductive_type): fixpoint_type :=
 [code to generate a mutual fixpoint from all inductive types
  of i to positive (provided you have no other types inside of it,
  or can convert them to others); written using the syntax of the
  Coq kernel module for instance].

A little like functors, but being able to inspect the structure
themselves. Of course you won't be able to prove anything on these
functions, but able to prove things on generated terms by these
functions. "Meta" would be some kind of generalisation of Ltac, but
instead of generating terms, it would be intended to generate any
gallina object.

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