Make progress on the standard library for HOL4

9 files changed, 1041 insertions, 91 deletions

diff --git a/backends/hol4/ilistScript.sml b/backends/hol4/ilistScript.sml
index 3e17dcc8..c871ba04 100644
--- a/backends/hol4/ilistScript.sml
+++ b/backends/hol4/ilistScript.sml
@@ -26,10 +26,25 @@ val len_def = Define ‘
    “index (i : int) [] = EL (Num i) []”
  *)
 val index_def = Define ‘
-  index (i : int) [] = EL (Num i) [] ∧
   index (i : int) (x :: ls) = if i = 0 then x else (if 0 < i then index (i - 1) ls else ARB)
 ’
 
+(* We use the following theorem as a rewriting theorem for [index]: it performs
+   better with the rewritings.
+
+   TODO: we could even write:
+   if (0 < i) ∨ (i > 0) ∨ ((0 ≤ i ∨ i >= 0) ∧ (i ≠ 0 ∨ 0 ≠ i)) then ...
+ *)
+Theorem index_eq:
+  (∀x ls. index 0 (x :: ls) = x) ∧
+  (∀i x ls. index i (x :: ls) =
+    if (0 < i) ∨ (0 ≤ i ∧ i ≠ 0) then index (i - 1) ls
+    else (if i = 0 then x else ARB))
+Proof
+  rw [index_def] >> fs [] >>
+  exfalso >> cooper_tac
+QED
+
 val update_def = Define ‘
   update ([] : 'a list) (i : int) (y : 'a) : 'a list = [] ∧
 
@@ -37,6 +52,20 @@ val update_def = Define ‘
     if i = 0 then y :: ls else (if 0 < i then x :: update ls (i - 1) y else x :: ls)
 ’
 
+Theorem update_eq:
+  (∀i y. update ([] : 'a list) (i : int) (y : 'a) : 'a list = []) ∧
+
+  (∀x ls y. update (x :: ls) 0 y = y :: ls) ∧
+
+  (∀x ls i y.
+   update (x :: ls) i y =
+     if (0 < i) ∨ (0 ≤ i ∧ i ≠ 0) then x :: update ls (i - 1) y
+     else if i < 0 then x :: ls else y :: ls)
+Proof
+  rw [update_def] >> fs [] >>
+  exfalso >> cooper_tac
+QED
+
 Theorem len_eq_LENGTH:
   ∀ls. len ls = &(LENGTH ls)
 Proof
@@ -49,11 +78,9 @@ Theorem index_eq_EL:
     i < len ls ⇒
     index i ls = EL (Num i) ls
 Proof  
-  Induct_on ‘ls’ >> rpt strip_tac >> fs [len_def, index_def] >>
+  Induct_on ‘ls’ >> rpt strip_tac >> fs [len_def, index_eq] >- int_tac >>
   Cases_on ‘i = 0’ >> fs [] >>
-  (* TODO: automate *)
-  sg ‘0 < i’ >- cooper_tac >> fs [] >>
-  Cases_on ‘Num i’ >- (exfalso >> cooper_tac) >> fs [] >>
+  Cases_on ‘Num i’ >- (int_tac) >> fs [] >>
   last_assum (qspec_assume ‘i - 1’) >>
   pop_assum sg_premise_tac >- cooper_tac >>
   sg ‘n = Num (i - 1)’ >- cooper_tac >> fs [] >>
diff --git a/backends/hol4/ilistTheory.sig b/backends/hol4/ilistTheory.sig
index 9612f063..249b362c 100644
--- a/backends/hol4/ilistTheory.sig
+++ b/backends/hol4/ilistTheory.sig
@@ -9,9 +9,11 @@ sig
   
   (*  Theorems  *)
     val append_len_eq : thm
+    val index_eq : thm
     val index_eq_EL : thm
     val len_append : thm
     val len_eq_LENGTH : thm
+    val update_eq : thm
   
   val ilist_grammars : type_grammar.grammar * term_grammar.grammar
 (*
@@ -21,8 +23,7 @@ sig
    
    [index_def]  Definition
       
-      ⊢ (∀i. index i [] = EL (Num i) []) ∧
-        ∀i x ls.
+      ⊢ ∀i x ls.
           index i (x::ls) =
           if i = 0 then x else if 0 < i then index (i − 1) ls else ARB
    
@@ -46,6 +47,15 @@ sig
         ∀l1 l2 l1' l2'.
           len l2 = len l2' ⇒ (l1 ⧺ l2 = l1' ⧺ l2' ⇔ l1 = l1' ∧ l2 = l2')
    
+   [index_eq]  Theorem
+      
+      ⊢ (∀x ls. index 0 (x::ls) = x) ∧
+        ∀i x ls.
+          index i (x::ls) =
+          if 0 < i ∨ 0 ≤ i ∧ i ≠ 0 then index (i − 1) ls
+          else if i = 0 then x
+          else ARB
+   
    [index_eq_EL]  Theorem
       
       ⊢ ∀i ls. 0 ≤ i ⇒ i < len ls ⇒ index i ls = EL (Num i) ls
@@ -58,6 +68,16 @@ sig
       
       ⊢ ∀ls. len ls = &LENGTH ls
    
+   [update_eq]  Theorem
+      
+      ⊢ (∀i y. update [] i y = []) ∧
+        (∀x ls y. update (x::ls) 0 y = y::ls) ∧
+        ∀x ls i y.
+          update (x::ls) i y =
+          if 0 < i ∨ 0 ≤ i ∧ i ≠ 0 then x::update ls (i − 1) y
+          else if i < 0 then x::ls
+          else y::ls
+   
    
 *)
 end
diff --git a/backends/hol4/primitivesArithScript.sml b/backends/hol4/primitivesArithScript.sml
index eb2548fd..6c96c908 100644
--- a/backends/hol4/primitivesArithScript.sml
+++ b/backends/hol4/primitivesArithScript.sml
@@ -78,6 +78,13 @@ Proof
   fs [Num]
 QED
 
+(* TODO: use as rewriting theorem by default? *)
+Theorem add_sub_same_eq:
+  ∀(i j : int). i + j - j = i
+Proof
+  cooper_tac
+QED
+
 Theorem num_sub_eq:
   !(x y z : int). x = y - z ==> 0 <= x ==> 0 <= z ==> Num y = Num z + Num x
 Proof
diff --git a/backends/hol4/primitivesArithTheory.sig b/backends/hol4/primitivesArithTheory.sig
index b2172b7c..e32b49d4 100644
--- a/backends/hol4/primitivesArithTheory.sig
+++ b/backends/hol4/primitivesArithTheory.sig
@@ -3,6 +3,7 @@ sig
   type thm = Thm.thm
   
   (*  Theorems  *)
+    val add_sub_same_eq : thm
     val ge_eq_le : thm
     val gt_eq_lt : thm
     val int_add : thm
@@ -31,6 +32,10 @@ sig
    
    [int_arith] Parent theory of "primitivesArith"
    
+   [add_sub_same_eq]  Theorem
+      
+      ⊢ ∀i j. i + j − j = i
+   
    [ge_eq_le]  Theorem
       
       ⊢ ∀x y. x ≥ y ⇔ y ≤ x
diff --git a/backends/hol4/primitivesBaseTacLib.sml b/backends/hol4/primitivesBaseTacLib.sml
index bff4f7c9..3f298a04 100644
--- a/backends/hol4/primitivesBaseTacLib.sml
+++ b/backends/hol4/primitivesBaseTacLib.sml
@@ -20,10 +20,12 @@ val pop_ignore_tac = pop_assum ignore_tac
 val exfalso : tactic =
   SUBGOAL_THEN “F” (fn th => ASSUME_TAC th >> fs[])
 
+val case_tac = CASE_TAC
 val try_tac = TRY
 val first_tac = FIRST
-val map_first = MAP_FIRST
+val map_first_tac = MAP_FIRST
 val fail_tac = FAIL_TAC
+val map_every_tac = MAP_EVERY
 
 fun qspec_assume x th = qspec_then x assume_tac th
 fun qspecl_assume xl th = qspecl_then xl assume_tac th
@@ -31,8 +33,8 @@ fun first_qspec_assume x = first_assum (qspec_assume x)
 fun first_qspecl_assume xl = first_assum (qspecl_assume xl)
 
 val all_tac = all_tac
-val cooper_tac = COOPER_TAC
 val pure_rewrite_tac = PURE_REWRITE_TAC
+val pure_asm_rewrite_tac = PURE_ASM_REWRITE_TAC
 val pure_once_rewrite_tac = PURE_ONCE_REWRITE_TAC
 
 (* Dependent rewrites *)
@@ -419,7 +421,7 @@ apply_dep_rewrites_match_concl_tac
 
    Leaves the premises as subgoals if [prove_premise] doesn't prove them.
  *)
