The following works. (I got the set-default-hints form from output of
the include-book form.)
(encapsulate
()
(local (include-book "arithmetic-5/top" :dir :system))
(local (set-default-hints
'((nonlinearp-default-hint stable-under-simplificationp
hist pspv))))
(defthm russinoff
(implies (and (rationalp a)
(rationalp b)
(rationalp c)
(<= 1 a)
(< 0 b)
(< 0 c)
(<= (expt a 2) (* b (+ c 1)))
(<= b (* 4 c)))
(< (expt (- a 1) 2) (* b c)))))
-- Matt
X-IronPort-MID: 58854409
X-IronPort-MID: 244575640
X-SBRS: 4.5
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result:
Ar4AAOyhpUzVx5rNkWdsb2JhbACXDYs+AQEBAQkLCgcRBB6sKZsDhUQEhFGIcxCCTYU3
X-IronPort-AV: E=Sophos;i="4.57,267,1283749200";
d="scan'208";a="244575640"
X-SpamScore: -21
X-BigFish: VPS-21(z2b68kz14e0M1432N98dN9371Pzz1202hzz8275bhz32i2a8h61h)
X-Spam-TCS-SCL: 0:0
X-WSS-ID: 0L9MCE2-02-D5L-02
X-M-MSG:
From: "Russinoff, David"<address@hidden>
CC: "address@hidden"<address@hidden>
Date: Fri, 1 Oct 2010 10:58:19 -0500
Thread-Topic: algebra problem
Thread-Index: ActhgTQ4BprFQxjpQaim1LoG0ECYFAAAEOLR
Accept-Language: en-US
Content-Language: en-US
X-MS-Has-Attach:
X-MS-TNEF-Correlator:
acceptlanguage: en-US
X-Reverse-DNS: ausb3extmailp02.amd.com
X-MIME-Autoconverted: from quoted-printable to 8bit by riley.its.utexas.edu
id o91Fx8Dc014294
X-Loop: address@hidden
X-Sequence: 211
X-no-archive: yes
List-Owner:<mailto:address@hidden>
X-SpamAssassin-Status: No, hits=-1.7 required=5.0
X-UTCS-Spam-Status: No, hits=-110 required=165
Sorry, I meant to say a>= 1.
________________________________________
From: address@hidden address@hidden On Behalf Of Pete Manolios
address@hidden
Sent: Friday, October 01, 2010 10:55 AM
To: Russinoff, David
Cc: address@hidden
Subject: Re: algebra problem
David,
Here is the formalization of your conjecture in ACL2.
(thm (implies (and (rationalp a)
(rationalp b)
(rationalp c)
(< 0 a)
(< 0 b)
(< 0 c)
(<= (expt a 2) (* b (+ c 1)))
(<= b (* 4 c)))
(< (expt (- a 1) 2) (* b c))))
I tried it in ACL2s, the ACL2 Sedan (the one I hinted you might want to
try).
After 0 seconds, here is what it returned:
We falsified the conjecture. Here is the counterexample:
-- (A 1/4), (B 13/23) and (C 9/47)
On Fri, Oct 1, 2010 at 11:39 AM, Russinoff, David
<address@hidden> wrote:
> Here is a high school algebra problem that I've been staring at for
> a couple of hours and is making me feel pretty stupid.
>
> Proposition: Let a, b, and c be positive rationals. If a^2<= b*(c+1)
> and b<= 4*c, then (a-1)^2< b*c.
>
> Proof: sqrt(b*(c+1)) - sqrt(b*c)<= sqrt(4*c*(c+1)) - sqrt(4*c*c)
> < sqrt(4*c*c + 4*c + 1) - 2*c
> = 2*c + 1 - 2*c
> = 1.
> Therefore, a<= sqrt(b*(c+1))< sqrt(b*c) + 1 and a - 1< sqrt(b*c).
>
> I need an ACL2 proof. I should be able to prove it without mentioning
> square roots. As J says (I paraphrase), "If it's true, you can prove it.
> So what?" But I'm still staring and feeling stupid.
>
>
--
Pete Manolios
Northeastern University
http://www.ccs.neu.edu/home/pete