Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <14645-0@swan.cl.cam.ac.uk>; Fri, 24 Apr 1992 00:58:13 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA05067; Thu, 23 Apr 92 16:46:45 -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 AA05063; Thu, 23 Apr 92 16:46:31 -0700 Received: from auk.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl id <14508-0@swan.cl.cam.ac.uk>; Fri, 24 Apr 1992 00:46:29 +0100 To: Jeffrey Joyce Cc: info-hol Subject: Re: arithmetic challenge In-Reply-To: Your message of 21 Apr 92 22:34:00 +0100. <4602*joyce@cs.ubc.ca> Date: Fri, 24 Apr 92 00:46:25 +0100 From: John Harrison Message-Id: <"swan.cl.ca.510:23.03.92.23.46.31"@cl.cam.ac.uk> Well, since nobody else has volunteered, here is a proof of the arithmetic theorem for HOL-88 v2.0. This took me about 3 hours in total (including proof planning), and the result is rather ugly (but then so was the theorem). John. ------------------------------------------------------------------------------ let GSYM = CONV_RULE(ONCE_DEPTH_CONV SYM_CONV);; let ADD_SUB2 = PROVE ("!a c. (c + a) - c = a", REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[ADD_SYM] THEN MATCH_ACCEPT_TAC ADD_SUB);; let HALF_LEVEN = PROVE ("!x y. ((2 * x) + y) DIV 2 = x + (y DIV 2)", REPEAT GEN_TAC THEN MATCH_MP_TAC DIV_UNIQUE THEN EXISTS_TAC "y MOD 2" THEN REWRITE_TAC[RIGHT_ADD_DISTRIB; LEFT_ADD_DISTRIB] THEN GEN_REWRITE_TAC (RATOR_CONV o RAND_CONV o RAND_CONV o ONCE_DEPTH_CONV) [] [MULT_SYM] THEN REWRITE_TAC[GSYM ADD_ASSOC] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[EQ_MONO_ADD_EQ] THEN ONCE_REWRITE_TAC[MULT_SYM] THEN MATCH_MP_TAC DIVISION THEN REWRITE_TAC[num_CONV "2"; LESS_0]);; let HALF_LEXP = PROVE ("!x y z. (((2 EXP (x + 1)) * y) + z) DIV 2 = ((2 EXP x) * y) + (z DIV 2)", REPEAT GEN_TAC THEN REWRITE_TAC[GSYM ADD1; EXP] THEN REWRITE_TAC[GSYM MULT_ASSOC; HALF_LEVEN]);; let LT_02 = PROVE ("0 < 2", REWRITE_TAC[num_CONV "2"; LESS_0]);; let LE_ADD = PROVE ("!m n. m <= n ==> ?p. n = m + p", REPEAT GEN_TAC THEN REWRITE_TAC[LESS_OR_EQ] THEN DISCH_THEN(DISJ_CASES_THEN2(ASSUME_TAC o MATCH_MP LESS_ADD) SUBST1_TAC) THENL [POP_ASSUM(X_CHOOSE_THEN "p:num" (SUBST1_TAC o SYM)) THEN EXISTS_TAC "p:num" THEN MATCH_ACCEPT_TAC ADD_SYM; EXISTS_TAC "0" THEN REWRITE_TAC[ADD_CLAUSES]]);; let LESS_ADD2 = PROVE ("!w x y z. w <= x /\ y < z ==> (w + y) < (x + z)", REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_THEN "a:num" SUBST1_TAC o MATCH_MP LE_ADD) (X_CHOOSE_THEN "b:num" SUBST1_TAC o MATCH_MP LESS_ADD_1)) THEN REWRITE_TAC[ADD_ASSOC; GSYM ADD1] THEN MATCH_MP_TAC LESS_EQ_IMP_LESS_SUC THEN ONCE_REWRITE_TAC[(EQT_ELIM o AC_CONV(ADD_ASSOC,ADD_SYM)) "((p + q) + r) + s = (p + r) + (q + s)"] THEN MATCH_ACCEPT_TAC LESS_EQ_ADD);; let DIV_DOUBLE = PROVE ("!y. 0 < y ==> !x. (x DIV y) DIV 2 = x DIV (2 * y)", GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN POP_ASSUM(MP_TAC o MATCH_MP DIVISION) THEN DISCH_THEN(ASSUME_TAC o SPEC "x:num") THEN MP_TAC(MATCH_MP DIVISION LT_02) THEN DISCH_THEN(MP_TAC o SPEC "x DIV y") THEN DISCH_THEN(CONJUNCTS_THEN2 (\th. RULE_ASSUM_TAC(SUBS[th])) ASSUME_TAC) THEN CONV_TAC SYM_CONV THEN MATCH_MP_TAC DIV_UNIQUE THEN EXISTS_TAC "(((x DIV y) MOD 2) * y) + (x MOD y)" THEN REWRITE_TAC[ADD_ASSOC; MULT_ASSOC; GSYM RIGHT_ADD_DISTRIB] THEN FIRST_ASSUM(UNDISCH_TAC o assert is_conj o concl) THEN DISCH_THEN(CONJUNCTS_THEN2 (SUBST1_TAC o EQT_INTRO) ASSUME_TAC) THEN REWRITE_TAC[] THEN CONV_TAC(RAND_CONV(ONCE_DEPTH_CONV num_CONV)) THEN REWRITE_TAC[MULT_CLAUSES] THEN MATCH_MP_TAC LESS_ADD2 THEN ASM_REWRITE_TAC[] THEN GEN_REWRITE_TAC RAND_CONV [] [SYM(el 3 (CONJUNCTS(SPEC_ALL MULT_CLAUSES)))] THEN MATCH_MP_TAC LESS_MONO_MULT THEN MP_TAC(MATCH_MP LESS_OR (ASSUME "((x DIV y) MOD 2) < 2")) THEN DISCH_THEN(MP_TAC o CONV_RULE(RAND_CONV num_CONV)) THEN REWRITE_TAC[LESS_EQ_MONO]);; let EXP_ADD = PROVE ("!x y. 2 EXP (x + y) = (2 EXP x) * (2 EXP y)", INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES; EXP; MULT_CLAUSES] THEN ASM_REWRITE_TAC[MULT_ASSOC]);; let DIV_EXP = PROVE ("!x y. (x DIV (2 EXP y)) DIV 2 = x DIV (2 EXP (y + 1))", REPEAT GEN_TAC THEN REWRITE_TAC[EXP_ADD] THEN REWRITE_TAC[num_CONV "1"; EXP; MULT_CLAUSES; ADD_CLAUSES] THEN ONCE_REWRITE_TAC[MULT_SYM] THEN MATCH_MP_TAC DIV_DOUBLE THEN REWRITE_TAC[num_CONV "2"; ZERO_LESS_EXP]);; let EXP_DM = PROVE ("!x y. x MOD (2 EXP y) = x - ((2 EXP y) * (x DIV (2 EXP y)))", let th1 = SPEC "2 EXP y" DIVISION in let th2 = REWRITE_RULE[ZERO_LESS_EXP; num_CONV "2"] th1 in let th3 = REWRITE_RULE[SYM(num_CONV "2")] th2 in let th4 = CONJUNCT1 (SPEC "x:num" th3) in REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[MULT_SYM] THEN FREEZE_THEN(\t. GEN_REWRITE_TAC (RAND_CONV o RATOR_CONV o RAND_CONV) [] [t]) th4 THEN REWRITE_TAC[ADD_SUB2]);; let EXP_DM_2 = PROVE ("!x. x MOD 2 = x - (2 * (x DIV 2))", GEN_TAC THEN SUBGOAL_THEN "2 = 2 EXP 1" SUBST1_TAC THEN REWRITE_TAC[EXP_DM] THEN REWRITE_TAC[num_CONV "1"; EXP] THEN REWRITE_TAC[SYM(num_CONV "1"); MULT_CLAUSES; ADD_CLAUSES]);; let DIV_LE = PROVE ("!x y. 0 < y ==> (y * (x DIV y)) <= x", REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP DIVISION) THEN DISCH_THEN(\th. GEN_REWRITE_TAC RAND_CONV [] [CONJUNCT1(SPEC_ALL th)]) THEN GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [] [MULT_SYM] THEN MATCH_ACCEPT_TAC LESS_EQ_ADD);; let MAIN_LEMMA = PROVE ("!a b c. b <= a /\ c <= b ==> ((a - b) + (b - c) = a - c)", REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN(CHOOSE_THEN SUBST1_TAC o MATCH_MP LE_ADD)) THEN REWRITE_TAC[GSYM ADD_ASSOC; ADD_SUB2] THEN MATCH_ACCEPT_TAC ADD_SYM);; let JOYCE = PROVE ("!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))))", REPEAT GEN_TAC THEN DISCH_THEN(X_CHOOSE_THEN "p:num" SUBST1_TAC o MATCH_MP LESS_ADD_1) THEN REWRITE_TAC[ADD_ASSOC; ADD_SUB] THEN REWRITE_TAC[GSYM ADD_ASSOC; ADD_SUB2] THEN REWRITE_TAC[SUB_PLUS; ADD_SUB; ADD_SUB2] THEN REWRITE_TAC[HALF_LEXP; DIV_EXP] THEN ONCE_REWRITE_TAC[(EQT_ELIM o AC_CONV(ADD_ASSOC,ADD_SYM)) "(a + b) + c = (a + c) + b"] THEN REWRITE_TAC[EQ_MONO_ADD_EQ] THEN GEN_REWRITE_TAC (RATOR_CONV o ONCE_DEPTH_CONV) [] [EXP_ADD] THEN ONCE_REWRITE_TAC[(EQT_ELIM o AC_CONV(MULT_ASSOC,MULT_SYM)) "a * b * c * d = d * b * a * c"] THEN REWRITE_TAC[GSYM LEFT_ADD_DISTRIB] THEN ONCE_REWRITE_TAC[MULT_SYM] THEN REWRITE_TAC[num_CONV "2"; MULT_EXP_MONO] THEN REWRITE_TAC[SYM(num_CONV "2")] THEN DISJ_CASES_THEN(REPEAT_TCL CHOOSE_THEN SUBST1_TAC) (SPEC "A:num" num_CASES) THEN REWRITE_TAC[MULT_CLAUSES; MULT_MONO_EQ] THEN REWRITE_TAC[EXP_DM; EXP_DM_2] THEN REWRITE_TAC[RIGHT_SUB_DISTRIB] THEN GEN_REWRITE_TAC (RATOR_CONV o RAND_CONV o RAND_CONV o ONCE_DEPTH_CONV) [] [MULT_SYM] THEN REWRITE_TAC[DIV_EXP; GSYM ADD1] THEN REWRITE_TAC[MULT_ASSOC] THEN REWRITE_TAC[ONCE_REWRITE_RULE[MULT_SYM] (GSYM(CONJUNCT2 EXP))] THEN MATCH_MP_TAC MAIN_LEMMA THEN CONJ_TAC THENL [MATCH_MP_TAC DIV_LE THEN REWRITE_TAC[num_CONV "2"; ZERO_LESS_EXP]; REWRITE_TAC[ADD1; GSYM DIV_EXP] THEN REWRITE_TAC[EXP_ADD; GSYM MULT_ASSOC] THEN ONCE_REWRITE_TAC[MULT_SYM] THEN MATCH_MP_TAC LESS_MONO_MULT THEN REWRITE_TAC[num_CONV "1"; EXP; MULT_CLAUSES; ADD_CLAUSES] THEN MATCH_MP_TAC DIV_LE THEN MATCH_ACCEPT_TAC LT_02]);;