The Coq mailing list

[Marcus Ramos <mvmramos AT gmail.com>]

Hi Pierre,

Thank you for your comments. I´ll try to add more details. It is all about language theory, the demonstration of a theorem that states that every regular _expression_ ("re") generates a language that can be also accepted by a finite automata ("fa"). 

1) The code below executes fast:

Definition t1 (c: ascii): trans := (q0,Some c,q1).

Definition ts2 (c: ascii): ts := ts_item (t1 c).

Definition a''' (c: ascii): f_automata := (q0,(ts2 c)).

Definition re2: re := re_sym "a"%char.

Eval compute in re_fa_equiv re2 (a''' "a"%char).

It basically defines a single parametrized transition ("trans") between states "q0" and "q1" with some input, a transition set ("ts") built out of this transition, and a finte automata with initial state "q0" and the transition set. This automata accepts the language with a single sentence made out of a single symbol.

On the other hand, regular _expression_ "re2" generates this same language. Finally, "re_fa_equiv" checks whether the regular _expression_ and the finite automata represent the same language. No problem here, and the answer is "true" after "Eval compute".

2) When I put all this inside a theorem, it becomes:

Theorem re_fa:

   forall r: re,

   exists a: f_automata, re_fa_equiv r a.

Proof.

induction r.

Definition q0: state := (0,true,false).

Definition ts0: ts := ts_empty.

Definition a': f_automata := (q0,ts0).

exists a'.

compute.

trivial.

Definition q1: state := (1,false,true).

Definition t0: trans := (q0,None,q1).

Definition ts1: ts := ts_item t0.

Definition a'': f_automata := (q0,ts1).

exists a''.

compute.

trivial.

Definition t1 (c: ascii): trans := (q0,Some c,q1).

Definition ts2 (c: ascii): ts := ts_item (t1 c).

Definition a''' (c: ascii): f_automata := (q0,(ts2 c)).

exists (a''' a).

compute.

Abort.

The first two base cases work fine. On the third, however (supposedly the same as case 1 presented above), when "compute" is executed, the problem happens. Naturally, the theorem is incomplete, but the problem is that I can´t advance because of this. Hope this will clear things a bit. Thank you again.

Best Regards,

Marcus.

2013/9/27 Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>

Hi,
This not usual. I would guess that your problem is something like
you ask
Eval compute in (fun (x : foo) => bar x)
and that's immediate but in the hypothesis of your proof you don't have
x : foo
but
x := term_that_allow_very_heavy_computation : foo
so
compute "bar x" -> compute "bar term_that_allow_very_heavy_computation" takes ages

It is impossible to make more useful comments without a concrete example of your problem.

All the best,
Pierre B.

Le 26 sept. 2013 à 02:37, Marcus Ramos <mvmramos AT gmail.com> a écrit :

> Hi,
>
> When I issue an "Eval compute" on a term with a call to a single Fixpoint, the
> answer is almost immediate.
>
> When I issue "compute" (for the same Fixpoint with the same arguments) inside
> a proof for a theorem, it takes a long while (>15 minutes) and finally I get
> the message "Invalid argument" (stack overflow?). Because of this, I can´t
> complete the proof of the theorem.
>
> Is this usual? Any hints why this happens? How could I trace the problem and
> fix it? I am using coqIDE 8.4pl1 in Windows 8.
>
> Thanks in advance,
> Marcus.