The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Here is an old post I sent (almost exactly 1 year before):

https://sympa-roc.inria.fr/wws/arc/coq-club/2010-12/msg00016.html

(don't forget to use UTF-8 encoding)

Maybe you could consider reading the whole thread for more information
on the declarative mode status.

There is also a simple proof on topological spaces, but AFAI remember,
it doesn't use any external lemma.

That is strange to say that, but if you really want the declarative
mode, you may be interested in having a look at mizar in Isabelle/Hol,
rather than keeping Coq; at least until A. Spiwack's new proof engine
is complete, because I guess nobody will make improvement doomed to be
broken in the declarative mode; and even after it is complete, I fear
that you will have to wait a long time before having some really
working stuff.

That is really a sad thing, since proof scripts are not "human
readable" and cezar scripts are; but in the meantime, they are so
verbose…

Le Mon, 28 Nov 2011 11:59:30 -0500,
John Nicol 
<nicol.john AT gmail.com>
 a écrit :

> Sorry, I should have sent a file.  (I wanted to make the case as
> self-contained as possible, but yes, I forgot to include the imports.)
>  File is attached; it uses the imports you mentioned.
> 
> I'm a beginner to Coq, but not a complete beginner to formalized
> systems.  Regarding a), b), c), d), and e), I am willing to take the
> pain of using the less-tested declarative mode, because I am only
> interested in writing declarative proofs.  (As a data point: I only
> considered Coq as a potential system once I found it had added a
> declarative mode.)
> 
> Regarding f), I'll try to listen to any advice I get ;-)  BTW, I read
> through the FAQ, Wiki, multiple sections in the Coq Manual (including
> the declarative one), looked for other declarative proofs (couldn't
> find them), and browsed the mailing list archives for references to
> Rpower before asking.
> 
> Cheers,
> John
> 
> On Mon, Nov 28, 2011 at 11:29 AM, AUGER Cedric 
> <Cedric.Auger AT lri.fr>
> 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.
> >