Rqe/inferpsign.ml

   1 (* ====================================================================== *)
   2 (*  INFERPSIGN                                                            *)
   3 (* ====================================================================== *)
   4
   5 (* ------------------------------------------------------------------------- *)
   6 (* Infer sign of p(x) at points from corresponding qi(x) with pi(x) = 0      *)
   7 (* ------------------------------------------------------------------------- *)
   8
   9 (* ---------------------------------------------------------------------- *)
  10 (*  INFERPSIGN                                                            *)
  11 (* ---------------------------------------------------------------------- *)
  12
  13
  14 let isign_eq_zero thm =
  15   let __,_,sign = dest_interpsign thm in
  16     sign = szero_tm;;
  17
  18 let isign_lt_zero thm =
  19   let __,_,sign = dest_interpsign thm in
  20     sign = sneg_tm;;
  21
  22 let isign_gt_zero thm =
  23   let __,_,sign = dest_interpsign thm in
  24     sign = spos_tm;;
  25
  26 (*
  27 let p_thm,q_thm = ith 1 split_thms
  28 *)
  29 let inferpsign_row vars sgns p_thm q_thm div_thms =
  30   let pthms = map (BETA_RULE o (PURE_REWRITE_RULE[interpsigns])) (interpsigns_thms2 p_thm) in
  31   let qthms = map (BETA_RULE o (PURE_REWRITE_RULE[interpsigns])) (interpsigns_thms2 q_thm) in
  32   let _,set,_ = dest_interpsigns p_thm in
  33   if can (get_index isign_eq_zero) pthms then (* there's a zero *)
  34     let ind = get_index isign_eq_zero pthms in
  35     let pthm = ith ind pthms in
  36     let qthm = ith ind qthms in
  37     let div_thm = ith ind div_thms in
  38     let div_thm' = GEN (hd vars) div_thm in
  39     let aks,pqr = dest_eq (concl div_thm) in
  40     let ak,s = dest_mult aks in
  41     let a,k = dest_pow ak in
  42     let pq,r = dest_plus pqr in
  43     let p,q = dest_mult pq in
  44     let parity_thm = PARITY_CONV k in
  45     let evenp = fst(dest_comb (concl parity_thm)) = even_tm in
  46     let sign_thm = FINDSIGN vars sgns a in
  47     let op,_,_ = get_binop (concl sign_thm) in
  48     if evenp then
  49       let nz_thm =
  50         if op = rlt then MATCH_MP ips_lt_nz_thm sign_thm
  51         else if op = rgt then MATCH_MP ips_gt_nz_thm sign_thm
  52         else if op = rneq then sign_thm
  53         else failwith "inferpsign: 0" in
  54       let imp_thms =
  55         CONJUNCTS(ISPEC set (MATCH_MPL[EVEN_DIV_LEM;div_thm';nz_thm;parity_thm])) in
  56       let _,_,qsign = dest_interpsign qthm in
  57       let mp_thm =
  58         if qsign = sneg_tm then ith 0 imp_thms
  59         else if qsign = spos_tm then ith 1 imp_thms
  60         else if qsign = szero_tm then ith 2 imp_thms
  61         else failwith "inferpsign: 1" in
  62       let final_thm = MATCH_MPL[mp_thm;pthm;qthm] in
  63         mk_interpsigns (final_thm::pthms)
  64     else (* k is odd *)
  65       if op = rgt then (* a > &0 *)
  66         let imp_thms =
  67           CONJUNCTS(ISPEC set (MATCH_MPL[GT_DIV_LEM;div_thm';sign_thm])) in
  68         let _,_,qsign = dest_interpsign qthm in
  69         let mp_thm =
  70           if qsign = sneg_tm then ith 0 imp_thms
  71           else if qsign = spos_tm then ith 1 imp_thms
  72           else if qsign = szero_tm then ith 2 imp_thms
  73           else failwith "inferpsign: 1" in
  74         let final_thm = MATCH_MPL[mp_thm;pthm;qthm] in
  75           mk_interpsigns (final_thm::pthms)
  76       else
  77         failwith "inferpsign: shouldn`t reach this point with an odd power and negative sign!  See PDIVIDES and return the correct div_thm"
  78   else (* no zero *)
  79     let p = snd(dest_mult (lhs(concl (hd div_thms)))) in
  80     let p1 = mk_abs(hd vars,p) in
  81     let pthm = ISPECL [set;p1] unknown_thm in
  82       mk_interpsigns (pthm::pthms);;
  83
  84 (* {{{ Doc *)
  85 (*
  86 split_interpsigns
  87    |- interpsigns
  88      [p0; p1; p2; q0; q1; q2]
  89      (\x. x < x1)
  90      [Pos; Pos; Pos; Neg; Neg; Neg]
  91
  92   -->
  93
  94 (
  95    |- interpsigns
  96      [p0; p1; p2]
  97      (\x. x < x1)
  98      [Pos; Pos; Pos]
  99 ,
 100    |- interpsigns
 101      [q0; q1; q2]
 102      (\x. x < x1)
 103      [ Neg; Neg; Neg]
 104 )
 105 *)
 106 (* }}} *)
 107 let split_interpsigns thm =
 108   let thms = interpsigns_thms2 thm in
 109   let n = length thms / 2 in
 110   let l,r = chop_list n thms in
 111     (mk_interpsigns l,mk_interpsigns r);;
 112
 113 let INFERPSIGN vars sgns mat_thm div_thms =
 114   let pts,pols,signs = dest_interpmat (concl mat_thm) in
 115   let n = length (dest_list pols) / 2 in
 116   let rol_thm,sgn_thm = interpmat_thms mat_thm in
 117   let part_thm = PARTITION_LINE_CONV (snd (dest_comb (concl rol_thm))) in
 118   let conj_thms = CONJUNCTS(REWRITE_RULE[ALL2;part_thm] sgn_thm) in
 119   let split_thms = map split_interpsigns conj_thms in
 120   let conj_thms' = map (fun (x,y) -> inferpsign_row vars sgns x y div_thms) split_thms in
 121   let all_thm = mk_all2_interpsigns part_thm conj_thms' in
 122   let mat_thm' = mk_interpmat_thm rol_thm all_thm in
 123     mat_thm';;
 124
 125 (* ---------------------------------------------------------------------- *)
 126 (*  Opt                                                                   *)
 127 (* ---------------------------------------------------------------------- *)
 128
 129 let MK_REP =
 130   let rep_tm = `REPLICATE:num -> sign -> sign list` in
 131   let len_tm = `LENGTH:real list -> num` in
 132   let one = `1` in
 133   let two = `2` in
 134   let unknown = `Unknown` in
 135   fun pts ->
 136     let num = mk_binop np (mk_binop nm two (mk_comb(len_tm,pts))) one in
 137     let len = length (dest_list pts) in
 138     let num2 = MK_SUC (2 * len + 1) in
 139     let lthm = ARITH_SIMP_CONV[LENGTH] num in
 140     let lthm2 = TRANS lthm num2 in
 141     let lthm3 = AP_THM (AP_TERM rep_tm lthm2) unknown in
 142       REWRITE_RULE[REPLICATE] lthm3;;
 143
 144 let INSERT_UNKNOWN_COL =
 145   fun mat_thm p ->
 146     let pts,_,_ = dest_interpmat (concl mat_thm) in
 147     let rep_thm = MK_REP pts in
 148     let mat_thm' = MATCH_MP INFERPSIGN_MATINSERT_THM mat_thm in
 149     let mat_thm'' = PURE_REWRITE_RULE[MAP2;rep_thm] mat_thm' in
 150       ISPEC p mat_thm'';;
 151
 152 let REMOVE_QS =
 153   fun mat_thm ->
 154     let _,pols,_ = dest_interpmat (concl mat_thm) in
 155     let len = length (dest_list pols) in
 156     if not (len mod 2 = 1) then failwith "odd pols?" else
 157     let mat_thm' = funpow (len / 2) (MATCH_MP REMOVE_LAST) mat_thm in
 158       REWRITE_RULE[MAP;BUTLAST;NOT_CONS_NIL;TL;HD;] mat_thm';;
 159
 160 let SPLIT_LIST n l ty =
 161   let l' = dest_list l in
 162   let l1',l2' = chop_list n l' in
 163   let l1,l2 = (mk_list(l1',ty),mk_list(l2',ty)) in
 164   let app_tm = mk_const("APPEND",[ty,aty]) in
 165   let l3 = mk_comb(mk_comb(app_tm,l1),l2) in
 166     SYM(REWRITE_CONV[APPEND] l3);;
 167
 168 (*
 169 let thm = asign
 170 *)
 171
 172 let prove_nonzero thm =
 173   let op,_,_ = get_binop (concl thm) in
 174   if op = rgt then MATCH_MP ips_gt_nz_thm thm
 175   else if op = rlt then MATCH_MP ips_lt_nz_thm thm
 176   else if op = rneq then thm
 177   else failwith "prove_nonzero: bad op";;
 178
 179 (*
 180 let mat_thm = mat_thm'
 181 let ind = 7
 182 *)
 183
 184
 185 let INFERPT =
 186   let unknown = `Unknown` in
 187   let zero = `Zero` in
 188   let pos = `Pos` in
 189   let neg = `Neg` in
 190   let pow = `(pow)` in
 191   let even_tm = `(EVEN)` in
 192   let odd_tm = `(ODD)` in
 193   let rr_ty = `:real -> real` in
 194   let sl_ty = `:sign list` in
 195   let s_ty = `:sign` in
 196   let imat = `interpmat` in
 197   let rr_length = mk_const("LENGTH",[rr_ty,aty]) in
 198   let s_length = mk_const("LENGTH",[s_ty,aty]) in
 199   let sl_length = mk_const("LENGTH",[sl_ty,aty]) in
 200   let imat = `interpmat` in
 201   fun vars sgns mat_thm div_thms ind ->
 202     let pts,pols,signs = dest_interpmat (concl mat_thm) in
 203     let pols' = dest_list pols in
 204     let signsl = dest_list signs in
 205     let signs' = map dest_list signsl in
 206     let pols_len = length (hd signs') in
 207     let pols_len2 = pols_len / 2 in
 208     let pt_sgnl = ith ind signsl in
 209     let pt_sgns = ith ind signs' in
 210     let zind = index zero pt_sgns in
 211     if zind > pols_len2 then mat_thm else (* return if not a zero of a p, only a q *)
 212     let psgn = ith (pols_len2 + zind) pt_sgns in
 213     let div_thm = ith (zind - 1) div_thms in
 214     let a,n = dest_binop pow (fst (dest_binop rm (lhs (concl div_thm)))) in
 215     let asign = FINDSIGN vars sgns a in
 216     let op,_,_ = get_binop (concl asign) in
 217     let par_thm = PARITY_CONV n in
 218     let par = fst(dest_comb(concl par_thm)) in
 219     let mp_thm =
 220       (* note: by def of PDIVIDES, we can`t have
 221          negative sign and odd power at this point *)
 222       (* n is even *)
 223       if par = even_tm then
 224         if psgn = pos then INFERPSIGN_POS_EVEN
 225         else if psgn = neg then INFERPSIGN_NEG_EVEN
 226         else if psgn = zero then INFERPSIGN_ZERO_EVEN
 227         else failwith "INFERPT: bad sign"
 228       else (* n is odd *)
 229         if psgn = pos then INFERPSIGN_POS_ODD_POS
 230         else if psgn = neg then INFERPSIGN_NEG_ODD_POS
 231         else if psgn = zero then INFERPSIGN_ZERO_ODD_POS
 232         else failwith "INFERPT: bad sign" in
 233     (* pols *)
 234     let split_pols1 = SPLIT_LIST zind pols rr_ty in
 235     let _,l2 = chop_list zind pols' in
 236     let split_pols2 = SPLIT_LIST pols_len2 (mk_list(l2,rr_ty)) rr_ty in
 237     let s1,t1 = dest_comb (rhs (concl split_pols1)) in
 238     let split_pols_thm = TRANS split_pols1 (AP_TERM s1 split_pols2) in
 239     (* pt_sgns *)
 240     let split_sgns1 = SPLIT_LIST zind pt_sgnl s_ty in
 241     let _,l3 = chop_list zind pt_sgns in
 242     let split_sgns2 = SPLIT_LIST pols_len2 (mk_list(l3,s_ty)) s_ty in
 243     let s2,t2 = dest_comb (rhs (concl split_sgns1)) in
 244     let split_pt_sgns_thm = TRANS split_sgns1 (AP_TERM s2 split_sgns2) in
 245     (* sgns *)
 246     let split_signs = SPLIT_LIST ind signs sl_ty in
 247     let r1,r3 = dest_comb(rhs (concl split_signs)) in
 248     let tl_thm = HD_CONV (ONCE_REWRITE_CONV[split_pt_sgns_thm]) r3 in
 249     let r4,_ = dest_comb (rhs (concl split_signs)) in
 250     let split_sgns_thm = TRANS split_signs (AP_TERM r4 tl_thm) in
 251     (* imat *)
 252     let mat1 = mk_comb(imat,pts) in
 253     let mat_thm1 = AP_TERM mat1 split_pols_thm in
 254     let mat_thm2 = MK_COMB(mat_thm1,split_sgns_thm) in
 255     let mat_thm3 = EQ_MP mat_thm2 mat_thm in
 256     (* length thms *)
 257     (* LENGTH ps = LENGTH s1 *)
 258     let ps = mk_list(tl(dest_list(snd(dest_comb s1))),rr_ty) in
 259     let ps_len = REWRITE_CONV[LENGTH] (mk_comb(rr_length,ps)) in
 260     let ss = mk_list(tl(dest_list(snd(dest_comb s2))),s_ty) in
 261     let ss_len = REWRITE_CONV[LENGTH] (mk_comb(s_length,ss)) in
 262     let ps_s1_thm = TRANS ps_len (SYM ss_len) in
 263     (* LENGTH qs = LENGTH s2 *)
 264     let k1 = tl (fst (chop_list pols_len2 (dest_list t1))) in
 265     let qs = mk_list(k1,rr_ty) in
 266     let qs_len = REWRITE_CONV[LENGTH] (mk_comb(rr_length,qs)) in
 267     let k2 = tl (fst (chop_list pols_len2 (dest_list t2))) in
 268     let s2s = mk_list(k2,s_ty) in
 269     let s2s_len = REWRITE_CONV[LENGTH] (mk_comb(s_length,s2s)) in
 270     let qs_s2_thm = TRANS qs_len (SYM s2s_len) in
 271     (* ODD (LENGTH sgns) *)
 272     let _,hdsgns = dest_comb r1 in
 273     let odd_thm = EQT_ELIM(REWRITE_CONV[LENGTH;ODD;EVEN;NOT_ODD;NOT_EVEN] (mk_comb(odd_tm,mk_comb(sl_length,hdsgns)))) in
 274     (* a <> 0 *)
 275     let a_thm =
 276       if par = even_tm then prove_nonzero asign
 277       else asign in
 278     let div_thm' = GEN (hd vars) div_thm in
 279     (* main *)
 280     let thm1 = BETA_RULE(MATCH_MPL[mp_thm;mat_thm3;ps_s1_thm;qs_s2_thm;odd_thm]) in
 281     let thm2 =
 282       if par = even_tm then MATCH_MPL[thm1;div_thm';a_thm;par_thm]
 283       else MATCH_MPL[thm1;div_thm';a_thm] in
 284       REWRITE_RULE[APPEND] thm2;;
 285
 286 (*
 287 let mat_thm = mat_thm'
 288 *)
 289 let INFERPTS vars sgns mat_thm div_thms =
 290   let pts,_,_ = dest_interpmat (concl mat_thm) in
 291   let len = 2 * length (dest_list pts) in
 292   let ods = filter odd (1--len) in
 293     itlist (fun i matthm -> INFERPT vars sgns matthm div_thms i) ods mat_thm;;
 294
 295
 296 let itvars,itsgns,itmat,itdivs = ref [],ref [],ref TRUTH,ref [];;
 297 (*
 298 let vars,sgns,mat_thm,div_thms = !itvars,!itsgns,!itmat,!itdivs
 299 *)
 300
 301 let INFERPSIGN2 vars sgns mat_thm div_thms =
 302   itvars := vars;
 303   itsgns := sgns;
 304   itmat := mat_thm;
 305   itdivs := div_thms;
 306   let _,bod = dest_binop rm (lhs (concl (hd div_thms))) in
 307   let p = mk_abs(hd vars,bod) in
 308   let mat_thm' = INSERT_UNKNOWN_COL mat_thm p in
 309   let mat_thm'' = INFERPTS vars sgns mat_thm' div_thms in
 310     REMOVE_QS mat_thm'';;
 311
 312
 313 (* ---------------------------------------------------------------------- *)
 314 (*  Timing                                                                *)
 315 (* ---------------------------------------------------------------------- *)
 316
 317 let INFERPSIGN vars sgns mat_thm div_thms =
 318   let start_time = Sys.time() in
 319   let res = INFERPSIGN vars sgns mat_thm div_thms in
 320     inferpsign_timer +.= (Sys.time() -. start_time);
 321     res;;
 322
 323 (*
 324
 325 let l1 = PDIVIDE [`x:real`]
 326   `&1 + x * (&1 + x * (&1 + x * &1))` `&1 + x * (&2 + x * &3)`;;
 327 let l2 = PDIVIDE [`x:real`]
 328   `&1 + x * (&1 + x * (&1 + x * &1))` `&2 + x * (-- &3 + x * &1)`;;
 329 let l3 = PDIVIDE [`x:real`]
 330   `&1 + x * (&1 + x * (&1 + x * &1))` `-- &4 + x * (&0 + x * &1)`;;
 331
 332 let div_thms = [l1;l2;l3];;
 333 let vars = [`x:real`];;
 334 let sgns = [ARITH_RULE `&1 > &0`];;
 335
 336 let mat_thm = ASSUME
 337   `interpmat [x1; x2; x3; x4; x5]
 338      [\x. &1 + x * (&2 + x * &3); \x. &2 + x * (-- &3 + x * &1); \x. -- &4 + x * (&0 + x * &1);
 339       \x. &8 + x * &4; \x. -- &7 + x * &11; \x. &5 + x * &5]
 340       [[Pos; Pos; Pos; Neg; Neg; Neg];
 341       [Pos; Pos; Zero; Zero; Neg; Neg];
 342       [Pos; Pos; Neg; Pos; Neg; Neg];
 343       [Pos; Pos; Neg; Pos; Neg; Zero];
 344       [Pos; Pos; Neg; Pos; Neg; Pos];
 345       [Pos; Pos; Neg; Pos; Zero; Pos];
 346       [Pos; Pos; Neg; Pos; Pos; Pos];
 347       [Pos; Zero; Neg; Pos; Pos; Pos];
 348       [Pos; Neg; Neg; Pos; Pos; Pos];
 349       [Pos; Zero; Zero; Pos; Pos; Pos];
 350       [Pos; Pos; Pos; Pos; Pos; Pos]]` ;;
 351
 352 INFERPSIGN vars sgns mat_thm div_thms
 353
 354
 355
 356
 357
 358
 359
 360
 361 *)