The Coq mailing list

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

Thanks, I tried the below (with the non-declarative statements), and
that lets me continue for now!

It looks like in declarative style, you do need a line like "have (x >
0) by _hyp."  But even with that, the hang still happens.

On Mon, Nov 28, 2011 at 11:59 AM, John Nicol 
<nicol.john AT gmail.com>
 wrote:
> 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.
>>
>