Update the hashmap proofs and fix some tactics

5 files changed, 300 insertions, 46 deletions

diff --git a/backends/hol4/ilistScript.sml b/backends/hol4/ilistScript.sml
index c871ba04..f382d95d 100644
--- a/backends/hol4/ilistScript.sml
+++ b/backends/hol4/ilistScript.sml
@@ -72,6 +72,14 @@ Proof
   Induct_on ‘ls’ >> fs [len_def] >> cooper_tac
 QED
 
+Theorem len_pos:
+  ∀ls. 0 ≤ len ls
+Proof
+  strip_tac >>
+  qspec_assume ‘ls’ len_eq_LENGTH >>
+  cooper_tac
+QED
+
 Theorem index_eq_EL:
   ∀(i: int) ls.
     0 ≤ i ⇒
diff --git a/backends/hol4/ilistTheory.sig b/backends/hol4/ilistTheory.sig
index 249b362c..f155a328 100644
--- a/backends/hol4/ilistTheory.sig
+++ b/backends/hol4/ilistTheory.sig
@@ -13,6 +13,7 @@ sig
     val index_eq_EL : thm
     val len_append : thm
     val len_eq_LENGTH : thm
+    val len_pos : thm
     val update_eq : thm
   
   val ilist_grammars : type_grammar.grammar * term_grammar.grammar
@@ -68,6 +69,10 @@ sig
       
       ⊢ ∀ls. len ls = &LENGTH ls
    
+   [len_pos]  Theorem
+      
+      ⊢ ∀ls. 0 ≤ len ls
+   
    [update_eq]  Theorem
       
       ⊢ (∀i y. update [] i y = []) ∧
diff --git a/backends/hol4/primitivesBaseTacLib.sml b/backends/hol4/primitivesBaseTacLib.sml
index a718392b..0363ad41 100644
--- a/backends/hol4/primitivesBaseTacLib.sml
+++ b/backends/hol4/primitivesBaseTacLib.sml
@@ -476,7 +476,16 @@ fun filter_assums_tac (keep : term -> bool) : tactic =
         [th] =>
         let
           (* Being a bit brutal - will optimize later *)
-          val tac = ntac (length asms) strip_tac >> irule th >> pure_asm_rewrite_tac []
+          val tac = ntac (length asms) strip_tac >>
+            (* Small subtlety: we have to use the primitive irule here,
+               because otherwise it won't work with goals of the shape
+               “x <> y”, as those are actually of the shape: “x = y ==> F”:
+               irule will attempt to match “F” with the goal, which will fail.
+             *)
+            prim_irule th >>
+            (* Prove the assumptions of the theorem by using the assumptions
+               in goal. TODO: simply use ‘simp []’? *)
+            pure_asm_rewrite_tac [] >> SIMP_TAC bool_ss []
           val th = prove (list_mk_imp (asms, g), tac)
           val th = foldl (fn (_, th) => UNDISCH th) th asms
         in th end
@@ -497,7 +506,16 @@ val dest_assums_conjs_tac : tactic =
         [th] =>
         let
           (* Being a bit brutal - will optimize later *)
-          val tac = ntac (length asms) strip_tac >> irule th >> pure_asm_rewrite_tac []
+          val tac = ntac (length asms) strip_tac >>
+            (* Small subtlety: we have to use the primitive irule here,
+               because otherwise it won't work with goals of the shape
+               “x <> y”, as those are actually of the shape: “x = y ==> F”:
+               irule will attempt to match “F” with the goal, which will fail.
+             *)
+            prim_irule th >>
+            (* Prove the assumptions of the theorem by using the assumptions
+               in goal. TODO: simply use ‘simp []’? *)
+            pure_asm_rewrite_tac [] >> SIMP_TAC bool_ss []
           val th = prove (list_mk_imp (asms, g), tac)
           val th = foldl (fn (_, th) => UNDISCH th) th asms
         in th end
