The Coq mailing list

[Pierre Corbineau <Pierre.Corbineau AT imag.fr>]

Hi,

The bug is known (Bug 2447) : the C-zar default automation uses 
congruence and congruence has a bug in the proof-generation code which 
makes it hang.

This bug is highly non-trivial: it involves problems with cycles in a 
pointer graph. I will fix it when I have Copious Free Time(TM).

The workaround for now would be to type something like:

then ((Rpower x 1) = x) by Rpower_1 using apply Rpower_1;auto.

The "then" instead of "have" is necessary here: you need x>0. The 'by 
Rpower_1' can be omited (but only because Rpower_1 is not a local 
hypothesis).

Cheers,

Pierre




On 11/28/2011 04:27 PM, John Nicol wrote:
> 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

--
Pierre Corbineau          | 
Pierre.Corbineau AT imag.fr
VERIMAG - Centre Équation | Tel: (+33 / 0) 4 56 52 04 42
2, avenue de Vignate      | Office nr B2G2
38610 GIÈRES - FRANCE     | http://www-verimag.imag.fr/~corbinea/
begin:vcard
fn:Pierre Corbineau
n:Corbineau;Pierre
org;quoted-printable:Universit=C3=A9 Joseph Fourier - Grenoble 1;Laboratoire VERIMAG - Polytech' Grenoble
adr;quoted-printable;quoted-printable:2, avenue de Vignate;;VERIMAG - Centre =C3=89QUATION ;GI=C3=88RES ;;38610;France
email;internet:Pierre.Corbineau AT imag.fr
title;quoted-printable:Ma=C3=AEtre de Conf=C3=A9rences
tel;work:+33 (0) 4 56 52 04 42
tel;fax:+33 (0) 4 56 52 03 44
x-mozilla-html:FALSE
url:http://www-verimag.imag.fr/~corbinea
version:2.1
end:vcard

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature