diff options
Diffstat (limited to 'backends/hol4')
| -rw-r--r-- | backends/hol4/divDefLib.sml | 890 | ||||
| -rw-r--r-- | backends/hol4/primitivesBaseTacLib.sml | 99 | ||||
| -rw-r--r-- | backends/hol4/primitivesLib.sml | 45 | ||||
| -rw-r--r-- | backends/hol4/primitivesScript.sml | 4 | ||||
| -rw-r--r-- | backends/hol4/primitivesTheory.sig | 22 | ||||
| -rw-r--r-- | backends/hol4/testHashmapScript.sml | 14 | ||||
| -rw-r--r-- | backends/hol4/testHashmapTheory.sig | 18 | ||||
| -rw-r--r-- | backends/hol4/testScript.sml | 9 | ||||
| -rw-r--r-- | backends/hol4/testTheory.sig | 5 |
9 files changed, 995 insertions, 111 deletions
diff --git a/backends/hol4/divDefLib.sml b/backends/hol4/divDefLib.sml new file mode 100644 index 00000000..bfd36af1 --- /dev/null +++ b/backends/hol4/divDefLib.sml @@ -0,0 +1,890 @@ +(* This file implements utilities to define potentially diverging functions *) + +open HolKernel boolLib bossLib Parse +open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory + +open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory +open primitivesLib + +(* TODO: +pred_def_thms -> pred_defs +pred_def_thm -> pred_def +raw_def_thms -> raw_defs +raw_def_thm -> raw_def + +fuel_defs_thm -> fuel_defs (and split the theorem) +*) + +(* TotalDefn.Define *) + +(* +Datatype: + list_t = + ListCons 't list_t + | ListNil +End +*) + +(* TODO: move *) +fun list_mk_arrow (tys : hol_type list) (ret_ty : hol_type) : hol_type = + foldr (fn (ty, aty) => ty --> aty) ret_ty tys + +(*“test (x : bool) = (x <> F)” *) + +val def_qt = ‘ + (even (i : int) : bool result = + if i = 0 then Return T else odd (i - 1)) /\ + (odd (i : int) : bool result = + if i = 0 then Return F else even (i - 1)) +’ +val def_tms = (strip_conj o list_mk_conj o rev) (Defn.parse_quote def_qt) +val def_tm = hd def_tms + +(* Small utilities *) +val current_goal : term option ref = ref NONE + +(* Save a goal in {!current_goal} then prove it. + + This way if the proof fails we can easily retrieve the goal for debugging + purposes. + *) +fun save_goal_and_prove (g, tac) : thm = + let + val _ = current_goal := SOME g + in + prove (g, tac) + end + + +(*val def_qt = ‘ +(nth_fuel (n : num) (ls : 't list_t) (i : u32) : 't result = + case n of + | 0 => Loop + | SUC n => + do case ls of + | ListCons x tl => + if u32_to_int i = (0:int) + then Return x + else + do + i0 <- u32_sub i (int_to_u32 1); + nth_fuel n tl i0 + od + | ListNil => + Fail Failure + od) +’*) + +val num_zero_tm = “0:num” +val num_suc_tm = “SUC: num -> num” +val num_ty = “:num” + +val fuel_def_suffix = "___fuel" (* TODO: name collisions *) +val fuel_var_name = "$n" (* TODO: name collisions *) +val fuel_var = mk_var (fuel_var_name, num_ty) +val fuel_var0 = fuel_var +val fuel_var1 = mk_var ("$m", “:num”) (* TODO: name collisions *) +val fuel_vars_le = “^fuel_var0 <= ^fuel_var1” + +val fuel_predicate_suffix = "___P" (* TODO: name collisions *) + +val bool_ty = “:bool” + +val alpha_tyvar : hol_type = “:'a” +val is_diverge_def = Define ‘ + is_diverge (r: 'a result) : bool = case r of Diverge => T | _ => F’ +val is_diverge_tm = “is_diverge: 'a result -> bool” +val diverge_tm = “Diverge : 'a result” + +val least_tm = “$LEAST” +val le_tm = (fst o strip_comb) “x:num <= y:num” +val true_tm = “T” +val false_tm = “F” + +fun mk_diverge_tm (ty : hol_type) : term = + let + val diverge_ty = mk_thy_type {Thy="primitives", Tyop="result", Args = [ty] } + val diverge_tm = mk_thy_const { Thy="primitives", Name="Diverge", Ty=diverge_ty } + in + diverge_tm + end + +fun mk_fuel_defs (def_tms : term list) : thm = + let + (* Retrieve the identifiers. + + Ex.: def_tm = “even (n : int) : bool result = if i = 0 then Return T else odd (i - 1))” + We want to retrive: id = “even” + *) + val app = lhs def_tm + val ids = map (fst o strip_comb o lhs) def_tms + (* In the definitions, replace the identifiers by new identifiers which use + fuel. + + Ex.: + def_fuel_tm = “ + even_fuel (fuel : nat) (n : int) : result bool = + case fuel of 0 => Diverge + | SUC fuel => + if i = 0 then Return T else odd_fuel (i - 1))” + *) + fun mk_fuel_id (id : term) : term = + let + val (id_str, ty) = dest_var id + (* Note: we use symbols forbidden in the generation of code to + prevent name collisions *) + val fuel_id_str = id_str ^ fuel_def_suffix + val fuel_id = mk_var (fuel_id_str, num_ty --> ty) + in fuel_id end + val fuel_ids = map mk_fuel_id ids + + val fuel_ids_with_fuel = map (fn id => mk_comb (id, fuel_var)) fuel_ids + + (* Recurse through the terms and replace the calls *) + val rwr_thms = map (ASSUME o mk_eq) (zip ids fuel_ids_with_fuel) + val fuel_tms = map (rhs o concl o (PURE_REWRITE_CONV rwr_thms)) def_tms + + (* Add the case over the fuel *) + fun add_fuel_case (tm : term) : term = + let + val (app, body) = dest_eq tm + (* Create the “Diverge” term with the proper type *) + val body_ty = type_of body + val return_ty = + case (snd o dest_type) body_ty of [ty] => ty + | _ => failwith "unexpected" + val diverge_tm = mk_diverge_tm return_ty + (* Create the “SUC fuel” term *) + val suc_tm = mk_comb (num_suc_tm, fuel_var) + val fuel_tm = TypeBase.mk_case (fuel_var, [(num_zero_tm, diverge_tm), (suc_tm, body)]) + in mk_eq (app, fuel_tm) end + val fuel_tms = map add_fuel_case fuel_tms + + (* Define the auxiliary definitions which use fuel *) + val fuel_defs_conj = list_mk_conj fuel_tms + (* Define the fuel definitions *) + val fuel_defs_thm = Define ‘^fuel_defs_conj’ + in + fuel_defs_thm + end + +(* +val (fuel_tms, fuel_defs_thm) = mk_fuel_defs def_tms +val fuel_def_tms = map (snd o strip_forall) ((strip_conj o concl) fuel_defs_thm) +val (def_tm, fuel_def_tm) = hd (zip def_tms fuel_def_tms) +*) + +fun mk_is_diverge_tm (fuel_tm : term) : term = + case snd (dest_type (type_of fuel_tm)) of + [ret_ty] => mk_comb (inst [alpha_tyvar |-> ret_ty] is_diverge_tm, fuel_tm) + | _ => failwith "mk_is_diverge_tm: unexpected" + +fun mk_fuel_predicate_defs (def_tm, fuel_def_tm) : thm = + let + (* From [even i] create the term [even_P i n], where [n] is the fuel *) + val (id, args) = (strip_comb o lhs) def_tm + val (id_str, id_ty) = dest_var id + val {Args=tys, Thy=thy, Tyop=tyop} = dest_thy_type id_ty + val _ = assert (fn x => x = "fun") tyop; + val tys = rev tys; + val ret_ty = hd tys; + val tys = rev (num_ty :: tl tys); + val pred_ty = list_mk_arrow tys bool_ty + val pred_id = mk_var (id_str ^ fuel_predicate_suffix, pred_ty) + val pred_tm = list_mk_comb (pred_id, append args [fuel_var]) + + (* Create the term ~is_diverge (even_fuel n i) *) + val fuel_tm = lhs fuel_def_tm + val not_is_diverge_tm = mk_neg (mk_is_diverge_tm fuel_tm) + + (* Create the term: even_P i n = ~(is_diverge (even_fuel n i) *) + val pred_def_tm = mk_eq (pred_tm, not_is_diverge_tm) + in + (* Create the definition *) + Define ‘^pred_def_tm’ + end + +(* +val pred_def_thms = map mk_fuel_predicate_defs (zip def_tms fuel_def_tms) +*) + +(* Tactic which makes progress in a proof by making a case disjunction (we use + this to explore all the paths in a function body). *) +fun case_progress (asms, g) = + let + val scrut = (strip_all_cases_get_scrutinee o lhs) g + in Cases_on ‘^scrut’ (asms, g) end + +(* Tactic to prove the fuel monotonicity theorem *) +fun prove_fuel_mono_tac (pred_def_thms : thm list) (fuel_defs_thm : thm) = + Induct_on ‘^fuel_var0’ >-( + (* The ___P predicates are false: n is 0 *) + fs pred_def_thms >> + fs [is_diverge_def] >> + pure_once_rewrite_tac [fuel_defs_thm] >> fs []) >> + gen_tac >> + Cases_on ‘^fuel_var1’ >-( + (* Contradiction: SUC n < 0 *) + rw [] >> exfalso >> int_tac) >> + fs pred_def_thms >> + fs [is_diverge_def] >> + pure_once_rewrite_tac [fuel_defs_thm] >> fs [bind_def] >> + (* Split the goals *) + rw [] >> + (* Explore all the paths *) + rpt (case_progress >> fs []) + +(* Prove the fuel monotonicity properties. + + We want to prove a theorem of the shape: + {[ + !n m. + (!i. n <= m ==> even___P i n ==> even___fuel n i = even___fuel m i) /\ + (!i. n <= m ==> odd___P i n ==> odd___fuel n i = odd___fuel m i) + ]} +*) +fun prove_fuel_mono (pred_def_thms : thm list) (fuel_defs_thm : thm) : thm = + let + val pred_tms = map (lhs o snd o strip_forall o concl) pred_def_thms + val fuel_tms = map (lhs o snd o strip_forall o concl) (CONJUNCTS fuel_defs_thm) + val pred_fuel_tms = zip pred_tms fuel_tms + (* Generate terms of the shape: + !i. n <= m ==> even___P i n ==> even___fuel n i = even___fuel m i + *) + fun mk_fuel_eq_tm (pred_tm, fuel_tm) : term = + let + (* Retrieve the variables which are not the fuel - for the quantifiers *) + val vars = (tl o snd o strip_comb) fuel_tm + (* Introduce the fuel term which uses “m” *) + val m_fuel_tm = subst [fuel_var0 |-> fuel_var1] fuel_tm + (* Introduce the equality *) + val fuel_eq_tm = mk_eq (fuel_tm, m_fuel_tm) + (* Introduce the implication with the _P pred *) + val fuel_eq_tm = mk_imp (pred_tm, fuel_eq_tm) + (* Introduce the “n <= m ==> ...” implication *) + val fuel_eq_tm = mk_imp (fuel_vars_le, fuel_eq_tm) + (* Quantify *) + val fuel_eq_tm = list_mk_forall (vars, fuel_eq_tm) + in fuel_eq_tm end + val fuel_eq_tms = map mk_fuel_eq_tm pred_fuel_tms + (* Create the conjunction *) + val fuel_eq_tms = list_mk_conj fuel_eq_tms +(* (* Add the “n <= m ==> ...” implication *) + val fuel_eq_tms = mk_imp (fuel_vars_le, fuel_eq_tms) *) + (* Qantify over the fuels *) + val fuel_eq_tms = list_mk_forall ([fuel_var0, fuel_var1], fuel_eq_tms) + in + (* Prove *) + save_goal_and_prove (fuel_eq_tms, prove_fuel_mono_tac pred_def_thms fuel_defs_thm) + end + +(* +val fuel_mono_thm = prove_fuel_mono pred_def_thms fuel_defs_thm +*) + +(* Prove the property about the least upper bound. + + We want to prove theorems of the shape: + {[ + (!n i. $LEAST (even___P i) <= n ==> even___fuel n i = even___fuel ($LEAST (even___P i)) i) + ]} + {[ + (!n i. $LEAST (odd___P i) <= n ==> odd___fuel n i = odd___fuel ($LEAST (odd___P i)) i) + ]} + + TODO: merge with other functions? (prove_pred_imp_fuel_eq_raw_thms) +*) +fun prove_least_fuel_mono (pred_def_thms : thm list) (fuel_mono_thm : thm) : thm list = + let + val thl = (CONJUNCTS o SPECL [fuel_var0, fuel_var1]) fuel_mono_thm + fun mk_least_fuel_thm (pred_def_thm, mono_thm) : thm = + let + (* Retrieve the predicate, without the fuel *) + val pred_tm = (lhs o snd o strip_forall o concl) pred_def_thm + val (pred_tm, args) = strip_comb pred_tm + val args = rev (tl (rev args)) + val pred_tm = list_mk_comb (pred_tm, args) + (* Add $LEAST *) + val least_pred_tm = mk_comb (least_tm, pred_tm) + (* Specialize all *) + val vars = (fst o strip_forall o concl) mono_thm + val th = SPECL vars mono_thm + (* Substitute in the mono theorem *) + val th = INST [fuel_var0 |-> least_pred_tm] th + (* Symmetrize the equality *) + val th = PURE_ONCE_REWRITE_RULE [EQ_SYM_EQ] th + (* Quantify *) + val th = GENL (fuel_var1 :: vars) th + in + th + end + in + map mk_least_fuel_thm (zip pred_def_thms thl) + end + +(* Prove theorems of the shape: + + {[ + !n i. even___P i n ==> $LEAST (even___P i) <= n + ]} + + TODO: merge with other functions? (prove_pred_imp_fuel_eq_raw_thms) + *) +fun prove_least_pred_thms (pred_def_thms : thm list) : thm list = + let + fun prove_least_pred_thm (pred_def_thm : thm) : thm = + let + val pred_tm = (lhs o snd o strip_forall o concl) pred_def_thm + val (pred_no_fuel_tm, args) = strip_comb pred_tm + val args = rev (tl (rev args)) + val pred_no_fuel_tm = list_mk_comb (pred_no_fuel_tm, args) + (* Make the “$LEAST (even___P i)” term *) + val least_pred_tm = mk_comb (least_tm, pred_no_fuel_tm) + (* Make the inequality *) + val tm = list_mk_comb (le_tm, [least_pred_tm, fuel_var0]) + (* Add the implication *) + val tm = mk_imp (pred_tm, tm) + (* Quantify *) + val tm = list_mk_forall (args, tm) + val tm = mk_forall (fuel_var0, tm) + (* Prove *) + val prove_tac = + rpt gen_tac >> + disch_tac >> + (* Use the "fundamental" property about $LEAST *) + qspec_assume ‘^pred_no_fuel_tm’ whileTheory.LEAST_EXISTS_IMP >> + (* Prove the premise *) + pop_assum sg_premise_tac >- (exists_tac fuel_var0 >> fs []) >> + rw [] >> + (* Finish the proof by contraposition *) + spose_not_then assume_tac >> + fs [not_le_eq_gt] + in + save_goal_and_prove (tm, prove_tac) + end + in + map prove_least_pred_thm pred_def_thms + end + + +(* +val least_pred_thms = prove_least_pred_thms pred_def_thms + +val least_pred_thm = hd least_pred_thms +*) + +(* Prove theorems of the shape: + + {[ + !n i. even___P i n ==> even___P i ($LEAST (even___P i)) + ]} +*) +fun prove_pred_n_imp_pred_least_thms (pred_def_thms : thm list) : thm list = + let + fun prove_pred_n_imp_pred_least (pred_def_thm : thm) : thm = + let + val pred_tm = (lhs o snd o strip_forall o concl) pred_def_thm + val (pred_no_fuel_tm, args) = strip_comb pred_tm + val args = rev (tl (rev args)) + val pred_no_fuel_tm = list_mk_comb (pred_no_fuel_tm, args) + (* Make the “$LEAST (even___P i)” term *) + val least_pred_tm = mk_comb (least_tm, pred_no_fuel_tm) + (* Make the “even___P i ($LEAST (even___P i))” *) + val tm = subst [fuel_var0 |-> least_pred_tm] pred_tm + (* Add the implication *) + val tm = mk_imp (pred_tm, tm) + (* Quantify *) + val tm = list_mk_forall (args, tm) + val tm = mk_forall (fuel_var0, tm) + (* The proof tactic *) + val prove_tac = + rpt gen_tac >> + disch_tac >> + (* Use the "fundamental" property about $LEAST *) + qspec_assume ‘^pred_no_fuel_tm’ whileTheory.LEAST_EXISTS_IMP >> + (* Prove the premise *) + pop_assum sg_premise_tac >- (exists_tac fuel_var0 >> fs []) >> + rw [] + in + save_goal_and_prove (tm, prove_tac) + end + in + map prove_pred_n_imp_pred_least pred_def_thms + end + +(* +val (pred_def_thm, mono_thm) = hd (zip pred_def_thms thl) +val least_fuel_mono_thms = prove_least_fuel_mono pred_def_thms fuel_defs_thm fuel_mono_thm + +val least_fuel_mono_thm = hd least_fuel_mono_thms +*) + +(* Define the "raw" definitions: + + {[ + even i = if (?n. even___P i n) then even___P ($LEAST (even___P i)) i else Diverge + ]} + *) +fun define_raw_defs (def_tms : term list) (pred_def_thms : thm list) (fuel_defs_thm : thm) : thm list = + let + fun define_raw_def (def_tm, (pred_def_thm, fuel_def_thm)) : thm = + let + val app = lhs def_tm + val pred_tm = (lhs o snd o strip_forall o concl) pred_def_thm + (* Make the “?n. even___P i n” term *) + val exists_fuel_tm = mk_exists (fuel_var0, pred_tm) + (* Make the “even___fuel ($LEAST (even___P i)) i” term *) + val fuel_tm = (lhs o snd o strip_forall o concl) fuel_def_thm + val (pred_tm, args) = strip_comb pred_tm + val args = rev (tl (rev args)) + val pred_tm = list_mk_comb (pred_tm, args) + val least_pred_tm = mk_comb (least_tm, pred_tm) + val fuel_tm = subst [fuel_var0 |-> least_pred_tm] fuel_tm + (* Create the Diverge term *) + val ret_ty = (hd o snd o dest_type) (type_of app) + (* Create the “if then else” *) + val body = TypeBase.mk_case (exists_fuel_tm, [(true_tm, fuel_tm), (false_tm, mk_diverge_tm ret_ty)]) + (* *) + val raw_def_tm = mk_eq (app, body) + in + Define ‘^raw_def_tm’ + end + in + map define_raw_def (zip def_tms (zip pred_def_thms (CONJUNCTS fuel_defs_thm))) + end + +(* +val raw_def_thms = define_raw_defs def_tms pred_def_thms fuel_defs_thm + *) + +(* +val pred_def_thm = hd pred_def_thms + +val pred_n_imp_pred_least_thms = prove_pred_n_imp_pred_least_thms pred_def_thms + +val pred_n_imp_pred_least_thm = hd pred_n_imp_pred_least_thms +*) + +(* Prove theorems of the shape: + + !n i. even___P i n ==> even___fuel n i = even i + *) +fun prove_pred_imp_fuel_eq_raw_def_thms + (pred_def_thms : thm list) + (fuel_def_tms : term list) + (least_fuel_mono_thms : thm list) + (least_pred_thms : thm list) + (pred_n_imp_pred_least_thms : thm list) + (raw_def_thms : thm list) : + thm list = + let + fun prove_thm (pred_def_thm, + (fuel_def_tm, + (least_fuel_mono_thm, + (least_pred_thm, + (pred_n_imp_pred_least_thm, raw_def_thm))))) : thm = + let + (* Generate: “even___P i n” *) + val pred_tm = (lhs o snd o strip_forall o concl) pred_def_thm + val (pred_no_fuel_tm, args) = strip_comb pred_tm + val args = rev (tl (rev args)) + (* Generate: “even___fuel n i” *) + val fuel_tm = lhs fuel_def_tm + (* Generate: “even i” *) + val raw_def_tm = (lhs o snd o strip_forall o concl) raw_def_thm + (* Generate: “even___fuel n i = even i” *) + val tm = mk_eq (fuel_tm, raw_def_tm) + (* Add the implication *) + val tm = mk_imp (pred_tm, tm) + (* Quantify *) + val tm = list_mk_forall (args, tm) + val tm = mk_forall (fuel_var0, tm) + (* Prove *) + val prove_tac = + rpt gen_tac >> + strip_tac >> + fs raw_def_thms >> + (* Case on ‘?n. even___P i n’ *) + CASE_TAC >> fs [] >> + (* Use the monotonicity property *) + irule least_fuel_mono_thm >> + imp_res_tac pred_n_imp_pred_least_thm >> fs [] >> + irule least_pred_thm >> fs [] + in + save_goal_and_prove (tm, prove_tac) + end + in + map prove_thm (zip pred_def_thms (zip fuel_def_tms (zip least_fuel_mono_thms + (zip least_pred_thms (zip pred_n_imp_pred_least_thms raw_def_thms))))) + end + +(* +val pred_imp_fuel_eq_raw_def_thms = + prove_pred_imp_fuel_eq_raw_def_thms + pred_def_thms fuel_def_tms least_fuel_mono_thms least_pred_thms + pred_n_imp_pred_least_thms raw_def_thms + +val (pred_def_thm, + (fuel_def_tm, + (least_fuel_mono_thm, + (least_pred_thm, + (pred_n_imp_pred_least_thm, raw_def_thm))))) = + hd (zip pred_def_thms (zip fuel_def_tms (zip least_fuel_mono_thms + (zip least_pred_thms (zip pred_n_imp_pred_least_thms raw_def_thms))))) + *) + + +(* Generate "expand" definitions of the following shape (we use them to + hide the raw function bodies, to control the rewritings): + + {[ + even___expand even odd i : bool result = + if i = 0 then Return T else odd (i - 1) + ]} + + {[ + odd___expand even odd i : bool result = + if i = 0 then Return F else even (i - 1) + ]} + + *) +fun gen_expand_defs (def_tms : term list) = + let + (* Generate the variables for “even”, “odd”, etc. *) + val fun_vars = map (fst o strip_comb o lhs) def_tms + val fun_tys = map type_of fun_vars + (* Generate the expansion *) + fun mk_def (def_tm : term) : thm = + let + val (exp_fun, args) = (strip_comb o lhs) def_tm + val (exp_fun_str, exp_fun_ty) = dest_var exp_fun + val exp_fun_str = exp_fun_str ^ expand_suffix + val exp_fun_ty = list_mk_arrow fun_tys exp_fun_ty + val exp_fun = mk_var (exp_fun_str, exp_fun_ty) + val exp_fun = list_mk_comb (exp_fun, fun_vars) + val exp_fun = list_mk_comb (exp_fun, args) + val tm = mk_eq (exp_fun, rhs def_tm) + in + Define ‘^tm’ + end + in + map mk_def def_tms + end + +(* +val def_tm = hd def_tms + +val expand_defs = gen_expand_defs def_tms +*) + +(* Small utility: + + Return the list: + {[ + (“even___P i n”, “even i = even___expand even odd i”), + ... + ]} + + *) +fun mk_termination_diverge_tms + (pred_def_thms : thm list) + (raw_def_thms : thm list) + (expand_defs : thm list) : + (term * term) list = + let + (* Create the substitution for the "expand" functions: + {[ + even -> even + odd -> odd + ... + ]} + + where on the left we have *variables* and on the right we have + the "raw" definitions. + *) + fun mk_fun_subst (def_tm, raw_def_thm) = + let + val var = (fst o strip_comb o lhs) def_tm + val f = (fst o strip_comb o lhs o snd o strip_forall o concl) raw_def_thm + in + (var |-> f) + end + val fun_subst = map mk_fun_subst (zip def_tms raw_def_thms) + + fun mk_tm (pred_def_thm, (raw_def_thm, expand_def)) : + term * term = + let + (* “even___P i n” *) + val pred_tm = (lhs o snd o strip_forall o concl) pred_def_thm + (* “even i = even___expand even odd i” *) + val expand_tm = (lhs o snd o strip_forall o concl) expand_def + val expand_tm = subst fun_subst expand_tm + val fun_tm = (lhs o snd o strip_forall o concl) raw_def_thm + val fun_eq_tm = mk_eq (fun_tm, expand_tm) + in (pred_tm, fun_eq_tm) end + in + map mk_tm (zip pred_def_thms (zip raw_def_thms expand_defs)) + end + +(* +val term_div_tms = + mk_termination_diverge_tms pred_def_thms raw_def_thms expand_defs +*) + +(* Prove the termination lemmas: + + {[ + !i. + (?n. even___P i n) ==> + even i = even___expand even odd i + ]} + *) +fun prove_termination_thms + (term_div_tms : (term * term) list) + (fuel_defs_thm : thm) + (pred_def_thms : thm list) + (raw_def_thms : thm list) + (expand_defs : thm list) + (pred_n_imp_pred_least_thms : thm list) + (pred_imp_fuel_eq_raw_def_thms : thm list) + : thm list = + let + (* Create a map from functions in the recursive group to lemmas + to apply *) + fun mk_rec_fun_eq_pair (fuel_def_thm, eq_th) = + let + val rfun = (get_fun_name_from_app o lhs o snd o strip_forall o concl) fuel_def_thm + in + (rfun, eq_th) + end + val rec_fun_eq_map = + Redblackmap.fromList const_name_compare ( + map mk_rec_fun_eq_pair + (zip (CONJUNCTS fuel_defs_thm) pred_imp_fuel_eq_raw_def_thms)) + + (* Small tactic which rewrites the recursive calls *) + fun rewrite_rec_call (asms, g) = + let + val scrut = (strip_all_cases_get_scrutinee o lhs) g + val fun_id = get_fun_name_from_app scrut (* This can fail *) + (* This can raise an exception - hence the handle at the end + of the function *) + val eq_th = Redblackmap.find (rec_fun_eq_map, fun_id) + val eq_th = (UNDISCH_ALL o SPEC_ALL) eq_th + (* Match the theorem *) + val eq_th_tm = (lhs o concl) eq_th + val (var_s, ty_s) = match_term eq_th_tm scrut + val eq_th = INST var_s (INST_TYPE ty_s eq_th) + val eq_th = thm_to_conj_implies eq_th + (* Some tactics *) + val premise_tac = fs pred_def_thms >> fs [is_diverge_def] + in + (* Apply the theorem, prove the premise, and rewrite *) + (prove_premise_then premise_tac assume_tac eq_th >> fs []) (asms, g) + end handle NotFound => all_tac (asms, g) + | HOL_ERR _ => all_tac (asms, g) (* Getting the function name can also fail *) + + fun prove_one ((pred_tm, fun_eq_tm), pred_n_imp_pred_least_thm) : + thm = + let + (* “?n. even___P i n” *) + val pred_tm = mk_exists (fuel_var0, pred_tm) + (* “even i = even___expand even odd i” *) + val tm = fun_eq_tm + (* Add the implication *) + val tm = mk_imp (pred_tm, tm) + (* Quantify *) + val (_, args) = strip_comb fun_tm + val tm = list_mk_forall (args, tm) + + (* Prove *) + val prove_tac = + rpt gen_tac >> + disch_tac >> + + (* Expand the raw definition and get rid of the ‘?n ...’ *) + pure_once_rewrite_tac raw_def_thms >> + pure_asm_rewrite_tac [] >> + + (* Simplify *) + fs [] >> + + (* Prove that: “even___P i $(LEAST ...)” *) + imp_res_tac pred_n_imp_pred_least_thm >> + + (* We don't need the ‘even___P i n’ assumption anymore: we have a more + precise one with the least upper bound *) + last_x_assum ignore_tac >> + + (* Expand *) + fs pred_def_thms >> + fs [is_diverge_def] >> + fs expand_defs >> + + (* We need to be a bit careful when expanding the definitions which use fuel: + it can make the simplifier loop. *) + rpt (pop_assum mp_tac) >> + pure_once_rewrite_tac [fuel_defs_thm] >> + rpt disch_tac >> + + (* Expand the binds *) + fs [bind_def] >> + + (* Explore all the paths by doing case disjunctions *) + rpt (rewrite_rec_call >> case_progress >> fs []) + in + save_goal_and_prove (tm, prove_tac) + end + in + map prove_one + (zip term_div_tms pred_n_imp_pred_least_thms) + end + +(* +val termination_thms = + prove_termination_thms term_div_tms fuel_defs_thm pred_def_thms + raw_def_thms expand_defs pred_n_imp_pred_least_thms + pred_imp_fuel_eq_raw_def_thms + +val expand_def = hd expand_defs + +val all_args = (zip pred_def_thms (zip raw_def_thms (zip expand_defs pred_n_imp_pred_least_thms))) +val (pred_def_thm, (raw_def_thm, (expand_def, pred_n_imp_pred_least_thm))) = hd all_args +val (pred_def_thm, (raw_def_thm, (expand_def, pred_n_imp_pred_least_thm))) = hd (tl all_args) + +set_goal ([], tm) +*) + +(* Prove the divergence lemmas: + + {[ + !i. + (!n. ~even___P i n) ==> + (!n. ~even___P i (SUC n)) ==> + even i = even___expand even odd i + ]} + + Note that the shape of the theorem is very precise: this helps for the proof. + Also, by correctly ordering the assumptions, we make sure that by rewriting + we don't convert one of the two to “T”. + *) +fun prove_divergence_thms + (term_div_tms : (term * term) list) + (fuel_defs_thm : thm) + (pred_def_thms : thm list) + (raw_def_thms : thm list) + (expand_defs : thm list) + : thm list = + let + (* Create a set containing the names of all the functions in the recursive group *) + fun get_rec_fun_id (fuel_def_thm : thm) = + (get_fun_name_from_app o lhs o snd o strip_forall o concl) fuel_def_thm + val rec_fun_set = + Redblackset.fromList const_name_compare ( + map get_rec_fun_id raw_def_thms) + + (* Small tactic which rewrites the recursive calls *) + fun rewrite_rec_call (asms, g) = + let + val scrut = (strip_all_cases_get_scrutinee o lhs) g + val fun_id = get_fun_name_from_app scrut (* This can fail *) + in + (* Check if the function is part of the group we are considering *) + if Redblackset.member (rec_fun_set, fun_id) then + let + (* Create a subgoal “odd i = Diverge” *) + val ret_ty = (hd o snd o dest_type o type_of) scrut + val g = mk_eq (scrut, mk_diverge_tm ret_ty) + + (* Create a subgoal: “?n. odd___P i n”. + + It is a bit cumbersome because we have to lookup the proper + predicate (from “odd” we need to lookup “odd___P”) and we + may have to perform substitutions... We hack a bit by using + a conversion to rewrite “odd i” to a term which contains + the “?n. odd___P i n” we are looking for. + *) + val exists_g = (rhs o concl) (PURE_REWRITE_CONV raw_def_thms scrut) + val (_, exists_g, _) = TypeBase.dest_case exists_g + (* The tactic to prove the subgoal *) + val prove_sg_tac = + pure_rewrite_tac raw_def_thms >> + Cases_on ‘^exists_g’ >> pure_asm_rewrite_tac [] >> fs [] >> + (* There must only remain the positive case (i.e., “?n. ...”): + we have a contradiction *) + exfalso >> + (* The end of the proof is done by opening the definitions *) + pop_assum mp_tac >> + fs pred_def_thms >> fs [is_diverge_def] + in + (SUBGOAL_THEN g assume_tac >- prove_sg_tac >> fs []) (asms, g) + end + else all_tac (asms, g) (* Nothing to do *) + end handle HOL_ERR _ => all_tac (asms, g) + + fun prove_one (pred_tm, fun_eq_tm) : + thm = + let + (* “!n. ~even___P i n” *) + val neg_pred_tm = mk_neg pred_tm + val pred_tm = mk_forall (fuel_var0, neg_pred_tm) + val pred_suc_tm = subst [fuel_var0 |-> numSyntax.mk_suc fuel_var0] neg_pred_tm + val pred_suc_tm = mk_forall (fuel_var0, pred_suc_tm) + + (* “even i = even___expand even odd i” *) + val tm = fun_eq_tm + + (* Add the implications *) + val tm = list_mk_imp ([pred_tm, pred_suc_tm], tm) + + (* Quantify *) + val (_, args) = strip_comb fun_tm + val tm = list_mk_forall (args, tm) + + (* Prove *) + val prove_tac = + rpt gen_tac >> + + pure_rewrite_tac raw_def_thms >> + rpt disch_tac >> + + (* This allows to simplify the “?n. even___P i n” *) + fs [] >> + (* We don't need the last assumption anymore *) + last_x_assum ignore_tac >> + + (* Expand *) + fs pred_def_thms >> fs [is_diverge_def] >> + fs expand_defs >> + + (* We need to be a bit careful when expanding the definitions which use fuel: + it can make the simplifier loop. + *) + pop_assum mp_tac >> + pure_once_rewrite_tac [fuel_defs_thm] >> + rpt disch_tac >> fs [] >> + + (* Evaluate all the paths *) + rpt (rewrite_rec_call >> case_progress >> fs []) + in + save_goal_and_prove (tm, prove_tac) + end + in + map prove_one term_div_tms + end + +(* +val divergence_thms = + prove_divergence_thms + term_div_tms + fuel_defs_thm + pred_def_thms + raw_def_thms + expand_defs + +val (pred_tm, fun_eq_tm) = hd term_div_tms + +set_goal ([], tm) + +val (asms, g) = top_goal () +*) diff --git a/backends/hol4/primitivesBaseTacLib.sml b/backends/hol4/primitivesBaseTacLib.sml index 28f8ab97..a718392b 100644 --- a/backends/hol4/primitivesBaseTacLib.sml +++ b/backends/hol4/primitivesBaseTacLib.sml @@ -5,6 +5,10 @@ struct open HolKernel boolLib bossLib Parse open boolTheory arithmeticTheory integerTheory intLib listTheory +val debug = ref false + +fun print_dbg msg = if !debug then print msg else () + (* Remark: below, we also have conversions *) val gsym = GSYM @@ -241,7 +245,7 @@ val th = SPEC_ALL NUM_SUB_1_EQ *) fun inst_match_in_terms (try_match: string Redblackset.set -> term -> term * thm) - (tl : term list) : thm list = + (tml : term list) : thm list = let (* We use a map when storing the theorems, to avoid storing the same theorem twice *) val inst_thms: (term, thm) Redblackmap.dict ref = ref (Redblackmap.mkDict Term.compare); @@ -253,7 +257,7 @@ fun inst_match_in_terms end handle HOL_ERR _ => (); (* Explore the term *) - val _ = app (dep_apply_in_subterms try_instantiate (Redblackset.empty String.compare)) tl; + val _ = List.app (dep_apply_in_subterms try_instantiate (Redblackset.empty String.compare)) tml; in map snd (Redblackmap.listItems (!inst_thms)) end @@ -265,20 +269,24 @@ fun inst_match_in_terms [keep]: if this function returns false on an instantiated theorem, ignore the theorem. *) -fun inst_match_concl_in_terms (keep : thm -> bool) (th : thm) (tl : term list) : thm list = +fun inst_match_concl_in_terms (keep : thm -> bool) (th : thm) (tml : term list) : thm list = let val th = (UNDISCH_ALL o SPEC_ALL) th; fun try_match bvars t = let - val inst_th = inst_match_concl bvars th t; - val c = concl inst_th; + val _ = print_dbg ("inst_match_concl_in_terms: " ^ term_to_string t ^ "\n") + val inst_th = inst_match_concl bvars th t + val c = concl inst_th + val _ = print_dbg ("inst_match_concl_in_terms: matched with success\n") in (* Check that we mustn't ignore the theorem *) if keep inst_th then (lhs (concl inst_th), inst_th) - else failwith "inst_match_concl_in_terms: ignore theorem" + else + let val _ = print_dbg ("inst_match_concl_in_terms: matched failed\n") in + failwith "inst_match_concl_in_terms: ignore theorem" end end; in - inst_match_in_terms try_match tl + inst_match_in_terms try_match tml end (* @@ -293,7 +301,7 @@ val thms = inst_match_concl_in_terms int_to_u32_id [t] instantiations of this theorem which make its first premise match subterms in the provided list of term. *) -fun inst_match_first_premise_in_terms (keep : thm -> bool) (th : thm) (tl : term list) : thm list = +fun inst_match_first_premise_in_terms (keep : thm -> bool) (th : thm) (tml : term list) : thm list = let val th = SPEC_ALL th; fun try_match bvars t = @@ -304,7 +312,7 @@ fun inst_match_first_premise_in_terms (keep : thm -> bool) (th : thm) (tl : term else failwith "inst_match_first_premise_in_terms: ignore theorem" end; in - inst_match_in_terms try_match tl + inst_match_in_terms try_match tml end (* @@ -321,13 +329,15 @@ val thms = inst_match_first_premise_in_terms th [t] Leaves the premises as subgoals if [prove_premise] doesn't prove them. *) fun apply_dep_rewrites_match_concl_with_terms_tac - (prove_premise : tactic) (then_tac : thm_tactic) (tl : term list) (th : thm) : tactic = + (prove_premise : tactic) (then_tac : thm_tactic) + (ignore_tml : term list) + (tml : term list) (th : thm) : tactic = let - val ignore = Redblackset.fromList Term.compare tl; - fun keep th = not (Redblackset.member (ignore, concl th)); + val ignore = Redblackset.fromList Term.compare ignore_tml + fun keep th = not (Redblackset.member (ignore, concl th)) (* Discharge the assumptions so that the goal is one single term *) - val thms = inst_match_concl_in_terms keep th tl; - val thms = map thm_to_conj_implies thms; + val thms = inst_match_concl_in_terms keep th tml + val thms = map thm_to_conj_implies thms in (* Apply each theorem *) map_every_tac (try_tac o sg_premise_then prove_premise then_tac) thms @@ -340,14 +350,16 @@ fun apply_dep_rewrites_match_concl_with_terms_tac *) fun apply_dep_rewrites_match_concl_with_all_tac (prove_premise : tactic) (then_tac : thm_tactic) (th : thm) : tactic = - fn (asms, g) => apply_dep_rewrites_match_concl_with_terms_tac prove_premise then_tac (g :: asms) th (asms, g) + fn (asms, g) => + apply_dep_rewrites_match_concl_with_terms_tac prove_premise then_tac asms (g :: asms) th (asms, g) (* Same as {!apply_dep_rewrites_match_concl_with_all_tac} but we only match the conclusion of the goal. *) fun apply_dep_rewrites_match_concl_with_goal_tac (prove_premise : tactic) (then_tac : thm_tactic) (th : thm) : tactic = - fn (asms, g) => apply_dep_rewrites_match_concl_with_terms_tac prove_premise then_tac [g] th (asms, g) + fn (asms, g) => + apply_dep_rewrites_match_concl_with_terms_tac prove_premise then_tac asms [g] th (asms, g) (* A theorem might be of the shape: [H => A = B /\ C = D], in which case we can split it into: @@ -362,7 +374,7 @@ fun split_rewrite_thm (th : thm) : thm list = val t = concl th; val (vars, t) = strip_forall t; val (impl, t) = strip_imp t; - val tl = strip_conj t; + val tml = strip_conj t; fun mk_goal (t : term) = list_mk_forall (vars, (list_mk_imp (impl, t))) val prove_tac = rpt gen_tac >> rpt disch_tac >> @@ -375,7 +387,7 @@ fun split_rewrite_thm (th : thm) : thm list = fun transform_th (th : thm) : thm = (GEN_ALL o thm_to_conj_implies o SPEC_ALL o UNDISCH_ALL o SPEC_ALL) th in - map (transform_th o mk_th) tl + map (transform_th o mk_th) tml end (* A dependent rewrite tactic which introduces the premises in a new goal. @@ -528,4 +540,55 @@ fun int_tac (asms, g) = first_tac [cooper_tac, exfalso >> cooper_tac]) (asms, g) end +(* Repeatedly destruct cases and return the last scrutinee we get *) +fun strip_all_cases_get_scrutinee (t : term) : term = + if TypeBase.is_case t + then + (* Remark.: [strip_case] is too smart for what we want. + For instance: (fst o strip_case) “if i = 0 then ... else ...” + returns “i” while we want to get “i = 0”. + + We use [dest_case] for this reason. + *) + (strip_all_cases_get_scrutinee o (fn (_, x, _) => x) o TypeBase.dest_case) t + else t + +(* +TypeBase.dest_case “case ls of [] => T | _ => F” +TypeBase.strip_case “case ls of [] => T | _ => F” +TypeBase.strip_case “case (if b then [] else [0, 1]) of [] => T | _ => F” +TypeBase.strip_case “3” +TypeBase.dest_case “3” + +strip_all_cases_get_scrutinee “case ls of [] => T | _ => F” +strip_all_cases_get_scrutinee “case (if b then [] else [0, 1]) of [] => T | _ => F” +strip_all_cases_get_scrutinee “3” +*) + +(* Lexicographic order over pairs *) +fun pair_compare (comp1 : 'a * 'a -> order) (comp2 : 'b * 'b -> order) + ((p1, p2) : (('a * 'b) * ('a * 'b))) : order = + let + val (x1, y1) = p1; + val (x2, y2) = p2; + in + case comp1 (x1, x2) of + LESS => LESS + | GREATER => GREATER + | EQUAL => comp2 (y1, y2) + end + +(* A constant name (theory, constant name) *) +type const_name = string * string + +val const_name_compare = pair_compare String.compare String.compare + +(* Given a function call [f y0 ... yn] return the name of the function *) +fun get_fun_name_from_app (t : term) : const_name = + let + val f = (fst o strip_comb) t; + val {Name=name, Thy=thy, Ty=_} = dest_thy_const f; + val cn = (thy, name); + in cn end + end diff --git a/backends/hol4/primitivesLib.sml b/backends/hol4/primitivesLib.sml index 543ded23..057c57bd 100644 --- a/backends/hol4/primitivesLib.sml +++ b/backends/hol4/primitivesLib.sml @@ -181,24 +181,6 @@ val massage : tactic = assume_bounds_for_all_int_vars >> rewrite_with_dep_int_lemmas -(* Lexicographic order over pairs *) -fun pair_compare (comp1 : 'a * 'a -> order) (comp2 : 'b * 'b -> order) - ((p1, p2) : (('a * 'b) * ('a * 'b))) : order = - let - val (x1, y1) = p1; - val (x2, y2) = p2; - in - case comp1 (x1, x2) of - LESS => LESS - | GREATER => GREATER - | EQUAL => comp2 (y1, y2) - end - -(* A constant name (theory, constant name) *) -type const_name = string * string - -val const_name_compare = pair_compare String.compare String.compare - (* The registered spec theorems, that {!progress} will automatically apply. The keys are the function names (it is a pair, because constant names @@ -265,14 +247,6 @@ fun get_spec_app (t : term) : term = else (fst o dest_eq) t; in t end -(* Given a function call [f y0 ... yn] return the name of the function *) -fun get_fun_name_from_app (t : term) : const_name = - let - val f = (fst o strip_comb) t; - val {Name=name, Thy=thy, Ty=_} = dest_thy_const f; - val cn = (thy, name); - in cn end - (* Register a spec theorem in the spec database. For the shape of spec theorems, see {!get_spec_thm_app}. @@ -376,25 +350,6 @@ val all_vec_lems = [ ] val _ = app register_spec_thm all_vec_lems -(* Repeatedly destruct cases and return the last scrutinee we get *) -fun strip_all_cases_get_scrutinee (t : term) : term = - if TypeBase.is_case t - then (strip_all_cases_get_scrutinee o fst o TypeBase.strip_case) t - else t - -(* -TypeBase.dest_case “case ls of [] => T | _ => F” -TypeBase.strip_case “case ls of [] => T | _ => F” -TypeBase.strip_case “case (if b then [] else [0, 1]) of [] => T | _ => F” -TypeBase.strip_case “3” -TypeBase.dest_case “3” - -strip_all_cases_get_scrutinee “case ls of [] => T | _ => F” -strip_all_cases_get_scrutinee “case (if b then [] else [0, 1]) of [] => T | _ => F” -strip_all_cases_get_scrutinee “3” -*) - - (* Provided the goal contains a call to a monadic function, return this function call. The goal should be of the shape: diff --git a/backends/hol4/primitivesScript.sml b/backends/hol4/primitivesScript.sml index 6dd9f6ec..969e9f6e 100644 --- a/backends/hol4/primitivesScript.sml +++ b/backends/hol4/primitivesScript.sml @@ -12,7 +12,7 @@ Datatype: End Datatype: - result = Return 'a | Fail error | Loop + result = Return 'a | Fail error | Diverge End Type M = ``: 'a result`` @@ -22,7 +22,7 @@ val bind_def = Define ` case x of Return y => f y | Fail e => Fail e - | Loop => Loop`; + | Diverge => Diverge`; val bind_name = fst (dest_const “bind”) diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig index bac7fd4f..cf550f00 100644 --- a/backends/hol4/primitivesTheory.sig +++ b/backends/hol4/primitivesTheory.sig @@ -451,7 +451,7 @@ sig ⊢ ∀x f. monad_bind x f = - case x of Return y => f y | Fail e => Fail e | Loop => Loop + case x of Return y => f y | Fail e => Fail e | Diverge => Diverge [error_BIJ] Definition @@ -781,13 +781,13 @@ sig ⊢ (∀a f f1 v. result_CASE (Return a) f f1 v = f a) ∧ (∀a f f1 v. result_CASE (Fail a) f f1 v = f1 a) ∧ - ∀f f1 v. result_CASE Loop f f1 v = v + ∀f f1 v. result_CASE Diverge f f1 v = v [result_size_def] Definition ⊢ (∀f a. result_size f (Return a) = 1 + f a) ∧ (∀f a. result_size f (Fail a) = 1 + error_size a) ∧ - ∀f. result_size f Loop = 0 + ∀f. result_size f Diverge = 0 [return_def] Definition @@ -993,7 +993,7 @@ sig [datatype_result] Theorem - ⊢ DATATYPE (result Return Fail Loop) + ⊢ DATATYPE (result Return Fail Diverge) [error2num_11] Theorem @@ -1411,33 +1411,33 @@ sig ⊢ ∀f0 f1 f2. ∃fn. (∀a. fn (Return a) = f0 a) ∧ (∀a. fn (Fail a) = f1 a) ∧ - fn Loop = f2 + fn Diverge = f2 [result_case_cong] Theorem ⊢ ∀M M' f f1 v. M = M' ∧ (∀a. M' = Return a ⇒ f a = f' a) ∧ - (∀a. M' = Fail a ⇒ f1 a = f1' a) ∧ (M' = Loop ⇒ v = v') ⇒ + (∀a. M' = Fail a ⇒ f1 a = f1' a) ∧ (M' = Diverge ⇒ v = v') ⇒ result_CASE M f f1 v = result_CASE M' f' f1' v' [result_case_eq] Theorem ⊢ result_CASE x f f1 v = v' ⇔ (∃a. x = Return a ∧ f a = v') ∨ (∃e. x = Fail e ∧ f1 e = v') ∨ - x = Loop ∧ v = v' + x = Diverge ∧ v = v' [result_distinct] Theorem - ⊢ (∀a' a. Return a ≠ Fail a') ∧ (∀a. Return a ≠ Loop) ∧ - ∀a. Fail a ≠ Loop + ⊢ (∀a' a. Return a ≠ Fail a') ∧ (∀a. Return a ≠ Diverge) ∧ + ∀a. Fail a ≠ Diverge [result_induction] Theorem - ⊢ ∀P. (∀a. P (Return a)) ∧ (∀e. P (Fail e)) ∧ P Loop ⇒ ∀r. P r + ⊢ ∀P. (∀a. P (Return a)) ∧ (∀e. P (Fail e)) ∧ P Diverge ⇒ ∀r. P r [result_nchotomy] Theorem - ⊢ ∀rr. (∃a. rr = Return a) ∨ (∃e. rr = Fail e) ∨ rr = Loop + ⊢ ∀rr. (∃a. rr = Return a) ∨ (∃e. rr = Fail e) ∨ rr = Diverge [u128_add_eq] Theorem diff --git a/backends/hol4/testHashmapScript.sml b/backends/hol4/testHashmapScript.sml index 249bc0bf..77c97651 100644 --- a/backends/hol4/testHashmapScript.sml +++ b/backends/hol4/testHashmapScript.sml @@ -37,17 +37,6 @@ val list_t_v_def = Define ‘ list_t_v (ListCons x tl) = x :: list_t_v tl ’ -(* TODO: move *) -Theorem index_eq: - (∀x ls. index 0 (x :: ls) = x) ∧ - (∀i x ls. index i (x :: ls) = - if (0 < i) ∨ (0 ≤ i ∧ i ≠ 0) then index (i - 1) ls - else (if i = 0 then x else ARB)) -Proof - rw [index_def] >> fs [] >> - exfalso >> cooper_tac -QED - Theorem nth_mut_fwd_spec: !(ls : 't list_t) (i : u32). u32_to_int i < len (list_t_v ls) ==> @@ -57,7 +46,7 @@ Theorem nth_mut_fwd_spec: | Loop => F Proof Induct_on ‘ls’ >> rw [list_t_v_def, len_def] >~ [‘ListNil’] - >-(massage >> exfalso >> cooper_tac) >> + >-(massage >> int_tac) >> pure_once_rewrite_tac [nth_mut_fwd_def] >> rw [] >> fs [index_eq] >> progress >> progress @@ -108,6 +97,7 @@ Theorem insert_lem: lookup key ls1 = SOME value /\ (* The other bindings are left unchanged *) (!k. k <> key ==> lookup k ls = lookup k ls1) + (* TODO: invariant *) | Fail _ => F | Loop => F Proof diff --git a/backends/hol4/testHashmapTheory.sig b/backends/hol4/testHashmapTheory.sig index 64312406..fd22e05b 100644 --- a/backends/hol4/testHashmapTheory.sig +++ b/backends/hol4/testHashmapTheory.sig @@ -15,7 +15,6 @@ sig (* Theorems *) val datatype_list_t : thm - val index_eq : thm val insert_lem : thm val list_t_11 : thm val list_t_Axiom : thm @@ -102,15 +101,6 @@ sig ⊢ DATATYPE (list_t ListCons ListNil) - [index_eq] Theorem - - ⊢ (∀x ls. index 0 (x::ls) = x) ∧ - ∀i x ls. - index i (x::ls) = - if 0 < i ∨ 0 ≤ i ∧ i ≠ 0 then index (i − 1) ls - else if i = 0 then x - else ARB - [insert_lem] Theorem [oracles: DISK_THM] [axioms: insert_def] [] @@ -120,8 +110,8 @@ sig Return ls1 => lookup key ls1 = SOME value ∧ ∀k. k ≠ key ⇒ lookup k ls = lookup k ls1 - | Fail v1 => F - | Loop => F + | Fail v3 => F + | Diverge => F [list_t_11] Theorem @@ -194,8 +184,8 @@ sig u32_to_int i < len (list_t_v ls) ⇒ case nth_mut_fwd ls i of Return x => x = index (u32_to_int i) (list_t_v ls) - | Fail v1 => F - | Loop => F + | Fail v3 => F + | Diverge => F *) diff --git a/backends/hol4/testScript.sml b/backends/hol4/testScript.sml index a2d15117..8b4d523c 100644 --- a/backends/hol4/testScript.sml +++ b/backends/hol4/testScript.sml @@ -1481,6 +1481,7 @@ val nth_fuel_P_def = Define ‘ nth_fuel_P ls i n = ~is_loop (nth_fuel n ls i) ’ +(* TODO: this is not the theorem we want: we want the one below *) Theorem nth_fuel_mono: !n m ls i. n <= m ==> @@ -1533,7 +1534,7 @@ Proof pop_assum mp_tac >> CASE_TAC >> fs [] QED -Theorem nth_fuel_least_fail_mono: +(*Theorem nth_fuel_least_fail_mono: !n ls i. n < $LEAST (nth_fuel_P ls i) ==> nth_fuel n ls i = Loop @@ -1544,7 +1545,7 @@ Proof fs [nth_fuel_P_def, is_loop_def] >> pop_assum mp_tac >> CASE_TAC -QED +QED*) Theorem nth_fuel_least_success_mono: !n ls i. @@ -1593,7 +1594,7 @@ val nth_expand_def = Define ‘ Fail Failure ’ -(* Prove the important theorems *) +(* Prove the important theorems: termination case *) Theorem nth_def_terminates: !ls i. (?n. nth_fuel_P ls i n) ==> @@ -1635,7 +1636,7 @@ Proof imp_res_tac nth_fuel_least_success_mono >> fs [] QED -(* Prove the important theorems *) +(* Prove the important theorems: divergence case *) Theorem nth_def_loop: !ls i. (!n. ~nth_fuel_P ls i n) ==> diff --git a/backends/hol4/testTheory.sig b/backends/hol4/testTheory.sig index c1034394..21b74a39 100644 --- a/backends/hol4/testTheory.sig +++ b/backends/hol4/testTheory.sig @@ -102,7 +102,6 @@ sig val nth_fuel_P_mono : thm val nth_fuel_def : thm val nth_fuel_ind : thm - val nth_fuel_least_fail_mono : thm val nth_fuel_least_success_mono : thm val nth_fuel_mono : thm val num2error_11 : thm @@ -695,10 +694,6 @@ sig P n ls i) ⇒ ∀v v1 v2. P v v1 v2 - [nth_fuel_least_fail_mono] Theorem - - ⊢ ∀n ls i. n < $LEAST (nth_fuel_P ls i) ⇒ nth_fuel n ls i = Loop - [nth_fuel_least_success_mono] Theorem ⊢ ∀n ls i. |