The Coq mailing list

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

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.