1open HolKernel boolLib Parse bossLib 2 3open finite_mapTheory 4open boolSimps 5 6val _ = new_theory "hol_dpll" 7 8val _ = set_fixity "satisfies_clause" (Infixl 500) 9val satisfies_clause_def = Define` 10 sigma satisfies_clause (c:('a # bool) list) = 11 EXISTS (\ (a,v). FLOOKUP sigma a = SOME v) c 12`; 13 14val satisfies_clause_thm = store_thm( 15 "satisfies_clause_thm", 16 ``(s satisfies_clause [] = F) /\ 17 (s satisfies_clause (h :: t) = 18 (FLOOKUP s (FST h) = SOME (SND h)) \/ 19 s satisfies_clause t)``, 20 SRW_TAC [][satisfies_clause_def] THEN Cases_on `h` THEN 21 SRW_TAC [][]); 22 23val _ = set_fixity "satisfies" (Infixl 500) 24val satisfies_def = Define` 25 sigma satisfies (cset : ('a # bool) list list) = 26 EVERY (\c. sigma satisfies_clause c) cset 27`; 28 29val satisfies_thm = store_thm( 30 "satisfies_thm", 31 ``(s satisfies [] = T) /\ 32 (s satisfies (c::cs) = s satisfies_clause c /\ s satisfies cs)``, 33 SRW_TAC [][satisfies_def]); 34 35val binds_def = Define`binds a p = (a = FST p)` 36 37val rewrite_def = Define` 38 (rewrite a v [] = []) /\ 39 (rewrite a v (c::cs) = if MEM (a,v) c then 40 rewrite a v cs 41 else 42 FILTER ($~ o binds a) c :: rewrite a v cs) 43`; 44 45val catom_def = Define` 46 (catom a [] = F) /\ 47 (catom a (h :: t) = (a = FST h) \/ catom a t) 48`; 49 50val atom_appears_def = Define` 51 atom_appears a cset = EXISTS (catom a) cset 52`; 53 54val LENGTH_FILTER_1 = prove( 55 ``LENGTH (FILTER P l) <= LENGTH l``, 56 Induct_on `l` THEN SRW_TAC [][] THEN DECIDE_TAC); 57 58val rewrite_noincrease = store_thm( 59 "rewrite_noincrease", 60 ``list_size LENGTH (rewrite a v cset) <= list_size LENGTH cset``, 61 Induct_on `cset` THEN 62 SRW_TAC [][rewrite_def, listTheory.list_size_def] THENL [ 63 DECIDE_TAC, 64 Q_TAC SUFF_TAC `LENGTH (FILTER ($~ o binds a) h) <= LENGTH h` 65 THEN1 DECIDE_TAC THEN 66 SRW_TAC [][LENGTH_FILTER_1] 67 ]); 68 69val lemma = prove( 70 ``catom a h ==> LENGTH (FILTER ($~ o binds a) h) < LENGTH h``, 71 Induct_on `h` THEN 72 SRW_TAC [][catom_def, binds_def, DECIDE ``x < SUC y = x <= y``, 73 LENGTH_FILTER_1] THEN 74 FULL_SIMP_TAC (srw_ss() ++ ARITH_ss) []); 75 76val rewrite_reduces_size = store_thm( 77 "rewrite_reduces_size", 78 ``atom_appears a cset ==> (list_size LENGTH (rewrite a v cset) < 79 list_size LENGTH cset)``, 80 Induct_on `cset` THEN SRW_TAC [][atom_appears_def] THENL [ 81 SRW_TAC [][listTheory.list_size_def, rewrite_def] THENL [ 82 ASSUME_TAC rewrite_noincrease THEN DECIDE_TAC, 83 ASSUME_TAC rewrite_noincrease THEN 84 Q_TAC SUFF_TAC `LENGTH (FILTER ($~ o binds a) h) < LENGTH h` 85 THEN1 DECIDE_TAC THEN 86 SRW_TAC [][lemma] 87 ], 88 89 SRW_TAC [][listTheory.list_size_def, rewrite_def] THENL [ 90 FULL_SIMP_TAC (srw_ss() ++ ARITH_ss) [atom_appears_def], 91 Q_TAC SUFF_TAC `LENGTH (FILTER ($~ o binds a) h) <= LENGTH h` 92 THEN1 FULL_SIMP_TAC (srw_ss() ++ ARITH_ss) [atom_appears_def] THEN 93 SRW_TAC [][LENGTH_FILTER_1] 94 ] 95 ]); 96 97val find_uprop_def = Define` 98 (find_uprop [] = NONE) /\ 99 (find_uprop (c::cs) = if LENGTH c = 1 then SOME (HD c) 100 else find_uprop cs) 101`; 102 103val find_uprop_works = store_thm( 104 "find_uprop_works", 105 ``(find_uprop cset = SOME (v',b)) ==> atom_appears v' cset``, 106 Induct_on `cset` THEN SRW_TAC [][find_uprop_def] THENL [ 107 SRW_TAC [][atom_appears_def] THEN Cases_on `h` THEN 108 FULL_SIMP_TAC (srw_ss()) [catom_def], 109 FULL_SIMP_TAC (srw_ss()) [atom_appears_def] 110 ]); 111 112val choose_def = Define` 113 choose cset = FST (HD (HD cset)) 114`; 115 116val choose_works = store_thm( 117 "choose_works", 118 ``~(cset = []) /\ ~MEM [] cset ==> atom_appears (choose cset) cset``, 119 Cases_on `cset` THEN SRW_TAC [][] THEN 120 Cases_on `h` THEN FULL_SIMP_TAC (srw_ss()) [choose_def] THEN 121 SRW_TAC [][atom_appears_def, catom_def]); 122 123val dpll_defn = Hol_defn "dpll" ` 124 dpll cset = 125 if cset = [] then SOME FEMPTY 126 else if MEM [] cset then NONE 127 else 128 case find_uprop cset of 129 NONE => (let splitv = choose cset 130 in 131 case dpll (rewrite splitv T cset) of 132 NONE => (case dpll (rewrite splitv F cset) of 133 NONE => NONE 134 | SOME fm => SOME (fm |+ (splitv,F))) 135 | SOME fm => SOME (fm |+ (splitv,T))) 136 | SOME (v,b) => 137 case dpll (rewrite v b cset) of 138 NONE => NONE 139 | SOME fm => SOME (fm |+ (v,b)) 140`; 141 142 143 144val (dpll_def, dpll_ind) = Defn.tprove( 145 dpll_defn, 146 WF_REL_TAC `measure (\cset. list_size LENGTH cset)` THEN 147 SRW_TAC [][] THENL [ 148 SRW_TAC [][rewrite_reduces_size, choose_works], 149 SRW_TAC [][rewrite_reduces_size, choose_works], 150 METIS_TAC [find_uprop_works, rewrite_reduces_size] 151 ]); 152 153val induct = 154 (SIMP_RULE (srw_ss()) [prim_recTheory.WF_measure, 155 prim_recTheory.measure_thm] o 156 Q.ISPEC `measure (\cset. list_size LENGTH cset)`) 157 relationTheory.WF_INDUCTION_THM 158 159val exrwt_lemma = prove( 160 ``!c v b fm. fm satisfies_clause FILTER ($~ o binds v) c ==> 161 fm |+ (v,b) satisfies_clause c``, 162 Induct THEN1 SRW_TAC [][satisfies_clause_thm] THEN 163 ASM_SIMP_TAC (srw_ss() ++ DNF_ss) 164 [pairTheory.FORALL_PROD, satisfies_clause_thm, 165 binds_def, finite_mapTheory.FLOOKUP_DEF, 166 finite_mapTheory.FAPPLY_FUPDATE_THM] THEN 167 SRW_TAC [][satisfies_clause_thm, finite_mapTheory.FLOOKUP_DEF, 168 finite_mapTheory.FAPPLY_FUPDATE_THM] THEN 169 FULL_SIMP_TAC (srw_ss()) [] THEN 170 POP_ASSUM MP_TAC THEN SRW_TAC [][]); 171 172val extend_rewrite = store_thm( 173 "extend_rewrite", 174 ``!fm v b. 175 fm satisfies rewrite v b cset ==> (fm |+ (v,b)) satisfies cset``, 176 Induct_on `cset` THEN SRW_TAC [][satisfies_thm, rewrite_def] THENL [ 177 Induct_on `h` THEN1 SRW_TAC [][] THEN 178 ASM_SIMP_TAC (srw_ss() ++ DNF_ss) 179 [pairTheory.FORALL_PROD, satisfies_clause_thm] THEN 180 SRW_TAC [][finite_mapTheory.FLOOKUP_DEF], 181 SRW_TAC [][exrwt_lemma] 182 ]); 183 184val dpll_satisfies = store_thm( 185 "dpll_satisfies", 186 ``!cset fm. (dpll cset = SOME fm) ==> fm satisfies cset``, 187 HO_MATCH_MP_TAC dpll_ind THEN SRW_TAC [][] THEN 188 POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC [dpll_def] THEN 189 SRW_TAC [][] THEN1 SRW_TAC [][satisfies_def] THEN 190 Cases_on `find_uprop cset` THENL [ 191 FULL_SIMP_TAC (srw_ss()) [LET_THM] THEN 192 Cases_on `dpll (rewrite (choose cset) T cset)` THEN 193 FULL_SIMP_TAC (srw_ss()) [] THENL [ 194 Cases_on `dpll (rewrite (choose cset) F cset)` THEN 195 FULL_SIMP_TAC (srw_ss()) [] THEN 196 SRW_TAC [][] THEN SRW_TAC [][extend_rewrite], 197 SRW_TAC [][extend_rewrite] 198 ], 199 FULL_SIMP_TAC (srw_ss()) [] THEN 200 Cases_on `x` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 201 Cases_on `dpll (rewrite q r cset)` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 202 SRW_TAC [][extend_rewrite] 203 ]); 204 205val empty_clause_unsatisfiable = prove( 206 ``!cset. MEM [] cset ==> !fm. ~(fm satisfies cset)``, 207 Induct THEN SRW_TAC [][satisfies_thm] THEN 208 SRW_TAC [][satisfies_clause_thm]); 209 210val option_cond = prove( 211 ``((if p then SOME x else NONE) = SOME y) = p /\ (x = y)``, 212 SRW_TAC [][]); 213 214val fm_gives_value = prove( 215 ``!cset fm v. 216 fm satisfies cset /\ v IN FDOM fm ==> 217 fm satisfies (rewrite v (fm ' v) cset)``, 218 Induct THEN SRW_TAC [][satisfies_thm, rewrite_def] THEN 219 Induct_on `h` THEN1 SRW_TAC [][] THEN 220 ASM_SIMP_TAC (srw_ss() ++ DNF_ss) 221 [pairTheory.FORALL_PROD, binds_def, option_cond, 222 satisfies_clause_thm, finite_mapTheory.FLOOKUP_DEF] THEN 223 SRW_TAC [][satisfies_clause_thm, finite_mapTheory.FLOOKUP_DEF] THEN 224 METIS_TAC []); 225 226val cpos_fm_gives_value = prove( 227 ``v IN FDOM fm /\ ~(fm satisfies (rewrite v (fm ' v) cset)) ==> 228 ~(fm satisfies cset)``, 229 METIS_TAC [fm_gives_value]); 230 231val novbind_lemma = prove( 232 ``~MEM (v,T) h /\ ~MEM (v,F) h ==> (FILTER ($~ o binds v) h = h)``, 233 Induct_on `h` THEN1 SRW_TAC [][] THEN 234 ASM_SIMP_TAC (srw_ss() ++ DNF_ss) 235 [pairTheory.FORALL_PROD, binds_def]); 236 237val partial_clause_1 = prove( 238 ``!h. fm satisfies_clause h /\ 239 ~(fm satisfies_clause FILTER ($~ o binds v) h) ==> 240 ?b. MEM (v,b) h``, 241 Induct THEN 242 ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD, binds_def] THEN 243 SRW_TAC [][satisfies_clause_thm, finite_mapTheory.FLOOKUP_DEF] THEN 244 METIS_TAC []); 245 246val partial_clause_sat = prove( 247 ``!h v b fm. 248 fm satisfies_clause h /\ 249 ~(fm satisfies_clause FILTER ($~ o binds v) h) /\ 250 MEM (v,b) h /\ ~MEM (v,~b) h ==> 251 v IN FDOM fm /\ (fm ' v = b)``, 252 Induct_on `h` THEN1 SRW_TAC [][] THEN 253 ASM_SIMP_TAC (srw_ss()) 254 [pairTheory.FORALL_PROD, binds_def, satisfies_clause_thm, 255 finite_mapTheory.FLOOKUP_DEF] THEN 256 SRW_TAC [][satisfies_clause_thm, finite_mapTheory.FLOOKUP_DEF] THEN 257 TRY (METIS_TAC []) THEN 258 IMP_RES_TAC partial_clause_1 THEN 259 `b = b'` by (Cases_on `b` THEN SRW_TAC [][] THEN 260 Cases_on `b'` THEN SRW_TAC [][] THEN 261 FULL_SIMP_TAC (srw_ss()) []) THEN 262 SRW_TAC [][] THEN METIS_TAC []); 263 264val not_sat_case_split = prove( 265 ``!cset fm. ~(fm satisfies (rewrite v T cset)) /\ 266 ~(fm satisfies (rewrite v F cset)) ==> 267 ~(fm satisfies cset)``, 268 Induct THEN SRW_TAC [][rewrite_def, satisfies_thm] THEN 269 TRY (METIS_TAC [novbind_lemma]) THEN 270 Cases_on `fm satisfies_clause h` THEN SRW_TAC [][] THENL [ 271 `v IN FDOM fm /\ (fm ' v = T)` 272 by (MATCH_MP_TAC partial_clause_sat THEN SRW_TAC [][] THEN 273 METIS_TAC []) THEN 274 MATCH_MP_TAC cpos_fm_gives_value THEN SRW_TAC [][], 275 `v IN FDOM fm /\ (fm ' v = F)` 276 by (MATCH_MP_TAC partial_clause_sat THEN SRW_TAC [][] THEN 277 METIS_TAC []) THEN 278 MATCH_MP_TAC cpos_fm_gives_value THEN SRW_TAC [][] 279 ]); 280 281val case_split_unsat = prove( 282 ``!cset. (!fm. ~(fm satisfies rewrite v F cset)) /\ 283 (!fm. ~(fm satisfies rewrite v T cset)) ==> 284 !fm. ~(fm satisfies cset)``, 285 Induct THEN SRW_TAC [][rewrite_def, satisfies_thm] THEN 286 Cases_on `fm satisfies_clause h` THEN SRW_TAC [][] THENL [ 287 Cases_on `fm satisfies_clause FILTER ($~ o binds v) h` THENL [ 288 `~(fm satisfies rewrite v T cset)` by METIS_TAC [] THEN 289 MATCH_MP_TAC not_sat_case_split THEN SRW_TAC [][], 290 `v IN FDOM fm /\ (fm ' v = F)` 291 by (MATCH_MP_TAC partial_clause_sat THEN SRW_TAC [][] THEN 292 METIS_TAC []) THEN 293 MATCH_MP_TAC cpos_fm_gives_value THEN SRW_TAC [][] 294 ], 295 Cases_on `fm satisfies_clause FILTER ($~ o binds v) h` THENL [ 296 `~(fm satisfies rewrite v F cset)` by METIS_TAC [] THEN 297 MATCH_MP_TAC not_sat_case_split THEN SRW_TAC [][], 298 `v IN FDOM fm /\ (fm ' v = T)` 299 by (MATCH_MP_TAC partial_clause_sat THEN SRW_TAC [][] THEN 300 METIS_TAC []) THEN 301 MATCH_MP_TAC cpos_fm_gives_value THEN SRW_TAC [][] 302 ], 303 `FILTER ($~ o binds v) h = h` by METIS_TAC [novbind_lemma] THEN 304 FULL_SIMP_TAC (srw_ss()) [] THEN 305 METIS_TAC [not_sat_case_split] 306 ]); 307 308val find_uprop_forces = prove( 309 ``!cset. (find_uprop cset = SOME (q, r)) ==> 310 !fm. ~(fm satisfies rewrite q (~r) cset)``, 311 Induct THEN SRW_TAC [][find_uprop_def, satisfies_thm, rewrite_def] THENL [ 312 Cases_on `h` THEN FULL_SIMP_TAC (srw_ss()) [] THENL [ 313 METIS_TAC [], 314 Cases_on `t` THEN FULL_SIMP_TAC (srw_ss()) [] 315 ], 316 Cases_on `h` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 317 SRW_TAC [][binds_def] THEN 318 Cases_on `t` THEN FULL_SIMP_TAC (srw_ss()) [satisfies_clause_thm] 319 ]); 320 321val dpll_unsatisfied = store_thm( 322 "dpll_unsatisfied", 323 ``!cset. (dpll cset = NONE) ==> !fm. ~(fm satisfies cset)``, 324 HO_MATCH_MP_TAC dpll_ind THEN GEN_TAC THEN STRIP_TAC THEN 325 ONCE_REWRITE_TAC [dpll_def] THEN 326 SRW_TAC [][empty_clause_unsatisfiable] THEN 327 Cases_on `find_uprop cset` THENL [ 328 FULL_SIMP_TAC (srw_ss()) [LET_THM] THEN 329 Cases_on `dpll (rewrite (choose cset) T cset)` THEN 330 FULL_SIMP_TAC (srw_ss()) [] THEN 331 Cases_on `dpll (rewrite (choose cset) F cset)` THEN 332 FULL_SIMP_TAC (srw_ss()) [] THEN 333 METIS_TAC [case_split_unsat], 334 FULL_SIMP_TAC (srw_ss()) [] THEN 335 Cases_on `x` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 336 Cases_on `dpll (rewrite q r cset)` THEN 337 FULL_SIMP_TAC (srw_ss()) [] THEN 338 IMP_RES_TAC find_uprop_forces THEN 339 Cases_on `r` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 340 METIS_TAC [case_split_unsat] 341 ]); 342 343val _ = EVAL ``dpll [[(1,T); (2,F); (3,T)]; [(1,F); (2,T)]]`` 344 345(* using the DPLL algorithm on HOL's boolean formula's via "reflection" *) 346(* it seems necessary to push the variable type through a substitution, mapping 347 into a type that will allow the "variables" of the original formula to be 348 compared with each other without worrying about their semantic content *) 349val interpret_clause_def = Define` 350 (interpret_clause f [] = F) /\ 351 (interpret_clause f ((h : 'a # bool) :: t) = 352 (f (FST h) = SND h) \/ interpret_clause f t) 353` 354val _ = export_rewrites ["interpret_clause_def"] 355 356val interpret_def = Define` 357 (interpret f [] = T) /\ 358 (interpret f (c::cs) = interpret_clause f c /\ interpret f cs) 359`; 360val _ = export_rewrites ["interpret_def"] 361 362val empty_clause_interpret = store_thm( 363 "empty_clause_interpret", 364 ``!cs. MEM [] cs ==> ~interpret f cs``, 365 Induct THEN SRW_TAC [][] THEN SRW_TAC [][]); 366 367val iclause_rewrite = store_thm( 368 "iclause_rewrite", 369 ``!c v. ~MEM (v,f v) c /\ interpret_clause f c ==> 370 interpret_clause f (FILTER ($~ o binds v) c)``, 371 Induct THEN1 SRW_TAC [][] THEN 372 ASM_SIMP_TAC (srw_ss() ++ DNF_ss) [pairTheory.FORALL_PROD, binds_def] THEN 373 SRW_TAC [][] THEN METIS_TAC []); 374 375val interpret_rewrite = store_thm( 376 "interpret_rewrite", 377 ``!cs v b. (f v = b) /\ interpret f cs ==> 378 interpret f (rewrite v b cs)``, 379 Induct THEN SRW_TAC [][rewrite_def] THEN METIS_TAC [iclause_rewrite]); 380 381val interpret_uprop = store_thm( 382 "interpret_uprop", 383 ``(find_uprop cs = SOME (q,r)) ==> ~interpret f (rewrite q (~r) cs)``, 384 Induct_on `cs` THEN SRW_TAC [][find_uprop_def, rewrite_def] THENL [ 385 Cases_on `h` THEN FULL_SIMP_TAC (srw_ss()) [] THENL [ 386 Cases_on `r` THEN FULL_SIMP_TAC (srw_ss()) [], 387 Cases_on `t` THEN FULL_SIMP_TAC (srw_ss()) [] 388 ], 389 Cases_on `h` THEN FULL_SIMP_TAC (srw_ss()) [binds_def] THEN 390 Cases_on `t` THEN FULL_SIMP_TAC (srw_ss()) [binds_def] 391 ]); 392 393(* might equally be able to get conclusion from !fm. ~(fm satisfies cs) *) 394val dpll_interpret = store_thm( 395 "dpll_interpret", 396 ``!cs f. (dpll cs = NONE) ==> (interpret f cs = F)``, 397 HO_MATCH_MP_TAC dpll_ind THEN GEN_TAC THEN STRIP_TAC THEN 398 ONCE_REWRITE_TAC [dpll_def] THEN SRW_TAC [][empty_clause_interpret] THEN 399 Cases_on `find_uprop cs` THENL [ 400 FULL_SIMP_TAC (srw_ss()) [LET_THM] THEN 401 Cases_on `dpll (rewrite (choose cs) T cs)` THEN 402 FULL_SIMP_TAC (srw_ss()) [] THEN 403 Cases_on `dpll (rewrite (choose cs) F cs)` THEN 404 FULL_SIMP_TAC (srw_ss()) [] THEN 405 METIS_TAC [interpret_rewrite], 406 FULL_SIMP_TAC (srw_ss()) [] THEN 407 Cases_on `x` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 408 Cases_on `dpll (rewrite q r cs)` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 409 `~interpret f (rewrite q (~r) cs)` by METIS_TAC [interpret_uprop] THEN 410 Cases_on `r` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 411 METIS_TAC [interpret_rewrite] 412 ]); 413 414val t0 = `` (((~a \/ p /\ ~q \/ ~p /\ q) /\ 415 (~(p /\ ~q \/ ~p /\ q) \/ a)) /\ 416 (~c \/ p /\ q) /\ (~(p /\ q) \/ c)) /\ 417 ~(~(p /\ q) \/ c /\ ~a)`` 418val t = rhs (concl 419 (SIMP_CONV bool_ss [LEFT_OR_OVER_AND, RIGHT_OR_OVER_AND, 420 GSYM CONJ_ASSOC, GSYM DISJ_ASSOC, 421 DE_MORGAN_THM] t0)) 422 423(* t must not only be in CNF, but with boolean operators right associated *) 424fun prove_cnf_unsat t = let 425 val cs = strip_conj t 426 val vars = free_vars t 427 val f = ``\n. EL n ^(listSyntax.mk_list(vars, bool))`` 428 fun var2n v = numSyntax.mk_numeral (Arbnum.fromInt (index (aconv v) vars)) 429 fun mk_clause c = let 430 val ds = strip_disj c 431 fun mkatom t = if is_neg t then ``(^(var2n (dest_neg t)), F)`` 432 else ``(^(var2n t), T)`` 433 in 434 listSyntax.mk_list(map mkatom ds, ``:num # bool``) 435 end 436 val clauses = listSyntax.mk_list (map mk_clause cs, ``:(num # bool) list``) 437 val th1 = SIMP_CONV (srw_ss()) [] ``interpret ^f ^clauses`` 438 val _ = aconv t (rhs (concl th1)) orelse raise Fail "translation failed" 439 val th2 = EVAL ``dpll ^clauses`` 440in 441 if is_const (rhs (concl th2)) then 442 TRANS (SYM th1) (ISPEC f (MATCH_MP dpll_interpret th2)) 443 else raise Fail "formula is propositionally satisfiable" 444end 445 446(* 0.3 seconds *) 447val example = time prove_cnf_unsat t 448 449val _ = export_theory(); 450