diff options
| -rw-r--r-- | backends/hol4/Test.sml | 225 |
1 files changed, 145 insertions, 80 deletions
diff --git a/backends/hol4/Test.sml b/backends/hol4/Test.sml index b29589d5..04bc3ec3 100644 --- a/backends/hol4/Test.sml +++ b/backends/hol4/Test.sml @@ -1,6 +1,7 @@ open HolKernel boolLib bossLib Parse -val _ = new_theory"test" +val primitives_theory_name = "Primitives" +val _ = new_theory primitives_theory_name (* SML declarations *) (* for example: *) @@ -101,32 +102,8 @@ val _ = deprecate_int () open arithmeticTheory -val m = Hol_pp.print_apropos; -val f = Hol_pp.print_find; - -(* -m “SUC (x : num) + y = _” -m “(ZERO : num) < SUC y” -m “(_ : num) < SUC y” -m “x < (y : num) <=> _” -f "ADD" -ADD - -val x = “1:num” -dest_term x -val (x1, x2) = dest_comb x -dest_term “0n:num” -dest_term “ZERO:num” -m “ZERO + (_ : num) = _” - -m “BIT1 _ = _” -NUMERAL_DEF - -val x = “ZERO = (0:num)” -dest_term x - -m “0 < SUC 0” -*) +val m = Hol_pp.print_apropos +val f = Hol_pp.print_find (* Display types on/off: M-h C-t *) (* Move back: M-h b *) @@ -134,10 +111,6 @@ m “0 < SUC 0” val _ = numLib.deprecate_num () val _ = numLib.prefer_num () -(* -m “!x. x = x” -*) - Theorem NAT_THM1: !(n : num). n < n + 1 Proof @@ -166,7 +139,7 @@ val _ = prefer_int () val _ = new_type ("u32", 0) val _ = new_type ("i32", 0) -val u32_min_def = Define ‘u32_min = (0:int)’ +(*val u32_min_def = Define ‘u32_min = (0:int)’*) val u32_max_def = Define ‘u32_max = (4294967295:int)’ (* TODO: change that *) @@ -186,7 +159,7 @@ val _ = new_constant ("int_to_i32", “:int -> i32”) val u32_to_int_bounds = new_axiom ( "u32_to_int_bounds", - “!n. u32_min <= u32_to_int n /\ u32_to_int n <= u32_max”) + “!n. 0 <= u32_to_int n /\ u32_to_int n <= u32_max”) val i32_to_int_bounds = new_axiom ( @@ -196,7 +169,7 @@ val i32_to_int_bounds = val int_to_u32_id = new_axiom ( "int_to_u32_id", - “!n. u32_min <= n /\ n <= u32_max ==> + “!n. 0 <= n /\ n <= u32_max ==> u32_to_int (int_to_u32 n) = n”) val int_to_i32_id = @@ -207,13 +180,13 @@ val int_to_i32_id = val mk_u32_def = Define ‘mk_u32 n = - if u32_min <= n /\ n <= u32_max then Return (int_to_u32 n) + if 0 <= n /\ n <= u32_max then Return (int_to_u32 n) else Fail Failure’ val u32_add_def = Define ‘u32_add x y = mk_u32 ((u32_to_int x) + (u32_to_int y))’ Theorem MK_U32_SUCCESS: - !n. u32_min <= n /\ n <= u32_max ==> + !n. 0 <= n /\ n <= u32_max ==> mk_u32 n = Return (int_to_u32 n) Proof rw[mk_u32_def] @@ -229,18 +202,18 @@ Proof exists_tac “int_to_u32 (u32_to_int x + u32_to_int y)” >> imp_res_tac MK_U32_SUCCESS >> (* There is probably a better way of doing this *) - sg ‘u32_min <= u32_to_int x’ >- (rw[u32_to_int_bounds]) >> - sg ‘u32_min <= u32_to_int y’ >- (rw[u32_to_int_bounds]) >> - fs [u32_min_def, u32_add_def] >> + sg ‘0 <= u32_to_int x’ >- (rw[u32_to_int_bounds]) >> + sg ‘0 <= u32_to_int y’ >- (rw[u32_to_int_bounds]) >> + fs [u32_add_def] >> irule int_to_u32_id >> - fs[u32_min_def] + fs[] QED val u32_sub_def = Define ‘u32_sub x y = mk_u32 ((u32_to_int x) - (u32_to_int y))’ Theorem U32_SUB_EQ: !x y. - u32_min <= u32_to_int x - u32_to_int y ==> + 0 <= u32_to_int x - u32_to_int y ==> ?z. u32_sub x y = Return z /\ u32_to_int z = u32_to_int x - u32_to_int y Proof rpt gen_tac >> @@ -250,13 +223,12 @@ Proof (* There is probably a better way of doing this *) sg ‘u32_to_int x − u32_to_int y ≤ u32_max’ >-( sg ‘u32_to_int x <= u32_max’ >- (rw[u32_to_int_bounds]) >> - sg ‘u32_min <= u32_to_int y’ >- (rw[u32_to_int_bounds]) >> - fs [u32_min_def] >> + sg ‘0 <= u32_to_int y’ >- (rw[u32_to_int_bounds]) >> COOPER_TAC ) >> - fs [u32_min_def, u32_sub_def] >> + fs [u32_sub_def] >> irule int_to_u32_id >> - fs[u32_min_def] + fs[] QED val mk_i32_def = Define @@ -301,10 +273,10 @@ val VEC_TO_LIST_NUM_BOUNDS = Theorem VEC_TO_LIST_INT_BOUNDS: !v. let l = int_of_num (LENGTH (vec_to_list v)) in - u32_min <= l /\ l <= u32_max + 0 <= l /\ l <= u32_max Proof gen_tac >> - rw [u32_min_def, u32_max_def] >> + rw [u32_max_def] >> assume_tac VEC_TO_LIST_NUM_BOUNDS >> fs[] QED @@ -434,10 +406,8 @@ val nth_def = new_axiom ("nth_def", “ (*** Examples of proofs on [nth] *) val list_t_v_def = Define ‘ - list_t_v ls = - case ls of - | ListCons x tl => x :: list_t_v tl - | ListNil => [] + list_t_v ListNil = [] /\ + list_t_v (ListCons x tl) = x :: list_t_v tl ’ (* TODO: move *) @@ -475,6 +445,120 @@ QED - auto lookup of spec lemmas *) +(* Add a list of theorems in the assumptions - TODO: move *) +fun ASSUME_TACL (thms : thm list) : tactic = + let + fun t thms = + case thms of + [] => ALL_TAC + | thm :: thms => ASSUME_TAC thm >> t thms + in + t thms + end + +(* The map from integer type to bounds lemmas *) +val integer_bounds_lemmas = + Redblackmap.fromList String.compare + [ + ("u32", u32_to_int_bounds), + ("i32", i32_to_int_bounds) + ] + +(* The integer types *) +val integer_types_names = + Redblackset.fromList String.compare + (map fst (Redblackmap.listItems integer_bounds_lemmas)) + +(* See {!assume_bounds_for_all_int_vars}. + + This tactic is in charge of adding assumptions for one variable. + *) + +fun assume_bounds_for_int_var + (asms: term Redblackset.set) (var : string) (ty : string) : + tactic = + let + (* Lookup the lemma to apply *) + val lemma = Redblackmap.find (integer_bounds_lemmas, ty); + (* Instantiate the lemma *) + val ty_t = mk_type (ty, []); + val var_t = mk_var (var, ty_t); + val lemma = SPEC var_t lemma; + (* Split the theorem into a list of conjuncts. + + The bounds are typically a conjunction: + {[ + ⊢ 0 ≤ u32_to_int x ∧ u32_to_int x ≤ u32_max: thm + ]} + *) + val lemmas = CONJUNCTS lemma; + (* Filter the conjuncts: some of them might already be in the context, + we don't want to introduce them again, as it would pollute it. + *) + val lemmas = filter (fn lem => not (Redblackset.member (asms, concl lem))) lemmas; + in + (* Introduce the assumptions in the context *) + ASSUME_TACL lemmas + end + +(* Introduce bound assumptions for all the machine integers in the context. + + Exemple: + ======== + If there is “x : u32” in the input set, then we introduce: + {[ + 0 <= u32_to_int x + u32_to_int x <= u32_max + ]} + *) +fun assume_bounds_for_all_int_vars (asms, g) = + let + (* Compute the set of integer variables in the context *) + val vars = free_varsl (g :: asms); + (* Compute the set of assumptions already present in the context *) + val asms_set = Redblackset.fromList Term.compare vars; + (* Filter the variables to keep only the ones with type machine integer, + decompose the types at the same time *) + fun decompose_var (v : term) : (string * string) = + let + val (v, ty) = dest_var v; + val {Args=args, Thy=thy, Tyop=ty} = dest_thy_type ty; + val _ = assert null args; + val _ = assert (fn thy => thy = primitives_theory_name) thy; + val _ = assert (fn ty => Redblackset.member (integer_types_names, ty)) ty; + in (v, ty) end; + val vars = mapfilter decompose_var vars; + (* Add assumptions for one variable *) + fun add_var_asm (v, ty) : tactic = + assume_bounds_for_int_var asms_set v ty; + (* Add assumptions for all the variables *) + fun add_vars_asm vl : tactic = + case vl of + [] => ALL_TAC + | v :: vl => + add_var_asm v >> add_vars_asm vl; + in + add_vars_asm vars (asms, g) + end + +(* +dest_thy_type “:u32” +val massage : tactic = assume_bounds_for_all_int_vars +val vl = vars +val (v::vl) = vl +*) + +(* +val (asms, g) = top_goal () +fun bounds_for_ints_in_list (vars : (string * hol_type) list) : tactic = + foldl + FAIL_TAC "" +val var = "x" +val ty = "u32" +*) + +val massage : tactic = assume_bounds_for_all_int_vars + Theorem nth_lem: !(ls : 't list_t) (i : u32). u32_to_int i < int_of_num (LENGTH (list_t_v ls)) ==> @@ -483,47 +567,34 @@ Theorem nth_lem: | Fail _ => F | Loop => F Proof - Induct_on ‘ls’ >~ [‘ListNil’] >> rpt strip_tac >> - PURE_ONCE_REWRITE_TAC [nth_def] >> rw [] >-( - (* TODO: automate this *) - fs [list_t_v_def, LENGTH] >> - qspec_then ‘i’ assume_tac u32_to_int_bounds >> - rw [] >> fs [u32_min_def] >> - intLib.COOPER_TAC - ) >- ( - PURE_ONCE_REWRITE_TAC [list_t_v_def] >> - rw [HD] - ) >> + Induct_on ‘ls’ >> fs [list_t_v_def, HD] >~ [‘ListNil’] >> + rpt strip_tac >> massage >> + PURE_ONCE_REWRITE_TAC [nth_def] >> rw [] >-(intLib.COOPER_TAC) >> (* TODO: we need specialized tactics here - first: subgoal *) - sg ‘u32_min <= u32_to_int i - u32_to_int (int_to_u32 1)’ >-( - fs [u32_min_def] >> - (* We need to detect that we're in the bounds, etc. *) + sg ‘0 <= u32_to_int i - u32_to_int (int_to_u32 1)’ >-( + (* TODO: automate *) DEP_ONCE_REWRITE_TAC [int_to_u32_id] >> - strip_tac >- (fs [u32_min_def, u32_max_def] >> COOPER_TAC) >> - sg ‘u32_min <= u32_to_int i’ >- (rw[u32_to_int_bounds]) >> - fs [u32_min_def] >> + strip_tac >- (fs [u32_max_def] >> COOPER_TAC) >> COOPER_TAC ) >> + (* TODO: automate *) imp_res_tac U32_SUB_EQ >> fs [st_ex_bind_def] >> - (* Automate this *) PURE_ONCE_REWRITE_TAC [list_t_v_def] >> rw [] >> (* Automate this *) sg ‘u32_to_int (int_to_u32 1) = 1’ >-( DEP_ONCE_REWRITE_TAC [int_to_u32_id] >> - fs [u32_min_def, u32_max_def] >> COOPER_TAC + fs [u32_max_def] >> COOPER_TAC ) >> - fs [] >> + massage >> fs [] >> (* TODO: automate this *) - sg ‘u32_min <= u32_to_int z’ >-(rw[u32_to_int_bounds]) >> fs [u32_min_def] >> qspec_then ‘u32_to_int z’ imp_res_tac NUM_SUB_1_EQ >> rw [] >> (* Finish the proof by recursion *) pop_last_assum (qspec_then ‘z’ assume_tac) >> pop_last_assum mp_tac >> - qspec_then ‘ListCons t ls’ assume_tac list_t_v_def >> + fs [list_t_v_def] >> rw [] >> fs [INT] >> sg ‘u32_to_int z < &LENGTH (list_t_v ls)’ >- COOPER_TAC >> - fs [] >> (* Rem.: rfs! *) rfs [] QED @@ -550,12 +621,6 @@ val nth_fuel_def = Define ‘ od ’ -(* -whileTheory.LEAST_DEF -type_of “$LEAST” -val x = “LEAST_DEF” -*) - val is_loop_def = Define ‘is_loop r = case r of Loop => T | _ => F’ val nth_fuel_P_def = Define ‘ |