The Coq mailing list

[Marcus Ramos <marcus.ramos AT univasf.edu.br>]

Hi again,

Thanks for the replies. Here is the Lemma (tries to prove the equivalence of the language generate by a single symbol regular _expression_ and a single transition finite automata).

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

I used "Show Proof", the proof term has a few thousand lines but I can´t save it. How do I handle this situation?

Thanks again.

Marcus.

2013/10/28 Abhishek Anand <abhishek.anand.iitg AT gmail.com>

You can do Show Proof just before Qed to get the exact term that has to be typechecked at Qed (I think).

Trying to type-check parts of the proof-term might help in isolating the problem.

-- Abhishek

On Mon, Oct 28, 2013 at 6:41 PM, Maxime Dénès <mail AT maximedenes.fr> wrote:

Hi,

In theory, a one tactic script can generate an arbitrarily complex proof term (which is checked at Qed), so you should give more information (like the lemma and its proof) if you want some advice.

Maxime.

On 10/28/2013 06:35 PM, Marcus Ramos 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.