1(* 2UOK Formalises (an improvement of) the main result in: 3UOK "Solving Problems with Finite Test Sets" 4UOK by Cristian S. Calude, Helmut J��rgensen, Shane Legg 5UOK 6UOK namely: 7UOK Every first-order formula (in prenex normal form) over the natural numbers is 8UOK "solved" by a single instance. 9UOK 10UOK Given a formula f in prenex normal form 11UOK 12UOK f := Qx1.Qx2....Qxs. P(x1,...,xs) (each Q in {���,���}), 13UOK 14UOK a "test instance" (n1,...,ns) is a valuation such that 15UOK 16UOK f is true iff P(n1,...,ns) is true 17UOK 18UOK The main result proved here is that every formula has a test instance. 19UOK 20UOK Thus, every first-order formula can be decided by checking a single instance. 21UOK This sounds surprising at first, until you realise what is not shown: how to 22UOK construct the test instance. 23UOK 24UOK The result in the paper is weaker: 25UOK Rather than a single instance, they show solvability by a finite test set. 26UOK A "test set" is a set T of instances such that 27UOK f is true iff f is true over T 28UOK where "f is true over T" means f is true when the quantifiers are relativised 29UOK to the domains represented by T. 30UOK 31UOK We prove their result as a corollary. 32*) 33 34open HolKernel boolLib boolSimps bossLib Parse mp_then 35 combinTheory listTheory rich_listTheory pred_setTheory 36 37val _ = temp_tight_equality(); 38 39val _ = new_theory "finite_test_set"; 40 41(* 42 Since we only care about prenex normal formulae, we design our datatypes to 43 represent these directly. First, quantifier-free formulae with de Bruijn 44 variables and a single Sheffer connective. 45*) 46 47(* Function "symbols" carry their semantics to avoid pointless naming. *) 48val _ = Datatype` 49 term = Var num | Fun (num list -> num) (term list)`; 50 51(* Similarly predicate symbols carry their semantics *) 52val _ = Datatype` 53 prop = Pred (num list -> bool) (term list) | Nand prop prop`; 54 55(* Note: this makes the language rather more expressive than desired. 56 We usually want f in (Fun f) and (Pred f) to be decidable. 57 However, this does not sabotage our main results: if these expressive 58 formulae are solvable, then in particular so are the less expressive ones. *) 59 60(* Semantics of quantifier-free formulae *) 61 62val val_term_def = tDefine"val_term"` 63 val_term env (Var n) = EL n env ��� 64 val_term env (Fun f ts) = f (MAP (val_term env) ts)` 65(WF_REL_TAC`measure (term_size o SND)` \\ Induct \\ EVAL_TAC 66 \\ rw[] \\ res_tac \\ rw[]); 67val _ = export_rewrites["val_term_def"]; 68 69val val_prop_def = Define` 70 val_prop env (Pred f ts) = f (MAP (val_term env) ts) ��� 71 val_prop env (Nand p1 p2) = ��(val_prop env p1 ��� val_prop env p2)`; 72val _ = export_rewrites["val_prop_def"]; 73 74(* Now we add quantifiers *) 75 76val _ = Datatype` 77 quan = Forall | Exists`; 78 79val _ = type_abbrev("form",``:quan list # prop``); 80 81val val_form_aux_def = tDefine"val_form_aux"` 82 val_form_aux ([],p) env = val_prop env p ��� 83 val_form_aux (Forall::qs,p) env = (���n. val_form_aux (qs,p) (n::env)) ��� 84 val_form_aux (Exists::qs,p) env = (���n. val_form_aux (qs,p) (n::env))` 85(WF_REL_TAC`measure (LENGTH o FST o FST)` \\ rw[]); 86val _ = export_rewrites["val_form_aux_def"]; 87 88val val_form_def = Define` 89 val_form (qs,p) = val_form_aux (qs,p) []`; 90 91(* A test of expressiveness: Goldbach's conjecture can be represented *) 92open dividesTheory 93 94val Goldbach_statement_def = Define` 95 Goldbach_statement ��� 96 ���n. 2 < n ��� EVEN n ��� ���p1 p2. prime p1 ��� prime p2 ��� n = p1 + p2`; 97 98(* This is unnecessary: everything could be built into the predicates themselves *) 99val _ = overload_on("Or",``��p1 p2. Nand (Nand p1 p1) (Nand p2 p2)``); 100 101val Goldbach_Pi1 = Q.store_thm("Goldbach_Pi1", 102 `���p. (* it would be nice to also say that p is decidable: this is true, 103 but the theory to express this fact isn't around to my knowledge *) 104 val_form ([Forall],p) ��� Goldbach_statement`, 105 qexists_tac` 106 Or (Pred ((��n. ��(2 < n ��� EVEN n)) o HD) [Var 0]) 107 (Pred ((��n. ���p1 p2. prime p1 ��� prime p2 ��� n = p1 + p2) o HD) [Var 0])` 108 \\ rw[val_form_def,Goldbach_statement_def] 109 \\ metis_tac[]); 110 111(* Solvability by a single instance *) 112 113(* 114 env is a test instance for f [= (qs,p)] if 115 f is true ��� p[env] is true 116*) 117val test_inst_def = Define` 118 test_inst env (qs,p) ��� 119 (LENGTH env = LENGTH qs) ��� 120 (val_form (qs,p) ��� val_prop env p)`; 121 122val solvable_def = Define` 123 solvable f ��� ���env. test_inst env f`; 124 125(* Non-constructive definition of test instances *) 126 127val nu_def = Define` 128 nu env Forall qs p = 129 (if val_form_aux (Forall::qs,p) env then 0 130 else LEAST m. ��val_form_aux (qs,p) (m::env)) ��� 131 nu env Exists qs p = 132 (if ��val_form_aux (Exists::qs,p) env then 0 133 else LEAST m. val_form_aux (qs,p) (m::env))`; 134 135val mk_test_inst_def = Define` 136 mk_test_inst env [] p = env ��� 137 mk_test_inst env (q::qs) p = 138 mk_test_inst ((nu env q qs p)::env) qs p`; 139 140val LENGTH_mk_test_inst = Q.store_thm("LENGTH_mk_test_inst[simp]", 141 `���qs env p. LENGTH (mk_test_inst env qs p) = LENGTH env + LENGTH qs`, 142 Induct \\ rw[mk_test_inst_def] \\ rw[]); 143 144val mk_test_inst_acc = Q.store_thm("mk_test_inst_acc", 145 `���qs env. ���env'. mk_test_inst env qs p = env'++env`, 146 Induct 147 \\ rw[mk_test_inst_def] 148 \\ metis_tac[CONS_APPEND,APPEND_ASSOC]); 149 150val val_mk_test_inst = Q.store_thm("val_mk_test_inst", 151 `���qs0 env qs1 p. 152 (val_form_aux (qs1,p) (DROP (LENGTH qs1) (mk_test_inst env (qs0 ++ qs1) p)) 153 ��� 154 val_form_aux (qs0 ++ qs1,p) env)`, 155 Induct \\ rw[mk_test_inst_def] 156 >- ( 157 qspecl_then[`qs1`,`env`]strip_assume_tac mk_test_inst_acc 158 \\ qspecl_then[`qs1`,`env`,`p`]mp_tac LENGTH_mk_test_inst 159 \\ pop_assum SUBST_ALL_TAC 160 \\ rw[DROP_APPEND,DROP_LENGTH_NIL_rwt] ) 161 \\ qmatch_goalsub_rename_tac`nu env q` 162 \\ Cases_on`q` \\ rw[] 163 \\ rw[nu_def] 164 \\ numLib.LEAST_ELIM_TAC 165 \\ metis_tac[] ); 166 167(* The main result *) 168 169val all_solvable = Q.store_thm("all_solvable", 170 `���f. solvable f`, 171 rw[solvable_def] 172 \\ Cases_on`f` 173 \\ qmatch_goalsub_rename_tac`(qs,p)` 174 \\ qexists_tac`mk_test_inst [] qs p` 175 \\ rw[test_inst_def] 176 \\ qspecl_then[`qs`,`[]`,`[]`,`p`]mp_tac val_mk_test_inst 177 \\ rw[val_form_def]); 178 179(* Solvability by test sets (as in the paper) *) 180 181(* relativising a formula *) 182 183val val_form_rel_def = Define` 184 val_form_rel [] ([],p) env = val_prop env p ��� 185 val_form_rel (d::ds) (Forall::qs,p) env = (���n::d. val_form_rel ds (qs,p) (n::env)) ��� 186 val_form_rel (d::ds) (Exists::qs,p) env = (���n::d. val_form_rel ds (qs,p) (n::env))` 187val _ = export_rewrites["val_form_rel_def"]; 188 189val val_form_iff_val_form_rel = Q.store_thm("val_form_iff_val_form_rel", 190 `val_form (qs,p) ��� val_form_rel (REPLICATE (LENGTH qs) UNIV) (qs,p) []`, 191 rw[val_form_def] 192 \\ qspec_tac(`[]:num list`,`env`) 193 \\ qid_spec_tac`qs` 194 \\ Induct \\ rw[] 195 \\ qmatch_goalsub_rename_tac`q::qs` 196 \\ Cases_on`q` \\ fs[RES_FORALL_THM,RES_EXISTS_THM]); 197 198(* A test set is a domain relativised to which a formula's truth is preserved *) 199 200val test_set_def = Define` 201 test_set ds (qs,p) ��� 202 (LENGTH ds = LENGTH qs) ��� 203 (val_form (qs,p) ��� val_form_rel ds (qs,p) [])`; 204 205(* 206 We are representing test sets as a list of domains for the quantifiers. 207 Here is how to retrieve the corresponding subset of the Cartesian product 208 N^(LENGTH qs) (represented as a list rather than actual tuples) 209*) 210val domains_to_set_def = Define 211 `domains_to_set ds = { ms | LIST_REL (IN) ms ds }`; 212 213(* Finitely solvable = has a finite test set *) 214val finitely_solvable_def = Define` 215 finitely_solvable q ��� 216 ���ds. test_set ds q ��� FINITE (domains_to_set ds)`; 217 218val FINITE_domains_to_set = Q.store_thm("FINITE_domains_to_set", 219 `FINITE (domains_to_set ds) ��� (EVERY FINITE ds ��� EXISTS ((=){}) ds)`, 220 rw[domains_to_set_def] 221 \\ Induct_on`ds` \\ rw[] 222 \\ qmatch_abbrev_tac`FINITE s ��� _` 223 \\ qmatch_goalsub_rename_tac`FINITE d ��� EVERY FINITE ds` 224 \\ qmatch_assum_abbrev_tac`FINITE ms ��� EVERY FINITE ds ��� _` 225 \\ `BIJ (��ls. (HD ls, TL ls)) s (d �� ms)` 226 by ( 227 simp[BIJ_IFF_INV] 228 \\ conj_tac >- ( 229 simp[Abbr`s`,Abbr`ms`,PULL_EXISTS] ) 230 \\ qexists_tac`��p. (FST p :: SND p)` 231 \\ simp[Abbr`s`,Abbr`ms`,PULL_EXISTS] ) 232 \\ Cases_on`d = ���` \\ fs[] 233 \\ `ms = ��� ��� EXISTS ((=){}) ds` 234 by ( 235 simp[Abbr`ms`] 236 \\ simp[EXTENSION] 237 \\ simp[EXISTS_MEM,LIST_REL_EL_EQN,MEM_EL] 238 \\ metis_tac[NOT_IN_EMPTY,CHOICE_DEF,EL_MAP,LENGTH_MAP] ) 239 \\ metis_tac[FINITE_BIJ,FINITE_CROSS_EQ,BIJ_INV] ); 240 241val test_inst_test_set = Q.store_thm("test_inst_test_set", 242 `test_inst env f ��� test_set (MAP (��m. {m}) (REVERSE env)) f`, 243 Cases_on`f` \\ rw[test_inst_def,test_set_def] 244 \\ qmatch_goalsub_rename_tac`val_form (qs,p)` 245 \\ Cases_on`LENGTH env = LENGTH qs` \\ fs[] 246 \\ AP_TERM_TAC 247 \\ pop_assum mp_tac 248 \\ Q.ISPEC_THEN`env`(SUBST_ALL_TAC o SYM) REVERSE_REVERSE 249 \\ qspec_tac(`REVERSE env`,`env`) \\ simp[] \\ gen_tac 250 \\ `val_prop (REVERSE env) = val_prop (REVERSE env ++ [])` by simp[] 251 \\ pop_assum SUBST_ALL_TAC 252 \\ qspec_tac(`[] : num list`,`env0`) 253 \\ map_every qid_spec_tac [`qs`,`env`] 254 \\ Induct \\ rw[] 255 \\ Cases_on`qs` \\ fs[] 256 \\ qmatch_goalsub_rename_tac`q::qs,p` 257 \\ qmatch_goalsub_rename_tac`{m}` 258 \\ first_x_assum(qspecl_then[`qs`,`[m] ++ env0`]mp_tac) 259 \\ Cases_on`q` \\ fs[RES_FORALL_THM,RES_EXISTS_THM]); 260 261val all_finitely_solvable = Q.store_thm("all_finitely_solvable", 262 `���f. finitely_solvable f`, 263 rw[finitely_solvable_def] 264 \\ qspec_then`f`mp_tac all_solvable 265 \\ rw[solvable_def] 266 \\ fs[test_inst_test_set] 267 \\ goal_assum(first_assum o mp_then Any mp_tac) 268 \\ simp[FINITE_domains_to_set,EVERY_MEM,MEM_MAP,PULL_EXISTS]); 269 270val _ = export_theory (); 271