Rqe/signs.ml

   1 (* ------------------------------------------------------------------------- *)
   2 (* Find sign of polynomial, using modulo-constant lookup and computation.    *)
   3 (* ------------------------------------------------------------------------- *)
   4
   5 let xterm_lt t1 t2 =
   6   try
   7     let n1,_ = dest_var t1 in
   8     let n2,_ = dest_var t2 in
   9     let i1 = String.sub n1 2 (String.length n1 - 2) in
  10     let i2 = String.sub n2 2 (String.length n2 - 2) in
  11     let x1 = int_of_string i1 in
  12     let x2 = int_of_string i2 in
  13       x1 < x2
  14   with _ -> failwith "xterm_lt: not an xvar?";;
  15
  16 (*
  17 String.sub n1 2 (String.length n1 - 2)
  18 substring
  19 let t1,t2 = `x_99:real`,`x_100:real`
  20 xterm_sort t1 t2
  21 t1 < t2
  22 *)
  23
  24
  25 let FINDSIGN =
  26   let p_tm = `p:real`
  27   and c_tm = `c:real`
  28   and fth = prove
  29    (`r (a * b * p) (&0) ==> (a * b = &1) ==> r p (&0)`,
  30     DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN
  31     ASM_REWRITE_TAC[REAL_MUL_ASSOC; REAL_MUL_LID]) in
  32   let rec FINDSIGN vars sgns p =
  33   try
  34     try SIGN_CONST p with Failure _ ->
  35     let mth = MONIC_CONV vars p in
  36     let p' = rand(concl mth) in
  37     let pth = find (fun th -> lhand(concl th) = p') sgns in
  38     let c = lhand(lhand(concl mth)) in
  39     let c' = term_of_rat(Int 1 // rat_of_term c) in
  40     let sth = SIGN_CONST c' in
  41     let rel_c = funpow 2 rator (concl sth) in
  42     let rel_p = funpow 2 rator (concl pth) in
  43     let th1 =
  44       if rel_p = req then if rel_c = rgt then pth_0g else pth_0l
  45       else if rel_p = rgt then if rel_c = rgt then pth_gg else pth_gl
  46       else if rel_p = rlt then if rel_c = rgt then pth_lg else pth_ll
  47       else if rel_p = rneq then if rel_c = rgt then pth_nzg else pth_nzl
  48       else failwith "FINDSIGN" in
  49     let th2 = MP (MP (INST [p',p_tm; c',c_tm] th1) pth) sth in
  50     let th3 = EQ_MP (LAND_CONV(RAND_CONV(K(SYM mth))) (concl th2)) th2 in
  51     let th4 = MATCH_MP fth th3 in
  52       MP th4 (EQT_ELIM(REAL_RAT_REDUCE_CONV(lhand(concl th4))))
  53   with Failure _ -> failwith "FINDSIGN" in
  54     FINDSIGN;;
  55
  56 (*
  57
  58 let vars = [`x:real`;`y:real`]
  59 let p =   `&7 + x * (&11 + x * (&10 + y * &7))`
  60
  61 let sgns = [ASSUME `&1 + x * (&11 / &7 + x * (&10 / &7 + y * &1)) < &0`]
  62 let sgns = [ASSUME `&1 + x * (&11 / &7 + x * (&10 / &7 + y * &1)) = &0`]
  63 let sgns = [ASSUME `&1 + x * (&11 / &7 + x * (&10 / &7 + y * &1)) > &0`]
  64 let sgns = [ASSUME `&1 + x * (&11 / &7 + x * (&10 / &7 + y * &1)) <> &0`]
  65
  66 FINDSIGN vars sgns p
  67 FINDSIGN vars sgns `-- &1`
  68
  69 *)
  70
  71
  72
  73 (*
  74 ASSERTSIGN [x,y] [] (|- &7 + x * (&11 + x * (&10 + y * -- &7)) < &0
  75
  76 -->
  77
  78 [-- &1 + x * (-- &11 / &7 + x * (-- &10 / &7 + y * &1)) > &0]
  79
  80
  81 ASSERTSIGN [x,y] [] (|- &7 + x * (&11 + x * (&10 + y * &7)) < &0
  82
  83 -->
  84
  85 [&1 + x * (&11 / &7 + x * (&10 / &7 + y * &1)) < &0]
  86
  87 *)
  88
  89
  90 let ASSERTSIGN vars sgns sgn_thm =
  91   let op,l,r = get_binop (concl sgn_thm) in
  92   let p_thm = MONIC_CONV vars l in
  93   let _,pl,pr = get_binop (concl p_thm) in
  94   let c,_ = dest_binop rm pl in
  95   let c_thm = SIGN_CONST c in
  96   let c_op,_,_ = get_binop (concl c_thm) in
  97   let sgn_thm' =
  98     if c_op = rlt & op = rlt then
  99       MATCH_MPL[signs_lem01;c_thm;sgn_thm;p_thm]
 100     else if c_op = rgt & op = rlt then
 101       MATCH_MPL[signs_lem02;c_thm;sgn_thm;p_thm]
 102     else if c_op = rlt & op = rgt then
 103       MATCH_MPL[signs_lem03;c_thm;sgn_thm;p_thm]
 104     else if c_op = rgt & op = rgt then
 105       MATCH_MPL[signs_lem04;c_thm;sgn_thm;p_thm]
 106     else if c_op = rlt & op = req then
 107       MATCH_MPL[signs_lem05;c_thm;sgn_thm;p_thm]
 108     else if c_op = rgt & op = req then
 109       MATCH_MPL[signs_lem06;c_thm;sgn_thm;p_thm]
 110     else if c_op = rlt & op = rneq then
 111       MATCH_MPL[signs_lem07;c_thm;sgn_thm;p_thm]
 112     else if c_op = rgt & op = rneq then
 113       MATCH_MPL[signs_lem08;c_thm;sgn_thm;p_thm]
 114     else failwith "ASSERTSIGN : 0" in
 115   try
 116     let sgn_thm'' = find (fun th -> lhand(concl th) = pr) sgns in
 117     let op1,l1,r1 = get_binop (concl sgn_thm') in
 118     let op2,l2,r2 = get_binop (concl sgn_thm'') in
 119       if (concl sgn_thm') = (concl sgn_thm'') then sgns
 120       else if op2 = rneq & (op1 = rlt or op1 = rgt) then sgn_thm'::snd (remove ((=) sgn_thm'') sgns)
 121       else failwith "ASSERTSIGN : 1"
 122   with Failure "find" -> sgn_thm'::sgns;;
 123
 124
 125
 126 (*
 127 let k0 = `&7 + x * (&11 + x * (&10 + y * -- &7))`
 128 MONIC_CONV vars k0
 129 let k1 = ASSUME `&7 + x * (&11 + x * (&10 + y * -- &7)) < &0`
 130 let k1 = ASSUME `&7 + x * (&11 + x * (&10 + y * &7)) < &0`
 131 let k1 = ASSUME `&7 + x * (&11 + x * (&10 + y * &7)) = &0`
 132 let k1 = ASSUME `&7 + x * (&11 + x * (&10 + y * &7)) <> &0`
 133 let sgn_thm = k1
 134
 135 ASSERTSIGN vars [ASSUME `&1 + x * (&11 / &7 + x * (&10 / &7 + y * &1)) <> &0`] k1
 136
 137 *)
 138
 139 (* ---------------------------------------------------------------------- *)
 140 (*  Case splitting                                                        *)
 141 (* ---------------------------------------------------------------------- *)
 142
 143
 144
 145 let SPLIT_ZERO vars sgns p cont_z cont_n ex_thms =
 146   try
 147     let sgn_thm = FINDSIGN vars sgns p in
 148     let op,l,r = get_binop (concl sgn_thm) in
 149       (if op = req then cont_z else cont_n) sgns ex_thms
 150   with Failure "FINDSIGN" ->
 151     let eq_tm = mk_eq(p,rzero) in
 152     let neq_tm = mk_neq(p,rzero) in
 153     let or_thm = ISPEC p signs_lem002 in
 154     (* zero *)
 155     let z_thm = cont_z (ASSERTSIGN vars sgns (ASSUME eq_tm)) ex_thms in
 156     let z_thm' = DISCH eq_tm z_thm in
 157     (* nonzero *)
 158     let nz_thm = cont_n (ASSERTSIGN vars sgns (ASSUME neq_tm)) ex_thms in
 159     let nz_thm' = DISCH neq_tm nz_thm in
 160     (* combine *)
 161     let ret = MATCH_MPL[signs_lem003;or_thm;z_thm';nz_thm'] in
 162     (* matching problem... must continue by hand *)
 163     let ldj,rdj = dest_disj (concl ret) in
 164     let lcj,rcj = dest_conj ldj in
 165     let a,_ = dest_binop req lcj in
 166     let p,p1 = dest_beq rcj in
 167     let _,rcj = dest_conj rdj in
 168     let p2 = rhs rcj in
 169     let pull_thm = ISPECL[a;p;p1;p2] PULL_CASES_THM in
 170     let ret' = MATCH_EQ_MP pull_thm ret in
 171       ret';;
 172
 173 (*
 174
 175 let ret = MATCH_MPL[lem3;or_thm]
 176 MATCH_MP ret z_thm'
 177
 178 ;nz_thm'] in
 179
 180 let vars,sgns,p,cont_z,cont_n,ex_thms = !sz_vars, !sz_sgns, !sz_p,!sz_cont_z, !sz_cont_n ,!sz_ex_thms
 181
 182
 183
 184     let ret = MATCH_MPL[lem3;or_thm;]
 185 let mp_thm = MATCH_MPL[lem3;or_thm;] in
 186 let vars, sgns, p,cont_z,  cont_n =  !sz_vars,!sz_sgns,!sz_p,!sz_cont_z,!sz_cont_n
 187
 188 let mp_thm = k1
 189
 190
 191 let t1 = ISPECL[`(?y. &0 + y * (&0 + x * &1) = &0)`;`T`;`T`;`&0 + x * &1`;`T`] t0
 192 MATCH_EQ_MP t1 k1
 193
 194
 195
 196 EQ_MP t1 k1
 197
 198 MATCH_EQ_MP PULL_CASES_THM k1
 199
 200 concl k1 = lhs (concl t1)
 201
 202 MATCH_EQ_MP PULL_CASES_THM k0
 203 let k0 = ASSUME `(&0 + x * &1 = &0) /\ ((?y. &0 + y * (&0 + x * &1) = &0) <=> T) \/
 204      &0 + x * &1 <> &0 /\
 205      (&0 + x * &1 > &0 /\ ((?x_1089. &0 + x_1089 * (&0 + x * &1) = &0) <=> T) \/
 206       &0 + x * &1 < &0 /\ ((?x_1084. &0 + x_1084 * (&0 + x * &1) = &0) <=> T))`;;
 207 let k1 = ASSUME `(&0 + x * &1 = &0) /\ ((?y. &0 + y * (&0 + x * &1) = &0) <=> T) \/
 208      &0 + x * &1 <> &0 /\
 209      (&0 + x * &1 > &0 /\ ((?y. &0 + y * (&0 + x * &1) = &0) <=> T) \/
 210       &0 + x * &1 < &0 /\ ((?y. &0 + y * (&0 + x * &1) = &0) <=> T))`;;
 211
 212 MATCH_MPL[PULL_CASES_THM;!sz_z_thm;!sz_nz_thm] in
 213
 214 let thm1 = ASSUME `(?x_32. (&0 + c * &1) + x_32 * ((&0 + b * &1) + x_32 * (&0 + a * &1)) = &0) <=> T`
 215 let thm2 =
 216 ASSUME `(&0 + a * ((&0 + b * (&0 + b * -- &1)) + a * (&0 + c * &4)) < &0 ==>
 217           ((?x. (&0 + c * &1) + x * ((&0 + b * &1) + x * (&0 + a * &1)) = &0) <=> F)) /\
 218         (&0 + a * ((&0 + b * (&0 + b * -- &1)) + a * (&0 + c * &4)) > &0 ==>
 219           ((?x_26. (&0 + c * &1) + x_26 * ((&0 + b * &1) + x_26 * (&0 + a * &1)) = &0) <=> T)) `
 220
 221
 222 MATCH_MPL
 223
 224 (* let PULL_CASES_THM = prove_by_refinement( *)
 225 (*   `((a = &0) ==> (p <=> p0)) ==> ((a <> &0) ==> (a < &0 ==> (p <=> p1)) /\ (a > &0 ==> (p <=> p2)))  *)
 226 (*     ==> (p <=> ((a = &0) /\ p0) \/ ((a < &0) /\ p1) \/ (a > &0 /\ p2))`, *)
 227 (* (\* {{{ Proof *\)
 228 [
 229   REWRITE_TAC[NEQ] THEN
 230   MAP_EVERY BOOL_CASES_TAC [`p:bool`; `p0:bool`; `p1:bool`; `p2:bool`] THEN
 231   ASM_REWRITE_TAC[NEQ] THEN TRY REAL_ARITH_TAC
 232 ]);;
 233 (\* }}} *\) *)
 234
 235 let PULL_CASES_THM = prove
 236  (`!a p p0 p1 p2.
 237 ((a = &0) /\ (p <=> p0) \/
 238    (a <> &0) /\ (a > &0 /\ (p <=> p1) \/ a < &0 /\ (p <=> p2))) <=>
 239    ((p <=> (a = &0) /\ p0 \/ a > &0 /\ p1 \/ a < &0 /\ p2))`,
 240 (* {{{ Proof *)
 241    REPEAT STRIP_TAC THEN  REWRITE_TAC[NEQ] THEN MAP_EVERY BOOL_CASES_TAC [`p:bool`; `p0:bool`; `p1:bool`; `p2:bool`] THEN
 242   ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
 243 (* }}} *)
 244
 245
 246 let vars, sgns, p, cont_z, cont_n =
 247 [`x:real`;`y:real`],
 248  empty_sgns,
 249 `&0 + y * &1`,
 250 (fun x -> (ASSUME `abc > def`,[])),
 251 (fun x -> (ASSUME `sean > steph`,[]))
 252
 253
 254 SPLIT_ZERO vars sgns p cont_z cont_n
 255
 256 ASSERTSIGN vars empty_sgns (ASSUME `&0 + y * &1 = &0`) ,
 257
 258 let vars = [`x:real`;`y:real`]
 259 let sgns = ASSERTSIGN vars [] (ASSUME `&7 + x * (&11 + x * (&10 + y * -- &7)) <> &0`)
 260 let p = `&7 + x * (&11 + x * (&10 + y * -- &7))`
 261 let cont_z = hd
 262 let cont_n = hd
 263 SPLIT_ZERO vars sgns p cont_z cont_n
 264
 265
 266 let k1 = ASSUME `&7 + x * (&11 + x * (&10 + y * &7)) < &0`
 267 let k1 = ASSUME `&7 + x * (&11 + x * (&10 + y * &7)) = &0`
 268 let k1 = ASSUME `&7 + x * (&11 + x * (&10 + y * &7)) <> &0`
 269 let sgn_thm = k1
 270 ASSERTSIGN vars [] k1
 271
 272 *)
 273
 274 let SPLIT_SIGN vars sgns p cont_p cont_n ex_thms =
 275   let sgn_thm = try FINDSIGN vars sgns p
 276                 with Failure "FINDSIGN" ->
 277                 failwith "SPLIT_SIGN: no sign -- should have sign assumption by now" in
 278   let gt_tm = mk_binop rgt p rzero in
 279   let lt_tm = mk_binop rlt p rzero in
 280   let op,_,_ = get_binop (concl sgn_thm) in
 281   if op = rgt then cont_p sgns ex_thms
 282   else if op = rlt then cont_n sgns ex_thms
 283   else if op = req then failwith "SPLIT_SIGN: lead coef is 0"
 284   else if op = rneq then
 285     let or_thm = MATCH_MP signs_lem0002 sgn_thm in
 286     (* < *)
 287     let lt_sgns = ASSERTSIGN vars sgns (ASSUME lt_tm) in
 288     let lt_thm = cont_n lt_sgns ex_thms in
 289     let lt_thm' = DISCH lt_tm lt_thm in
 290      (* > *)
 291     let gt_sgns = ASSERTSIGN vars sgns (ASSUME gt_tm) in
 292     let gt_thm = cont_p gt_sgns ex_thms in
 293     let gt_thm' = DISCH gt_tm gt_thm in
 294     (* combine *)
 295     let ret = MATCH_MPL[signs_lem0003;or_thm;gt_thm';lt_thm'] in
 296     (* matching problem... must continue by hand *)
 297     let ldj,rdj = dest_disj (concl ret) in
 298     let lcj,rcj = dest_conj ldj in
 299     let a,_ = dest_binop rgt lcj in
 300     let p,p1 = dest_beq rcj in
 301     let _,rcj = dest_conj rdj in
 302     let p2 = rhs rcj in
 303     let pull_thm = ISPECL[a;p;p1;p2] PULL_CASES_THM_NZ in
 304     let ret' = MATCH_EQ_MP (MATCH_MP pull_thm sgn_thm) ret in
 305       ret'
 306   else failwith "SPLIT_SIGN: unknown op";;
 307
 308
 309 (*
 310 let vars, sgns, p,cont_p,  cont_n =  !ss_vars,!ss_sgns,!ss_p,!ss_cont_p,!ss_cont_n
 311 [`x`],
 312 [ASSUME `&0 + x * &1 <> &0`; ARITH_RULE ` &1 > &0`],
 313 `&0 + x * &1`
 314
 315 let ss_vars, ss_sgns, ss_p,ss_cont_p, ss_cont_n =  ref [],ref [],ref `T`,ref (fun x -> TRUTH,[]),ref(fun x -> TRUTH,[]);;
 316   ss_vars := vars;
 317   ss_sgns := sgns;
 318   ss_p := p;
 319   ss_cont_p := cont_p;
 320   ss_cont_n := cont_n;
 321
 322
 323
 324 let vars, sgns, p, cont_p, cont_n =
 325 [`x:real`;`y:real`],
 326 ASSERTSIGN vars empty_sgns (ASSUME `&0 + y * &1 <> &0`) ,
 327 `&0 + y * &1`,
 328 (fun x -> (ASSUME `P > def`,[])),
 329 (fun x -> (ASSUME `sean > steph`,[]))
 330
 331 SPLIT_SIGN vars sgns p cont_z cont_n
 332
 333
 334 let vars = [`x:real`;`y:real`]
 335 let sgns = ASSERTSIGN vars [] (ASSUME `&7 + x * (&11 + x * (&10 + y * -- &7)) <> &0`)
 336 let p = `&7 + x * (&11 + x * (&10 + y * -- &7))`
 337 let cont_p = hd
 338 let cont_n = hd
 339 SPLIT_SIGN vars sgns p cont_p cont_n
 340
 341 let sgns = ASSERTSIGN vars [] (ASSUME `&7 + x * (&11 + x * (&10 + y * -- &7)) <> &0`)
 342
 343 let k1 = ASSUME `&7 + x * (&11 + x * (&10 + y * &7)) < &0`
 344 let k1 = ASSUME `&7 + x * (&11 + x * (&10 + y * &7)) = &0`
 345 let k1 = ASSUME `&7 + x * (&11 + x * (&10 + y * &7)) <> &0`
 346 let sgn_thm = k1
 347 ASSERTSIGN vars [] k1
 348
 349
 350
 351
 352 *)