(* ========================================================================= *) (* Naive quantifier elimination for complex numbers. *) (* ========================================================================= *) needs "Complex/fundamental.ml";; (* ------------------------------------------------------------------------- *) (* Useful lemma I should have proved ages ago. *) (* ------------------------------------------------------------------------- *) (* ------------------------------------------------------------------------- *) (* It would be nicer to prove this without using algebraic closure... *) (* ------------------------------------------------------------------------- *) (* ------------------------------------------------------------------------- *) (* Arithmetic operations on multivariate polynomials. *) (* ------------------------------------------------------------------------- *) let MPOLY_BASE_CONV = let MPOLY_NORM_CONV = let MPOLY_ADD_CONV,MPOLY_TADD_CONV = let add_conv0 = GEN_REWRITE_CONV I (butlast (CONJUNCTS POLY_ADD_CLAUSES)) and add_conv1 = GEN_REWRITE_CONV I [last (CONJUNCTS POLY_ADD_CLAUSES)] and add_conv = REWR_CONV(GSYM POLY_ADD) in let rec MPOLY_ADD_CONV avs tm = if avs = [] then COMPLEX_RAT_ADD_CONV tm else (add_conv THENC LAND_CONV(MPOLY_TADD_CONV avs) THENC MPOLY_NORM_CONV (tl avs)) tm and MPOLY_TADD_CONV avs tm = (add_conv0 ORELSEC (add_conv1 THENC LAND_CONV (MPOLY_ADD_CONV (tl avs)) THENC RAND_CONV (MPOLY_TADD_CONV avs))) tm in MPOLY_ADD_CONV,MPOLY_TADD_CONV;; let MPOLY_CMUL_CONV,MPOLY_TCMUL_CONV,MPOLY_MUL_CONV,MPOLY_TMUL_CONV = let cmul_conv0 = GEN_REWRITE_CONV I [CONJUNCT1 poly_cmul] and cmul_conv1 = GEN_REWRITE_CONV I [CONJUNCT2 poly_cmul] and cmul_conv = REWR_CONV(GSYM POLY_CMUL) and mul_conv0 = GEN_REWRITE_CONV I [CONJUNCT1 POLY_MUL_CLAUSES] and mul_conv1 = GEN_REWRITE_CONV I [CONJUNCT1(CONJUNCT2 POLY_MUL_CLAUSES)] and mul_conv2 = GEN_REWRITE_CONV I [CONJUNCT2(CONJUNCT2 POLY_MUL_CLAUSES)] and mul_conv = REWR_CONV(GSYM POLY_MUL) in let rec MPOLY_CMUL_CONV avs tm = (cmul_conv THENC LAND_CONV(MPOLY_TCMUL_CONV avs)) tm and MPOLY_TCMUL_CONV avs tm = (cmul_conv0 ORELSEC (cmul_conv1 THENC LAND_CONV (MPOLY_MUL_CONV (tl avs)) THENC RAND_CONV (MPOLY_TCMUL_CONV avs))) tm and MPOLY_MUL_CONV avs tm = if avs = [] then COMPLEX_RAT_MUL_CONV tm else (mul_conv THENC LAND_CONV(MPOLY_TMUL_CONV avs)) tm and MPOLY_TMUL_CONV avs tm = (mul_conv0 ORELSEC (mul_conv1 THENC MPOLY_TCMUL_CONV avs) ORELSEC (mul_conv2 THENC COMB2_CONV (RAND_CONV(MPOLY_TCMUL_CONV avs)) (COMB2_CONV (RAND_CONV(MPOLY_BASE_CONV (tl avs))) (MPOLY_TMUL_CONV avs)) THENC MPOLY_TADD_CONV avs)) tm in MPOLY_CMUL_CONV,MPOLY_TCMUL_CONV,MPOLY_MUL_CONV,MPOLY_TMUL_CONV;; let MPOLY_SUB_CONV = let MPOLY_POW_CONV = let cnv_0 = GEN_REWRITE_CONV I [CONJUNCT1 complex_pow] and cnv_1 = GEN_REWRITE_CONV I [CONJUNCT2 complex_pow] in let rec MPOLY_POW_CONV avs tm = try (cnv_0 THENC MPOLY_BASE_CONV avs) tm with Failure _ -> (RAND_CONV num_CONV THENC cnv_1 THENC (RAND_CONV (MPOLY_POW_CONV avs)) THENC MPOLY_MUL_CONV avs) tm in MPOLY_POW_CONV;; (* ------------------------------------------------------------------------- *) (* Recursive conversion to polynomial form. *) (* ------------------------------------------------------------------------- *) let POLYNATE_CONV = let ELIM_SUB_CONV = REWR_CONV (SIMPLE_COMPLEX_ARITH `x - y = x + Cx(--(&1)) * y`) and ELIM_NEG_CONV = REWR_CONV (SIMPLE_COMPLEX_ARITH `--x = Cx(--(&1)) * x`) and ELIM_POW_0_CONV = GEN_REWRITE_CONV I [CONJUNCT1 complex_pow] and ELIM_POW_1_CONV = RAND_CONV num_CONV THENC GEN_REWRITE_CONV I [CONJUNCT2 complex_pow] in let rec ELIM_POW_CONV tm = (ELIM_POW_0_CONV ORELSEC (ELIM_POW_1_CONV THENC RAND_CONV ELIM_POW_CONV)) tm in let polynet = itlist (uncurry net_of_conv) [`x pow n`,(fun cnv avs -> LAND_CONV (cnv avs) THENC MPOLY_POW_CONV avs); `x * y`,(fun cnv avs -> BINOP_CONV (cnv avs) THENC MPOLY_MUL_CONV avs); `x + y`,(fun cnv avs -> BINOP_CONV (cnv avs) THENC MPOLY_ADD_CONV avs); `x - y`,(fun cnv avs -> BINOP_CONV (cnv avs) THENC MPOLY_SUB_CONV avs); `--x`,(fun cnv avs -> ELIM_NEG_CONV THENC (cnv avs))] empty_net in let rec POLYNATE_CONV avs tm = try snd(hd(lookup tm polynet)) POLYNATE_CONV avs tm with Failure _ -> MPOLY_BASE_CONV avs tm in POLYNATE_CONV;; (* ------------------------------------------------------------------------- *) (* Cancellation conversion. *) (* ------------------------------------------------------------------------- *) let POLY_PAD_RULE = let POLY_CANCEL_EQ_CONV =let RESOLVE_EQ_RAW = let RESOLVE_EQ asm tm = let th = RESOLVE_EQ_RAW asm tm in try EQF_ELIM th with Failure _ -> EQT_ELIM th;; let RESOLVE_EQ_THEN = let MATCH_pth = MATCH_MP (TAUT `(p ==> (q <=> q1)) /\ (~p ==> (q <=> q2)) ==> (q <=> (p /\ q1 \/ ~p /\ q2))`) in fun asm tm yfn nfn -> try let th = RESOLVE_EQ asm tm in if is_neg(concl th) then nfn (th::asm) th else yfn (th::asm) th with Failure _ -> let tm' = mk_neg tm in let yth = DISCH tm (yfn (ASSUME tm :: asm) (ASSUME tm)) and nth = DISCH tm' (nfn (ASSUME tm' :: asm) (ASSUME tm')) in MATCH_pth (CONJ yth nth);; let POLY_CANCEL_ENE_CONV avs n ath eth tm = if is_neg tm then RAND_CONV(POLY_CANCEL_EQ_CONV avs n ath eth) tm else POLY_CANCEL_EQ_CONV avs n ath eth tm;; let RESOLVE_NE = let NEGATE_NEGATE_RULE = GEN_REWRITE_RULE I [TAUT `p <=> (~p <=> F)`] in fun asm tm -> try let th = RESOLVE_EQ asm (rand tm) in if is_neg(concl th) then EQT_INTRO th else NEGATE_NEGATE_RULE th with Failure _ -> REFL tm;; (* ------------------------------------------------------------------------- *) (* Conversion for division of polynomials. *) (* ------------------------------------------------------------------------- *) let LAST_CONV = GEN_REWRITE_CONV REPEATC [LAST_CLAUSES];; let LENGTH_CONV = let cnv_0 = GEN_REWRITE_CONV I [CONJUNCT1 LENGTH] and cnv_1 = GEN_REWRITE_CONV I [CONJUNCT2 LENGTH] in let rec LENGTH_CONV tm = try cnv_0 tm with Failure _ -> (cnv_1 THENC RAND_CONV LENGTH_CONV THENC NUM_SUC_CONV) tm in LENGTH_CONV;; let EXPAND_EX_BETA_CONV = let POLY_DIVIDES_PAD_RULE = let POLY_DIVIDES_PAD_CONST_RULE = let EXPAND_EX_BETA_RESOLVE_CONV asm tm = let th1 = EXPAND_EX_BETA_CONV tm in let djs = disjuncts(rand(concl th1)) in let th2 = end_itlist MK_DISJ (map (RESOLVE_NE asm) djs) in TRANS th1 th2;; let POLY_DIVIDES_CONV = (* ------------------------------------------------------------------------- *) (* Apply basic Nullstellensatz principle. *) (* ------------------------------------------------------------------------- *) let BASIC_QUELIM_CONV = (* ------------------------------------------------------------------------- *) (* Put into canonical form by multiplying inequalities. *) (* ------------------------------------------------------------------------- *) let POLY_NE_MULT_CONV = let CORE_QUELIM_CONV = let CONJ_AC_RULE = AC CONJ_ACI in let CORE_QUELIM_CONV asm avs tm = let ev,bod = dest_exists tm in let cjs = conjuncts bod in let eqs,neqs = partition is_eq cjs in if eqs = [] then let th1 = MK_EXISTS ev (POLY_NE_MULT_CONV avs bod) in TRANS th1 (BASIC_QUELIM_CONV asm avs (rand(concl th1))) else if length eqs > 1 then failwith "CORE_QUELIM_CONV: Sanity failure" else if neqs = [] then BASIC_QUELIM_CONV asm avs tm else let tm1 = mk_conj(hd eqs,list_mk_conj neqs) in let th1 = CONJ_AC_RULE(mk_eq(bod,tm1)) in let th2 = CONV_RULE(funpow 2 RAND_CONV(POLY_NE_MULT_CONV avs)) th1 in let th3 = MK_EXISTS ev th2 in TRANS th3 (BASIC_QUELIM_CONV asm avs (rand(concl th3))) in CORE_QUELIM_CONV;; (* ------------------------------------------------------------------------- *) (* Main elimination coversion (for a single quantifier). *) (* ------------------------------------------------------------------------- *) let RESOLVE_EQ_NE = let DNE_RULE = GEN_REWRITE_RULE I [TAUT `((p <=> T) <=> (~p <=> F)) /\ ((p <=> F) <=> (~p <=> T))`] in fun asm tm -> if is_neg tm then DNE_RULE(RESOLVE_EQ_RAW asm (rand tm)) else RESOLVE_EQ_RAW asm tm;; let COMPLEX_QUELIM_CONV = (* ------------------------------------------------------------------------- *) (* NNF conversion doing "conditionals" ~(p /\ q \/ ~p /\ r) intelligently. *) (* ------------------------------------------------------------------------- *) let NNF_COND_CONV =let pth_1 =prove (`(p = Cx(&0)) /\ ~(a = Cx(&0)) ==> !q b. (q = Cx(&0)) <=> (a * q - b * p = Cx(&0))`,(* ------------------------------------------------------------------------- *) (* Overall procedure for multiple quantifiers in any first order formula. *) (* ------------------------------------------------------------------------- *) let FULL_COMPLEX_QUELIM_CONV = let ELIM_FORALL_CONV =let NOT_EXISTS_UNIQUE_THM =prove (`~(?!x. P x) <=> (!x. ~P x) \/ ?x x'. P x /\ P x' /\ ~(x = x')`,