Make progress on the primitives library for HOL4

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 ()