1(* ========================================================================= *) 2(* FILE : mleDiophProve.sml *) 3(* DESCRIPTION : Verifying that a set corresponds to its description by *) 4(* a Diophantine equation. *) 5(* AUTHOR : (c) Thibault Gauthier, Czech Technical University *) 6(* DATE : 2020 *) 7(* ========================================================================= *) 8 9structure mleDiophProve :> mleDiophProve = 10struct 11 12open HolKernel Abbrev boolLib aiLib numTheory arithmeticTheory 13pred_setTheory numSyntax 14 15val ERR = mk_HOL_ERR "mleDiophProve" 16val selfdir = HOLDIR ^ "/examples/AI_tasks" 17 18(* ------------------------------------------------------------------------- 19 Useful terms and provers 20 ------------------------------------------------------------------------- *) 21 22val pred = mk_var ("p",``:num -> bool``) 23val vk = mk_var ("k",``:num``) 24val vx = mk_var ("x",``:num``) 25val vy = mk_var ("y",``:num``) 26val vz = mk_var ("z",``:num``) 27val vn = mk_var ("n",``:num``) 28val cP = mk_var ("p",``:num -> bool``); 29val cQ = mk_var ("q",``:num -> bool``); 30 31val disj16 = list_mk_disj 32 (List.tabulate (16, fn i => (mk_eq (vn,term_of_int i)))); 33 34val tm16 = term_of_int 16 35fun mod16 x = mk_mod (x,tm16) 36fun less16 x = mk_less (x,tm16) 37fun eq0 x = mk_eq (mod16 x, zero_tm) 38fun diff0 x = mk_neg (mk_eq (mod16 x, zero_tm)) 39fun rep16 x = {redex = x, residue = mod16 x} 40 41fun PROVE_EVAL tm = EQT_ELIM (EVAL tm) 42 43fun inst_v16 v thm = INST [{redex = v, residue = mk_mod (v,tm16)}] thm 44 45(* ------------------------------------------------------------------------- 46 Case distinction theorems 47 ------------------------------------------------------------------------- *) 48 49val goal:goal = ([], mk_eq (``n < 16``, disj16)); 50 51fun CASES_LEFT_TAC goal = 52 let val v = hd (free_vars_lr (snd goal)) in 53 (SPEC_TAC (v,v) THEN Cases THENL [simp [],ALL_TAC]) goal 54 end 55 56val LESS16 = TAC_PROOF (([],mk_eq (less16 vn,disj16)), 57 NTAC 16 CASES_LEFT_TAC THEN simp []); 58 59val MOD16 = 60 let val thm = TAC_PROOF (([],``n MOD 16 < 16``), simp []) in 61 MATCH_MP (fst (EQ_IMP_RULE LESS16)) thm 62 end 63 64val plenum = List.tabulate (16, fn x => mk_comb(cP,term_of_int x)) 65val plgen = mk_imp (list_mk_conj plenum, mk_comb(cP,vn)) 66val PRED16 = PROVE_HYP MOD16 67 (inst_v16 vn (TAC_PROOF (([disj16],plgen), METIS_TAC []))); 68 69(* ------------------------------------------------------------------------- 70 Proves that a solution exists 71 ------------------------------------------------------------------------- *) 72 73val triplesubl = 74 let 75 val l = List.tabulate (16,I) 76 val triplel = map triple_of_list (cartesian_productl [l,l,l]) 77 fun f (a,b,c) = 78 [{redex = vx, residue = term_of_int a}, 79 {redex = vy, residue = term_of_int b}, 80 {redex = vz, residue = term_of_int c}] 81 in 82 map f triplel 83 end 84 85fun EXISTS_TRIPLE_TAC (xw,yw,zw) goal = 86 let 87 val sub = [{redex = vx, residue = xw}, 88 {redex = vy, residue = yw}, 89 {redex = vz, residue = zw}] 90 val thm = PROVE_EVAL (subst sub (snd (strip_exists (snd goal)))) 91 in 92 (EXISTS_TAC xw THEN EXISTS_TAC yw THEN EXISTS_TAC zw THEN ACCEPT_TAC thm) 93 goal 94 end 95 96fun POLY_EXISTS_SOL poly = 97 let 98 val poly16 = subst (map rep16 [vx,vy,vz]) poly 99 val instl = map_assoc (C subst poly) triplesubl 100 fun is_provable x = term_eq T (rhs (concl (EVAL (eq0 x)))) 101 val (sub,_) = valOf (List.find (is_provable o snd) instl) 102 val (xw,yw,zw) = triple_of_list (map #residue sub) 103 in 104 TAC_PROOF (([], list_mk_exists ([vx,vy,vz],eq0 poly16)), 105 EXISTS_TRIPLE_TAC (xw,yw,zw)) 106 end 107 108(* 109load "mleDiophProve"; open mleDiophProve; 110val poly = ``2 + 14 * x * y * z``; 111val thm = POLY_EXISTS_SOL poly; 112*) 113 114(* ------------------------------------------------------------------------- 115 Proves that a solution does not exist 116 ------------------------------------------------------------------------- *) 117 118fun enumvar v tm = (tm, List.tabulate (16, 119 fn x => subst [{redex = v, residue = term_of_int x}] tm)) 120 121fun forall_enum v (gen,thml) = 122 let 123 val instthm = INST [{redex = cP, residue = mk_abs (v, diff0 gen)}, 124 {redex = vn, residue = v}] PRED16 125 val convthm = UNDISCH (CONV_RULE (TOP_DEPTH_CONV BETA_CONV) instthm) 126 in 127 PROVE_HYP (LIST_CONJ thml) convthm 128 end 129 130fun forall_enumz (gen,thml) = 131 forall_enum vz (gen,thml) 132fun forall_enumy (gen,thml) = 133 forall_enum vy (subst [rep16 vz] gen, thml) 134fun forall_enumx (gen,thml) = 135 forall_enum vx (subst (map rep16 [vy,vz]) gen, thml) 136 137fun POLY_NEG_EXISTS_SOL poly = 138 let 139 val polyx = [enumvar vx poly] 140 val polyxy = map_snd (map (enumvar vy)) polyx 141 val polyxyz = (map_snd (map_snd (map (enumvar vz)))) polyxy 142 val polyxyzthm = 143 (map_snd (map_snd (map_snd (map (PROVE_EVAL o diff0))))) polyxyz 144 val polyxythm = map_snd (map_snd (map forall_enumz)) polyxyzthm 145 val polyxthm = map_snd (map forall_enumy) polyxythm 146 val polythm = singleton_of_list (map forall_enumx polyxthm) 147 val poly16 = subst (map rep16 [vx,vy,vz]) poly 148 val negex = mk_neg (list_mk_exists ([vx,vy,vz], eq0 poly16)) 149 val convthm = normalForms.PURE_NNF_CONV negex 150 in 151 MP (snd (EQ_IMP_RULE convthm)) (GENL [vx,vy,vz] polythm) 152 end 153 154(* 155load "mleDiophProve"; open mleDiophProve; 156val poly = ``1 + 14 * x * y * z``; 157val thm = POLY_NEG_EXISTS_SOL poly; 158*) 159 160(* ------------------------------------------------------------------------- 161 Express the verified formula as an equality between sets 162 ------------------------------------------------------------------------- *) 163 164val PQ16 = 165 let 166 fun mk_pq i = 167 mk_eq (mk_comb (cP, term_of_int i), mk_comb (cQ, term_of_int i)); 168 val pqconjl = list_mk_conj (List.tabulate (16,mk_pq)); 169 val goal = ([pqconjl],``(\k. k < 16 /\ p k) = (\n. n < 16 /\ q n)``) 170 in 171 TAC_PROOF 172 (goal, ABS_TAC THEN CONV_TAC (REWRITE_CONV [LESS16]) THEN METIS_TAC []) 173 end 174 175val PQSET16 = 176 let val thm = METIS_PROVE [] 177 ``((p :num -> bool) = q) ==> ({u :num | p u} = {v :num | q v})`` 178 in 179 HO_MATCH_MP thm PQ16 180 end 181 182fun ENUMSET il = 183 let 184 val disj = list_mk_disj (map (fn x => mk_eq (vn,term_of_int x)) il) 185 val a = pred_setSyntax.mk_set_spec (vn,disj) 186 val b = pred_setSyntax.mk_set (map term_of_int il) 187 in 188 TAC_PROOF (([],mk_eq (a,b)), simp [EXTENSION,IN_SING,IN_INSERT]) 189 end 190 191fun CONJLESS16 il = 192 let 193 val disj = list_mk_disj (map (fn x => mk_eq (vn,term_of_int x)) il) 194 val disjless = mk_conj (less16 vn, disj) 195 in 196 TAC_PROOF (([],mk_eq (disjless,disj)), METIS_TAC [LESS16]) 197 end 198 199(* ------------------------------------------------------------------------- 200 Prove that the two predicates are equal on the same input 201 ------------------------------------------------------------------------- *) 202 203fun PROVE_PQEQ poly il k = 204 let 205 val disj = list_mk_disj (map (fn x => mk_eq (vn,term_of_int x)) il) 206 val qdef = mk_abs (vn, disj) 207 val poly16 = subst (map rep16 [vx,vy,vz]) poly 208 val pdef = mk_abs (vk, list_mk_exists ([vx,vy,vz], eq0 poly16)) 209 val convthm = BETA_CONV (mk_comb (pdef,term_of_int k)) 210 val thm1 = 211 let val polyk = subst [{redex = vk, residue = term_of_int k}] poly in 212 if mem k il 213 then POLY_EXISTS_SOL polyk 214 else POLY_NEG_EXISTS_SOL polyk 215 end 216 val thm1' = PURE_ONCE_REWRITE_RULE [SYM convthm] thm1 217 val qtm = mk_comb (qdef,term_of_int k) 218 val tac = CONV_TAC (TOP_DEPTH_CONV BETA_CONV) THEN DECIDE_TAC 219 val thm2 = if mem k il 220 then TAC_PROOF (([],qtm), tac) 221 else TAC_PROOF (([],mk_neg qtm), tac) 222 val predeq = mk_eq (mk_comb (pdef,term_of_int k), 223 mk_comb (qdef,term_of_int k)) 224 in 225 METIS_PROVE [thm1',thm2] predeq 226 end 227 228(* ------------------------------------------------------------------------- 229 Verify that the polynomial describes the set 230 ------------------------------------------------------------------------- *) 231 232fun DIOPH_PROVE (poly,il) = 233 let 234 val pql = List.tabulate (16, PROVE_PQEQ poly il) 235 val pq = LIST_CONJ pql 236 val pdef = (rator o lhs o concl o hd) pql 237 val qdef = (rator o rhs o concl o hd) pql 238 val inst = (INST [{redex = cP, residue = pdef}, 239 {redex = cQ, residue = qdef}] PQSET16) 240 val seteq = PROVE_HYP pq inst 241 val reduce = CONV_RULE (TOP_DEPTH_CONV BETA_CONV) seteq 242 val rmless16 = PURE_ONCE_REWRITE_RULE [CONJLESS16 il] reduce 243 in 244 PURE_ONCE_REWRITE_RULE [ENUMSET il] rmless16 245 end 246 247(* 248load "mleDiophProve"; open mleDiophProve; 249val poly = ``k + 14 * x * y * z``; 250val il = [0,2,4,6,8,10,12,14]; 251val thm = DIOPH_PROVE (poly,il); 252*) 253 254(* ------------------------------------------------------------------------- 255 Verify the solutions produced during evaluation. 256 ------------------------------------------------------------------------- *) 257 258(* 259load "aiLib"; open aiLib; 260load "mleDiophLib"; open mleDiophLib; 261load "mleDiophSynt"; open mleDiophSynt; 262load "mleDiophProve"; open mleDiophProve; 263 264val dir2 = HOLDIR ^ "/examples/AI_tasks/dioph_results_nolimit/test_tnn"; 265fun g i = #read_result ft_extsearch_uniform (dir2 ^ "/" ^ its i); 266val boardl = mapfilter (valOf o #3) (List.tabulate (200,g)); length boardl; 267val pairl = map (fn (a,b,_) => (veri_of_poly a, graph_to_il b)) boardl; 268 269fun f i x = (print_endline (its i); DIOPH_PROVE x); 270val (thml,t) = add_time (mapi f) pairl; length thml; 271 272fun f_charl cl = case cl of 273 [] => [] 274 | [a] => [a] 275 | a :: b :: m => if Char.isSpace a andalso Char.isSpace b 276 then f_charl (b :: m) 277 else if Char.isSpace a 278 then #" " :: f_charl (b :: m) 279 else a :: f_charl (b :: m) 280; 281val minspace = implode o f_charl o explode; 282val _ = writel (dir2 ^ "/theorems") (map (minspace o string_of_goal o dest_thm) thml); 283*) 284 285end (* struct *) 286 287