The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Not having your code, I cannot test it, but I find it bad taste to have
"Definition" inside of a proof. Either you want it global and define it
before, either you want something local and rely on tactics such as
"set" or "assert" or "pose".


Le Fri, 18 Oct 2013 15:43:59 -0300,
Marcus Ramos 
<mvmramos AT gmail.com>
 a écrit :

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