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