Finish the proofs of the hashmap

5 files changed, 98 insertions, 9 deletions

diff --git a/backends/hol4/ilistScript.sml b/backends/hol4/ilistScript.sml
index 2183ef77..fb0c7688 100644
--- a/backends/hol4/ilistScript.sml
+++ b/backends/hol4/ilistScript.sml
@@ -16,6 +16,7 @@ val len_def = Define ‘
   len [] : int = 0 /\
   len (x :: ls) : int = 1 + len ls
 ’
+val _ = BasicProvers.export_rewrites ["len_def"]
 
 (* Return the ith element of a list.
 
@@ -117,6 +118,7 @@ Theorem len_append:
 Proof
   rw [len_eq_LENGTH] >> cooper_tac
 QED
+val _ = BasicProvers.export_rewrites ["len_append"]
 
 Theorem append_len_eq:
   (∀l1 l2 l1' l2'.
@@ -129,6 +131,18 @@ Proof
   rw [len_eq_LENGTH] >> fs [APPEND_11_LENGTH]
 QED
 
+Theorem drop_more_than_length:
+  ∀ ls i.
+  len ls ≤ i ⇒
+  drop i ls = []
+Proof
+  Induct_on ‘ls’ >>
+  rw [drop_def] >>
+  qspec_assume ‘ls’ len_pos >> try_tac int_tac >>
+  last_x_assum irule >>
+  int_tac
+QED
+
 (* TODO: prove more theorems, and add rewriting theorems *)
 
 val _ = export_theory ()
diff --git a/backends/hol4/ilistTheory.sig b/backends/hol4/ilistTheory.sig
index da7cdbb3..26f455d6 100644
--- a/backends/hol4/ilistTheory.sig
+++ b/backends/hol4/ilistTheory.sig
@@ -11,6 +11,7 @@ sig
   (*  Theorems  *)
     val append_len_eq : thm
     val drop_eq : thm
+    val drop_more_than_length : thm
     val index_eq : thm
     val index_eq_EL : thm
     val len_append : thm
@@ -62,6 +63,10 @@ sig
           drop i (x::ls) =
           if 0 < i ∨ 0 ≤ i ∧ i ≠ 0 then drop (i − 1) ls else x::ls
    
+   [drop_more_than_length]  Theorem
+      
+      ⊢ ∀ls i. len ls ≤ i ⇒ drop i ls = []
+   
    [index_eq]  Theorem
       
       ⊢ (∀x ls. index 0 (x::ls) = x) ∧
diff --git a/backends/hol4/primitivesArithTheory.sig b/backends/hol4/primitivesArithTheory.sig
index 84b9b67a..85a627d2 100644
--- a/backends/hol4/primitivesArithTheory.sig
+++ b/backends/hol4/primitivesArithTheory.sig
@@ -15,13 +15,16 @@ sig
     val le_eq_ge : thm
     val lt_eq_gt : thm
     val mul_pos_left_le : thm
+    val mul_pos_left_lt : thm
     val mul_pos_right_le : thm
+    val mul_pos_right_lt : thm
     val not_ge_eq_lt : thm
     val not_gt_eq_le : thm
     val not_le_eq_gt : thm
     val not_lt_eq_ge : thm
     val num_sub_1_eq : thm
     val num_sub_eq : thm
+    val pos_div_pos_ge : thm
     val pos_div_pos_is_pos : thm
     val pos_div_pos_le : thm
     val pos_div_pos_le_init : thm
@@ -30,9 +33,13 @@ sig
     val pos_mod_pos_is_pos : thm
     val pos_mod_pos_le_init : thm
     val pos_mod_pos_lt : thm
+    val pos_mul_2_div_pos_decompose : thm
     val pos_mul_left_pos_le : thm
+    val pos_mul_left_pos_lt : thm
+    val pos_mul_pos_div_pos_decompose : thm
     val pos_mul_pos_is_pos : thm
     val pos_mul_right_pos_le : thm
+    val pos_mul_right_pos_lt : thm
   
   val primitivesArith_grammars : type_grammar.grammar * term_grammar.grammar
 (*
@@ -88,10 +95,18 @@ sig
       
       ⊢ ∀a x y. 0 ≤ a ⇒ x ≤ y ⇒ a * x ≤ a * y
    
+   [mul_pos_left_lt]  Theorem
+      
+      ⊢ ∀a x y. 0 < a ⇒ x < y ⇒ a * x < a * y
+   
    [mul_pos_right_le]  Theorem
       
       ⊢ ∀a x y. 0 ≤ a ⇒ x ≤ y ⇒ x * a ≤ y * a
    
+   [mul_pos_right_lt]  Theorem
+      
+      ⊢ ∀a x y. 0 < a ⇒ x < y ⇒ x * a < y * a
+   
    [not_ge_eq_lt]  Theorem
       
       ⊢ ∀x y. ¬(x ≥ y) ⇔ x < y
@@ -116,6 +131,10 @@ sig
       
       ⊢ ∀x y z. x = y − z ⇒ 0 ≤ x ⇒ 0 ≤ z ⇒ Num y = Num z + Num x
    
+   [pos_div_pos_ge]  Theorem
+      
+      ⊢ ∀x y d. 0 ≤ x ⇒ 0 ≤ y ⇒ 0 < d ⇒ x ≥ y ⇒ x / d ≥ y / d
+   
    [pos_div_pos_is_pos]  Theorem
       
       ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ 0 ≤ x / y
@@ -148,10 +167,22 @@ sig
       
       ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ x % y < y
    
+   [pos_mul_2_div_pos_decompose]  Theorem
+      
+      ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ x / y + x / y ≤ x * 2 / y
+   
    [pos_mul_left_pos_le]  Theorem
       
       ⊢ ∀a x. 0 < a ⇒ 0 ≤ x ⇒ x ≤ a * x
    
+   [pos_mul_left_pos_lt]  Theorem
+      
+      ⊢ ∀a x. 1 < a ⇒ 0 < x ⇒ x < a * x
+   
+   [pos_mul_pos_div_pos_decompose]  Theorem
+      
+      ⊢ ∀x y z. 0 ≤ x ⇒ 0 ≤ y ⇒ 0 < z ⇒ x / z + y / z ≤ (x + y) / z
+   
    [pos_mul_pos_is_pos]  Theorem
       
       ⊢ ∀x y. 0 ≤ x ⇒ 0 ≤ y ⇒ 0 ≤ x * y
@@ -160,6 +191,10 @@ sig
       
       ⊢ ∀a x. 0 < a ⇒ 0 ≤ x ⇒ x ≤ x * a
    
+   [pos_mul_right_pos_lt]  Theorem
+      
+      ⊢ ∀a x. 1 < a ⇒ 0 < x ⇒ x < x * a
+   
    
 *)
 end
diff --git a/backends/hol4/primitivesScript.sml b/backends/hol4/primitivesScript.sml
index 4378f9c3..82da4de9 100644
--- a/backends/hol4/primitivesScript.sml
+++ b/backends/hol4/primitivesScript.sml
@@ -1702,16 +1702,16 @@ QED
 
 Theorem update_spec:
   ∀ls i y.
-    0 <= i ⇒
-    i < len ls ⇒
     len (update ls i y) = len ls ∧
-    index i (update ls i y) = y ∧
-    ∀j. j < len ls ⇒ j ≠ i ⇒ index j (update ls i y) = index j ls
+    (0 <= i ⇒
+     i < len ls ⇒
+     index i (update ls i y) = y ∧
+     ∀j. j < len ls ⇒ j ≠ i ⇒ index j (update ls i y) = index j ls)
 Proof
   Induct_on ‘ls’ >> Cases_on ‘i = 0’ >> rw [update_def, len_def, index_def] >>
   try_tac (exfalso >> cooper_tac) >>
   try_tac (
-    pop_last_assum (qspecl_assume [‘i' - 1’, ‘y’]) >>
+    pop_last_assum (qspecl_assume [‘i' - 1’, ‘y’]) >> fs [] >>
     pop_assum sg_premise_tac >- cooper_tac >>
     pop_assum sg_premise_tac >- cooper_tac >>
     rw [])
@@ -1722,6 +1722,13 @@ Proof
     rw [])
 QED
 
+Theorem len_update:
+  ∀ ls i y. len (update ls i y) = len ls
+Proof
+ fs [update_spec]
+QED
+val _ = BasicProvers.export_rewrites ["len_update"]
+
 Theorem index_update_same:
   ∀ls i j y.
     0 <= i ⇒
@@ -1832,6 +1839,18 @@ Proof
   sg_dep_rewrite_all_tac index_update_same >- cooper_tac >> fs []
 QED
 
+Theorem vec_to_list_vec_update:
+  ∀ v i x. vec_to_list (vec_update v i x) = update (vec_to_list v) (usize_to_int i) x
+Proof
+  rw [vec_update_def] >>
+  qspec_assume ‘v’ vec_len_spec >>
+  qspecl_assume [‘v’, ‘i’, ‘x’] vec_update_eq >> fs [] >>
+  qspecl_assume [‘vec_to_list v’, ‘usize_to_int i’, ‘x’] update_len >>
+  sg_dep_rewrite_all_tac mk_vec_axiom >- fs [] >>
+  fs []
+QED
+val _ = export_rewrites ["vec_to_list_vec_update"]
+
 Definition vec_index_fwd_def:
   vec_index_fwd v i =
     if usize_to_int i ≤ usize_to_int (vec_len v)
diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig
index 7e03987b..ae7f083d 100644
--- a/backends/hol4/primitivesTheory.sig
+++ b/backends/hol4/primitivesTheory.sig
@@ -278,6 +278,7 @@ sig
     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 len_update : thm
     val mk_isize_unfold : thm
     val mk_usize_unfold : thm
     val mk_vec_unfold : thm
@@ -349,6 +350,7 @@ sig
     val vec_push_back_unfold : thm
     val vec_to_list_int_bounds : thm
     val vec_to_list_vec_new : thm
+    val vec_to_list_vec_update : thm
     val vec_update_eq : thm
   
   val primitives_grammars : type_grammar.grammar * term_grammar.grammar
@@ -1907,6 +1909,10 @@ sig
             if i16_min ≤ n ∧ n ≤ i16_max then n
             else isize_to_int (int_to_isize n)
    
+   [len_update]  Theorem
+      
+      ⊢ ∀ls i y. len (update ls i y) = len ls
+   
    [mk_isize_unfold]  Theorem
       
       [oracles: DISK_THM] [axioms: isize_bounds] []
@@ -2305,10 +2311,11 @@ sig
    [update_spec]  Theorem
       
       ⊢ ∀ls i y.
-          0 ≤ i ⇒
-          i < len ls ⇒
-          len (update ls i y) = len ls ∧ index i (update ls i y) = y ∧
-          ∀j. j < len ls ⇒ j ≠ i ⇒ index j (update ls i y) = index j ls
+          len (update ls i y) = len ls ∧
+          (0 ≤ i ⇒
+           i < len ls ⇒
+           index i (update ls i y) = y ∧
+           ∀j. j < len ls ⇒ j ≠ i ⇒ index j (update ls i y) = index j ls)
    
    [usize_add_eq]  Theorem
       
@@ -2454,6 +2461,15 @@ sig
       [oracles: DISK_THM] [axioms: mk_vec_axiom, usize_bounds] []
       ⊢ vec_to_list vec_new = []
    
+   [vec_to_list_vec_update]  Theorem
+      
+      [oracles: DISK_THM]
+      [axioms: mk_vec_axiom, usize_to_int_bounds,
+       usize_to_int_int_to_usize, usize_bounds, vec_to_list_num_bounds] []
+      ⊢ ∀v i x.
+          vec_to_list (vec_update v i x) =
+          update (vec_to_list v) (usize_to_int i) x
+   
    [vec_update_eq]  Theorem
       
       [oracles: DISK_THM]