1structure OmegaSimple :> OmegaSimple = 2struct 3(* ---------------------------------------------------------------------- 4 Takes a closed existentially quantified formula where the body of 5 the formula is a conjunction of <=-constraints. 6 7 A <=-constraint is always of the form 8 0 <= c_1*v_1 + c_2 * v_2 + c_3 * v_3 + ... + n 9 10 With each c_i and the n an integer literal. The n may be zero, but 11 must be present. 12 13 Attempts to reduce the formula to true or false using the MLshadow 14 code in OmegaMLShadow. 15 ---------------------------------------------------------------------- *) 16 17open HolKernel boolLib intSyntax 18open integerTheory 19 20val lhand = rand o rator 21 22val ERR = mk_HOL_ERR "OmegaSimple"; 23 24(* Fix the grammar used by this file *) 25structure Parse = struct 26 open Parse 27 val (Type,Term) = parse_from_grammars integer_grammars 28end 29 30 31(* ---------------------------------------------------------------------- 32 var_sorted ct 33 34 Checks that the variables in constraint ct (a term) appear in order 35 from left to right, and aren't duplicated. 36 ---------------------------------------------------------------------- *) 37 38fun vars_sorted ct = let 39 fun recurse [] = true 40 | recurse [_] = true 41 | recurse (t::(ts as (u::us))) = let 42 val vname = #1 o dest_var o #2 o dest_mult 43 in 44 String.<(vname t, vname u) 45 end 46in 47 recurse (#1 (front_last (strip_plus (rand ct)))) 48end 49 50(* ---------------------------------------------------------------------- 51 add_term_to_db db t next kont 52 53 Adds a term to an OmegaMLShadow database, and continues with next if 54 this doesn't do anything untoward, or kont if this generates a 55 "result" immediately (which can come about if there is already a term 56 in the database that contradicts what we have). 57 ---------------------------------------------------------------------- *) 58 59fun add_term_to_db db vars t next kont = let 60 open OmegaMLShadow 61 val df as (f,d) = term_to_dfactoid vars t 62in 63 if false_factoid f then kont (CONTR d) 64 else if true_factoid f then next db kont 65 else add_check_factoid db (gcd_check_dfactoid df) next kont 66end 67 68(* ---------------------------------------------------------------------- 69 determine_width cstlist 70 71 determines the number of free variables in cstlist, and then adds 72 one to give the necessary width of the MLShadow database. 73 ---------------------------------------------------------------------- *) 74 75fun determine_width cstlist = 76 HOLset.numItems (FVL cstlist empty_tmset) + 1 77 78(* ---------------------------------------------------------------------- 79 isolate_var v t 80 81 t is a term of the form 0 <= c1 * v1 + ... + vn * cn + n 82 where v is one of the vi's. This function moves things around so 83 that v is on its own with a positive coefficient on one side or the 84 other of the <=. 85 ---------------------------------------------------------------------- *) 86 87val SYMLE_ADDL = GSYM integerTheory.INT_LE_ADDL 88val LE_NEG = REWRITE_RULE [INT_NEG_LMUL, INT_NEGNEG] 89 (SPECL [``c * v:int``, ``~y:int``] INT_LE_NEG) 90fun isolate_var v t = let 91 val r = rand t 92 fun findv_c t = let 93 val (l,r) = dest_plus t 94 val (c,v') = dest_mult r 95 in 96 if v = v' then c else findv_c l 97 end handle HOL_ERR _ => #1 (dest_mult t) 98 val c = findv_c (lhand r) 99 val (flip, addthis) = if is_negated c then (false, mk_mult(rand c, v)) 100 else (true, mk_mult(mk_negated c, v)) 101 val add_th = SPECL [r,addthis] SYMLE_ADDL 102 open OmegaMath 103in 104 K add_th THENC 105 RAND_CONV SORT_AND_GATHER1_CONV THENC 106 (if flip then REWR_CONV LE_NEG THENC LAND_CONV NEG_SUM_CONV else ALL_CONV) 107end t 108 109(* ---------------------------------------------------------------------- 110 verify_combination v th1 th2 111 112 Does variable elimination on v, given a "lower-bound" theorem th1, 113 and an "upper-bound" theorem th2. Both th1 and th2 are of the form 114 0 <= c1 * v1 + ... + vn * cn + n 115 In th1, the coefficient of v will be positive, and in th2, negative. 116 ---------------------------------------------------------------------- *) 117 118fun verify_combination v th1 th2 = let 119 open CooperMath OmegaMath 120 val lowth = CONV_RULE (isolate_var v) th1 121 val upth = CONV_RULE (isolate_var v) th2 122 val lo_c = lhand (rand (concl lowth)) 123 val hi_c = lhand (lhand (concl upth)) 124 val lo = int_of_term lo_c 125 val hi = int_of_term hi_c 126 val lh = lcm(lo,hi) 127 val lo_f = term_of_int (Arbint.div(lh,lo)) 128 val hi_f = term_of_int (Arbint.div(lh,hi)) 129 fun multhru_by c th = 130 if c = one_tm then th 131 else let 132 val zero_lt_c = EQT_ELIM (REDUCE_CONV (mk_less(zero_tm, c))) 133 val res = 134 EQ_MP (SYM (MP (SPECL [c, lhand (concl th), rand (concl th)] 135 INT_LE_MONO) 136 zero_lt_c)) 137 th 138 in 139 CONV_RULE (BINOP_CONV LINEAR_MULT) res 140 end 141 val newlo = multhru_by lo_f lowth 142 val newhi = multhru_by hi_f upth 143 val elim = MATCH_MP INT_LE_TRANS (CONJ newlo newhi) 144in 145 CONV_RULE (REWR_CONV int_arithTheory.le_move_all_right THENC 146 RAND_CONV (RAND_CONV NEG_SUM_CONV THENC 147 SORT_AND_GATHER_CONV)) elim 148end 149 150(* ---------------------------------------------------------------------- 151 verify_gcd_check th 152 153 Eliminates a common divisor from the coefficients of the variables in 154 theorem th, which is of the standard form. 155 ---------------------------------------------------------------------- *) 156 157fun verify_gcd_check th = let 158 open CooperMath 159 val t = concl th 160 val cs = List.mapPartial (total (#1 o dest_mult)) (strip_plus (rand t)) 161 val ics = map (Arbint.abs o int_of_term) cs 162 val d = gcdl ics 163 val d_t = term_of_int d 164 val rwt = MATCH_MP (SPEC d_t int_arithTheory.elim_le_coeffs) 165 (EQT_ELIM (REDUCE_CONV (mk_less(zero_tm, d_t)))) 166in 167 CONV_RULE (RAND_CONV (factor_out d d_t THENC 168 REWRITE_CONV [GSYM INT_LDISTRIB]) THENC 169 REWR_CONV rwt THENC 170 RAND_CONV (RAND_CONV REDUCE_CONV)) th 171end 172 173(* ---------------------------------------------------------------------- 174 verify_contr (th1, th2) 175 176 return [..] |- F 177 given the theorems th1 and th2, which between them say contradictory 178 things. They will be of the form 0 <= X + c and 0 <= ~X + d 179 and ~c is not <= d. X may be the sum of multiple ci * vi pairs. 180 ---------------------------------------------------------------------- *) 181 182fun verify_contr (th1, th2) = let 183 val isolate_X = REWR_CONV int_arithTheory.le_move_right_left THENC 184 REWRITE_CONV [INT_NEGNEG, INT_ADD_LID, INT_NEG_ADD, 185 INT_NEG_LMUL] 186 val th1' = CONV_RULE isolate_X th1 187 val th2' = CONV_RULE (RAND_CONV (REWR_CONV INT_ADD_COMM) THENC 188 isolate_X) th2 189 open CooperMath 190in 191 CONV_RULE REDUCE_CONV (MATCH_MP INT_LE_TRANS (CONJ th1' th2')) 192end 193 194 195(* ---------------------------------------------------------------------- 196 verify_derivation tm vars d 197 198 takes a purported derivation of false, and uses it to equate tm to 199 false. 200 ---------------------------------------------------------------------- *) 201 202fun verify_derivation tm vars d = let 203 open OmegaMLShadow 204 fun verifyd d = 205 case d of 206 ASM t => ASSUME t 207 | REAL_COMBIN(i, d1, d2) => let 208 val th1 = verifyd d1 209 val th2 = verifyd d2 210 in 211 verify_combination (List.nth(vars, i)) th1 th2 212 end 213 | GCD_CHECK d0 => verify_gcd_check (verifyd d0) 214 | DIRECT_CONTR (d1,d2) => 215 verify_contr(verifyd d1, verifyd d2) 216 val falsity = verifyd d 217 val (bvars, body) = strip_exists tm 218 val bodyths = CONJUNCTS (ASSUME body) 219 fun elimhyps th [] = th 220 | elimhyps th (cth::cths) = if HOLset.isEmpty (hypset th) then th 221 else elimhyps (PROVE_HYP cth th) cths 222 val hyps_elimmed = elimhyps falsity bodyths 223 fun foldthis (v, th) = let 224 val newhyp = mk_exists(v, hd (hyp th)) 225 in 226 CHOOSE(v, ASSUME(newhyp)) th 227 end 228 val exists_f = List.foldr foldthis hyps_elimmed bvars 229in 230 EQF_INTRO (NOT_INTRO (DISCH_ALL exists_f)) 231end 232 233 234(* ---------------------------------------------------------------------- 235 verify_satisfaction tm vars vm 236 237 vm maps integers to integers, where the domain is an index into the 238 list vars. Use this to provide witnesses that prove tm = T 239 ---------------------------------------------------------------------- *) 240 241fun verify_satisfaction tm vars vm = let 242 fun prove_exists t = 243 if is_exists t then let 244 val (v, bod) = dest_exists t 245 val i = index (fn u => u = v) vars 246 val n = PIntMap.find i vm 247 val n_t = term_of_int n 248 val newbod = Term.subst [v |-> n_t] bod 249 val subth = prove_exists newbod 250 in 251 EXISTS(t, n_t) subth 252 end 253 else EQT_ELIM (CooperMath.REDUCE_CONV t) 254in 255 EQT_INTRO (prove_exists tm) 256end 257 258(* ---------------------------------------------------------------------- 259 verify_result tm vars r 260 261 takes a term and a result from the MLShadow and attempts to turn it 262 into a theorem, where vars is the list of variables occuring in tm, 263 in order. 264 ---------------------------------------------------------------------- *) 265 266fun verify_result tm vars r = let 267 open OmegaMLShadow 268in 269 case r of 270 CONTR d => verify_derivation tm vars d 271 | SATISFIABLE vm => verify_satisfaction tm vars vm 272 | NO_CONCL => raise ERR "verify_result" "ML shadow chasing inconclusive" 273end 274 275(* ---------------------------------------------------------------------- 276 simple_CONV t 277 278 attempts to use ML shadow chasing to prove t either true or false. 279 ---------------------------------------------------------------------- *) 280 281fun simple_CONV t = let 282 val (vars, body) = strip_exists t 283 val svars = Listsort.sort Term.compare vars 284 val bcs = strip_conj body 285 fun add_ts db tl next kont = 286 case tl of 287 [] => next db kont 288 | (t::ts) => 289 add_term_to_db db svars t (fn db => fn k => add_ts db ts next k) kont 290 open OmegaMLShadow 291 val ordered_vars = Listsort.sort Term.compare vars 292in 293 add_ts (dbempty (length vars + 1)) bcs work (verify_result t ordered_vars) 294end 295 296(* testing code: 297 298 fun toTerm l = let 299 open intSyntax 300 val clist = map Arbint.fromInt l 301 val lim = length clist - 1 302 303 fun clist2term (x, (acc, n)) = let 304 val c = intSyntax.term_of_int x 305 val cx = if n = lim then c 306 else mk_mult(c, mk_var("x"^Int.toString n, int_ty)) 307 in 308 case acc of 309 NONE => (SOME cx, n + 1) 310 | SOME a => (SOME(mk_plus(a, cx)), n + 1) 311 end 312 in 313 mk_leq(zero_tm, valOf (#1 (List.foldl clist2term (NONE, 0) clist))) 314 end 315 316 fun test l = let 317 val body = list_mk_conj (map toTerm l) 318 val g = list_mk_exists(free_vars body, body) 319 in 320 time simple_CONV g; 321 time Cooper.COOPER_CONV g 322 end; 323 324 test [[2,3,6],[~1,~4,7]]; (* exact elimination *) 325 test [[2,3,4],[~3,~4,7]]; (* dark shadow test *) 326 test [[2,3,4],[~3,~4,7],[4,5,~10]]; (* another dark shadow *) 327 test [[2,3,4],[~3,~4,7],[4,~5,~10]]; (* also satisfiable *) 328 test [[~3,~1,6],[2,1,~5],[3,~1,~3]]; (* a contradiction *) 329 test [[11,13,~27], [~11,~13,45],[7,~9,10],[~7,9,4]]; (* no conclusion *) 330 331*) 332 333end (* struct *) 334