Examples/dlo.ml

   1 (* ========================================================================= *)
   2 (* Dense linear order decision procedure for reals, by Sean McLaughlin.      *)
   3 (* ========================================================================= *)
   4
   5 prioritize_real();;
   6
   7 (* ---------------------------------------------------------------------- *)
   8 (*  Util                                                                  *)
   9 (* ---------------------------------------------------------------------- *)
  10
  11 let list_conj =
  12   let t_tm = `T` in
  13   fun l -> if l = [] then t_tm else end_itlist (curry mk_conj) l;;
  14
  15 let mk_lt = mk_binop `(<)`;;
  16
  17 (* ---------------------------------------------------------------------- *)
  18 (*  cnnf                                                                  *)
  19 (* ---------------------------------------------------------------------- *)
  20
  21 let DOUBLE_NEG_CONV =
  22   let dn_thm = TAUT `!x. ~(~ x) <=> x` in
  23   let dn_conv =
  24     fun tm ->
  25       let tm' = dest_neg (dest_neg tm) in
  26         ISPEC tm' dn_thm in
  27     dn_conv;;
  28
  29 let IMP_CONV =
  30   let i_thm = TAUT `!a b. (a ==> b) <=> (~a \/ b)` in
  31   let i_conv =
  32     fun tm ->
  33       let (a,b) = dest_imp tm in
  34         ISPECL [a;b] i_thm in
  35     i_conv;;
  36
  37 let BEQ_CONV =
  38   let beq_thm = TAUT `!a b. (a = b) <=> (a /\ b \/ ~a /\ ~b)` in
  39   let beq_conv =
  40     fun tm ->
  41       let (a,b) = dest_eq tm in
  42         ISPECL [a;b] beq_thm in
  43     beq_conv;;
  44
  45 let NEG_AND_CONV =
  46   let na_thm = TAUT `!a b. ~(a /\ b) <=> (~a \/ ~b)` in
  47   let na_conv =
  48     fun tm ->
  49       let (a,b) = dest_conj (dest_neg tm) in
  50         ISPECL [a;b] na_thm in
  51     na_conv;;
  52
  53 let NEG_OR_CONV =
  54   let no_thm = TAUT `!a b. ~(a \/ b) <=> (~a /\ ~b)` in
  55   let no_conv =
  56     fun tm ->
  57       let (a,b) = dest_disj (dest_neg tm) in
  58         ISPECL [a;b] no_thm in
  59     no_conv;;
  60
  61 let NEG_IMP_CONV =
  62   let ni_thm = TAUT `!a b. ~(a ==> b) <=> (a /\ ~b)` in
  63   let ni_conv =
  64     fun tm ->
  65       let (a,b) = dest_imp (dest_neg tm) in
  66         ISPECL [a;b] ni_thm in
  67     ni_conv;;
  68
  69 let NEG_BEQ_CONV =
  70   let nbeq_thm = TAUT `!a b. ~(a = b) <=> (a /\ ~b \/ ~a /\ b)` in
  71   let nbeq_conv =
  72     fun tm ->
  73       let (a,b) = dest_eq (dest_neg tm) in
  74         ISPECL [a;b] nbeq_thm in
  75     nbeq_conv;;
  76
  77
  78 (* tm = (p /\ q0) \/ (~p /\ q1) *)
  79 let dest_cases tm =
  80   try
  81     let (l,r) = dest_disj tm in
  82     let (p,q0) = dest_conj l in
  83     let (np,q1) = dest_conj r in
  84       if mk_neg p = np then (p,q0,q1) else failwith "not a cases term"
  85   with Failure _ -> failwith "not a cases term";;
  86
  87 let is_cases = can dest_cases;;
  88
  89 let CASES_CONV =
  90   let c_thm =
  91     TAUT `!p q0 q1. ~(p /\ q0 \/ ~p /\ q1) <=> (p /\ ~q0 \/ ~p /\ ~q1)` in
  92   let cc =
  93     fun tm ->
  94       let (p,q0,q1) = dest_cases tm in
  95         ISPECL [p;q0;q1] c_thm in
  96     cc;;
  97
  98 let QE_SIMPLIFY_CONV =
  99   let NOT_EXISTS_UNIQUE_THM = prove
 100    (`~(?!x. P x) <=> (!x. ~P x) \/ ?x x'. P x /\ P x' /\ ~(x = x')`,
 101     REWRITE_TAC[EXISTS_UNIQUE_THM; DE_MORGAN_THM; NOT_EXISTS_THM] THEN
 102     REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; CONJ_ASSOC]) in
 103   let tauts =
 104     [TAUT `~(~p) <=> p`;
 105      TAUT `~(p /\ q) <=> ~p \/ ~q`;
 106      TAUT `~(p \/ q) <=> ~p /\ ~q`;
 107      TAUT `~(p ==> q) <=> p /\ ~q`;
 108      TAUT `p ==> q <=> ~p \/ q`;
 109      NOT_FORALL_THM;
 110      NOT_EXISTS_THM;
 111      EXISTS_UNIQUE_THM;
 112      NOT_EXISTS_UNIQUE_THM;
 113      TAUT `~(p = q) <=> (p /\ ~q) \/ (~p /\ q)`;
 114      TAUT `(p = q) <=> (p /\ q) \/ (~p /\ ~q)`;
 115      TAUT `~(p /\ q \/ ~p /\ r) <=> p /\ ~q \/ ~p /\ ~r`] in
 116   GEN_REWRITE_CONV TOP_SWEEP_CONV tauts;;
 117
 118 let CNNF_CONV =
 119   let refl_conj = REFL `(/\)`
 120   and refl_disj = REFL `(\/)` in
 121   fun lfn_conv ->
 122     let rec cnnf_conv tm =
 123       if is_conj tm  then
 124         let (p,q) = dest_conj tm in
 125         let thm1 = cnnf_conv p in
 126         let thm2 = cnnf_conv q in
 127           MK_COMB (MK_COMB (refl_conj,thm1),thm2)
 128       else if is_disj tm  then
 129         let (p,q) = dest_disj tm in
 130         let thm1 = cnnf_conv p in
 131         let thm2 = cnnf_conv q in
 132           MK_COMB (MK_COMB (refl_disj,thm1),thm2)
 133       else if is_imp tm then
 134         let (p,q) = dest_imp tm in
 135         let thm1 = cnnf_conv (mk_neg p) in
 136         let thm2 = cnnf_conv q in
 137           TRANS (IMP_CONV tm) (MK_COMB(MK_COMB(refl_disj,thm1),thm2))
 138       else if is_iff tm then
 139         let (p,q) = dest_eq tm in
 140         let pthm = cnnf_conv p in
 141         let qthm = cnnf_conv q in
 142         let npthm = cnnf_conv (mk_neg p) in
 143         let nqthm = cnnf_conv (mk_neg q) in
 144         let thm1 = MK_COMB(MK_COMB(refl_conj,pthm),qthm) in
 145         let thm2 = MK_COMB(MK_COMB(refl_conj,npthm),nqthm) in
 146           TRANS (BEQ_CONV tm) (MK_COMB(MK_COMB(refl_disj,thm1),thm2))
 147       else if is_neg tm then
 148         let tm' = dest_neg tm in
 149           if is_neg tm' then
 150             let tm'' = dest_neg tm' in
 151             let thm = cnnf_conv tm in
 152               TRANS (DOUBLE_NEG_CONV tm'') thm
 153           else if is_conj tm' then
 154             let (p,q) = dest_conj tm' in
 155             let thm1 = cnnf_conv (mk_neg p) in
 156             let thm2 = cnnf_conv (mk_neg q) in
 157               TRANS (NEG_AND_CONV tm) (MK_COMB(MK_COMB(refl_disj,thm1),thm2))
 158           else if is_cases tm' then
 159             let (p,q0,q1) = dest_cases tm in
 160             let thm1 = cnnf_conv (mk_conj(p,mk_neg q0)) in
 161             let thm2 = cnnf_conv (mk_conj(mk_neg p,mk_neg q1)) in
 162               TRANS (CASES_CONV tm) (MK_COMB(MK_COMB(refl_disj,thm1),thm2))
 163           else if is_disj tm' then
 164             let (p,q) = dest_disj tm' in
 165             let thm1 = cnnf_conv (mk_neg p) in
 166             let thm2 = cnnf_conv (mk_neg q) in
 167               TRANS (NEG_OR_CONV tm) (MK_COMB(MK_COMB(refl_conj,thm1),thm2))
 168           else if is_imp tm' then
 169             let (p,q) = dest_imp tm' in
 170             let thm1 = cnnf_conv p in
 171             let thm2 = cnnf_conv (mk_neg q) in
 172               TRANS (NEG_IMP_CONV tm) (MK_COMB(MK_COMB(refl_conj,thm1),thm2))
 173           else if is_iff tm' then
 174             let (p,q) = dest_eq tm' in
 175             let pthm = cnnf_conv p in
 176             let qthm = cnnf_conv q in
 177             let npthm = cnnf_conv (mk_neg p) in
 178             let nqthm = cnnf_conv (mk_neg q) in
 179             let thm1 = MK_COMB (MK_COMB(refl_conj,pthm),nqthm) in
 180             let thm2 = MK_COMB(MK_COMB(refl_conj,npthm),qthm) in
 181               TRANS (NEG_BEQ_CONV tm) (MK_COMB(MK_COMB(refl_disj,thm1),thm2))
 182           else lfn_conv tm
 183       else lfn_conv tm in
 184       QE_SIMPLIFY_CONV THENC cnnf_conv THENC QE_SIMPLIFY_CONV;;
 185
 186
 187 (*
 188
 189 let tests = [
 190 `~(a /\ b)`;
 191 `~(a \/ b)`;
 192 `~(a ==> b)`;
 193 `~(a:bool <=> b)`;
 194 `~ ~ a`;
 195 ];;
 196
 197 map (CNNF_CONV (fun x -> REFL x)) tests;;
 198 *)
 199
 200
 201 (* ---------------------------------------------------------------------- *)
 202 (*  Real Lists                                                            *)
 203 (* ---------------------------------------------------------------------- *)
 204
 205 let MINL = new_recursive_definition list_RECURSION
 206   `(MINL [] default = default) /\
 207    (MINL (CONS h t) default = min h (MINL t default))`;;
 208
 209 let MAXL = new_recursive_definition list_RECURSION
 210   `(MAXL [] default = default) /\
 211    (MAXL (CONS h t) default = max h (MAXL t default))`;;
 212
 213 let MAX_LT = prove
 214  (`!x y z. max x y < z <=> x < z /\ y < z`,
 215   REWRITE_TAC[real_max] THEN MESON_TAC[REAL_LET_TRANS; REAL_LE_TOTAL]);;
 216
 217 let MIN_GT = prove
 218  (`!x y z. x < real_min y z <=> x < y /\ x < z`,
 219   REWRITE_TAC[real_min] THEN MESON_TAC[REAL_LTE_TRANS; REAL_LE_TOTAL]);;
 220
 221 let ALL_LT_LEMMA = prove
 222  (`!left x lefts. ALL (\l. l < x) (CONS left lefts) <=> MAXL lefts left < x`,
 223   GEN_TAC THEN GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[MAXL; ALL] THEN
 224   SPEC_TAC(`t:real list`,`t:real list`) THEN LIST_INDUCT_TAC THEN
 225   REWRITE_TAC[ALL; MAXL; MAX_LT] THEN ASM_MESON_TAC[MAX_LT]);;
 226
 227 let ALL_GT_LEMMA = prove
 228  (`!right x rights.
 229         ALL (\r. x < r) (CONS right rights) <=> x < MINL rights right`,
 230   GEN_TAC THEN GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[MINL; ALL] THEN
 231   SPEC_TAC(`t:real list`,`t:real list`) THEN LIST_INDUCT_TAC THEN
 232   REWRITE_TAC[ALL; MINL; MIN_GT] THEN ASM_MESON_TAC[MIN_GT]);;
 233
 234 (* ---------------------------------------------------------------------- *)
 235 (*  Axioms                                                                *)
 236 (* ---------------------------------------------------------------------- *)
 237
 238 let REAL_DENSE = prove
 239  (`!x y. x < y ==> ?z. x < z /\ z < y`,
 240   REPEAT STRIP_TAC THEN EXISTS_TAC `(x + y) / &2` THEN
 241   SIMP_TAC[REAL_LT_LDIV_EQ; REAL_LT_RDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN
 242   POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
 243
 244 let REAL_LT_EXISTS = prove(`!x. ?y. x < y`,
 245   GEN_TAC THEN
 246   EXISTS_TAC `x + &1` THEN
 247   REAL_ARITH_TAC);;
 248
 249 let REAL_GT_EXISTS = prove(`!x. ?y. y < x`,
 250   GEN_TAC THEN
 251   EXISTS_TAC `x - &1` THEN
 252   REAL_ARITH_TAC);;
 253
 254 (* ---------------------------------------------------------------------- *)
 255 (*  lfn_dlo                                                               *)
 256 (* ---------------------------------------------------------------------- *)
 257
 258 let LFN_DLO_CONV =
 259   PURE_REWRITE_CONV[
 260     REAL_ARITH `~(s < t) <=> ((s = t) \/ (t < s))`;
 261     REAL_ARITH `~(s = t) <=> (s < t \/ t < s)`;
 262   ];;
 263
 264 (* ------------------------------------------------------------------------- *)
 265 (* Proforma theorems to support the main inference step.                     *)
 266 (* ------------------------------------------------------------------------- *)
 267
 268 let PROFORMA_LEFT = prove
 269  (`!l ls. (?x. ALL (\l. l < x) (CONS l ls)) <=> T`,
 270   REWRITE_TAC[ALL_LT_LEMMA] THEN MESON_TAC[REAL_LT_EXISTS]);;
 271
 272 let PROFORMA_RIGHT = prove
 273  (`!r rs. (?x. ALL (\r. x < r) (CONS r rs)) <=> T`,
 274   REWRITE_TAC[ALL_GT_LEMMA] THEN MESON_TAC[REAL_GT_EXISTS]);;
 275
 276 let PROFORMA_BOTH = prove
 277  (`!l ls r rs.
 278         (?x. ALL (\l. l < x) (CONS l ls) /\ ALL (\r. x < r) (CONS r rs)) <=>
 279         ALL (\l. ALL (\r. l < r) (CONS r rs)) (CONS l ls)`,
 280   REWRITE_TAC[ALL_LT_LEMMA; ALL_GT_LEMMA] THEN
 281   MESON_TAC[REAL_DENSE; REAL_LT_TRANS]);;
 282
 283 (* ------------------------------------------------------------------------- *)
 284 (* Deal with ?x. <conjunction of strict inequalities all involving x>        *)
 285 (* ------------------------------------------------------------------------- *)
 286
 287 let mk_rlist = let ty = `:real` in fun x -> mk_list(x,ty);;
 288
 289 let expand_all = PURE_REWRITE_RULE
 290   [ALL; BETA_THM; GSYM CONJ_ASSOC; TAUT `a /\ T <=> a`];;
 291
 292 let DLO_EQ_CONV fm =
 293   let x,p = dest_exists fm in
 294   let xl,xr = partition (fun t -> rand t = x) (conjuncts p) in
 295   let lefts = map lhand xl and rights = map rand xr in
 296   let th1 =
 297     if lefts = [] then SPECL [hd rights; mk_rlist(tl rights)] PROFORMA_RIGHT
 298     else if rights = [] then SPECL [hd lefts; mk_rlist(tl lefts)] PROFORMA_LEFT
 299     else SPECL [hd lefts; mk_rlist(tl lefts); hd rights; mk_rlist(tl rights)]
 300                PROFORMA_BOTH in
 301   let th2 = CONV_RULE (LAND_CONV(GEN_ALPHA_CONV x)) (expand_all th1) in
 302   let p' = snd(dest_exists(lhand(concl th2))) in
 303   let th3 = MK_EXISTS x (CONJ_ACI_RULE(mk_eq(p,p'))) in
 304   TRANS th3 th2;;
 305
 306 (* ------------------------------------------------------------------------- *)
 307 (* Deal with general ?x. <conjunction of atoms>                              *)
 308 (* ------------------------------------------------------------------------- *)
 309
 310 let eq_triv_conv =
 311   let pth_triv = prove
 312    (`((?x. x = x) <=> T) /\
 313      ((?x. x = t) <=> T) /\
 314      ((?x. t = x) <=> T) /\
 315      ((?x. (x = t) /\ P x) <=> P t) /\
 316      ((?x. (t = x) /\ P x) <=> P t)`,
 317     MESON_TAC[]) in
 318   GEN_REWRITE_CONV I [pth_triv]
 319
 320 and eq_refl_conv =
 321   let pth_refl = prove
 322    (`(?x. (x = x) /\ P x) <=> (?x. P x)`,
 323     MESON_TAC[]) in
 324   GEN_REWRITE_CONV I [pth_refl]
 325
 326 and lt_refl_conv =
 327   GEN_REWRITE_CONV DEPTH_CONV
 328    [REAL_LT_REFL; AND_CLAUSES; EXISTS_SIMP];;
 329
 330 let rec DLOBASIC_CONV fm =
 331   try let x,p = dest_exists fm in
 332       let cjs = conjuncts p in
 333       try let eq = find (fun e -> is_eq e & (lhs e = x or rhs e = x)) cjs in
 334           let cjs' = eq::setify(subtract cjs [eq]) in
 335           let p' = list_mk_conj cjs' in
 336           let th1 = MK_EXISTS x (CONJ_ACI_RULE(mk_eq(p,p'))) in
 337           let fm' = rand(concl th1) in
 338           try TRANS th1 (eq_triv_conv fm') with Failure _ ->
 339           TRANS th1 ((eq_refl_conv THENC DLOBASIC_CONV) fm')
 340       with Failure _ ->
 341           if mem (mk_lt x x) cjs then lt_refl_conv fm
 342           else DLO_EQ_CONV fm
 343   with Failure _ -> (print_qterm fm; failwith "dlobasic");;
 344
 345 (* ------------------------------------------------------------------------- *)
 346 (* Overall quantifier elimination.                                           *)
 347 (* ------------------------------------------------------------------------- *)
 348
 349 let AFN_DLO_CONV vars =
 350   PURE_REWRITE_CONV[
 351     REAL_ARITH `s <= t <=> ~(t < s)`;
 352     REAL_ARITH `s >= t <=> ~(s < t)`;
 353     REAL_ARITH `s > t <=> t < s`
 354   ];;
 355
 356 let dest_binop_op tm =
 357   try
 358     let f,r = dest_comb tm in
 359     let op,l = dest_comb f in
 360       (l,r,op)
 361   with Failure _ -> failwith "dest_binop_op";;
 362
 363 let forall_thm = prove(`!P. (!x. P x) <=> ~ (?x. ~ P x)`,MESON_TAC[])
 364 and or_exists_conv = PURE_REWRITE_CONV[OR_EXISTS_THM]
 365 and triv_exists_conv = REWR_CONV EXISTS_SIMP
 366 and push_exists_conv = REWR_CONV RIGHT_EXISTS_AND_THM
 367 and not_tm = `(~)`
 368 and or_tm = `(\/)`
 369 and t_tm = `T`
 370 and f_tm = `F`;;
 371
 372 let LIFT_QELIM_CONV afn_conv nfn_conv qfn_conv =
 373   let rec qelift_conv vars fm =
 374     if fm = t_tm or fm = f_tm then REFL fm
 375     else if is_neg fm then
 376       let thm1 = qelift_conv vars (dest_neg fm) in
 377         MK_COMB(REFL not_tm,thm1)
 378     else if is_conj fm or is_disj fm or is_imp fm or is_iff fm then
 379       let (p,q,op) = dest_binop_op fm in
 380       let thm1 = qelift_conv vars p in
 381       let thm2 = qelift_conv vars q in
 382         MK_COMB(MK_COMB((REFL op),thm1),thm2)
 383     else if is_forall fm then
 384       let (x,p) = dest_forall fm in
 385       let nex_thm = BETA_RULE (ISPEC (mk_abs(x,p)) forall_thm) in
 386       let elim_thm = qelift_conv vars (mk_exists(x,mk_neg p)) in
 387         TRANS nex_thm (MK_COMB (REFL not_tm,elim_thm))
 388     else if is_exists fm then
 389       let (x,p) = dest_exists fm in
 390       let thm1 = qelift_conv (x::vars) p in
 391       let thm1a = MK_EXISTS x thm1 in
 392       let thm2 = nfn_conv (rhs(concl thm1)) in
 393       let thm2a = MK_EXISTS x thm2 in
 394       let djs = disjuncts (rhs (concl thm2)) in
 395       let djthms = map (qelim x vars) djs in
 396       let thm3 = end_itlist
 397         (fun thm1 thm2 -> MK_COMB(MK_COMB (REFL or_tm,thm1),thm2)) djthms in
 398       let split_ex_thm = GSYM (or_exists_conv (lhs (concl thm3))) in
 399       let thm3a = TRANS split_ex_thm thm3 in
 400         TRANS (TRANS thm1a thm2a) thm3a
 401     else
 402       afn_conv vars fm
 403   and qelim x vars p =
 404     let cjs = conjuncts p in
 405     let ycjs,ncjs = partition (mem x o frees) cjs in
 406     if ycjs = [] then triv_exists_conv(mk_exists(x,p))
 407     else if ncjs = [] then qfn_conv vars (mk_exists(x,p)) else
 408     let th1 = CONJ_ACI_RULE
 409      (mk_eq(p,mk_conj(list_mk_conj ncjs,list_mk_conj ycjs))) in
 410     let th2 = CONV_RULE (RAND_CONV push_exists_conv) (MK_EXISTS x th1) in
 411     let t1,t2 = dest_comb (rand(concl th2)) in
 412     TRANS th2 (AP_TERM t1 (qfn_conv vars t2)) in
 413   fun fm -> ((qelift_conv (frees fm)) THENC QE_SIMPLIFY_CONV) fm;;
 414
 415 let QELIM_DLO_CONV =
 416   (LIFT_QELIM_CONV AFN_DLO_CONV ((CNNF_CONV LFN_DLO_CONV) THENC DNF_CONV)
 417     (fun v -> DLOBASIC_CONV)) THENC (REWRITE_CONV[]);;
 418
 419 (* ---------------------------------------------------------------------- *)
 420 (*  Test                                                                  *)
 421 (* ---------------------------------------------------------------------- *)
 422
 423 let tests = [
 424   `!x y. ?z. z < x /\ z < y`;
 425   `?z. x < x /\ z < y`;
 426   `?z. x < z /\ z < y`;
 427   `!x. x < a ==> x < b`;
 428   `!a b. (!x. (x < a) <=> (x < b)) <=> (a = b)`; (* long time *)
 429   `!x. ?y. x < y`;
 430   `!x y z. x < y /\ y < z ==> x < z`;
 431   `!x y. x < y \/ (x = y) \/ y < x`;
 432   `!x y. x < y \/ (x = y) \/ y < x`;
 433   `?x y. x < y /\ y < x`;
 434   `!x y. ?z. z < x /\ x < y`;
 435   `!x y. ?z. z < x /\ z < y`;
 436   `!x y. x < y ==> ?z. x < z /\ z < y`;
 437   `!x y. ~(x = y) ==> ?u. u < x /\ (y < u \/ x < y)`;
 438   `?x. x = x:real`;
 439   `?x.(x = x) /\ (x = y)`;
 440   `?z. x < z /\ z < y`;
 441   `?z. x <= z /\ z <= y`;
 442   `?z. x < z /\ z <= y`;
 443   `!x y z. ?u. u < x /\ u < y /\ u < z`;
 444   `!y. x < y /\ y < z ==> w < z`;
 445   `!x y . x < y`;
 446   `?z. z < x /\ x < y`;
 447   `!a b. (!x. x < a ==> x < b) <=> (a <= b)`;
 448   `!x. x < a ==> x < b`;
 449   `!x. x < a ==> x <= b`;
 450   `!a b. ?x. ~(x = a) \/ ~(x = b) \/ (a = b:real)`;
 451   `!x y. x <= y \/ x > y`;
 452   `!x y. x <= y \/ x < y`
 453 ];;
 454
 455 map (time QELIM_DLO_CONV) tests;;