summaryrefslogtreecommitdiff
path: root/backends
diff options
context:
space:
mode:
authorSon Ho2023-01-24 16:45:06 +0100
committerSon HO2023-06-04 21:54:38 +0200
commit74b44a30d61de9d8077bcb416cced6fa242cb6cf (patch)
treeac28981c3b810dfb008e1e57978c7fa4c7318df0 /backends
parent89e064531a7d853b7f87e2ca936852d57ceec1a6 (diff)
Make progress on the primitives library for HOL4
Diffstat (limited to '')
-rw-r--r--backends/hol4/primitivesArithScript.sml2
-rw-r--r--backends/hol4/primitivesBaseTacLib.sml22
-rw-r--r--backends/hol4/primitivesScript.sml184
3 files changed, 196 insertions, 12 deletions
diff --git a/backends/hol4/primitivesArithScript.sml b/backends/hol4/primitivesArithScript.sml
index d251a7cc..fa2f144d 100644
--- a/backends/hol4/primitivesArithScript.sml
+++ b/backends/hol4/primitivesArithScript.sml
@@ -68,7 +68,7 @@ Proof
rw [LE_EQ_GE] >>
sg ‘y <> 0’ >- COOPER_TAC >>
qspecl_then [‘\x. x >= 0’, ‘x’, ‘y’] ASSUME_TAC INT_DIV_FORALL_P >>
- fs [] >> POP_IGNORE_TAC >> rw [] >- COOPER_TAC >>
+ fs [] >> pop_ignore_tac >> rw [] >- COOPER_TAC >>
fs [NOT_LT_EQ_GE] >>
(* Proof by contradiction: assume k < 0 *)
spose_not_then ASSUME_TAC >>
diff --git a/backends/hol4/primitivesBaseTacLib.sml b/backends/hol4/primitivesBaseTacLib.sml
index 3da1423b..b5d9918e 100644
--- a/backends/hol4/primitivesBaseTacLib.sml
+++ b/backends/hol4/primitivesBaseTacLib.sml
@@ -9,8 +9,26 @@ open boolTheory arithmeticTheory integerTheory intLib listTheory
To be used in conjunction with {!pop_assum} for instance.
*)
-fun IGNORE_TAC (_ : thm) : tactic = ALL_TAC
+fun ignore_tac (_ : thm) : tactic = ALL_TAC
-val POP_IGNORE_TAC = POP_ASSUM IGNORE_TAC
+val pop_ignore_tac = pop_assum ignore_tac
+
+(* TODO: no exfalso tactic?? *)
+val ex_falso : tactic =
+ SUBGOAL_THEN “F” (fn th => ASSUME_TAC th >> fs[])
+
+fun qspec_assume x th = qspec_then x assume_tac th
+fun qspecl_assume xl th = qspecl_then xl assume_tac th
+fun first_qspec_assume x = first_assum (qspec_assume x)
+fun first_qspecl_assume xl = first_assum (qspecl_assume xl)
+
+
+
+val cooper_tac = COOPER_TAC
+val pure_once_rewrite_tac = PURE_ONCE_REWRITE_TAC
+
+(* Dependent rewrites *)
+val dep_pure_once_rewrite_tac = dep_rewrite.DEP_PURE_ONCE_REWRITE_TAC
+val dep_pure_rewrite_tac = dep_rewrite.DEP_PURE_REWRITE_TAC
end
diff --git a/backends/hol4/primitivesScript.sml b/backends/hol4/primitivesScript.sml
index 56a876d4..85efeb61 100644
--- a/backends/hol4/primitivesScript.sml
+++ b/backends/hol4/primitivesScript.sml
@@ -1,7 +1,7 @@
open HolKernel boolLib bossLib Parse
open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory
-open primitivesArithTheory
+open primitivesArithTheory primitivesBaseTacLib
val primitives_theory_name = "primitives"
val _ = new_theory primitives_theory_name
@@ -185,11 +185,13 @@ val all_to_int_bounds_lemmas = [
Note that for isize and usize, we write the lemmas in such a way that the
proofs are easily automatable for constants.
*)
+(* TODO: rename those *)
val int_to_isize_id =
new_axiom ("int_to_isize_id",
“!n. (i16_min <= n \/ isize_min <= n) /\ (n <= i16_max \/ n <= isize_max) ==>
isize_to_int (int_to_isize n) = n”)
+(* TODO: remove the condition on u16_max, and make the massage tactic automatically use usize_bounds *)
val int_to_usize_id =
new_axiom ("int_to_usize_id",
“!n. 0 <= n /\ (n <= u16_max \/ n <= usize_max) ==> usize_to_int (int_to_usize n) = n”)
@@ -234,6 +236,7 @@ val int_to_u128_id =
new_axiom ("int_to_u128_id",
“!n. 0 <= n /\ n <= u128_max ==> u128_to_int (int_to_u128 n) = n”)
+(* TODO: rename *)
val all_conversion_id_lemmas = [
int_to_isize_id,
int_to_i8_id,
@@ -249,6 +252,20 @@ val all_conversion_id_lemmas = [
int_to_u128_id
]
+val int_to_i8_i8_to_int = new_axiom ("int_to_i8_i8_to_int", “∀i. int_to_i8 (i8_to_int i) = i”)
+val int_to_i16_i16_to_int = new_axiom ("int_to_i16_i16_to_int", “∀i. int_to_i16 (i16_to_int i) = i”)
+val int_to_i32_i32_to_int = new_axiom ("int_to_i32_i32_to_int", “∀i. int_to_i32 (i32_to_int i) = i”)
+val int_to_i64_i64_to_int = new_axiom ("int_to_i64_i64_to_int", “∀i. int_to_i64 (i64_to_int i) = i”)
+val int_to_i128_i128_to_int = new_axiom ("int_to_i128_i128_to_int", “∀i. int_to_i128 (i128_to_int i) = i”)
+val int_to_isize_isize_to_int = new_axiom ("int_to_isize_isize_to_int", “∀i. int_to_isize (isize_to_int i) = i”)
+
+val int_to_u8_u8_to_int = new_axiom ("int_to_u8_u8_to_int", “∀i. int_to_u8 (u8_to_int i) = i”)
+val int_to_u16_u16_to_int = new_axiom ("int_to_u16_u16_to_int", “∀i. int_to_u16 (u16_to_int i) = i”)
+val int_to_u32_u32_to_int = new_axiom ("int_to_u32_u32_to_int", “∀i. int_to_u32 (u32_to_int i) = i”)
+val int_to_u64_u64_to_int = new_axiom ("int_to_u64_u64_to_int", “∀i. int_to_u64 (u64_to_int i) = i”)
+val int_to_u128_u128_to_int = new_axiom ("int_to_u128_u128_to_int", “∀i. int_to_u128 (u128_to_int i) = i”)
+val int_to_usize_usize_to_int = new_axiom ("int_to_usize_usize_to_int", “∀i. int_to_usize (usize_to_int i) = i”)
+
(** Utilities to define the arithmetic operations *)
val mk_isize_def = Define
‘mk_isize n =
@@ -1247,24 +1264,173 @@ val all_div_eqs = [
val _ = new_type ("vec", 1)
val _ = new_constant ("vec_to_list", “:'a vec -> 'a list”)
+(* TODO: we could also make ‘mk_vec’ return ‘'a vec’ (no result) *)
+val _ = new_constant ("mk_vec", “:'a list -> 'a vec result”)
+
val VEC_TO_LIST_NUM_BOUNDS =
- new_axiom (
- "VEC_TO_LIST_BOUNDS",
+ new_axiom ("VEC_TO_LIST_BOUNDS",
“!v. let l = LENGTH (vec_to_list v) in
- (0:num) <= l /\ l <= (4294967295:num)”)
+ (0:num) <= l /\ l <= Num usize_max”)
Theorem VEC_TO_LIST_INT_BOUNDS:
- !v. let l = int_of_num (LENGTH (vec_to_list v)) in
- 0 <= l /\ l <= u32_max
+ !v. 0 <= int_of_num (LENGTH (vec_to_list v)) /\ int_of_num (LENGTH (vec_to_list v)) <= usize_max
Proof
gen_tac >>
- rw [u32_max_def] >>
assume_tac VEC_TO_LIST_NUM_BOUNDS >>
- fs[]
+ pop_assum (qspec_then ‘v’ ASSUME_TAC) >>
+ pop_assum MP_TAC >>
+ PURE_ONCE_REWRITE_TAC [GSYM INT_LE] >>
+ sg ‘0 ≤ usize_max’ >- (ASSUME_TAC usize_bounds >> fs [u16_max_def] >> COOPER_TAC) >>
+ metis_tac [INT_OF_NUM]
+QED
+
+val VEC_LEN_DEF = Define ‘vec_len v = int_to_usize (int_of_num (LENGTH (vec_to_list v)))’
+Theorem VEC_LEN_SPEC:
+ ∀v.
+ vec_len v = int_to_usize (&(LENGTH (vec_to_list v))) ∧
+ 0 ≤ &(LENGTH (vec_to_list v)) ∧ &(LENGTH (vec_to_list v)) ≤ usize_max
+Proof
+ gen_tac >> rw [VEC_LEN_DEF] >>
+ qspec_then ‘v’ ASSUME_TAC VEC_TO_LIST_INT_BOUNDS >>
+ fs []
QED
-val VEC_LEN_DEF = Define ‘vec_len v = int_to_u32 (int_of_num (LENGTH (vec_to_list v)))’
+val MK_VEC_SPEC = new_axiom ("MK_VEC_SPEC", “∀l. &(LENGTH l) ≤ usize_max ⇒ ∃v. mk_vec l = Return v ∧ vec_to_list v = l”)
+val VEC_NEW_DEF = Define ‘vec_new = case mk_vec [] of Return v => v’
+Theorem VEC_NEW_SPEC:
+ vec_to_list vec_new = []
+Proof
+ rw [VEC_NEW_DEF] >>
+ qabbrev_tac ‘l = []’ >>
+ qspec_then ‘l’ ASSUME_TAC MK_VEC_SPEC >>
+ Cases_on ‘mk_vec l’ >>
+ rfs [markerTheory.Abbrev_def, NOT_LE_EQ_GT] >> fs [] >>
+ ASSUME_TAC usize_bounds >> fs[u16_max_def] >> TRY (ex_falso >> COOPER_TAC) >>
+ sg ‘0 ≤ usize_max’ >- COOPER_TAC >>
+ fs []
+QED
+
+val VEC_PUSH_DEF = Define ‘vec_push_back v x = mk_vec (vec_to_list v ++ [x])’
+Theorem VEC_PUSH_SPEC:
+ ∀v x. usize_to_int (vec_len v) < usize_max ⇒
+ ∃vx. vec_push_back v x = Return vx ∧
+ vec_to_list vx = vec_to_list v ++ [x]
+Proof
+ rpt strip_tac >> fs [VEC_PUSH_DEF] >>
+ qspec_then ‘v’ ASSUME_TAC VEC_LEN_SPEC >> rw [] >>
+ qspec_then ‘vec_to_list v ++ [x]’ ASSUME_TAC MK_VEC_SPEC >>
+ fs [VEC_LEN_DEF] >> rw [] >>
+ pop_assum irule >>
+ pop_last_assum MP_TAC >>
+ dep_rewrite.DEP_PURE_ONCE_REWRITE_TAC all_conversion_id_lemmas >> fs [] >>
+ COOPER_TAC
+QED
+
+val UPDATE_DEF = Define ‘
+ update ([] : 'a list) (i : num) (y : 'a) : 'a list = [] ∧
+ update (_ :: ls) (0: num) y = y :: ls ∧
+ update (x :: ls) (SUC i) y = x :: update ls i y
+’
+
+Theorem UPDATE_LENGTH:
+ ∀ls i y. LENGTH (update ls i y) = LENGTH ls
+Proof
+ Induct_on ‘ls’ >> Cases_on ‘i’ >> rw [UPDATE_DEF]
+QED
+
+Theorem UPDATE_SPEC:
+ ∀ls i y. i < LENGTH ls ==>
+ LENGTH (update ls i y) = LENGTH ls ∧
+ EL i (update ls i y) = y ∧
+ ∀j. j < LENGTH ls ⇒ j ≠ i ⇒ EL j (update ls i y) = EL j ls
+Proof
+ Induct_on ‘ls’ >> Cases_on ‘i’ >> rw [UPDATE_DEF] >>
+ Cases_on ‘j’ >> fs []
+QED
+
+(* TODO: this is the base definition for index. Shall we remove the ‘return’ type? *)
+val VEC_INDEX_DEF = Define ‘
+ vec_index i v = if usize_to_int i ≤ usize_to_int (vec_len v) then Return (EL (Num (usize_to_int i)) (vec_to_list v)) else Fail Failure’
+
+(* TODO: shortcut for qspec_then ... ASSUME_TAC *)
+(* TODO: use cooper_tac everywhere *)
+(* TODO: use pure_once_rewrite_tac everywhere *)
+
+(* TODO: injectivity lemmas for ..._to_int *)
+Theorem USIZE_TO_INT_INJ:
+ ∀i j. usize_to_int i = usize_to_int j ⇔ i = j
+Proof
+ rpt strip_tac >>
+ qspec_assume ‘i’ int_to_usize_usize_to_int >>
+ qspec_assume ‘j’ int_to_usize_usize_to_int >>
+ metis_tac []
+QED
+
+Theorem USIZE_TO_INT_NEQ_INJ:
+ ∀i j. i <> j ==> usize_to_int i <> usize_to_int j
+Proof
+ metis_tac [USIZE_TO_INT_INJ]
+QED
+
+(* TODO: move *)
+Theorem INT_OF_NUM:
+ ∀i. 0 ≤ i ⇒ &Num i = i
+Proof
+ metis_tac[integerTheory.INT_OF_NUM]
+QED
+
+Theorem INT_OF_NUM_NEQ_INJ:
+ ∀n m. &n ≠ &m ⇒ n ≠ m
+Proof
+ metis_tac [INT_OF_NUM_INJ]
+QED
+
+(* TODO: automate: take assumption, intro first premise as subgoal *)
+
+val VEC_INSERT_BACK_DEF = Define ‘
+ vec_insert_back (v : 'a vec) (i : usize) (x : 'a) = mk_vec (update (vec_to_list v) (Num (usize_to_int i)) x)’
+Theorem VEC_INSERT_BACK_SPEC:
+ ∀v i x.
+ usize_to_int i < usize_to_int (vec_len v) ⇒
+ ∃nv. vec_insert_back v i x = Return nv ∧
+ vec_len v = vec_len nv ∧
+ vec_index i nv = Return x ∧
+ (* TODO: usize_to_int j ≠ usize_to_int i ? *)
+ (∀j. usize_to_int j < usize_to_int (vec_len nv) ⇒ j ≠ i ⇒ vec_index j nv = vec_index j v)
+Proof
+ rpt strip_tac >> fs [VEC_INSERT_BACK_DEF] >>
+ qspec_assume ‘update (vec_to_list v) (Num (usize_to_int i)) x’ MK_VEC_SPEC >>
+ qspecl_assume [‘vec_to_list v’, ‘Num (usize_to_int i)’, ‘x’] UPDATE_LENGTH >>
+ fs [] >>
+ qspec_assume ‘v’ VEC_LEN_SPEC >>
+ rw [] >> gvs [] >>
+ fs [VEC_LEN_DEF, VEC_INDEX_DEF] >>
+ sg ‘usize_to_int (int_to_usize (&LENGTH (vec_to_list v))) = &LENGTH (vec_to_list v)’ >-(irule int_to_usize_id >> COOPER_TAC) >>
+ fs [] >>
+ qspecl_assume [‘vec_to_list v’, ‘Num (usize_to_int i)’, ‘x’] UPDATE_SPEC >> rfs [] >>
+ sg ‘Num (usize_to_int i) < LENGTH (vec_to_list v)’ >-(
+ (* TODO: automate *)
+ pure_once_rewrite_tac [GSYM INT_LT] >>
+ dep_pure_once_rewrite_tac [INT_OF_NUM] >>
+ qspec_assume ‘i’ usize_to_int_bounds >> fs []
+ ) >>
+ fs [] >>
+ (* Case: !j. j <> i ==> ... *)
+ rpt strip_tac >>
+ first_x_assum irule >>
+ rw [] >-(
+ (* TODO: automate *)
+ irule INT_OF_NUM_NEQ_INJ >>
+ dep_pure_rewrite_tac [INT_OF_NUM] >>
+ rw [usize_to_int_bounds] >>
+ metis_tac [USIZE_TO_INT_NEQ_INJ]
+ ) >>
+ (* TODO: automate *)
+ pure_once_rewrite_tac [GSYM INT_LT] >>
+ dep_pure_once_rewrite_tac [INT_OF_NUM] >>
+ qspec_assume ‘j’ usize_to_int_bounds >> fs []
+QED
val _ = export_theory ()