Make progress on the HOL4 backend

2 files changed, 298 insertions, 42 deletions

diff --git a/backends/hol4/primitivesScript.sml b/backends/hol4/primitivesScript.sml
index 4a1f5fdd..8cd54f33 100644
--- a/backends/hol4/primitivesScript.sml
+++ b/backends/hol4/primitivesScript.sml
@@ -1661,6 +1661,9 @@ val vec_to_list_num_bounds =
   new_axiom ("vec_to_list_num_bounds",
     “!v. (0:num) <= LENGTH (vec_to_list v) /\ LENGTH (vec_to_list v) <= Num usize_max”)
 
+val mk_vec_axiom = new_axiom ("mk_vec_axiom",
+  “∀l. len l ≤ usize_max ⇒ vec_to_list (mk_vec l) = l”)
+
 Theorem update_len:
   ∀ls i y. len (update ls i y) = len ls
 Proof
@@ -1732,41 +1735,61 @@ Proof
   fs []
 QED
 
-val vec_index_def = Define ‘
-  vec_index i v =
-    if usize_to_int i ≤ usize_to_int (vec_len v)
-    then Return (index (usize_to_int i) (vec_to_list v))
-    else Fail Failure’
+Definition vec_new_def:
+  vec_new = mk_vec []
+End
 
-val mk_vec_axiom = new_axiom ("mk_vec_axiom",
-  “∀l. len l ≤ usize_max ⇒ vec_to_list (mk_vec l) = l”)
+Theorem vec_to_list_vec_new:
+  vec_to_list vec_new = []
+Proof
+  fs [vec_new_def] >>
+  sg_dep_rewrite_all_tac mk_vec_axiom >> fs [len_def] >>
+  assume_tac usize_bounds >> fs [u16_max_def] >> int_tac
+QED
+val _ = BasicProvers.export_rewrites ["vec_to_list_vec_new"]
 
-(* A custom unfolding theorem for evaluation *)
+Theorem vec_len_vec_new:
+  vec_len vec_new = int_to_usize 0
+Proof
+  fs [vec_len_def, vec_new_def] >>
+  sg_dep_rewrite_all_tac usize_to_int_int_to_usize >> fs [len_def, u16_max_def] >>
+  assume_tac usize_bounds >> fs [u16_max_def] >> int_tac
+QED
+val _ = BasicProvers.export_rewrites ["vec_len_vec_new"]
+
+(* A custom unfolding theorem for evaluation - we compare to “u16_max” rather
+   than “usize_max” on purpose. *)
 Theorem mk_vec_unfold:
-  ∀l. vec_to_list (mk_vec l) = if len l ≤ usize_max then l else vec_to_list (mk_vec l)
+  ∀l. vec_to_list (mk_vec l) = if len l ≤ u16_max then l else vec_to_list (mk_vec l)
 Proof
+  rw [] >> Cases_on ‘len l ≤ u16_max’ >> fs [] >>
+  assume_tac usize_bounds >>
+  sg ‘len l ≤ usize_max’ >- int_tac >>
   metis_tac [mk_vec_axiom]
 QED
 val _ = evalLib.add_unfold_thm "mk_vec_unfold"
 
-(* Defining ‘vec_insert_back’ *)
-val vec_insert_back_def = Define ‘
-  vec_insert_back (v : 'a vec) (i : usize) (x : 'a) =
-    if usize_to_int i < usize_to_int (vec_len v) then
-      Return (mk_vec (update (vec_to_list v) (usize_to_int i) x))
-    else Fail Failure’
+(* Helper *)
+Definition vec_index_def:
+  vec_index v i = index (usize_to_int i) (vec_to_list v)
+End
 
-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 ∧
-    (∀j. usize_to_int j < usize_to_int (vec_len nv) ⇒
-          usize_to_int j ≠ usize_to_int i ⇒
-          vec_index j nv = vec_index j v)
-Proof
-  rpt strip_tac >> fs [vec_insert_back_def] >>
+(* Helper *)
+Definition vec_update_def:
+  vec_update v i x = mk_vec (update (vec_to_list v) (usize_to_int i) x)
+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 ∧
+      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)
+Proof
+  rpt strip_tac >> fs [vec_update_def] >>
   qspec_assume ‘update (vec_to_list v) (usize_to_int i) x’ mk_vec_axiom >>
   sg_dep_rewrite_all_tac update_len >> fs [] >>
   qspec_assume ‘v’ vec_len_spec >> gvs [] >>
