The Coq mailing list

[John Nicol <nicol.john AT gmail.com>]

Thanks for the info!  Reading through the thread, it does sound like
Czar is not supported enough for serious usage.  That's too bad -- I
was hoping that would be the future path of Coq.

Over the years, I've spent a good deal of time looking at HOL, and
more recently, Isar mode in Isabelle (Isabelle/ZF, which is also not
that popular).  Isar appears supported, and they're developing a
next-gen IDE, which is nice if you haven't used Emacs since the
mid-90s ;-).  But (not going into the details) I've run into many
difficulties with Isabelle before even beginning, whereas with Coq and
CoqIDE, I was almost able to complete a proof "out of the box".  Well,
a base case of a minor theorem anyway.

Oh well.  I guess the lesson for me is that the current systems still
aren't ready for me (or I'm not ready for them :-) ).  Thanks for your
time.  I'll continue to watch Coq's progress.

Cheers,
John

On Tue, Nov 29, 2011 at 5:58 AM, AUGER Cedric 
<Cedric.Auger AT lri.fr>
 wrote:
> 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.
>> >
>
>