@@ -508,32 +526,37 @@ 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_num_ty = “:num”
-val int_tac_pat1 = “(x : 'a) <> (y : 'a)”
-val int_tac_pat2 = “(x : 'a) = (y : 'a)”
+val int_tac_pats = [
+    “x: int = y”,
+    “x: int <= y”,
+    “x: int < y”,
+    “x: int >= y”,
+    “x: int > y”,
+    “x: num = y”,
+    “x: num <= y”,
+    “x: num < y”,
+    “x: num >= y”,
+    “x: num > y”
+]
+val int_tac_ops = Redblackset.fromList Term.compare (map (fst o strip_comb) int_tac_pats)  
 
 (* 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/equalities which terms are not between terms of type “:int”
-       or “:num”.
+    (* Following the bug we discovered in COOPER_TAC, we keep only the terms:
+       - which are inequalities/equalities between terms of type “:int” or “:num”.
+       - which are comparisons of terms of tyep “:int” or “:num”
 
        TODO: issue/PR for HOL4
      *)
-    fun keep_with_pat (asm : term) (pat : term) : bool =
-      let
-        val (_, s) = match_term pat asm
-      in
-        case s of
-          [{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
-    fun keep (asm : term) : bool =
-      forall (keep_with_pat asm) [int_tac_pat1, int_tac_pat2]
+    fun keep (x : term) : bool =
+    let
+      val x = if is_neg x then dest_neg x else x
+    in
+      case strip_comb x of
+        (y, [_, _]) => Redblackset.member (int_tac_ops, y)
+      | _ => false
+    end
  in
    (dest_assums_conjs_tac >>
     filter_assums_tac keep >>
diff --git a/backends/hol4/testHashmapScript.sml b/backends/hol4/testHashmapScript.sml
index 77c97651..7108776d 100644
--- a/backends/hol4/testHashmapScript.sml
+++ b/backends/hol4/testHashmapScript.sml
@@ -43,7 +43,7 @@ Theorem nth_mut_fwd_spec:
     case nth_mut_fwd ls i of
     | Return x => x = index (u32_to_int i) (list_t_v ls)
     | Fail _ => F
-    | Loop => F
+    | Diverge => F
 Proof
   Induct_on ‘ls’ >> rw [list_t_v_def, len_def] >~ [‘ListNil’]
   >-(massage >> int_tac) >>
@@ -52,6 +52,8 @@ Proof
   progress >> progress
 QED
 
+val _ = register_spec_thm nth_mut_fwd_spec
+
 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 =
@@ -71,10 +73,8 @@ val insert_def = new_axiom ("insert_def", “
 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
+      0 ≤ i ⇒ i < j ⇒ j < len ls ⇒
+      FST (index i ls) ≠ FST (index j ls)
 ’
 
 val lookup_raw_def = Define ‘
@@ -87,19 +87,18 @@ val lookup_def = Define ‘
   lookup key ls = lookup_raw key (list_t_v ls)
 ’
 
-Theorem insert_lem:
+(* Lemma about ‘insert’, without the invariant *)
+Theorem insert_lem_aux:
   !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)
-      (* TODO: invariant *)
     | Fail _ => F
-    | Loop => F
+    | Diverge => F
 Proof
   Induct_on ‘ls’ >> rw [list_t_v_def] >~ [‘ListNil’] >>
   pure_once_rewrite_tac [insert_def] >> rw []
@@ -108,16 +107,177 @@ Proof
   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) >>
+  progress >>
   fs [lookup_def, lookup_raw_def, list_t_v_def]
 QED
 
+Theorem distinct_keys_cons:
+  ∀ k v ls.
+  (∀ i. 0 ≤ i ⇒ i < len ls ⇒ FST (index i ls) ≠ k) ⇒
+  distinct_keys ls ⇒
+  distinct_keys ((k,v) :: ls)
+Proof
+  rw [] >>
+  rw [distinct_keys_def] >>
+  Cases_on ‘i = 0’ >> fs []
+  >-(
+    (* Use the first hypothesis *)
+    fs [index_eq] >>
+    last_x_assum (qspecl_assume [‘j - 1’]) >>
+    sg ‘0 ≤ j - 1’ >- int_tac >>
+    fs [len_def] >>
+    sg ‘j - 1 < len ls’ >- int_tac >>
+    fs []
+  ) >>
+  (* Use the second hypothesis *)
+  sg ‘0 < i’ >- int_tac >>
+  sg ‘0 < j’ >- int_tac >>
+  fs [distinct_keys_def, index_eq, len_def] >>
+  first_x_assum (qspecl_assume [‘i - 1’, ‘j - 1’]) >>
+  sg ‘0 ≤ i - 1 ∧ i - 1 < j - 1 ∧ j - 1 < len ls’ >- int_tac >>
+  fs []
+QED
+
+Theorem distinct_keys_tail:
+  ∀ k v ls.
+  distinct_keys ((k,v) :: ls) ⇒
+  distinct_keys ls
+Proof
+  rw [distinct_keys_def] >>
+  last_x_assum (qspecl_assume [‘i + 1’, ‘j + 1’]) >>
+  fs [len_def] >>
+  sg ‘0 ≤ i + 1 ∧ i + 1 < j + 1 ∧ j + 1 < 1 + len ls’ >- int_tac >> fs [] >>
+  sg ‘0 < i + 1 ∧ 0 < j + 1’ >- int_tac >> fs [index_eq] >>
+  sg ‘i + 1 - 1 = i ∧ j + 1 - 1 = j’ >- int_tac >> fs []
+QED
+
+Theorem insert_index_neq:
+  ∀ q k v ls0 ls1 i.
+  (∀ j. 0 ≤ j ∧ j < len (list_t_v ls0) ⇒ q ≠ FST (index j (list_t_v ls0))) ⇒
+  q ≠ k ⇒
+  insert k v ls0 = Return ls1 ⇒
+  0 ≤ i ⇒
+  i < len (list_t_v ls1) ⇒
+  FST (index i (list_t_v ls1)) ≠ q
+Proof
+  ntac 3 strip_tac >>
+  Induct_on ‘ls0’ >> rw [] >~ [‘ListNil’]
+  >-(
+    fs [insert_def] >>
+    sg ‘ls1 = ListCons (k,v) ListNil’ >- fs [] >> fs [list_t_v_def, len_def] >>
+    sg ‘i = 0’ >- int_tac >> fs [index_eq]) >>
+  Cases_on ‘t’ >>
+  Cases_on ‘i = 0’ >> fs []
+  >-(
+    qpat_x_assum ‘insert _ _ _ = _’ mp_tac >>
+    simp [MK_BOUNDED insert_def 1, bind_def] >>
+    Cases_on ‘q' = k’ >> rw []
+    >- (fs [list_t_v_def, index_eq]) >>
+    Cases_on ‘insert k v ls0’ >> fs [] >>
+    (* TODO: would be good to have a tactic which inverts equalities of the
+       shape ‘ListCons (q',r) a = ls1’ *)
+    sg ‘ls1 = ListCons (q',r) a’ >- fs [] >> fs [list_t_v_def, index_eq] >>
+    first_x_assum (qspec_assume ‘0’) >>
+    fs [len_def] >>
+    strip_tac >>
+    qspec_assume ‘list_t_v ls0’ len_pos >>
+    sg ‘0 < 1 + len (list_t_v ls0)’ >- int_tac >>
+    fs []) >>
+  qpat_x_assum ‘insert _ _ _ = _’ mp_tac >>
+  simp [MK_BOUNDED insert_def 1, bind_def] >>
+  Cases_on ‘q' = k’ >> rw []
+  >-(
+    fs [list_t_v_def, index_eq, len_def] >>
+    first_x_assum (qspec_assume ‘i’) >> rfs []) >>
+  Cases_on ‘insert k v ls0’ >> fs [] >>
+  sg ‘ls1 = ListCons (q',r) a’ >- fs [] >> fs [list_t_v_def, index_eq] >>
+  last_x_assum (qspec_assume ‘i - 1’) >>
+  fs [len_def] >>
+  sg ‘0 ≤ i - 1 ∧ i - 1 < len (list_t_v a)’ >- int_tac >> fs [] >>
+  first_x_assum irule >>
+  rw [] >>
+  last_x_assum (qspec_assume ‘j + 1’) >>
+  rfs [] >>
+  sg ‘j + 1 < 1 + len (list_t_v ls0) ∧ j + 1 − 1 = j ∧ j + 1 ≠ 0’ >- int_tac >> fs []
+QED
+
+Theorem distinct_keys_insert_index_neq:
+  ∀ k v q r ls0 ls1 i.
+  distinct_keys ((q,r)::list_t_v ls0) ⇒
+  q ≠ k ⇒
+  insert k v ls0 = Return ls1 ⇒
+  0 ≤ i ⇒
+  i < len (list_t_v ls1) ⇒
+  FST (index i (list_t_v ls1)) ≠ q
+Proof
+  rw [] >>
+  (* Use the first assumption to prove the following assertion *)
+  sg ‘∀ j. 0 ≤ j ∧ j < len (list_t_v ls0) ⇒ q ≠ FST (index j (list_t_v ls0))’
+  >-(
+    strip_tac >>
+    fs [distinct_keys_def] >>
+    last_x_assum (qspecl_assume [‘0’, ‘j + 1’]) >>
+    fs [index_eq] >>
+    sg ‘j + 1 - 1 = j’ >- int_tac >> fs [len_def] >>
+    rw []>>
+    first_x_assum irule >> int_tac) >>
+  qspecl_assume [‘q’, ‘k’, ‘v’, ‘ls0’, ‘ls1’, ‘i’] insert_index_neq >>
+  fs []
+QED
+
+Theorem distinct_keys_insert:
+  ∀ k v ls0 ls1.
+  distinct_keys (list_t_v ls0) ⇒
+  insert k v ls0 = Return ls1 ⇒
+  distinct_keys (list_t_v ls1)
+Proof
+  Induct_on ‘ls0’ >~ [‘ListNil’]
+  >-(
+    rw [distinct_keys_def, list_t_v_def, insert_def] >>
+    fs [list_t_v_def, len_def] >>
+    int_tac) >>  
+  Cases >>
+  pure_once_rewrite_tac [insert_def] >> fs[] >>
+  rw [] >> fs []
+  >-(
+    (* k = q *)
+    last_x_assum ignore_tac >>
+    fs [distinct_keys_def] >>
+    rw [] >>
+    last_x_assum (qspecl_assume [‘i’, ‘j’]) >>
+    rfs [list_t_v_def, len_def] >>
+    sg ‘0 < j’ >- int_tac >>
+    Cases_on ‘i = 0’ >> fs [index_eq] >>
+    sg ‘0 < i’ >- int_tac >> fs []) >>
+  (* k ≠ q: recursion *)
+  Cases_on ‘insert k v ls0’ >> fs [bind_def] >>
+  last_x_assum (qspecl_assume [‘k’, ‘v’, ‘a’]) >>
+  rfs [] >>
+  sg ‘ls1 = ListCons (q,r) a’ >- fs [] >> fs [list_t_v_def] >>
+  imp_res_tac distinct_keys_tail >> fs [] >>
+  irule distinct_keys_cons >> rw [] >>
+  metis_tac [distinct_keys_insert_index_neq]
+QED  
+
+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) ∧
+      (* The keys are still pairwise disjoint *)
+      distinct_keys (list_t_v ls1)
+    | Fail _ => F
+    | Diverge => F
+Proof
+  rw [] >>
+  qspecl_assume [‘ls’, ‘key’, ‘value’] insert_lem_aux >>
+  case_tac >> fs [] >>
+  metis_tac [distinct_keys_insert]
+QED
+
 val _ = export_theory ()
diff --git a/backends/hol4/testHashmapTheory.sig b/backends/hol4/testHashmapTheory.sig
index fd22e05b..16031716 100644
--- a/backends/hol4/testHashmapTheory.sig
+++ b/backends/hol4/testHashmapTheory.sig
@@ -15,7 +15,13 @@ sig
   
   (*  Theorems  *)
     val datatype_list_t : thm
+    val distinct_keys_cons : thm
+    val distinct_keys_insert : thm
+    val distinct_keys_insert_index_neq : thm
+    val distinct_keys_tail : thm
+    val insert_index_neq : thm
     val insert_lem : thm
+    val insert_lem_aux : thm
     val list_t_11 : thm
     val list_t_Axiom : thm
     val list_t_case_cong : thm
@@ -52,12 +58,10 @@ sig
       ⊢ ∀ls.
           distinct_keys ls ⇔
           ∀i j.
-            0 < i ⇒
-            i < len ls ⇒
-            0 < j ⇒
+            0 ≤ i ⇒
+            i < j ⇒
             j < len ls ⇒
-            FST (index i ls) = FST (index j ls) ⇒
-            i = j
+            FST (index i ls) ≠ FST (index j ls)
    
    [list_t_TY_DEF]  Definition
       
@@ -101,6 +105,48 @@ sig
       
       ⊢ DATATYPE (list_t ListCons ListNil)
    
+   [distinct_keys_cons]  Theorem
+      
+      ⊢ ∀k v ls.
+          (∀i. 0 ≤ i ⇒ i < len ls ⇒ FST (index i ls) ≠ k) ⇒
+          distinct_keys ls ⇒
+          distinct_keys ((k,v)::ls)
+   
+   [distinct_keys_insert]  Theorem
+      
+      [oracles: DISK_THM] [axioms: insert_def] []
+      ⊢ ∀k v ls0 ls1.
+          distinct_keys (list_t_v ls0) ⇒
+          insert k v ls0 = Return ls1 ⇒
+          distinct_keys (list_t_v ls1)
+   
+   [distinct_keys_insert_index_neq]  Theorem
+      
+      [oracles: DISK_THM] [axioms: insert_def] []
+      ⊢ ∀k v q r ls0 ls1 i.
+          distinct_keys ((q,r)::list_t_v ls0) ⇒
+          q ≠ k ⇒
+          insert k v ls0 = Return ls1 ⇒
+          0 ≤ i ⇒
+          i < len (list_t_v ls1) ⇒
+          FST (index i (list_t_v ls1)) ≠ q
+   
+   [distinct_keys_tail]  Theorem
+      
+      ⊢ ∀k v ls. distinct_keys ((k,v)::ls) ⇒ distinct_keys ls
+   
+   [insert_index_neq]  Theorem
+      
+      [oracles: DISK_THM] [axioms: insert_def] []
+      ⊢ ∀q k v ls0 ls1 i.
+          (∀j. 0 ≤ j ∧ j < len (list_t_v ls0) ⇒
+               q ≠ FST (index j (list_t_v ls0))) ⇒
+          q ≠ k ⇒
+          insert k v ls0 = Return ls1 ⇒
+          0 ≤ i ⇒
+          i < len (list_t_v ls1) ⇒
+          FST (index i (list_t_v ls1)) ≠ q
+   
    [insert_lem]  Theorem
       
       [oracles: DISK_THM] [axioms: insert_def] []
@@ -109,8 +155,20 @@ sig
           case insert key value ls of
             Return ls1 =>
               lookup key ls1 = SOME value ∧
+              (∀k. k ≠ key ⇒ lookup k ls = lookup k ls1) ∧
+              distinct_keys (list_t_v ls1)
+          | Fail v1 => F
+          | Diverge => F
+   
+   [insert_lem_aux]  Theorem
+      
+      [oracles: DISK_THM] [axioms: insert_def] []
+      ⊢ ∀ls key value.
+          case insert key value ls of
+            Return ls1 =>
+              lookup key ls1 = SOME value ∧
               ∀k. k ≠ key ⇒ lookup k ls = lookup k ls1
-          | Fail v3 => F
+          | Fail v1 => F
           | Diverge => F
    
    [list_t_11]  Theorem
@@ -184,7 +242,7 @@ sig
           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 v3 => F
+          | Fail v1 => F
           | Diverge => F