From 32aac5994198d90ca682ab92e3763c887cf24fa7 Mon Sep 17 00:00:00 2001 From: John Harrison Date: Thu, 17 Oct 2024 06:15:38 +0000 Subject: [PATCH] Fixed a couple of bugs in the handling of div/rem in INT_ARITH that were collectively limiting its ability to reason about formulas using several div/rem operations with distinct arguments. For example, this didn't work before but now does: let hbar = prove (`!x. abs x <= &2 pow 15 ==> let sqdmulh = (&2 * &0x4ebf * x) div &2 pow 16 in let srshr = (sqdmulh + &2 pow 10) div &2 pow 11 in abs(x - &3329 * srshr) <= &1664`, CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN INT_ARITH_TAC);; Also fixed identical degenerate-case bugs in the decision procedures RING_RULE and INTEGRAL_DOMAIN_RULE (the latter bug being also inherited by FIELD_TAC). Previously these would fail if the input problem was so trivial that the initial normalization converted it to "true", e.g. RING_RULE `x:A = ring_1 r ==> x = ring_1 r`;; INTEGRAL_DOMAIN_RULE `ring_mul r x z = y ==> ring_mul r x z = y`;; Also added a few more very basic ring lemmas: FIELD_POLY_RING IMAGE_POLY_EXTEND POLY_VAR_EQ_CONST --- CHANGES | 35 +++++++++++++++++++++ Library/ringtheory.ml | 71 ++++++++++++++++++++++++++++++++++--------- int.ml | 5 +-- 3 files changed, 94 insertions(+), 17 deletions(-) diff --git a/CHANGES b/CHANGES index ee940c41..e0280f01 100644 --- a/CHANGES +++ b/CHANGES @@ -8,6 +8,41 @@ * page: https://github.com/jrh13/hol-light/commits/master * * ***************************************************************** +Wed 16th Oct 2024 Library/ringtheory.ml + +Fixed identical degenerate-case bugs in the decision procedures +RING_RULE and INTEGRAL_DOMAIN_RULE (the latter bug being also +inherited by FIELD_TAC). Previously these would fail if the input +problem was so trivial that the initial normalization converted +it to "true", e.g. + + RING_RULE `x:A = ring_1 r ==> x = ring_1 r`;; + + INTEGRAL_DOMAIN_RULE `ring_mul r x z = y ==> ring_mul r x z = y`;; + +Wed 16th Oct 2024 int.ml + +Fixed a couple of bugs in the handling of div/rem in INT_ARITH that +were collectively limiting its ability to reason about formulas using +several div/rem operations with distinct arguments. For example, this +didn't work before but now does: + + let hbar = prove + (`!x. abs x <= &2 pow 15 + ==> let sqdmulh = (&2 * &0x4ebf * x) div &2 pow 16 in + let srshr = (sqdmulh + &2 pow 10) div &2 pow 11 in + abs(x - &3329 * srshr) <= &1664`, + CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN INT_ARITH_TAC);; + +Sat 12th Oct 2024 update_database/passim [new directory] + +Merged updates from June Lee completing support for OCaml version 5. As +well as fixing deprecated functions and adding a new "switch-5" option +in the Makefile, this enables the use of dynamic updating of the theorem +search database, which was a significant gap in earlier OCaml 5 support. +As part of this, the "update_database*.ml" files have been moved to a +new subdirectory "update_database". + Wed 9th Oct 2024 Library/ringtheory.ml Added a number of miscellaneous and simple ring theory lemmas: diff --git a/Library/ringtheory.ml b/Library/ringtheory.ml index 823e9196..fc4a56cf 100644 --- a/Library/ringtheory.ml +++ b/Library/ringtheory.ml @@ -7950,11 +7950,13 @@ let RING_RULE = GEN_REWRITE_CONV REDEPTH_CONV [RIGHT_AND_EXISTS_THM; LEFT_AND_EXISTS_THM] THENC GEN_REWRITE_CONV TOP_DEPTH_CONV [GSYM DISJ_ASSOC] THENC - GEN_REWRITE_CONV TOP_DEPTH_CONV [GSYM CONJ_ASSOC] in + GEN_REWRITE_CONV TOP_DEPTH_CONV [GSYM CONJ_ASSOC] + and true_tm = `T` in let RING_RULE_BASIC tm = let avs,bod = strip_forall tm in let th1 = init_conv bod in let tm' = rand(concl th1) in + if tm' = true_tm then EQT_ELIM th1 else let avs',bod' = strip_forall tm' in let th2 = end_itlist CONJ (map RING_RING_CORE (conjuncts bod')) in let th3 = EQ_MP (SYM th1) (GENL avs' th2) in @@ -15689,6 +15691,16 @@ let RING_POLYNOMIAL_VAR = prove REWRITE_TAC[FINITE_SING; SUBSET; IN_ELIM_THM; IN_SING] THEN REWRITE_TAC[poly_var] THEN MESON_TAC[]);; +let POLY_VAR_EQ_CONST = prove + (`!(r:A ring) (v:V) c. + poly_var r v = poly_const r c <=> trivial_ring r /\ c = ring_0 r`, + REPEAT GEN_TAC THEN REWRITE_TAC[poly_var; poly_const; TRIVIAL_RING_10] THEN + EQ_TAC THEN SIMP_TAC[COND_ID] THEN + GEN_REWRITE_TAC LAND_CONV [FUN_EQ_THM] THEN DISCH_THEN(fun th -> + MP_TAC(SPEC `monomial_var (v:V)` th) THEN + MP_TAC(SPEC `monomial_1:V->num` th)) THEN + REWRITE_TAC[MONOMIAL_VAR_1] THEN MESON_TAC[]);; + let RING_POLYNOMIAL_0 = prove (`!r. ring_polynomial r (poly_0 r:(V->num)->A)`, REWRITE_TAC[poly_0; RING_POLYNOMIAL_CONST; RING_0]);; @@ -17122,6 +17134,28 @@ let POLY_SUBRING_GENERATED_1 = prove GEN_TAC THEN GEN_REWRITE_TAC RAND_CONV [GSYM POLY_SUBRING_GENERATED] THEN AP_TERM_TAC THEN REWRITE_TAC[UNIV_1] THEN SET_TAC[]);; +let IMAGE_POLY_EXTEND = prove + (`!(f:A->B) k l (s:V->bool) a. + ring_homomorphism(k,l) f /\ + (!i. i IN s ==> a i IN ring_carrier l) + ==> IMAGE (poly_extend(k,l) f a) (ring_carrier(poly_ring k s)) = + ring_carrier + (subring_generated l (IMAGE a s UNION IMAGE f (ring_carrier k)))`, + REPEAT STRIP_TAC THEN + MP_TAC(ISPECL [`poly_ring (k:A ring) (s:V->bool)`; `l:B ring`; + `poly_extend(k,l) (f:A->B) (a:V->B)`; + `{poly_const (k:A ring) c | c | c IN ring_carrier k} UNION + {poly_var k (x:V) | x IN s}`] + SUBRING_GENERATED_BY_HOMOMORPHIC_IMAGE) THEN + REWRITE_TAC[POLY_SUBRING_GENERATED] THEN + REWRITE_TAC[SUBSET; FORALL_IN_UNION; FORALL_IN_GSPEC] THEN + ASM_SIMP_TAC[RING_HOMOMORPHISM_POLY_EXTEND; POLY_VAR; POLY_CONST] THEN + DISCH_THEN(SUBST1_TAC o SYM) THEN AP_TERM_TAC THEN AP_TERM_TAC THEN + REWRITE_TAC[IMAGE_UNION; GSYM IMAGE_o; SIMPLE_IMAGE] THEN + GEN_REWRITE_TAC RAND_CONV [UNION_COMM] THEN BINOP_TAC THEN + MATCH_MP_TAC IMAGE_EQ THEN + ASM_SIMP_TAC[POLY_EXTEND_VAR; POLY_EXTEND_CONST; o_THM]);; + let IMAGE_POLY_EXTEND_1 = prove (`!(f:A->B) k l a. ring_homomorphism(k,l) f /\ a IN ring_carrier l @@ -17129,19 +17163,9 @@ let IMAGE_POLY_EXTEND_1 = prove (ring_carrier(poly_ring k (:1))) = ring_carrier (subring_generated l (a INSERT IMAGE f (ring_carrier k)))`, - REPEAT STRIP_TAC THEN - MP_TAC(ISPECL [`poly_ring (k:A ring) (:1)`; `l:B ring`; - `poly_extend(k,l) (f:A->B) (\v:1. a)`; - `poly_var k one INSERT - IMAGE (poly_const k) (ring_carrier k:A->bool)`] - SUBRING_GENERATED_BY_HOMOMORPHIC_IMAGE) THEN - REWRITE_TAC[POLY_SUBRING_GENERATED_1] THEN - REWRITE_TAC[SUBSET; FORALL_IN_INSERT; FORALL_IN_IMAGE] THEN - ASM_SIMP_TAC[RING_HOMOMORPHISM_POLY_EXTEND; POLY_VAR_UNIV; POLY_CONST] THEN - DISCH_THEN(SUBST1_TAC o SYM) THEN AP_TERM_TAC THEN AP_TERM_TAC THEN - REWRITE_TAC[IMAGE_CLAUSES; GSYM IMAGE_o] THEN - ASM_SIMP_TAC[POLY_EXTEND_VAR] THEN AP_TERM_TAC THEN - MATCH_MP_TAC IMAGE_EQ THEN ASM_SIMP_TAC[o_THM; POLY_EXTEND_CONST]);; + REPEAT STRIP_TAC THEN ASM_SIMP_TAC[IMAGE_POLY_EXTEND] THEN + REWRITE_TAC[UNIV_1; IMAGE_CLAUSES] THEN + AP_TERM_TAC THEN AP_TERM_TAC THEN SET_TAC[]);; let POLY_EXTEND_INTO_SUBRING_GENERATED = prove (`!r r' s (h:A->B) v (x:V->B) p. @@ -19812,6 +19836,21 @@ let RING_UNIT_POLY_RING = prove EXISTS_TAC `r:A ring` THEN ASM_SIMP_TAC[RING_HOMOMORPHISM_POLY_CONST]]]);; +let FIELD_POLY_RING = prove + (`!(r:A ring) (s:V->bool). field(poly_ring r s) <=> field r /\ s = {}`, + REPEAT GEN_TAC THEN + ASM_CASES_TAC `s:V->bool = {}` THEN ASM_REWRITE_TAC[] THENL + [ASM_MESON_TAC[ISOMORPHIC_POLY_RING_TRIVIAL; ISOMORPHIC_RING_FIELDNESS]; + FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY])] THEN + DISCH_THEN(X_CHOOSE_TAC `x:V`) THEN + REWRITE_TAC[FIELD_EQ_ALL_UNITS; GSYM TRIVIAL_RING_10; TRIVIAL_POLY_RING] THEN + ASM_CASES_TAC `trivial_ring(r:A ring)` THEN ASM_REWRITE_TAC[] THEN + REWRITE_TAC[RING_UNIT_POLY_RING] THEN + DISCH_THEN(MP_TAC o SPEC `poly_var (r:A ring) (x:V)`) THEN + ASM_REWRITE_TAC[POLY_VAR] THEN + REWRITE_TAC[POLY_RING; GSYM POLY_CONST_0; POLY_VAR_EQ_CONST] THEN + ASM_SIMP_TAC[poly_var; MONOMIAL_VAR_1; NOT_IMP; RING_UNIT_0]);; + let RING_UNIT_POWSER_RING = prove (`!(r:A ring) (s:V->bool) p. ring_unit (powser_ring r s) p <=> @@ -20423,11 +20462,13 @@ let INTEGRAL_DOMAIN_RULE = GEN_REWRITE_CONV REDEPTH_CONV [RIGHT_AND_EXISTS_THM; LEFT_AND_EXISTS_THM] THENC GEN_REWRITE_CONV TOP_DEPTH_CONV [GSYM DISJ_ASSOC] THENC - GEN_REWRITE_CONV TOP_DEPTH_CONV [GSYM CONJ_ASSOC] in + GEN_REWRITE_CONV TOP_DEPTH_CONV [GSYM CONJ_ASSOC] + and true_tm = `T` in let INTEGRAL_DOMAIN_RULE_BASIC tm = let avs,bod = strip_forall tm in let th1 = init_conv bod in let tm' = rand(concl th1) in + if tm' = true_tm then EQT_ELIM th1 else let avs',bod' = strip_forall tm' in let th2 = end_itlist CONJ (map INTEGRAL_DOMAIN_CORE (conjuncts bod')) in let th3 = EQ_MP (SYM th1) (GENL avs' th2) in diff --git a/int.ml b/int.ml index 922de631..caf1d596 100755 --- a/int.ml +++ b/int.ml @@ -2218,7 +2218,8 @@ let INT_ARITH = let is_div = is_binop div_tm and is_rem = is_binop rem_tm in fun tm -> is_div tm || is_rem tm in let rec conv tm = - try let t = find_term (fun t -> is_divrem t && free_in t tm) tm in + try let t = hd(sort free_in + (find_terms (fun t -> is_divrem t && free_in t tm) tm)) in let x = lhand t and y = rand t in let dtm = mk_comb(mk_comb(div_tm,x),y) and rtm = mk_comb(mk_comb(rem_tm,x),y) in @@ -2230,7 +2231,7 @@ let INT_ARITH = (funpow 2 BINDER_CONV(RAND_CONV BETA2_CONV))) th1 in let th3 = CONV_RULE(RAND_CONV (funpow 2 BINDER_CONV INT_REDUCE_CONV)) th2 in - CONV_RULE(RAND_CONV(RAND_CONV conv)) th3 + CONV_RULE(RAND_CONV(BINDER_CONV(BINDER_CONV(RAND_CONV conv)))) th3 with Failure _ -> REFL tm in let rec topconv tm = if is_forall tm || is_exists tm then BINDER_CONV topconv tm