diff options
Diffstat (limited to 'backends/hol4')
| -rw-r--r-- | backends/hol4/primitivesArithScript.sml | 14 | ||||
| -rw-r--r-- | backends/hol4/primitivesArithTheory.sig | 10 | ||||
| -rw-r--r-- | backends/hol4/primitivesBaseTacLib.sml | 32 | ||||
| -rw-r--r-- | backends/hol4/primitivesLib.sml | 39 | ||||
| -rw-r--r-- | backends/hol4/primitivesScript.sml | 39 | ||||
| -rw-r--r-- | backends/hol4/primitivesTheory.sig | 39 |
6 files changed, 155 insertions, 18 deletions
diff --git a/backends/hol4/primitivesArithScript.sml b/backends/hol4/primitivesArithScript.sml index 679ed2cd..727fc8c2 100644 --- a/backends/hol4/primitivesArithScript.sml +++ b/backends/hol4/primitivesArithScript.sml @@ -209,4 +209,18 @@ Proof cooper_tac QED +Theorem pos_mod_pos_lt: + ∀ x y. 0 ≤ x ⇒ 0 < y ⇒ x % y < y +Proof + rw [] >> + qspecl_assume [‘x’, ‘y’] integerTheory.INT_MOD_BOUNDS >> + sg ‘y ≠ 0 ∧ ~(y < 0)’ >- int_tac >> fs [] +QED + +Theorem pos_mod_pos_ineqs: + ∀x y. 0 ≤ x ⇒ 0 < y ⇒ 0 ≤ x % y ∧ x % y < y +Proof + metis_tac [pos_mod_pos_is_pos, pos_mod_pos_lt] +QED + val _ = export_theory () diff --git a/backends/hol4/primitivesArithTheory.sig b/backends/hol4/primitivesArithTheory.sig index f7ecccab..531797ac 100644 --- a/backends/hol4/primitivesArithTheory.sig +++ b/backends/hol4/primitivesArithTheory.sig @@ -23,8 +23,10 @@ sig val pos_div_pos_is_pos : thm val pos_div_pos_le : thm val pos_div_pos_le_init : thm + val pos_mod_pos_ineqs : thm val pos_mod_pos_is_pos : thm val pos_mod_pos_le_init : thm + val pos_mod_pos_lt : thm val pos_mul_pos_is_pos : thm val primitivesArith_grammars : type_grammar.grammar * term_grammar.grammar @@ -113,6 +115,10 @@ sig ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ x / y ≤ x + [pos_mod_pos_ineqs] Theorem + + ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ 0 ≤ x % y ∧ x % y < y + [pos_mod_pos_is_pos] Theorem ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ 0 ≤ x % y @@ -121,6 +127,10 @@ sig ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ x % y ≤ x + [pos_mod_pos_lt] Theorem + + ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ x % y < y + [pos_mul_pos_is_pos] Theorem ⊢ ∀x y. 0 ≤ x ⇒ 0 ≤ y ⇒ 0 ≤ x * y diff --git a/backends/hol4/primitivesBaseTacLib.sml b/backends/hol4/primitivesBaseTacLib.sml index d19903b1..f256d330 100644 --- a/backends/hol4/primitivesBaseTacLib.sml +++ b/backends/hol4/primitivesBaseTacLib.sml @@ -293,15 +293,28 @@ fun inst_match_concl_in_terms (keep : thm -> bool) (ths : thm Net.net) (tml : te (* Then, match more precisely for every theorem found *) fun try_match (bvars : string Redblackset.set) t th = let - val _ = print_dbg ("inst_match_concl_in_terms: " ^ term_to_string t ^ "\n") + val _ = print_dbg ("inst_match_concl_in_terms:\n- thm: " ^ thm_to_string th ^ + "\n- term: " ^ 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) + if keep inst_th then + let val _ = print_dbg "inst_match_concl_in_terms: keeping theorem\n\n" in + (* There are several possibilities: + - initially, we only kept the lhs of the conclusion (with premises) + of the theorem + - now, we keep the whole theorem + The reason is that it happens that we can prove the premise of some + instantiation but not on another instantiation, even though the + conclusion is the same: in that case we want to keep both. + For instance: + + *) + (concl (DISCH_ALL inst_th), inst_th) end else - let val _ = print_dbg ("inst_match_concl_in_terms: matched failed\n") in + let val _ = print_dbg ("inst_match_concl_in_terms: ignore theorem\n\n") in failwith "inst_match_concl_in_terms: ignore theorem" end end (* Compose *) @@ -311,8 +324,19 @@ fun inst_match_concl_in_terms (keep : thm -> bool) (ths : thm Net.net) (tml : te in mapfilter (try_match bvars t) matched_thms end + (* *) + val thms = inst_match_in_terms try_match_on_thms tml + (* Debug *) + val _ = + if !debug then + let + val thms_s = String.concatWith "\n" (map thm_to_string thms) + in + print ("inst_match_concl_in_terms: instantiated theorems:\n" ^ thms_s ^ "\n\n") + end + else () in - inst_match_in_terms try_match_on_thms tml + thms end (* diff --git a/backends/hol4/primitivesLib.sml b/backends/hol4/primitivesLib.sml index 5339dec9..0a89be4c 100644 --- a/backends/hol4/primitivesLib.sml +++ b/backends/hol4/primitivesLib.sml @@ -6,6 +6,23 @@ open primitivesBaseTacLib primitivesTheory val primitives_theory_name = "primitives" +val debug = ref false + +fun print_dbg msg = if !debug then print msg else () + +fun print_dbg_goal msg (asms, g) = + if !debug then + let + val asms_s = map term_to_string asms + val g_s = term_to_string g + val s = "[" ^ (String.concatWith ", " asms_s) ^ "]" ^ " ⊢ " ^ g_s + val _ = print (msg ^ "goal: " ^ s ^ "\n") + in + ALL_TAC (asms, g) + end + else + ALL_TAC (asms, g) + (* Small utility: compute the set of assumptions in the context. We isolate this code in a utility in order to be able to improve it: @@ -144,7 +161,10 @@ val integer_conversion_lemmas_list = [ u16_to_int_int_to_u16, u32_to_int_int_to_u32, u64_to_int_int_to_u64, - u128_to_int_int_to_u128 + u128_to_int_int_to_u128, + (* Additional conservative lemmas for isize/usize *) + isize_to_int_int_to_isize_i16_bounds, + usize_to_int_int_to_usize_u16_bounds ] (* Using a net for efficiency *) @@ -162,7 +182,9 @@ val integer_conversion_lemmas_net = net_of_rewrite_thms integer_conversion_lemma *) val rewrite_with_dep_int_lemmas : tactic = let - val prove_premise = full_simp_tac simpLib.empty_ss integer_bounds_defs_list >> int_tac + val prove_premise = + (print_dbg_goal "rewrite_with_dep_int_lemmas: prove_premise:\n" >> + full_simp_tac simpLib.empty_ss integer_bounds_defs_list >> int_tac) (* Rewriting based on matching the conclusion. *) val then_tac1 = (fn th => full_simp_tac simpLib.empty_ss [th]) val rewr_tac1 = apply_dep_rewrites_match_concl_with_all_tac prove_premise then_tac1 @@ -515,9 +537,18 @@ val progress : tactic = if null thl then raise (failwith "progress: could not find a suitable theorem to apply") else (); + (* Small helper to remove the equality introduced by the applied spec + (of the shape “f x = Return y” for instance), if there is *) + val remove_eq = try_tac (qpat_x_assum ‘^fgoal = _’ ignore_tac) + in - (* Attempt to use the theorems one by one *) - map_first_tac progress_with thl (asms, g) + (* We do 3 operations: + - attempt to use the theorems one by one + - remove (if there is) the equality introduced by the applied spec + (of the shape “f x = Return y” for instance) + - refold the monadic let-bindings + *) + (map_first_tac progress_with thl >> remove_eq >> fs [GSYM bind_def]) (asms, g) end (* Small utility: check that a term evaluates to “Return” (used by the unit tests) *) diff --git a/backends/hol4/primitivesScript.sml b/backends/hol4/primitivesScript.sml index 7920454b..4378f9c3 100644 --- a/backends/hol4/primitivesScript.sml +++ b/backends/hol4/primitivesScript.sml @@ -24,6 +24,13 @@ End val bind_name = fst (dest_const “bind”) +Theorem bind_return_fail_div_eq: + (bind (Return x) f = f x) ∧ (bind (Fail e) f = Fail e) ∧ (bind Diverge f = Diverge) +Proof + fs [bind_def] +QED +val _ = BasicProvers.export_rewrites ["bind_return_fail_div_eq"] + Definition return_def: (return : 'a -> 'a M) x = Return x @@ -273,6 +280,23 @@ val all_int_to_scalar_to_int_lemmas = [ u128_to_int_int_to_u128 ] +(* Additional conversion lemmas for isize/usize *) +Theorem isize_to_int_int_to_isize_i16_bounds: + !n. i16_min <= n /\ n <= i16_max ==> isize_to_int (int_to_isize n) = n +Proof + rw [] >> irule isize_to_int_int_to_isize >> + assume_tac isize_bounds >> + int_tac +QED + +Theorem usize_to_int_int_to_usize_u16_bounds: + !n. 0 <= n /\ n <= u16_max ==> usize_to_int (int_to_usize n) = n +Proof + rw [] >> irule usize_to_int_int_to_usize >> + assume_tac usize_bounds >> + int_tac +QED + val prove_int_to_scalar_to_int_unfold_tac = assume_tac isize_bounds >> (* Only useful for isize of course *) assume_tac usize_bounds >> (* Only useful for usize of course *) @@ -677,7 +701,7 @@ val all_div_defs = [ In HOL4, it has the sign of the divisor. *) val int_rem_def = Define ‘int_rem (x : int) (y : int) : int = - if (x >= 0 /\ y >= 0) \/ (x < 0 /\ y < 0) then x % y else -(x % y)’ + if (0 ≤ x /\ 0 ≤ y) \/ (x < 0 /\ y < 0) then x % y else -(x % y)’ (* Checking consistency with Rust *) val _ = prove(“int_rem 1 2 = 1”, EVAL_TAC) @@ -685,6 +709,12 @@ val _ = prove(“int_rem (-1) 2 = -1”, EVAL_TAC) val _ = prove(“int_rem 1 (-2) = 1”, EVAL_TAC) val _ = prove(“int_rem (-1) (-2) = -1”, EVAL_TAC) +Theorem pos_rem_pos_ineqs: + ∀x y. 0 ≤ x ⇒ 0 < y ⇒ 0 ≤ int_rem x y ∧ int_rem x y < y +Proof + rw [int_rem_def] >> metis_tac [pos_mod_pos_ineqs] +QED + val isize_rem_def = Define ‘isize_rem x y = if isize_to_int y = 0 then Fail Failure else mk_isize (int_rem (isize_to_int x) (isize_to_int y))’ val i8_rem_def = Define ‘i8_rem x y = @@ -1781,13 +1811,14 @@ End Theorem vec_update_eq: ∀ v i x. - usize_to_int i < usize_to_int (vec_len v) ⇒ let nv = vec_update v i x in - vec_len v = vec_len nv ∧ + len (vec_to_list nv) = len (vec_to_list v) ∧ + len (update (vec_to_list v) (usize_to_int i) x) = len (vec_to_list v) ∧ + (usize_to_int i < len (vec_to_list v) ⇒ vec_index nv i = x ∧ (∀j. usize_to_int j < usize_to_int (vec_len nv) ⇒ usize_to_int j ≠ usize_to_int i ⇒ - vec_index nv j = vec_index v j) + vec_index nv j = vec_index v j)) Proof rpt strip_tac >> fs [vec_update_def] >> qspec_assume ‘update (vec_to_list v) (usize_to_int i) x’ mk_vec_axiom >> diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig index e4051212..7e03987b 100644 --- a/backends/hol4/primitivesTheory.sig +++ b/backends/hol4/primitivesTheory.sig @@ -213,6 +213,7 @@ sig val vec_update_def : thm (* Theorems *) + val bind_return_fail_div_eq : thm val datatype_error : thm val datatype_result : thm val error2num_11 : thm @@ -275,6 +276,7 @@ sig val isize_neg_eq : thm val isize_rem_eq : thm val isize_sub_eq : thm + val isize_to_int_int_to_isize_i16_bounds : thm val isize_to_int_int_to_isize_unfold : thm val mk_isize_unfold : thm val mk_usize_unfold : thm @@ -283,6 +285,7 @@ sig val num2error_ONTO : thm val num2error_error2num : thm val num2error_thm : thm + val pos_rem_pos_ineqs : thm val result_11 : thm val result_Axiom : thm val result_case_cong : thm @@ -333,6 +336,7 @@ sig val usize_mul_eq : thm val usize_rem_eq : thm val usize_sub_eq : thm + val usize_to_int_int_to_usize_u16_bounds : thm val usize_to_int_int_to_usize_unfold : thm val vec_index_back_spec : thm val vec_index_fwd_spec : thm @@ -855,7 +859,7 @@ sig ⊢ ∀x y. int_rem x y = - if x ≥ 0 ∧ y ≥ 0 ∨ x < 0 ∧ y < 0 then x % y else -(x % y) + if 0 ≤ x ∧ 0 ≤ y ∨ x < 0 ∧ y < 0 then x % y else -(x % y) [is_diverge_def] Definition @@ -1366,6 +1370,11 @@ sig vec_update v i x = mk_vec (update (vec_to_list v) (usize_to_int i) x) + [bind_return_fail_div_eq] Theorem + + ⊢ monad_bind (Return x) f = f x ∧ monad_bind (Fail e) f = Fail e ∧ + monad_bind Diverge f = Diverge + [datatype_error] Theorem ⊢ DATATYPE (error Failure) @@ -1884,6 +1893,12 @@ sig ∃z. isize_sub x y = Return z ∧ isize_to_int z = isize_to_int x − isize_to_int y + [isize_to_int_int_to_isize_i16_bounds] Theorem + + [oracles: DISK_THM] [axioms: isize_to_int_int_to_isize, isize_bounds] + [] + ⊢ ∀n. i16_min ≤ n ∧ n ≤ i16_max ⇒ isize_to_int (int_to_isize n) = n + [isize_to_int_int_to_isize_unfold] Theorem [oracles: DISK_THM] @@ -1932,6 +1947,10 @@ sig ⊢ num2error 0 = Failure + [pos_rem_pos_ineqs] Theorem + + ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ 0 ≤ int_rem x y ∧ int_rem x y < y + [result_11] Theorem ⊢ (∀a a'. Return a = Return a' ⇔ a = a') ∧ @@ -2348,6 +2367,11 @@ sig ∃z. usize_sub x y = Return z ∧ usize_to_int z = usize_to_int x − usize_to_int y + [usize_to_int_int_to_usize_u16_bounds] Theorem + + [oracles: DISK_THM] [axioms: usize_to_int_int_to_usize, usize_bounds] + [] ⊢ ∀n. 0 ≤ n ∧ n ≤ u16_max ⇒ usize_to_int (int_to_usize n) = n + [usize_to_int_int_to_usize_unfold] Theorem [oracles: DISK_THM] @@ -2436,14 +2460,17 @@ sig [axioms: vec_to_list_num_bounds, usize_bounds, usize_to_int_int_to_usize, usize_to_int_bounds, mk_vec_axiom] [] ⊢ ∀v i x. - usize_to_int i < usize_to_int (vec_len v) ⇒ (let nv = vec_update v i x in - vec_len v = vec_len nv ∧ vec_index nv i = x ∧ - ∀j. usize_to_int j < usize_to_int (vec_len nv) ⇒ - usize_to_int j ≠ usize_to_int i ⇒ - vec_index nv j = vec_index v j) + len (vec_to_list nv) = len (vec_to_list v) ∧ + len (update (vec_to_list v) (usize_to_int i) x) = + len (vec_to_list v) ∧ + (usize_to_int i < len (vec_to_list v) ⇒ + vec_index nv i = x ∧ + ∀j. usize_to_int j < usize_to_int (vec_len nv) ⇒ + usize_to_int j ≠ usize_to_int i ⇒ + vec_index nv j = vec_index v j)) *) |