The Coq mailing list

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

Hi Daniel,

Thank you very much for your comments and suggestions. I guess I have been pushing too hard in inductive types, definitions and fixpoints (in the computational perspective), and did not explore well the use and possibilities of inductive propositions. Thus the enormous amount of time required in my computations. I´ll try to do that now, following your idea, right after I get a better undestanding of it (I am still a beginner with Coq).

Best Regards,

Marcus.

2013/10/30 Daniel Schepler <dschepler AT gmail.com>

I'd second the comment on the ascii type -- why restrict yourself to ascii strings when the standard regex -> finite automaton compilation algorithms should work for lists over any finite alphabet?

Also, just as a matter of style, from your description it sounds like re_fa_equiv is a complex function returning a Prop.  Personally, I'd prefer to make re_fa_equiv into a function returning bool, and then say re_fa_equiv (re_sym c) f = true.  Or better yet, define re_fa_equiv conceptually as re_fa_equiv r f := (forall l:list alphabet, re_matches r l <-> fa_accepts f l).  Here re_matches could be a simple inductive Prop whose constructors are something like:
re_matches re_empty nil
re_matches (re_sym c) (c :: nil)
re_matches r1 l1 -> re_matches r2 l2 -> re_matches (re_concat r1 r2) (l1 ++ l2)
re_matches r1 l -> re_matches (re_disj r1 r2) l
re_matches r2 l -> re_matches (re_disj r1 r2) l
re_matches (kleine_star r) nil
re_matches r l1 -> re_matches (kleine_star r) l2 -> re_matches (kleine_star r) (l1 ++ l2)

And then you could either make a computation function re_fa_equiv_dec return { re_fa_equiv r f } + { ~ re_fa_equiv r f }, or prove that a bool return value is equal to true iff re_fa_equiv r f.  (Sure, that would make the re_fa_sym result a lot simpler to prove, as you'd just have to exhibit a three-state finite automaton I think, and then destruct the input lists into nil, (ne c :: _), (c :: nil), or (c :: c' :: _) and check the automaton returns the right result in each case.  The interesting part would be in proving that your compilation function results in an automaton satisfying re_fa_equiv, anyway.)

(Of course, judging by some examples in the Coq standard library, I might be a bit strange for not liking definitions of a Prop that are defined in terms of a computing function when there's an equivalent, more conceptual definition.  Who knows?)
--

Daniel Schepler

On Mon, Oct 28, 2013 at 8:35 PM, AUGER Cédric <sedrikov AT gmail.com> wrote:

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