The Coq mailing list

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

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

Attachment: test.v
Description: Binary data