The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

I roughly agree with points d) to e), and to some extent with points
b) and c). Even if the declarative mode is not adapted for massive
proving, it has an obvious proof-explanation purpose and I would not
throw this style of proof away without giving it a serious chance. For
that, we (ideally) need feedback from users. Opportunities for
improvements exist (e.g. a better integration with the computation
features of the "imperative" mode, but also vice-versa the integration
of some of its good features to the imperative mode, e.g. dealing with
cases in a user-chosen order, or bullets, which fortunately have
recently been made available in the imperative language too). The real
issue from the point of view of the development of Coq is that man
power is missing as the author of C-zar, Pierre Corbineau, is himself
missing, using his own words, Copious Free Time.

Point f) is irrelevant.

Hugo

On Mon, Nov 28, 2011 at 05:29:29PM +0100, AUGER Cedric wrote:
> Le Mon, 28 Nov 2011 10:27:11 -0500,
> John Nicol 
> <nicol.john AT gmail.com>
>  a écrit :
> 
> > Hi there,
> > 
> > I'm new to Coq, so this is probably obvious.
> 
> Indeed it is in imperative proof style!
> 
> > I'm trying to use Rpower declaratively (I don't want to do an
> > imperative proof, so I haven't tested that).  Coq starts churning
> > every time I do so, and eventually I run out of patience.  (Also: the
> > IDE completely locks up, so I can't click interrupt.)
> 
> In imperative style, it doesn't hang up that often.
> 
> > I've isolated the problem I'm having to the following test lemma,
> > which is I think a restatement of Rpower_1, which I think is also in
> > R_scope.  (Theorem Rpower_1 : forall x:R, 0 < x -> x ^R 1 = x.)
> > 
> > Open Local Scope R_scope.
> > Lemma test_Rpower_1:
> >   forall x:R,
> >   x > 0 -> (Rpower x 1) = x.
> > proof.
> >   let x:R be such that (x > 0).
> > have ((Rpower x 1) = x) by Rpower_1.  (*This line causes problems. *)
> > end proof.
> > Qed.
> > 
> > What am I missing?
> > 
> > Thanks,
> > John
> 
> First of all, some advices to have quick answers:
> . provide self contained files, (ie. put the "Require Import Reals."
> and so), because I hate (and so, I guess that some others do) guess
> what libraries are used.
> . if you really are a beginner, then avoid using the declarative style,
> since:
>  a) very few of us use it, so few of us will be able to reply
>  b) very few of us use it, so it is not as tested as the "regular" way,
>     and so is more bug prone
>  c) it hides a lot of Coq mechanisms, so you may have harder time to
>     understand errors
>  d) it is very verbose, so you will spend a lot of time doing quite
>     useless stuff
>  e) you have less control than regular way (unless you switch using
>     'escape')
>  f) we recently had some user which wanted to use this style, and
>     he wasn't really reading our replies and hints, so …
> 
> Require Import Rbase.
> Require Import Rpower.
> 
> Open Local Scope R_scope.
> Lemma test_Rpower_1:
>   forall x:R,
>   x > 0 -> (Rpower x 1) = x.
> proof.
>   define X as Rpower_1.
>   let x:R be such that (x > 0).
>   then (0 < x). (* I am not sure it is necessary in full declarative 
> scripts*)
>   escape. (* sorry, I have no solution for your problem here, but I am
>              not an expert of the declarative style; at least it
>              isolates the non declarative parts *)
>    now apply Rpower_1.
>   return.
> end proof.
> Qed.
>