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