The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

Pattern matching on the 256 cases of ascii is definitely a bad idea. Well, maybe not that bad for one function, but if you do that on all your functions on ascii, it is not surprising, you get bad performance issues. Try to regroup your symbols in something like:

Inductive num := N0 | N1 | … | N9.
Inductive alpha := Aa | … | A z.
Inductive binary := Plus | Mul | Div …
Inductive delim := Paren | Brace | Bracket.
…
Inductive char := Num(n : num) | Alpha(a:alpha, up:bool) | Bin(b:binary) | Delim(d:delim, opening:bool) | …

This might help a lot for pratical examples.

2013/10/30 Marcus Ramos <marcus.ramos AT univasf.edu.br>

Hi Matthieu,

Sure, here it is:

Lemma re_fa_sym:

      forall c: ascii,

      exists f: f_automata,

      re_fa_equiv (re_sym c) f.

Proof.

intros.

exists (a'''' c).

case c as [[][][][][][][][]]; compute; trivial.

Qed.

The function "re_fa_equiv" calls many other operations that I do not include here for the sake of space. Basically it converts the regular _expression_ "re_sym c" into a finite automata, and then does all necessary operations and checks in order to determine if they represent the same language - or not. A lot of operations indeed.

Regards,

Marcus.

2013/10/30 Matthieu Sozeau <matthieu.sozeau AT inria.fr>

Hi Marcus,

  could you show us the demonstration in question?

Best,
-- Matthieu

On 28 oct. 2013, at 23:33, Marcus Ramos <mvmramos AT gmail.com> wrote:

> Hi,
>
> It takes a few minutes to run the demonstration of a lemma with a few lines in it, but when it reaches "Qed", it takes more than 40 minutes just for it. Why is that so?
>
> Thanks in advance,
> Marcus.

--
.../Sedrikov\...