The Coq mailing list

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

Hi Auger,

Thanks, but I am not sure I understand your final suggestion. I appreciate if you can provide more details, otherwise never mind and thanks anyway.

Regards,

Marcus.

2013/10/29 AUGER Cédric <sedrikov AT gmail.com>

Le Mon, 28 Oct 2013 22:04:21 -0200,
Marcus Ramos <marcus.ramos AT univasf.edu.br> a écrit :

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

Did you really need to use the ascii type? Couldn’t you define your own
type? Your "case c as [[][][][][][][][]]; compute" is likely to be the
culprit as it generates 256 cases. With more smartness, this might be
dramatically reduced. Or maybe simply start with something like:
"intros c; exists (a''''' c); <unfold, cbv …, or compute so that each
occurrence of 'c' is a generalizable _expression_ of the form "t c"
where 't' is some function>; generalize <t c>; clear c; intros tc;
destruct tc …"

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