Make good progress on the proofs of the hashmap in HOL4

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