The Coq mailing list

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