-fun apply_dep_rewrites_match_first_premise_tac
+fun apply_dep_rewrites_match_first_premise_with_all_tac
   (keep : thm -> bool)
   (prove_premise : tactic) (then_tac : thm_tactic) (th : thm) : tactic =
   fn (asms, g) =>
@@ -435,7 +437,90 @@ fun apply_dep_rewrites_match_first_premise_tac
         end;
     in
       (* Apply each theorem *)
-      MAP_EVERY apply_tac thms (asms, g)
+      map_every_tac apply_tac thms (asms, g)
     end
 
+val cooper_tac = COOPER_TAC
+
+(* TODO: COOPER_TAC fails in the proof below, because of x <> y. We should
+   create an issue/PR for HOL4.
+
+Theorem cooper_fail:
+  ∀(x y : 'a). x ≠ y ==> 0 ≤ i ==> i ≠ 0 ⇒ 0 < i
+Proof
+  rw [] >> cooper_tac
+QED
+
+*)
+
+(* Filter the assumptions in the goal *)
+fun filter_assums_tac (keep : term -> bool) : tactic =
+  fn (asms, g) =>
+  let
+    val kept_asms = filter keep asms
+    (* The validation function *)
+    fun valid thms =
+      case thms of
+        [th] =>
+        let
+          (* Being a bit brutal - will optimize later *)
+          val tac = ntac (length asms) strip_tac >> irule th >> pure_asm_rewrite_tac []
+          val th = prove (list_mk_imp (asms, g), tac)
+          val th = foldl (fn (_, th) => UNDISCH th) th asms
+        in th end
+      | _ => failwith "filter_assums: expected exactly one theorem"
+  in
+    ([(kept_asms, g)], valid)
+  end
+
+(* Destruct the conjunctions in the assumptions *)
+val dest_assums_conjs_tac : tactic =
+  fn (asms, g) =>
+  let
+    (* Destruct the conjunctions *)
+    val dest_asms = flatten (map (rev o strip_conj) asms)
+    (* The validation function *)
+    fun valid thms =
+      case thms of
+        [th] =>
+        let
+          (* Being a bit brutal - will optimize later *)
+          val tac = ntac (length asms) strip_tac >> irule th >> pure_asm_rewrite_tac []
+          val th = prove (list_mk_imp (asms, g), tac)
+          val th = foldl (fn (_, th) => UNDISCH th) th asms
+        in th end
+      | _ => failwith "dest_assums_conjs: expected exactly one theorem"
+  in
+    ([(dest_asms, g)], valid)
+  end
+
+(* Defining those here so that they are evaluated once and for all (parsing
+   depends on the context) *)
+val int_tac_int_ty = “:int”
+val int_tac_pat = “(x : 'a) <> (y : 'a)”
+
+(* We boost COOPER_TAC a bit *)
+fun int_tac (asms, g) =
+  let
+    (* Following the bug we discovered in COOPER_TAC, we filter all the
+       inequalities which terms are not between terms of type “:int”.
+
+       TODO: issue/PR for HOL4
+     *)
+    fun keep (asm : term) : bool =
+      let
+        val (_, s) = match_term int_tac_pat asm
+      in
+        case s of
+          [{redex = _, residue = ty}] => ty = int_tac_int_ty
+        | [] => (* Can happen if the term has exactly the same types as the pattern - unlikely *) false
+        | _ =>  failwith "int_tac: match error"
+      end
+      handle HOL_ERR _ => true
+   in
+     (dest_assums_conjs_tac >>
+      filter_assums_tac keep >>
+      first_tac [cooper_tac, exfalso >> cooper_tac]) (asms, g)
+   end
+
 end
diff --git a/backends/hol4/primitivesScript.sml b/backends/hol4/primitivesScript.sml
index 5dba408e..6dd9f6ec 100644
--- a/backends/hol4/primitivesScript.sml
+++ b/backends/hol4/primitivesScript.sml
@@ -125,8 +125,8 @@ val all_bound_defs = [
 ]
 
 (* The following bounds are valid for all architectures *)
-val isize_bounds = new_axiom ("isize_bounds", “isize_min <= i16_min /\ isize_max >= i16_max”)
-val usize_bounds = new_axiom ("usize_bounds", “usize_max >= u16_max”)
+val isize_bounds = new_axiom ("isize_bounds", “isize_min <= i16_min /\ i16_max <= isize_max”)
+val usize_bounds = new_axiom ("usize_bounds", “u16_max <= usize_max”)
 
 (* Conversion bounds *)
 val isize_to_int_bounds = new_axiom ("isize_to_int_bounds",
@@ -534,7 +534,7 @@ fun prove_arith_op_eq (asms, g) =
     val y = (snd o dest_comb) y_to_int;
     val rw_thms = int_rem_def :: List.concat [all_rem_defs, all_add_defs, all_sub_defs, all_mul_defs, all_div_defs, all_mk_int_defs, all_to_int_bounds_lemmas, all_conversion_id_lemmas];
     fun inst_first_lem arg lems =
-      map_first (fn th => (assume_tac (SPEC arg th) handle HOL_ERR _ => fail_tac "")) lems;
+      map_first_tac (fn th => (assume_tac (SPEC arg th) handle HOL_ERR _ => fail_tac "")) lems;
   in
     (rpt gen_tac >>
      rpt disch_tac >>
@@ -661,21 +661,6 @@ Theorem isize_add_eq:
 Proof
   prove_arith_op_eq
 QED
-
-val all_add_eqs = [
-  isize_add_eq,
-  i8_add_eq,
-  i16_add_eq,
-  i32_add_eq,
-  i64_add_eq,
-  i128_add_eq,
-  usize_add_eq,
-  u8_add_eq,
-  u16_add_eq,
-  u32_add_eq,
-  u64_add_eq,
-  u128_add_eq
-]
       
 Theorem u8_sub_eq:
   !x y.
@@ -779,21 +764,6 @@ Proof
   prove_arith_op_eq
 QED
 
-val all_sub_eqs = [
-  isize_sub_eq,
-  i8_sub_eq,
-  i16_sub_eq,
-  i32_sub_eq,
-  i64_sub_eq,
-  i128_sub_eq,
-  usize_sub_eq,
-  u8_sub_eq,
-  u16_sub_eq,
-  u32_sub_eq,
-  u64_sub_eq,
-  u128_sub_eq
-]
-
 Theorem u8_mul_eq:
   !x y.
     u8_to_int x * u8_to_int y <= u8_max ==>
@@ -896,21 +866,6 @@ Proof
   prove_arith_op_eq
 QED
 
-val all_mul_eqs = [
-  isize_mul_eq,
-  i8_mul_eq,
-  i16_mul_eq,
-  i32_mul_eq,
-  i64_mul_eq,
-  i128_mul_eq,
-  usize_mul_eq,
-  u8_mul_eq,
-  u16_mul_eq,
-  u32_mul_eq,
-  u64_mul_eq,
-  u128_mul_eq
-]
-
 Theorem u8_div_eq:
   !x y.
     u8_to_int y <> 0 ==>
@@ -1019,21 +974,6 @@ Proof
   prove_arith_op_eq
 QED
 
-val all_div_eqs = [
-  isize_div_eq,
-  i8_div_eq,
-  i16_div_eq,
-  i32_div_eq,
-  i64_div_eq,
-  i128_div_eq,
-  usize_div_eq,
-  u8_div_eq,
-  u16_div_eq,
-  u32_div_eq,
-  u64_div_eq,
-  u128_div_eq
-]
-
 Theorem u8_rem_eq:
   !x y.
     u8_to_int y <> 0 ==>
@@ -1144,21 +1084,6 @@ Proof
   prove_arith_op_eq
 QED
 
-val all_rem_eqs = [
-  isize_rem_eq,
-  i8_rem_eq,
-  i16_rem_eq,
-  i32_rem_eq,
-  i64_rem_eq,
-  i128_rem_eq,
-  usize_rem_eq,
-  u8_rem_eq,
-  u16_rem_eq,
-  u32_rem_eq,
-  u64_rem_eq,
-  u128_rem_eq
-]
-
 
 (***
  * Vectors
diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig
index 583f66bd..bac7fd4f 100644
--- a/backends/hol4/primitivesTheory.sig
+++ b/backends/hol4/primitivesTheory.sig
@@ -249,11 +249,11 @@ sig
    [isize_bounds]  Axiom
       
       [oracles: ] [axioms: isize_bounds] []
-      ⊢ isize_min ≤ i16_min ∧ isize_max ≥ i16_max
+      ⊢ isize_min ≤ i16_min ∧ i16_max ≤ isize_max
    
    [usize_bounds]  Axiom
       
-      [oracles: ] [axioms: usize_bounds] [] ⊢ usize_max ≥ u16_max
+      [oracles: ] [axioms: usize_bounds] [] ⊢ u16_max ≤ usize_max
    
    [isize_to_int_bounds]  Axiom
       
diff --git a/backends/hol4/testHashmapScript.sml b/backends/hol4/testHashmapScript.sml
new file mode 100644
index 00000000..71b0109d
--- /dev/null
+++ b/backends/hol4/testHashmapScript.sml
@@ -0,0 +1,679 @@
+open HolKernel boolLib bossLib Parse
+open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory
+
+open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory
+
+val _ = new_theory "testHashmap"
+
+val primitives_theory_name = "primitives"
+
+(* 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:
+   for now we simply put all the assumptions in a set, but in the future
+   we might want to split the assumptions which are conjunctions in order
+   to be more precise.
+ *)
+fun compute_asms_set ((asms,g) : goal) : term Redblackset.set =
+  Redblackset.fromList Term.compare asms
+
+val integer_bounds_defs_list = [
+  i8_min_def,
+  i8_max_def,
+  i16_min_def,
+  i16_max_def,
+  i32_min_def,
+  i32_max_def,
+  i64_min_def,
+  i64_max_def,
+  i128_min_def,
+  i128_max_def,
+  u8_max_def,
+  u16_max_def,
+  u32_max_def,
+  u64_max_def,
+  u128_max_def
+]
+
+val integer_bounds_lemmas =
+  Redblackmap.fromList String.compare
+  [
+    ("isize", isize_to_int_bounds),
+    ("i8", i8_to_int_bounds),
+    ("i16", i16_to_int_bounds),
+    ("i32", i32_to_int_bounds),
+    ("i64", i64_to_int_bounds),
+    ("i128", i128_to_int_bounds),
+    ("usize", usize_to_int_bounds),
+    ("u8", u8_to_int_bounds),
+    ("u16", u16_to_int_bounds),
+    ("u32", u32_to_int_bounds),
+    ("u64", u64_to_int_bounds),
+    ("u128", u128_to_int_bounds)
+  ]
+
+val integer_types_names =
+  Redblackset.fromList String.compare
+  (map fst (Redblackmap.listItems integer_bounds_lemmas))
+
+(* See {!assume_bounds_for_all_int_vars}.
+
+   This tactic is in charge of adding assumptions for one variable.
+ *)
+fun assume_bounds_for_int_var
+  (asms_set: term Redblackset.set) (var : string) (ty : string) :
+  tactic =
+  let
+    (* Lookup the lemma to apply *)
+    val lemma = Redblackmap.find (integer_bounds_lemmas, ty);
+    (* Instantiate the lemma *)
+    val ty_t = mk_type (ty, []);
+    val var_t = mk_var (var, ty_t);
+    val lemma = SPEC var_t lemma;
+    (* Split the theorem into a list of conjuncts.
+
+       The bounds are typically a conjunction:
+       {[
+         ⊢ 0 ≤ u32_to_int x ∧ u32_to_int x ≤ u32_max: thm
+       ]}
+     *)
+    val lemmas = CONJUNCTS lemma;
+    (* Filter the conjuncts: some of them might already be in the context,
+       we don't want to introduce them again, as it would pollute it.
+     *)
+    val lemmas = filter (fn lem => not (Redblackset.member (asms_set, concl lem))) lemmas;
+   in
+  (* Introduce the assumptions in the context *)
+  assume_tacl lemmas
+  end
+
+(* Introduce bound assumptions for all the machine integers in the context.
+
+   Exemple:
+   ========
+   If there is “x : u32” in the input set, then we introduce:
+   {[
+     0 <= u32_to_int x
+     u32_to_int x <= u32_max
+   ]}
+ *)
+fun assume_bounds_for_all_int_vars (asms, g) =
+  let
+    (* Compute the set of integer variables in the context *)
+    val vars = free_varsl (g :: asms);
+    (* Compute the set of assumptions already present in the context *)
+    val asms_set = compute_asms_set (asms, g);
+    val vartys_set = ref (Redblackset.empty String.compare);
+    (* Filter the variables to keep only the ones with type machine integer,
+       decompose the types at the same time *)
+    fun decompose_var (v : term) : (string * string) =
+      let
+        val (v, ty) = dest_var v;
+        val {Args=args, Thy=thy, Tyop=ty} = dest_thy_type ty;
+        val _ = assert null args;
+        val _ = assert (fn thy => thy = primitives_theory_name) thy;
+        val _ = assert (fn ty => Redblackset.member (integer_types_names, ty)) ty;
+        val _ = vartys_set := Redblackset.add (!vartys_set, ty);
+      in (v, ty) end;
+    val vars = mapfilter decompose_var vars; 
+    (* Add assumptions for one variable *)
+    fun add_var_asm (v, ty) : tactic =
+      assume_bounds_for_int_var asms_set v ty;
+    (* Add the bounds for isize, usize *)
+    val size_bounds =
+      append
+        (if Redblackset.member (!vartys_set, "usize") then CONJUNCTS usize_bounds else [])
+        (if Redblackset.member (!vartys_set, "isize") then CONJUNCTS isize_bounds else []);
+    val size_bounds =
+      filter (fn th => not (Redblackset.member (asms_set, concl th))) size_bounds;
+  in
+    ((* Add assumptions for all the variables *)
+     map_every_tac add_var_asm vars >>
+     (* Add assumptions about the size bounds *)
+     assume_tacl size_bounds) (asms, g)
+  end
+
+val integer_conversion_lemmas_list = [
+  isize_to_int_int_to_isize,
+  i8_to_int_int_to_i8,
+  i16_to_int_int_to_i16,
+  i32_to_int_int_to_i32,
+  i64_to_int_int_to_i64,
+  i128_to_int_int_to_i128,
+  usize_to_int_int_to_usize,
+  u8_to_int_int_to_u8,
+  u16_to_int_int_to_u16,
+  u32_to_int_int_to_u32,
+  u64_to_int_int_to_u64,
+  u128_to_int_int_to_u128
+]
+
+(* Look for conversions from integers to machine integers and back.
+   {[
+     u32_to_int (int_to_u32 x)
+   ]}
+
+   Attempts to prove and apply equalities of the form:
+   {[
+     u32_to_int (int_to_u32 x) = x
+   ]}
+ *)
+val rewrite_with_dep_int_lemmas : tactic =
+  (* We're not trying to be smart: we just try to rewrite with each theorem at
+     a time *)
+  let
+    val prove_premise = full_simp_tac simpLib.empty_ss integer_bounds_defs_list >> cooper_tac;
+    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;
+    val then_tac2 = (fn th => full_simp_tac simpLib.empty_ss [th]);
+    val rewr_tac2 = apply_dep_rewrites_match_first_premise_with_all_tac (fn _ => true) prove_premise then_tac2;
+  in
+      map_every_tac rewr_tac1 integer_conversion_lemmas_list >>
+      map_every_tac rewr_tac2 []
+  end
+
+(* Massage a bit the goal, for instance by introducing integer bounds in the
+   assumptions.
+*)
+val massage : tactic =
+  assume_bounds_for_all_int_vars >>
+  rewrite_with_dep_int_lemmas
+
+(* Lexicographic order over pairs *)
+fun pair_compare (comp1 : 'a * 'a -> order) (comp2 : 'b * 'b -> order)
+  ((p1, p2) : (('a * 'b) * ('a * 'b))) : order =
+  let
+    val (x1, y1) = p1;
+    val (x2, y2) = p2;
+  in
+    case comp1 (x1, x2) of
+      LESS => LESS
+    | GREATER => GREATER
+    | EQUAL => comp2 (y1, y2)
+  end
+
+(* A constant name (theory, constant name) *)
+type const_name = string * string
+
+val const_name_compare = pair_compare String.compare String.compare
+
+(* The registered spec theorems, that {!progress} will automatically apply.
+
+   The keys are the function names (it is a pair, because constant names
+   are made of the theory name and the name of the constant itself).
+
+   Also note that we can store several specs per definition (in practice, when
+   looking up specs, we will try them all one by one, in a LIFO order).
+
+   We store theorems where all the premises are in the goal, with implications
+   (i.e.: [⊢ H0 ==> ... ==> Hn ==> H], not  [H0, ..., Hn ⊢ H]).
+
+   We do this because, when doing proofs by induction, {!progress} might have to
+   handle *unregistered* theorems coming the current goal assumptions and of the shape
+   (the conclusion of the theorem is an assumption, and we want to ignore this assumption):
+   {[
+     [∀i. u32_to_int i < &LENGTH (list_t_v ls) ⇒
+         case nth ls i of
+           Return x => ...
+         | ...      => ...]
+     ⊢ ∀i. u32_to_int i < &LENGTH (list_t_v ls) ⇒
+         case nth ls i of
+           Return x => ...
+         | ...      => ...
+   ]}
+ *)
+val reg_spec_thms: (const_name, thm) Redblackmap.dict ref =
+  ref (Redblackmap.mkDict const_name_compare)
+
+(* Retrieve the specified application in a spec theorem.
+
+   A spec theorem for a function [f] typically has the shape:
+   {[
+     !x0 ... xn.
+       H0 ==> ... Hm ==>
+         (exists ...
+           (exists ... . f y0 ... yp = ... /\ ...) \/
+           (exists ... . f y0 ... yp = ... /\ ...) \/
+           ...
+   ]}
+
+   Or:
+   {[
+    !x0 ... xn.
+      H0 ==> ... Hm ==>
+        case f y0 ... yp of
+          ... => ...
+        | ... =>  ...
+   ]}
+
+   We return: [f y0 ... yp]
+*)
+fun get_spec_app (t : term) : term =
+  let
+    (* Remove the universally quantified variables, the premises and
+       the existentially quantified variables *)
+    val t = (snd o strip_exists o snd o strip_imp o snd o strip_forall) t;
+    (* Remove the exists, take the first disjunct *)
+    val t = (hd o strip_disj o snd o strip_exists) t;
+    (* Split the conjunctions and take the first conjunct *)
+    val t = (hd o strip_conj) t;
+    (* Remove the case if there is, otherwise destruct the equality *)
+    val t =
+      if TypeBase.is_case t then let val (_, t, _) = TypeBase.dest_case t in t end
+      else (fst o dest_eq) t;
+  in t end
+
+(* Given a function call [f y0 ... yn] return the name of the function *)
+fun get_fun_name_from_app (t : term) : const_name =
+  let
+    val f = (fst o strip_comb) t;
+    val {Name=name, Thy=thy, Ty=_} = dest_thy_const f;
+    val cn = (thy, name);
+  in cn end
+
+(* Register a spec theorem in the spec database.
+
+   For the shape of spec theorems, see {!get_spec_thm_app}.
+ *)
+fun register_spec_thm (th: thm) : unit =
+  let
+    (* Transform the theroem a bit before storing it *)
+    val th = SPEC_ALL th;
+    (* Retrieve the app ([f x0 ... xn]) *)
+    val f = get_spec_app (concl th);
+    (* Retrieve the function name *)
+    val cn = get_fun_name_from_app f;
+  in
+    (* Store *)
+    reg_spec_thms := Redblackmap.insert (!reg_spec_thms, cn, th)
+  end
+
+val all_add_eqs = [
+  isize_add_eq,
+  i8_add_eq,
+  i16_add_eq,
+  i32_add_eq,
+  i64_add_eq,
+  i128_add_eq,
+  usize_add_eq,
+  u8_add_eq,
+  u16_add_eq,
+  u32_add_eq,
+  u64_add_eq,
+  u128_add_eq
+]
+val _ = app register_spec_thm all_add_eqs
+
+val all_sub_eqs = [
+  isize_sub_eq,
+  i8_sub_eq,
+  i16_sub_eq,
+  i32_sub_eq,
+  i64_sub_eq,
+  i128_sub_eq,
+  usize_sub_eq,
+  u8_sub_eq,
+  u16_sub_eq,
+  u32_sub_eq,
+  u64_sub_eq,
+  u128_sub_eq
+]
+val _ = app register_spec_thm all_sub_eqs
+
+val all_mul_eqs = [
+  isize_mul_eq,
+  i8_mul_eq,
+  i16_mul_eq,
+  i32_mul_eq,
+  i64_mul_eq,
+  i128_mul_eq,
+  usize_mul_eq,
+  u8_mul_eq,
+  u16_mul_eq,
+  u32_mul_eq,
+  u64_mul_eq,
+  u128_mul_eq
+]
+val _ = app register_spec_thm all_mul_eqs
+
+val all_div_eqs = [
+  isize_div_eq,
+  i8_div_eq,
+  i16_div_eq,
+  i32_div_eq,
+  i64_div_eq,
+  i128_div_eq,
+  usize_div_eq,
+  u8_div_eq,
+  u16_div_eq,
+  u32_div_eq,
+  u64_div_eq,
+  u128_div_eq
+]
+val _ = app register_spec_thm all_div_eqs
+
+val all_rem_eqs = [
+  isize_rem_eq,
+  i8_rem_eq,
+  i16_rem_eq,
+  i32_rem_eq,
+  i64_rem_eq,
+  i128_rem_eq,
+  usize_rem_eq,
+  u8_rem_eq,
+  u16_rem_eq,
+  u32_rem_eq,
+  u64_rem_eq,
+  u128_rem_eq
+]
+val _ = app register_spec_thm all_rem_eqs
+
+val all_vec_lems = [
+  vec_len_spec,
+  vec_insert_back_spec
+]
+val _ = app register_spec_thm all_vec_lems
+
+(* Repeatedly destruct cases and return the last scrutinee we get *)
+fun strip_all_cases_get_scrutinee (t : term) : term =
+  if TypeBase.is_case t
+  then (strip_all_cases_get_scrutinee o fst o TypeBase.strip_case) t
+  else t
+
+(*
+TypeBase.dest_case “case ls of [] => T | _ => F”
+TypeBase.strip_case “case ls of [] => T | _ => F”
+TypeBase.strip_case “case (if b then [] else [0, 1]) of [] => T | _ => F”
+TypeBase.strip_case “3”
+TypeBase.dest_case “3”
+
+strip_all_cases_get_scrutinee “case ls of [] => T | _ => F”
+strip_all_cases_get_scrutinee “case (if b then [] else [0, 1]) of [] => T | _ => F”
+strip_all_cases_get_scrutinee “3”
+*)
+
+
+(* Provided the goal contains a call to a monadic function, return this function call.
+
+   The goal should be of the shape:
+   1.
+   {[
+     case (* potentially expanded function body *) of
+       ... => ...
+     | ... => ...
+   ]}
+
+   2. Or:
+   {[
+     exists ... .
+       ... (* potentially expanded function body *) = Return ... /\
+       ... (* Various properties *)
+   ]}
+
+   3. Or a disjunction of cases like the one above, below existential binders
+   (actually: note sure this last case exists in practice):
+   {[
+     exists ... .
+       (exists ... . (* body *) = Return ... /\ ...) \/
+       ...
+   ]}
+
+   The function body should be of the shape:
+   {[
+     x <- f y0 ... yn;
+     ...
+   ]}
+
+   Or (typically if we expanded the monadic binds):
+   {[
+     case f y0 ... yn of
+     ...
+   ]}
+
+   Or simply (typically if we reached the end of the function we're analyzing):
+   {[
+     f y0 ... yn
+   ]}
+
+   For all the above cases we would return [f y0 ... yn].
+ *)
+fun get_monadic_app_call (t : term) : term =
+  (* We do something slightly imprecise but hopefully general and robut *)
+  let
+     (* Case 3.: strip the existential binders, and take the first disjuntion *)
+     val t = (hd o strip_disj o snd o strip_exists) t;
+     (* Case 2.: strip the existential binders, and take the first conjunction *)
+     val t = (hd o strip_conj o snd o strip_exists) t;
+     (* If it is an equality, take the lhs *)
+     val t = if is_eq t then lhs t else t;
+     (* Expand the binders to transform them to cases *)
+     val t =
+       (rhs o concl) (REWRITE_CONV [bind_def] t)
+       handle UNCHANGED => t;
+     (* Strip all the cases *)
+     val t = strip_all_cases_get_scrutinee t;
+  in t end
+
+(* Use the given theorem to progress by one step (we use this when
+   analyzing a function body: this goes forward by one call to a monadic function).
+
+   We transform the goal by:
+   - pushing the theorem premises to a subgoal
+   - adding the theorem conclusion in the assumptions in another goal, and
+     getting rid of the monadic call
+
+  Then [then_tac] receives as paramter the monadic call on which we applied
+  the lemma. This can be useful, for instance, to make a case disjunction.
+
+  This function is the most primitive of the [progress...] functions.
+ *)
+fun pure_progress_with (premise_tac : tactic)
+  (then_tac : term -> thm_tactic) (th : thm) : tactic =
+  fn (asms,g) =>
+  let
+    (* Remove all the universally quantified variables from the theorem *)
+    val th = SPEC_ALL th;
+    (* Retrieve the monadic call from the goal *)
+    val fgoal = get_monadic_app_call g;
+    (* Retrieve the app call from the theroem *)
+    val gth = get_spec_app (concl th);
+    (* Match and instantiate *)
+    val (var_s, ty_s) = match_term gth fgoal;
+    (* Instantiate the theorem *)
+    val th = INST var_s (INST_TYPE ty_s th);
+    (* Retrieve the premises of the theorem *)
+    val th = PURE_REWRITE_RULE [GSYM satTheory.AND_IMP] th;
+  in
+    (* Apply the theorem *)
+    sg_premise_then premise_tac (then_tac fgoal) th (asms, g)
+  end
+
+(*
+val (asms, g) = top_goal ()
+val t = g
+
+val th = U32_SUB_EQ
+
+val premise_tac =  massage >> TRY COOPER_TAC
+fun then_tac fgoal =
+  fn thm => ASSUME_TAC thm >> Cases_on ‘^fgoal’ >>
+  rw [] >> fs [st_ex_bind_def] >> massage >> fs []
+
+pure_progress_with premise_tac then_tac th
+*)
+
+fun progress_with (th : thm) : tactic =
+  let
+    val premise_tac = massage >> fs [] >> rw [] >> TRY COOPER_TAC;
+    fun then_tac fgoal thm =
+      ASSUME_TAC thm >> Cases_on ‘^fgoal’ >>
+      rw [] >> fs [bind_def] >> massage >> fs [];
+  in
+    pure_progress_with premise_tac then_tac th
+  end
+
+(*
+progress_with U32_SUB_EQ
+*)
+
+(* This function lookups the theorem to use to make progress *)
+val progress : tactic =
+  fn (asms, g) =>
+  let
+    (* Retrieve the monadic call from the goal *)
+    val fgoal = get_monadic_app_call g;
+    val fname = get_fun_name_from_app fgoal;
+    (* Lookup the theorem: first look in the assumptions (we might want to
+       use the inductive hypothesis for instance) *)
+    fun asm_to_spec asm =
+      let
+        (* Fail if there are no universal quantifiers *)
+        val _ =
+          if is_forall asm then asm
+          else assert is_forall ((snd o strip_imp) asm);
+        val asm_fname = (get_fun_name_from_app o get_spec_app) asm;
+        (* Fail if the name is not the one we're looking for *)
+        val _ = assert (fn n => fname = n) asm_fname;
+      in
+        ASSUME asm
+      end
+    val asms_thl = mapfilter asm_to_spec asms;
+    (* Lookup a spec in the database *)
+    val thl =
+      case Redblackmap.peek (!reg_spec_thms, fname) of
+        NONE => asms_thl
+      | SOME spec => spec :: asms_thl;
+    val _ =
+      if null thl then
+        raise (failwith "progress: could not find a suitable theorem to apply")
+      else ();
+  in
+    (* Attempt to use the theorems one by one *)
+    map_first_tac progress_with thl (asms, g)
+  end
+
+(*
+ * Examples of proofs
+ *)
+
+Datatype:
+  list_t =
+    ListCons 't list_t
+  | ListNil
+End
+
+val nth_mut_fwd_def = Define ‘
+  nth_mut_fwd (ls : 't list_t) (i : u32) : 't result =
+  case ls of
+  | ListCons x tl =>
+    if u32_to_int i = (0:int)
+    then Return x
+    else
+      do
+      i0 <- u32_sub i (int_to_u32 1);
+      nth_mut_fwd tl i0
+      od
+  | ListNil => 
+    Fail Failure
+’
+                                            
+(*** Examples of proofs on [nth] *)
+val list_t_v_def = Define ‘
+  list_t_v ListNil = [] /\
+  list_t_v (ListCons x tl) = x :: list_t_v tl
+’
+
+(* TODO: move *)
+Theorem index_eq:
+  (∀x ls. index 0 (x :: ls) = x) ∧
+  (∀i x ls. index i (x :: ls) =
+    if (0 < i) ∨ (0 ≤ i ∧ i ≠ 0) then index (i - 1) ls
+    else (if i = 0 then x else ARB))
+Proof
+  rw [index_def] >> fs [] >>
+  exfalso >> cooper_tac
+QED
+
+Theorem nth_mut_fwd_lem:
+  !(ls : 't list_t) (i : u32).
+    u32_to_int i < len (list_t_v ls) ==>
+    case nth_mut_fwd ls i of
+    | Return x => x = index (u32_to_int i) (list_t_v ls)
+    | Fail _ => F
+    | Loop => F
+Proof
+  Induct_on ‘ls’ >> rw [list_t_v_def, len_def] >~ [‘ListNil’]
+  >-(massage >> exfalso >> cooper_tac) >>
+  pure_once_rewrite_tac [nth_mut_fwd_def] >> rw [] >>
+  fs [index_eq] >>
+  progress >> progress
+QED
+
+val _ = new_constant ("insert", “: u32 -> 't -> (u32 # 't) list_t -> (u32 # 't) list_t result”)
+val insert_def = new_axiom ("insert_def", “
+ insert (key : u32) (value : 't) (ls : (u32 # 't) list_t) : (u32 # 't) list_t result =
+  case ls of
+  | ListCons (ckey, cvalue) tl =>
+    if ckey = key
+    then Return (ListCons (ckey, value) tl)
+    else
+      do
+      tl0 <- insert key value tl;
+      Return (ListCons (ckey, cvalue) tl0)
+      od
+  | ListNil => Return (ListCons (key, value) ListNil)
+ ”)
+
+(* Property that keys are pairwise distinct *)
+val distinct_keys_def = Define ‘
+  distinct_keys (ls : (u32 # 't) list) =
+    !i j.
+      0 < i ⇒ i < len ls ==>
+      0 < j ⇒ j < len ls ==>
+      FST (index i ls) = FST (index j ls) ⇒
+      i = j
+’
+
+val lookup_raw_def = Define ‘
+  lookup_raw key [] = NONE /\
+  lookup_raw key ((k, v) :: ls) =
+    if k = key then SOME v else lookup_raw key ls
+’
+
+val lookup_def = Define ‘
+  lookup key ls = lookup_raw key (list_t_v ls)
+’
+
+Theorem insert_lem:
+  !ls key value.
+    (* The keys are pairwise distinct *)
+    distinct_keys (list_t_v ls) ==>
+    case insert key value ls of
+    | Return ls1 =>
+      (* We updated the binding *)
+      lookup key ls1 = SOME value /\
+      (* The other bindings are left unchanged *)
+      (!k. k <> key ==> lookup k ls = lookup k ls1)
+    | Fail _ => F
+    | Loop => F
+Proof
+  Induct_on ‘ls’ >> rw [list_t_v_def] >~ [‘ListNil’] >>
+  pure_once_rewrite_tac [insert_def] >> rw []
+  >- (rw [lookup_def, lookup_raw_def, list_t_v_def])
+  >- (rw [lookup_def, lookup_raw_def, list_t_v_def]) >>
+  case_tac >> rw []
+  >- (rw [lookup_def, lookup_raw_def, list_t_v_def])
+  >- (rw [lookup_def, lookup_raw_def, list_t_v_def]) >>
+  progress
+  >- (
+    (* Disctinct keys *)
+    fs [distinct_keys_def] >>
+    rpt strip_tac >>
+    first_x_assum (qspecl_assume [‘i + 1’, ‘j + 1’]) >> fs [] >>
+    pop_assum irule >>
+    fs [index_eq, add_sub_same_eq, len_def] >>
+    int_tac) >>
+  fs [lookup_def, lookup_raw_def, list_t_v_def]
+QED
+
+val _ = export_theory ()
diff --git a/backends/hol4/testHashmapTheory.sig b/backends/hol4/testHashmapTheory.sig
new file mode 100644
index 00000000..a08511cd
--- /dev/null
+++ b/backends/hol4/testHashmapTheory.sig
@@ -0,0 +1,202 @@
+signature testHashmapTheory =
+sig
+  type thm = Thm.thm
+  
+  (*  Axioms  *)
+    val insert_def : thm
+  
+  (*  Definitions  *)
+    val distinct_keys_def : thm
+    val list_t_TY_DEF : thm
+    val list_t_case_def : thm
+    val list_t_size_def : thm
+    val list_t_v_def : thm
+    val lookup_def : thm
+  
+  (*  Theorems  *)
+    val datatype_list_t : thm
+    val index_eq : thm
+    val insert_lem : thm
+    val list_t_11 : thm
+    val list_t_Axiom : thm
+    val list_t_case_cong : thm
+    val list_t_case_eq : thm
+    val list_t_distinct : thm
+    val list_t_induction : thm
+    val list_t_nchotomy : thm
+    val lookup_raw_def : thm
+    val lookup_raw_ind : thm
+    val nth_mut_fwd_def : thm
+    val nth_mut_fwd_ind : thm
+    val nth_mut_fwd_lem : thm
+  
+  val testHashmap_grammars : type_grammar.grammar * term_grammar.grammar
+(*
+   [primitives] Parent theory of "testHashmap"
+   
+   [insert_def]  Axiom
+      
+      [oracles: ] [axioms: insert_def] []
+      ⊢ insert key value ls =
+        case ls of
+          ListCons (ckey,cvalue) tl =>
+            if ckey = key then Return (ListCons (ckey,value) tl)
+            else
+              do
+                tl0 <- insert key value tl;
+                Return (ListCons (ckey,cvalue) tl0)
+              od
+        | ListNil => Return (ListCons (key,value) ListNil)
+   
+   [distinct_keys_def]  Definition
+      
+      ⊢ ∀ls.
+          distinct_keys ls ⇔
+          ∀i j.
+            0 < i ⇒
+            i < len ls ⇒
+            0 < j ⇒
+            j < len ls ⇒
+            FST (index i ls) = FST (index j ls) ⇒
+            i = j
+   
+   [list_t_TY_DEF]  Definition
+      
+      ⊢ ∃rep.
+          TYPE_DEFINITION
+            (λa0'.
+                 ∀ $var$('list_t').
+                   (∀a0'.
+                      (∃a0 a1.
+                         a0' =
+                         (λa0 a1.
+                              ind_type$CONSTR 0 a0
+                                (ind_type$FCONS a1 (λn. ind_type$BOTTOM)))
+                           a0 a1 ∧ $var$('list_t') a1) ∨
+                      a0' =
+                      ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM) ⇒
+                      $var$('list_t') a0') ⇒
+                   $var$('list_t') a0') rep
+   
+   [list_t_case_def]  Definition
+      
+      ⊢ (∀a0 a1 f v. list_t_CASE (ListCons a0 a1) f v = f a0 a1) ∧
+        ∀f v. list_t_CASE ListNil f v = v
+   
+   [list_t_size_def]  Definition
+      
+      ⊢ (∀f a0 a1.
+           list_t_size f (ListCons a0 a1) = 1 + (f a0 + list_t_size f a1)) ∧
+        ∀f. list_t_size f ListNil = 0
+   
+   [list_t_v_def]  Definition
+      
+      ⊢ list_t_v ListNil = [] ∧
+        ∀x tl. list_t_v (ListCons x tl) = x::list_t_v tl
+   
+   [lookup_def]  Definition
+      
+      ⊢ ∀key ls. lookup key ls = lookup_raw key (list_t_v ls)
+   
+   [datatype_list_t]  Theorem
+      
+      ⊢ DATATYPE (list_t ListCons ListNil)
+   
+   [index_eq]  Theorem
+      
+      ⊢ (∀x ls. index 0 (x::ls) = x) ∧
+        ∀i x ls.
+          index i (x::ls) =
+          if 0 < i ∨ 0 ≤ i ∧ i ≠ 0 then index (i − 1) ls
+          else if i = 0 then x
+          else ARB
+   
+   [insert_lem]  Theorem
+      
+      [oracles: DISK_THM] [axioms: insert_def] []
+      ⊢ ∀ls key value.
+          distinct_keys (list_t_v ls) ⇒
+          case insert key value ls of
+            Return ls1 =>
+              lookup key ls1 = SOME value ∧
+              ∀k. k ≠ key ⇒ lookup k ls = lookup k ls1
+          | Fail v1 => F
+          | Loop => F
+   
+   [list_t_11]  Theorem
+      
+      ⊢ ∀a0 a1 a0' a1'.
+          ListCons a0 a1 = ListCons a0' a1' ⇔ a0 = a0' ∧ a1 = a1'
+   
+   [list_t_Axiom]  Theorem
+      
+      ⊢ ∀f0 f1. ∃fn.
+          (∀a0 a1. fn (ListCons a0 a1) = f0 a0 a1 (fn a1)) ∧
+          fn ListNil = f1
+   
+   [list_t_case_cong]  Theorem
+      
+      ⊢ ∀M M' f v.
+          M = M' ∧ (∀a0 a1. M' = ListCons a0 a1 ⇒ f a0 a1 = f' a0 a1) ∧
+          (M' = ListNil ⇒ v = v') ⇒
+          list_t_CASE M f v = list_t_CASE M' f' v'
+   
+   [list_t_case_eq]  Theorem
+      
+      ⊢ list_t_CASE x f v = v' ⇔
+        (∃t l. x = ListCons t l ∧ f t l = v') ∨ x = ListNil ∧ v = v'
+   
+   [list_t_distinct]  Theorem
+      
+      ⊢ ∀a1 a0. ListCons a0 a1 ≠ ListNil
+   
+   [list_t_induction]  Theorem
+      
+      ⊢ ∀P. (∀l. P l ⇒ ∀t. P (ListCons t l)) ∧ P ListNil ⇒ ∀l. P l
+   
+   [list_t_nchotomy]  Theorem
+      
+      ⊢ ∀ll. (∃t l. ll = ListCons t l) ∨ ll = ListNil
+   
+   [lookup_raw_def]  Theorem
+      
+      ⊢ (∀key. lookup_raw key [] = NONE) ∧
+        ∀v ls key k.
+          lookup_raw key ((k,v)::ls) =
+          if k = key then SOME v else lookup_raw key ls
+   
+   [lookup_raw_ind]  Theorem
+      
+      ⊢ ∀P. (∀key. P key []) ∧
+            (∀key k v ls. (k ≠ key ⇒ P key ls) ⇒ P key ((k,v)::ls)) ⇒
+            ∀v v1. P v v1
+   
+   [nth_mut_fwd_def]  Theorem
+      
+      ⊢ ∀ls i.
+          nth_mut_fwd ls i =
+          case ls of
+            ListCons x tl =>
+              if u32_to_int i = 0 then Return x
+              else do i0 <- u32_sub i (int_to_u32 1); nth_mut_fwd tl i0 od
+          | ListNil => Fail Failure
+   
+   [nth_mut_fwd_ind]  Theorem
+      
+      ⊢ ∀P. (∀ls i.
+               (∀x tl i0. ls = ListCons x tl ∧ u32_to_int i ≠ 0 ⇒ P tl i0) ⇒
+               P ls i) ⇒
+            ∀v v1. P v v1
+   
+   [nth_mut_fwd_lem]  Theorem
+      
+      ⊢ ∀ls i.
+          u32_to_int i < len (list_t_v ls) ⇒
+          case nth_mut_fwd ls i of
+            Return x => x = index (u32_to_int i) (list_t_v ls)
+          | Fail v1 => F
+          | Loop => F
+   
+   
+*)
+end