summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2023-01-31 18:24:47 +0100
committerSon HO2023-06-04 21:54:38 +0200
commitbbe4a8b234d183e36c157dbc6b9900214e405a52 (patch)
tree3894ae7606ae5f9aa5f6dc3d56007d40b94e6339
parentbc2a51e89f198ab33549a59a59bcf418921f8529 (diff)
Start working on divDefLib for diverging definitions
-rw-r--r--backends/hol4/divDefLib.sml890
-rw-r--r--backends/hol4/primitivesBaseTacLib.sml99
-rw-r--r--backends/hol4/primitivesLib.sml45
-rw-r--r--backends/hol4/primitivesScript.sml4
-rw-r--r--backends/hol4/primitivesTheory.sig22
-rw-r--r--backends/hol4/testHashmapScript.sml14
-rw-r--r--backends/hol4/testHashmapTheory.sig18
-rw-r--r--backends/hol4/testScript.sml9
-rw-r--r--backends/hol4/testTheory.sig5
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.