Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <26562-0@swan.cl.cam.ac.uk>; Wed, 15 Apr 1992 12:54:09 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA05614; Wed, 15 Apr 92 04:34:26 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA05610; Wed, 15 Apr 92 04:34:13 -0700 Received: from guillemot.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl id <25591-0@swan.cl.cam.ac.uk>; Wed, 15 Apr 1992 11:58:15 +0100 To: Jeffrey Joyce Cc: info-hol , Tom.Melham@uk.ac.cam.cl In-Reply-To: Your message of 15 Apr 92 02:46:00 +0100. <4580*joyce@cs.ubc.ca> Date: Wed, 15 Apr 92 11:58:09 +0100 From: Tom Melham Message-Id: <"swan.cl.ca.594:15.03.92.10.58.25"@cl.cam.ac.uk> Regarding Jeff's recent message: > In reply to Matt Kaufmann's request for challenging theorems ... > here is a (what I believe is) a theorem of natural number arithmetic > that exceeded my threshold for the amount of HOL-hacking effort that > I'm willing to invest in something of this size/complexity. > > "!A B C n i. > i < n ==> > (((((2 EXP (n - i)) * (A * (B MOD (2 EXP i)))) + (C DIV (2 EXP i))) DIV > 2) + > ((B DIV ((2 EXP i) MOD 2)) * (A * (2 EXP (n - 1)))) = > ((2 EXP (n - (i + 1))) * (A * (B MOD (2 EXP (i + 1))))) + > (C DIV (2 EXP (i + 1))))" > > ... > If there are any HOL-hackers out there looking for a challenge, I'd > be interested in whether if anyone can prove this theorem with > HOL in under 4 hours and less than a page of ML source code. I'm afraid that either there's a typo, or I've made a mistake, or this is in fact a non-theorem. A counterexample, running in version 2.0 using the reduce library, is attached. To be fair, it took me 3/4 of an hour or so to find the counterexample, which was suggested by a failed proof attempt... Tom ============================================================================ SOURCE: load_library `reduce`;; let th1 = ASSUME "!A B C n i. i < n ==> (((((2 EXP (n - i)) * (A * (B MOD (2 EXP i)))) + (C DIV (2 EXP i))) DIV 2) + ((B DIV ((2 EXP i) MOD 2)) * (A * (2 EXP (n - 1)))) = ((2 EXP (n - (i + 1))) * (A * (B MOD (2 EXP (i + 1))))) + (C DIV (2 EXP (i + 1))))";; let th2 = SPECL ["1";"2";"0";"1";"0"] th1;; let th3 = REWRITE_RULE [EXP;ADD_CLAUSES;MULT_CLAUSES;SUB_EQUAL_0;SUB_0] th2;; let th4 = CONV_RULE (ONCE_DEPTH_CONV REDUCE_CONV) th3;; let th5 = NOT_INTRO(DISCH_ALL th4);; --------------------------------------------------------------------- LOG: %ghol _ _ __ _ __ __ |___ |__| | | | |__| |__| | | | |__| |__ |__| |__| Version 2.0 (Sun4/Allegro), built on 25/10/91 #load_library `reduce`;; Loading library `reduce` ... Extending help search path. Loading boolean conversions........ Loading arithmetic conversions.................. Loading general conversions, rule and tactic..... Library `reduce` loaded. () : void #let th1 = ASSUME "!A B C n i. i < n ==> (((((2 EXP (n - i)) * (A * (B MOD (2 EXP i)))) + (C DIV (2 EXP i))) DIV 2) + ((B DIV ((2 EXP i) MOD 2)) * (A * (2 EXP (n - 1)))) = ((2 EXP (n - (i + 1))) * (A * (B MOD (2 EXP (i + 1))))) + (C DIV (2 EXP (i + 1))))";; ########th1 = . |- !A B C n i. i < n ==> (((((2 EXP (n - i)) * (A * (B MOD (2 EXP i)))) + (C DIV (2 EXP i))) DIV 2) + ((B DIV ((2 EXP i) MOD 2)) * (A * (2 EXP (n - 1)))) = ((2 EXP (n - (i + 1))) * (A * (B MOD (2 EXP (i + 1))))) + (C DIV (2 EXP (i + 1)))) #let th2 = SPECL ["1";"2";"0";"1";"0"] th1;; th2 = . |- 0 < 1 ==> (((((2 EXP (1 - 0)) * (1 * (2 MOD (2 EXP 0)))) + (0 DIV (2 EXP 0))) DIV 2) + ((2 DIV ((2 EXP 0) MOD 2)) * (1 * (2 EXP (1 - 1)))) = ((2 EXP (1 - (0 + 1))) * (1 * (2 MOD (2 EXP (0 + 1))))) + (0 DIV (2 EXP (0 + 1)))) #let th3 = REWRITE_RULE [EXP;ADD_CLAUSES;MULT_CLAUSES;SUB_EQUAL_0;SUB_0] th2;; Theorem SUB_0 autoloaded from theory `arithmetic`. SUB_0 = |- !m. (0 - m = 0) /\ (m - 0 = m) Theorem SUB_EQUAL_0 autoloaded from theory `arithmetic`. SUB_EQUAL_0 = |- !c. c - c = 0 Theorem MULT_CLAUSES autoloaded from theory `arithmetic`. MULT_CLAUSES = |- !m n. (0 * m = 0) /\ (m * 0 = 0) /\ (1 * m = m) /\ (m * 1 = m) /\ ((SUC m) * n = (m * n) + n) /\ (m * (SUC n) = m + (m * n)) Theorem ADD_CLAUSES autoloaded from theory `arithmetic`. ADD_CLAUSES = |- (0 + m = m) /\ (m + 0 = m) /\ ((SUC m) + n = SUC(m + n)) /\ (m + (SUC n) = SUC(m + n)) Definition EXP autoloaded from theory `arithmetic`. EXP = |- (!m. m EXP 0 = 1) /\ (!m n. m EXP (SUC n) = m * (m EXP n)) th3 = . |- 0 < 1 ==> (((((2 EXP 1) * (2 MOD 1)) + (0 DIV 1)) DIV 2) + (2 DIV (1 MOD 2)) = (2 MOD (2 EXP 1)) + (0 DIV (2 EXP 1))) #let th4 = CONV_RULE (ONCE_DEPTH_CONV REDUCE_CONV) th3;; th4 = . |- F #let th5 = NOT_INTRO(DISCH_ALL th4);; th5 = |- ~(!A B C n i. i < n ==> (((((2 EXP (n - i)) * (A * (B MOD (2 EXP i)))) + (C DIV (2 EXP i))) DIV 2) + ((B DIV ((2 EXP i) MOD 2)) * (A * (2 EXP (n - 1)))) = ((2 EXP (n - (i + 1))) * (A * (B MOD (2 EXP (i + 1))))) + (C DIV (2 EXP (i + 1)))))