Rqe/inferisign.ml

   1 exception Isign of (thm * ((term * thm) list));;
   2
   3 (* ---------------------------------------------------------------------- *)
   4 (*  Opt                                                                   *)
   5 (* ---------------------------------------------------------------------- *)
   6
   7 let get_mp =
   8   let unknown = `Unknown` in
   9   let pos = `Pos` in
  10   let zero = `Zero` in
  11   let neg = `Neg` in
  12     fun upper_sign lower_sign deriv_sign ->
  13         (* Pos Pos *)
  14         if upper_sign = pos &&
  15            lower_sign = pos &&
  16            deriv_sign = pos then INFERISIGN_POS_POS_POS
  17         else if upper_sign = pos &&
  18            lower_sign = pos &&
  19            deriv_sign = neg then INFERISIGN_POS_POS_NEG
  20         (* Pos Neg *)
  21         else if upper_sign = pos &&
  22            lower_sign = neg &&
  23            deriv_sign = pos then INFERISIGN_POS_NEG_POS
  24         else if upper_sign = pos &&
  25            lower_sign = neg &&
  26            deriv_sign = neg then INFERISIGN_POS_NEG_NEG
  27         (* Pos Zero *)
  28         else if upper_sign = pos &&
  29            lower_sign = zero &&
  30            deriv_sign = pos then INFERISIGN_POS_ZERO_POS
  31         else if upper_sign = pos &&
  32            lower_sign = zero &&
  33            deriv_sign = neg then INFERISIGN_POS_ZERO_NEG
  34         (* Neg Pos *)
  35         else if upper_sign = neg &&
  36            lower_sign = pos &&
  37            deriv_sign = pos then INFERISIGN_NEG_POS_POS
  38         else if upper_sign = neg &&
  39            lower_sign = pos &&
  40            deriv_sign = neg then INFERISIGN_NEG_POS_NEG
  41         (* Neg Neg *)
  42         else if upper_sign = neg &&
  43            lower_sign = neg &&
  44            deriv_sign = pos then INFERISIGN_NEG_NEG_POS
  45         else if upper_sign = neg &&
  46            lower_sign = neg &&
  47            deriv_sign = neg then INFERISIGN_NEG_NEG_NEG
  48         (* Neg Zero *)
  49         else if upper_sign = neg &&
  50            lower_sign = zero &&
  51            deriv_sign = pos then INFERISIGN_NEG_ZERO_POS
  52         else if upper_sign = neg &&
  53            lower_sign = zero &&
  54            deriv_sign = neg then INFERISIGN_NEG_ZERO_NEG
  55         (* Zero Pos *)
  56         else if upper_sign = zero &&
  57            lower_sign = pos &&
  58            deriv_sign = pos then INFERISIGN_ZERO_POS_POS
  59         else if upper_sign = zero &&
  60            lower_sign = pos &&
  61            deriv_sign = neg then INFERISIGN_ZERO_POS_NEG
  62         (* Zero Neg *)
  63         else if upper_sign = zero &&
  64            lower_sign = neg &&
  65            deriv_sign = pos then INFERISIGN_ZERO_NEG_POS
  66         else if upper_sign = zero &&
  67            lower_sign = neg &&
  68            deriv_sign = neg then INFERISIGN_ZERO_NEG_NEG
  69         (* Zero Zero *)
  70         else if upper_sign = zero &&
  71            lower_sign = zero &&
  72            deriv_sign = pos then INFERISIGN_ZERO_ZERO_POS
  73         else if upper_sign = zero &&
  74            lower_sign = zero &&
  75            deriv_sign = neg then INFERISIGN_ZERO_ZERO_NEG
  76         else failwith "bad signs in thm";;
  77
  78
  79 let tvars,tdiff,tmat,tex = ref [],ref TRUTH,ref TRUTH,ref [];;
  80 (*
  81   let vars,diff_thm,mat_thm,ex_thms = !tvars,!tdiff,!tmat,!tex
  82 INFERISIGN vars diff_thm mat_thm ex_thms
  83
  84 let vars,diff_thm,mat_thm,ex_thms = vars, pdiff_thm, mat_thm''', ((v1,exthm1)::(v2,exthm2)::ex_thms)
  85 *)
  86
  87 let rec INFERISIGN =
  88   let real_app = `APPEND:real list -> real list -> real list` in
  89   let sign_app = `APPEND:(sign list) list -> (sign list) list -> (sign list) list` in
  90   let real_len = `LENGTH:real list -> num` in
  91   let sign_len = `LENGTH:(sign list) list -> num` in
  92   let unknown = `Unknown` in
  93   let pos = `Pos` in
  94   let zero = `Zero` in
  95   let neg = `Neg` in
  96   let num_mul = `( * ):num -> num -> num` in
  97   let num_add = `( + ):num -> num -> num` in
  98   let real_ty = `:real` in
  99   let one = `1` in
 100   let two = `2` in
 101   let f = `F` in
 102   let imat = `interpmat` in
 103   let sl_ty = `:sign list` in
 104   fun vars diff_thm mat_thm ex_thms ->
 105     try
 106       tvars := vars;
 107       tdiff := diff_thm;
 108       tmat := mat_thm;
 109       tex := ex_thms;
 110       let pts,ps,sgns = dest_interpmat (concl mat_thm) in
 111       let pts' = dest_list pts in
 112       if pts' = [] then mat_thm,ex_thms else
 113       let sgns' = dest_list sgns in
 114       let sgnl = map dest_list sgns' in
 115       let i = get_index (fun x -> hd x = unknown) sgnl in
 116       if i mod 2 = 1 then failwith "bad shifted matrix" else
 117       let p::p'::_ = dest_list ps in
 118       let p_thm = ABS (hd vars) (POLY_ENLIST_CONV vars (snd(dest_abs p))) in
 119       let p'_thm = ONCE_REWRITE_RULE[GSYM diff_thm] (ABS (hd vars) (POLY_ENLIST_CONV vars (snd(dest_abs p')))) in
 120       let pts1,qts1 = chop_list (i / 2 - 1) pts' in
 121       let ps_thm = REWRITE_CONV[p_thm;p'_thm] ps in
 122       let pts2 = mk_list(pts1,real_ty) in
 123       let pts3 = mk_comb(mk_comb(real_app,pts2),mk_list(qts1,real_ty)) in
 124       let pts_thm = prove(mk_eq(pts,pts3),REWRITE_TAC[APPEND]) in
 125       let sgns1,rgns1 = chop_list (i - 1) sgns' in
 126       let sgns2 = mk_list(sgns1,sl_ty) in
 127       let sgns3 = mk_comb(mk_comb(sign_app,sgns2),mk_list(rgns1,sl_ty)) in
 128       let sgns_thm = prove(mk_eq(sgns,sgns3),REWRITE_TAC[APPEND]) in
 129       let len1 = mk_comb(sign_len,sgns2) in
 130       let len2 = mk_binop num_add (mk_binop num_mul two (mk_comb(real_len,pts2))) one in
 131       let len_thm = prove(mk_eq(len1,len2),REWRITE_TAC[LENGTH] THEN ARITH_TAC) in
 132       let mat_thm1 = MK_COMB(MK_COMB((AP_TERM imat pts_thm), ps_thm),sgns_thm) in
 133       let mat_thm2 = EQ_MP mat_thm1 mat_thm in
 134       let upper_sign = hd (ith (i - 1) sgnl) in
 135       let lower_sign = hd (ith (i + 1) sgnl) in
 136       let deriv_sign = hd (tl (ith i sgnl)) in
 137       let mp_thm = get_mp upper_sign lower_sign deriv_sign in
 138       let mat_thm3 = MATCH_MP (MATCH_MP mp_thm mat_thm2) len_thm in
 139       let mat_thm4 = REWRITE_RULE[GSYM p_thm;GSYM p'_thm;APPEND] mat_thm3 in
 140       let c = concl mat_thm4 in
 141       if c = f then raise (Isign (mat_thm4,ex_thms)) else
 142       if not (is_exists c) then
 143         INFERISIGN vars diff_thm mat_thm4 ex_thms else
 144       let x,bod = dest_exists c in
 145       let x' = new_var real_ty in
 146       let assume_thm = ASSUME (subst [x',x] bod) in
 147         INFERISIGN vars diff_thm assume_thm ((x',mat_thm4)::ex_thms)
 148   with
 149     Failure "get_index" -> mat_thm,ex_thms
 150   | Failure x -> failwith ("INFERISIGN: " ^ x);;
 151
 152 (*
 153 let vars,diff_thm,mat_thm,ex_thms =  vars,pdiff_thm, mat_thm''',[]
 154
 155 let mat_thm = ASSUME ` interpmat [x_25; x1; x2; x4; x5; x_26]
 156      [\x. &1 + x * (&1 + x * (&1 + x * &1)); \x. &1 + x * (&2 + x * &3);
 157      \x. &2 + x * (-- &3 + x * &1); \x. -- &4 + x * (&0 + x * &1)]
 158      [[Neg; Pos; Pos; Pos];
 159       [Neg; Pos; Pos; Pos];
 160       [Unknown; Pos; Pos; Pos];
 161       [Pos; Pos; Pos; Zero];
 162       [Unknown; Neg; Pos; Neg];
 163       [Unknown; Neg; Neg; Neg];
 164       [Unknown; Neg; Pos; Neg];
 165       [Pos; Zero; Zero; Neg];
 166       [Unknown; Pos; Neg; Neg];
 167       [Pos; Pos; Zero; Zero];
 168       [Unknown; Pos; Pos; Pos];
 169       [Pos; Pos; Pos; Pos];
 170       [Pos; Pos; Pos; Pos]]`
 171
 172 *)
 173
 174
 175 (* ---------------------------------------------------------------------- *)
 176 (*  Timing                                                                *)
 177 (* ---------------------------------------------------------------------- *)
 178
 179 let INFERISIGN vars diff_thm mat_thm ex_thms =
 180   let start_time = Sys.time() in
 181   let res = INFERISIGN vars diff_thm mat_thm ex_thms in
 182     inferisign_timer +.= (Sys.time() -. start_time);
 183     res;;
 184
 185 (* {{{ Examples *)
 186
 187 (*
 188 let is_thms = isigns_thms'''
 189
 190 let vars,diff_thm,mat_thm =
 191 [`w:real`; `z:real`; `y:real`; `x:real`],
 192 ASSUME `poly_diff [&0 + y * (&0 + x * &1); &0 + z * -- &1] = [&0 + z * -- &1]`,
 193 ASSUME `interpmat [x_178; x_179]
 194      [\w. (&0 + y * (&0 + x * &1)) + w * (&0 + z * -- &1); \w. &0 + z * -- &1]
 195      [[Pos; Neg]; [Pos; Neg]; [Unknown; Neg]; [Neg; Neg]; [Neg; Neg]]`
 196
 197 INFERISIGN vars pdiff_thm mat_thm
 198
 199 let diff
 200 let vars,diff_thm,mat_thm =
 201
 202
 203
 204 let vars,diff_thm,mat_thm =
 205 [`x:real`],
 206 ASSUME `poly_diff [&0; &2; &0; &4] = [&2; &0; &12]`,
 207 ASSUME `interpmat [x_79; x_68; x_80]
 208         [\x. &0 + x * (&2 + x * (&0 + x * &4)); \x. &2 + x * (&0 + x * &12);
 209         \x. &4 + x * (&0 + x * &2)]
 210         [[Neg; Pos; Pos]; [Neg; Pos; Pos]; [Unknown; Pos; Pos]; [Unknown; Pos; Pos]; [Unknown; Pos; Pos]; [Pos; Pos; Pos]; [Pos; Pos; Pos]]`
 211
 212
 213
 214 let mat_thm = mat_thm'''
 215 let diff_thm = pdiff_thm
 216 INFERISIGN vars pdiff_thm mat_thm'''
 217
 218 let diff_thm = POLY_DIFF_CONV `poly_diff [&1; &1; &1; &1]`;;
 219
 220 let vars = [`x:real`]
 221
 222 let mat_thm = ASSUME
 223   `interpmat
 224      [xminf; x1; x4; x5; xinf]
 225      [\x. &1 + x * (&1 + x * (&1 + x * &1)); \x. &1 + x * (&2 + x * &3); \x. &2 + x * (-- &3 + x * &1); \x. -- &4 + x * (&0 + x * &1)]
 226      [[Neg; Pos; Pos; Pos];
 227       [Neg; Pos; Pos; Pos];
 228       [Unknown; Pos; Pos; Pos];
 229       [Neg; Pos; Pos; Zero];
 230       [Unknown; Pos; Pos; Neg];
 231       [Pos; Pos; Zero; Neg];
 232       [Unknown; Pos; Neg; Neg];
 233       [Pos; Pos; Zero; Zero];
 234       [Unknown; Pos; Pos; Pos];
 235       [Pos; Pos; Pos; Pos];
 236       [Pos; Pos; Pos; Pos]]`;;
 237
 238 let mat_thm1,_ = INFERISIGN vars diff_thm mat_thm []
 239
 240 *)
 241 (* }}} *)