Reorganize the HOL4 files and fix some issues with the arithmetic proofs

4 files changed, 568 insertions, 763 deletions

diff --git a/backends/hol4/primitivesBaseTacLib.sml b/backends/hol4/primitivesBaseTacLib.sml
index 3f298a04..28f8ab97 100644
--- a/backends/hol4/primitivesBaseTacLib.sml
+++ b/backends/hol4/primitivesBaseTacLib.sml
@@ -330,7 +330,7 @@ fun apply_dep_rewrites_match_concl_with_terms_tac
     val thms = map thm_to_conj_implies thms;
   in
     (* Apply each theorem *)
-    MAP_EVERY (sg_premise_then prove_premise then_tac) thms
+    map_every_tac (try_tac o sg_premise_then prove_premise then_tac) thms
   end
 
 (* Attempt to apply dependent rewrites with a theorem by matching its
@@ -497,30 +497,35 @@ val dest_assums_conjs_tac : tactic =
 (* 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)”
+val int_tac_num_ty = “:num”
+val int_tac_pat1 = “(x : 'a) <> (y : 'a)”
+val int_tac_pat2 = “(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”.
+       inequalities/equalities which terms are not between terms of type “:int”
+       or “:num”.
 
        TODO: issue/PR for HOL4
      *)
-    fun keep (asm : term) : bool =
+    fun keep_with_pat (asm : term) (pat : term) : bool =
       let
-        val (_, s) = match_term int_tac_pat asm
+        val (_, s) = match_term pat asm
       in
         case s of
-          [{redex = _, residue = ty}] => ty = int_tac_int_ty
+          [{redex = _, residue = ty}] => (ty = int_tac_int_ty orelse ty = int_tac_num_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
+    fun keep (asm : term) : bool =
+      forall (keep_with_pat asm) [int_tac_pat1, int_tac_pat2]
+ 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/primitivesLib.sml b/backends/hol4/primitivesLib.sml
index 5803c531..543ded23 100644
--- a/backends/hol4/primitivesLib.sml
+++ b/backends/hol4/primitivesLib.sml
@@ -1,9 +1,557 @@
 (* Advanced tactics for the primitives library *)
-structure primitivesBaseTacLib =
+structure primitivesLib =
 struct
 
 open HolKernel boolLib bossLib Parse
 open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory
-open primitivesBaseTacLib primitivesTheory
+
+open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory
+
+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 >> int_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 =
+      mp_tac thm >> strip_tac >> Cases_on ‘^fgoal’ >>
+      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
 
 end
diff --git a/backends/hol4/testHashmapScript.sml b/backends/hol4/testHashmapScript.sml
index 71b0109d..249bc0bf 100644
--- a/backends/hol4/testHashmapScript.sml
+++ b/backends/hol4/testHashmapScript.sml
@@ -2,556 +2,10 @@ open HolKernel boolLib bossLib Parse
 open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory
 
 open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory
+open primitivesLib
 
 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
  *)
@@ -594,7 +48,7 @@ Proof
   exfalso >> cooper_tac
 QED
 
-Theorem nth_mut_fwd_lem:
+Theorem nth_mut_fwd_spec:
   !(ls : 't list_t) (i : u32).
     u32_to_int i < len (list_t_v ls) ==>
     case nth_mut_fwd ls i of
diff --git a/backends/hol4/testHashmapTheory.sig b/backends/hol4/testHashmapTheory.sig
deleted file mode 100644
index a08511cd..00000000
--- a/backends/hol4/testHashmapTheory.sig
+++ /dev/null
@@ -1,202 +0,0 @@
-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