The Coq mailing list

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

Hi there,

I'm new to Coq, so this is probably obvious.

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

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