@@ -1778,4 +1801,110 @@ Proof
   sg_dep_rewrite_all_tac index_update_same >- cooper_tac >> fs []
 QED
 
+Definition vec_index_fwd_def:
+  vec_index_fwd v i =
+    if usize_to_int i ≤ usize_to_int (vec_len v)
+    then Return (vec_index v i)
+    else Fail Failure
+End
+
+Definition vec_index_back_def:
+  vec_index_back v i =
+    if usize_to_int i < usize_to_int (vec_len v) then Return () else Fail Failure
+End
+
+Definition vec_index_mut_fwd_def:
+  vec_index_mut_fwd v i =
+    if usize_to_int i ≤ usize_to_int (vec_len v)
+    then Return (vec_index v i)
+    else Fail Failure
+End
+
+Definition vec_index_mut_back_def:
+  vec_index_mut_back v i x =
+    if usize_to_int i ≤ usize_to_int (vec_len v)
+    then Return (vec_update v i x)
+    else Fail Failure
+End
+
+Theorem vec_index_fwd_spec:
+  ∀v i.
+    usize_to_int i < usize_to_int (vec_len v) ⇒
+    vec_index_fwd v i = Return (vec_index v i)
+Proof
+  rw [vec_index_fwd_def]
+QED
+
+Theorem vec_index_back_spec:
+  ∀v i.
+    usize_to_int i < usize_to_int (vec_len v) ⇒
+    vec_index_back v i = Return ()
+Proof
+  rw [vec_index_back_def]
+QED
+
+Theorem vec_index_mut_fwd_spec:
+  ∀v i.
+    usize_to_int i < usize_to_int (vec_len v) ⇒
+    vec_index_mut_fwd v i = Return (vec_index v i)
+Proof
+  rw [vec_index_mut_fwd_def]
+QED
+
+Theorem vec_index_mut_back_spec:
+  ∀v i x.
+    usize_to_int i < usize_to_int (vec_len v) ⇒
+    vec_index_mut_back v i x = Return (vec_update v i x)
+Proof
+  rw [vec_index_mut_back_def]
+QED
+
+Definition vec_insert_back_def:
+  vec_insert_back (v : 'a vec) (i : usize) (x : 'a) =
+    if usize_to_int i < usize_to_int (vec_len v) then
+      Return (vec_update v i x)
+    else Fail Failure
+End
+
+Theorem vec_insert_back_spec:
+  ∀v i x.
+    usize_to_int i < usize_to_int (vec_len v) ⇒
+    vec_insert_back v i x = Return (vec_update v i x)
+Proof
+  rw [vec_insert_back_def]
+QED
+
+Definition vec_push_back_def:
+  vec_push_back (v : 'a vec) (x : 'a) : ('a vec) result =
+    if usize_to_int (vec_len v) < usize_max then
+      Return (mk_vec ((vec_to_list v) ++ [x]))
+    else Fail Failure
+End
+
+Theorem vec_push_back_unfold:
+  ∀ v x. vec_push_back (v : 'a vec) (x : 'a) : ('a vec) result =
+    if usize_to_int (vec_len v) < u16_max ∨ usize_to_int (vec_len v) < usize_max then
+      Return (mk_vec ((vec_to_list v) ++ [x]))
+    else Fail Failure
+Proof
+  assume_tac usize_bounds >>
+  rw [vec_push_back_def] >> fs [] >>
+  int_tac
+QED
+val _ = evalLib.add_unfold_thm "vec_push_back_unfold"
+
+Theorem vec_push_back_spec:
+  ∀ v x.
+    usize_to_int (vec_len v) < usize_max ⇒
+    ∃ nv. vec_push_back v x = Return nv ∧
+    vec_to_list nv = vec_to_list v ++ [x]
+Proof
+  rw [vec_push_back_def, vec_len_def] >>
+  qspec_assume ‘v’ vec_len_spec >>
+  sg_dep_rewrite_all_tac usize_to_int_int_to_usize >- int_tac >> fs [] >>
+  sg_dep_rewrite_all_tac mk_vec_axiom
+  >- (fs [len_append, len_def, vec_len_def] >> int_tac) >>
+  fs []
+QED
+
 val _ = export_theory ()
diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig
index 45caf234..2407e2f2 100644
--- a/backends/hol4/primitivesTheory.sig
+++ b/backends/hol4/primitivesTheory.sig
@@ -201,9 +201,16 @@ sig
     val usize_mul_def : thm
     val usize_rem_def : thm
     val usize_sub_def : thm
+    val vec_index_back_def : thm
     val vec_index_def : thm
+    val vec_index_fwd_def : thm
+    val vec_index_mut_back_def : thm
+    val vec_index_mut_fwd_def : thm
     val vec_insert_back_def : thm
     val vec_len_def : thm
+    val vec_new_def : thm
+    val vec_push_back_def : thm
+    val vec_update_def : thm
   
   (*  Theorems  *)
     val datatype_error : thm
@@ -327,9 +334,18 @@ sig
     val usize_rem_eq : thm
     val usize_sub_eq : thm
     val usize_to_int_int_to_usize_unfold : thm
+    val vec_index_back_spec : thm
+    val vec_index_fwd_spec : thm
+    val vec_index_mut_back_spec : thm
+    val vec_index_mut_fwd_spec : thm
     val vec_insert_back_spec : thm
     val vec_len_spec : thm
+    val vec_len_vec_new : thm
+    val vec_push_back_spec : thm
+    val vec_push_back_unfold : thm
     val vec_to_list_int_bounds : thm
+    val vec_to_list_vec_new : thm
+    val vec_update_eq : thm
   
   val primitives_grammars : type_grammar.grammar * term_grammar.grammar
 (*
@@ -1285,12 +1301,39 @@ sig
       
       ⊢ ∀x y. usize_sub x y = mk_usize (usize_to_int x − usize_to_int y)
    
+   [vec_index_back_def]  Definition
+      
+      ⊢ ∀v i.
+          vec_index_back v i =
+          if usize_to_int i < usize_to_int (vec_len v) then Return ()
+          else Fail Failure
+   
    [vec_index_def]  Definition
       
-      ⊢ ∀i v.
-          vec_index i v =
+      ⊢ ∀v i. vec_index v i = index (usize_to_int i) (vec_to_list v)
+   
+   [vec_index_fwd_def]  Definition
+      
+      ⊢ ∀v i.
+          vec_index_fwd v i =
+          if usize_to_int i ≤ usize_to_int (vec_len v) then
+            Return (vec_index v i)
+          else Fail Failure
+   
+   [vec_index_mut_back_def]  Definition
+      
+      ⊢ ∀v i x.
+          vec_index_mut_back v i x =
+          if usize_to_int i ≤ usize_to_int (vec_len v) then
+            Return (vec_update v i x)
+          else Fail Failure
+   
+   [vec_index_mut_fwd_def]  Definition
+      
+      ⊢ ∀v i.
+          vec_index_mut_fwd v i =
           if usize_to_int i ≤ usize_to_int (vec_len v) then
-            Return (index (usize_to_int i) (vec_to_list v))
+            Return (vec_index v i)
           else Fail Failure
    
    [vec_insert_back_def]  Definition
@@ -1298,13 +1341,31 @@ sig
       ⊢ ∀v i x.
           vec_insert_back v i x =
           if usize_to_int i < usize_to_int (vec_len v) then
-            Return (mk_vec (update (vec_to_list v) (usize_to_int i) x))
+            Return (vec_update v i x)
           else Fail Failure
    
    [vec_len_def]  Definition
       
       ⊢ ∀v. vec_len v = int_to_usize (len (vec_to_list v))
    
+   [vec_new_def]  Definition
+      
+      ⊢ vec_new = mk_vec []
+   
+   [vec_push_back_def]  Definition
+      
+      ⊢ ∀v x.
+          vec_push_back v x =
+          if usize_to_int (vec_len v) < usize_max then
+            Return (mk_vec (vec_to_list v ⧺ [x]))
+          else Fail Failure
+   
+   [vec_update_def]  Definition
+      
+      ⊢ ∀v i x.
+          vec_update v i x =
+          mk_vec (update (vec_to_list v) (usize_to_int i) x)
+   
    [datatype_error]  Theorem
       
       ⊢ DATATYPE (error Failure)
@@ -1851,9 +1912,9 @@ sig
    
    [mk_vec_unfold]  Theorem
       
-      [oracles: DISK_THM] [axioms: mk_vec_axiom] []
+      [oracles: DISK_THM] [axioms: mk_vec_axiom, usize_bounds] []
       ⊢ ∀l. vec_to_list (mk_vec l) =
-            if len l ≤ usize_max then l else vec_to_list (mk_vec l)
+            if len l ≤ u16_max then l else vec_to_list (mk_vec l)
    
    [num2error_11]  Theorem
       
@@ -2295,20 +2356,35 @@ sig
             if 0 ≤ n ∧ n ≤ u16_max then n
             else usize_to_int (int_to_usize n)
    
+   [vec_index_back_spec]  Theorem
+      
+      ⊢ ∀v i.
+          usize_to_int i < usize_to_int (vec_len v) ⇒
+          vec_index_back v i = Return ()
+   
+   [vec_index_fwd_spec]  Theorem
+      
+      ⊢ ∀v i.
+          usize_to_int i < usize_to_int (vec_len v) ⇒
+          vec_index_fwd v i = Return (vec_index v i)
+   
+   [vec_index_mut_back_spec]  Theorem
+      
+      ⊢ ∀v i x.
+          usize_to_int i < usize_to_int (vec_len v) ⇒
+          vec_index_mut_back v i x = Return (vec_update v i x)
+   
+   [vec_index_mut_fwd_spec]  Theorem
+      
+      ⊢ ∀v i.
+          usize_to_int i < usize_to_int (vec_len v) ⇒
+          vec_index_mut_fwd v i = Return (vec_index v i)
+   
    [vec_insert_back_spec]  Theorem
       
-      [oracles: DISK_THM]
-      [axioms: vec_to_list_num_bounds, usize_bounds,
-       int_to_usize_usize_to_int, usize_to_int_bounds,
-       usize_to_int_int_to_usize, mk_vec_axiom] []
       ⊢ ∀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 ∧
-            ∀j. usize_to_int j < usize_to_int (vec_len nv) ⇒
-                usize_to_int j ≠ usize_to_int i ⇒
-                vec_index j nv = vec_index j v
+          vec_insert_back v i x = Return (vec_update v i x)
    
    [vec_len_spec]  Theorem
       
@@ -2318,11 +2394,62 @@ sig
       ⊢ ∀v. vec_len v = int_to_usize (len (vec_to_list v)) ∧
             0 ≤ len (vec_to_list v) ∧ len (vec_to_list v) ≤ usize_max
    
+   [vec_len_vec_new]  Theorem
+      
+      [oracles: DISK_THM]
+      [axioms: mk_vec_axiom, int_to_usize_usize_to_int,
+       usize_to_int_int_to_usize, usize_bounds] []
+      ⊢ vec_len vec_new = int_to_usize 0
+   
+   [vec_push_back_spec]  Theorem
+      
+      [oracles: DISK_THM]
+      [axioms: usize_to_int_int_to_usize, mk_vec_axiom,
+       int_to_usize_usize_to_int, usize_bounds, vec_to_list_num_bounds] []
+      ⊢ ∀v x.
+          usize_to_int (vec_len v) < usize_max ⇒
+          ∃nv.
+            vec_push_back v x = Return nv ∧
+            vec_to_list nv = vec_to_list v ⧺ [x]
+   
+   [vec_push_back_unfold]  Theorem
+      
+      [oracles: DISK_THM] [axioms: usize_bounds] []
+      ⊢ ∀v x.
+          vec_push_back v x =
+          if
+            usize_to_int (vec_len v) < u16_max ∨
+            usize_to_int (vec_len v) < usize_max
+          then
+            Return (mk_vec (vec_to_list v ⧺ [x]))
+          else Fail Failure
+   
    [vec_to_list_int_bounds]  Theorem
       
       [oracles: DISK_THM] [axioms: usize_bounds, vec_to_list_num_bounds] []
       ⊢ ∀v. 0 ≤ len (vec_to_list v) ∧ len (vec_to_list v) ≤ usize_max
    
+   [vec_to_list_vec_new]  Theorem
+      
+      [oracles: DISK_THM] [axioms: mk_vec_axiom, usize_bounds] []
+      ⊢ vec_to_list vec_new = []
+   
+   [vec_update_eq]  Theorem
+      
+      [oracles: DISK_THM]
+      [axioms: vec_to_list_num_bounds, usize_bounds,
+       int_to_usize_usize_to_int, usize_to_int_bounds,
+       usize_to_int_int_to_usize, 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)
+   
    
 *)
 end