Make more proofs about the hashmap proto

5 files changed, 225 insertions, 4 deletions

diff --git a/backends/hol4/primitivesArithScript.sml b/backends/hol4/primitivesArithScript.sml
index 6c96c908..2682e507 100644
--- a/backends/hol4/primitivesArithScript.sml
+++ b/backends/hol4/primitivesArithScript.sml
@@ -18,6 +18,12 @@ val le_eq_ge = store_thm("le_eq_ge", “!(x y : int). x <= y <=> y >= x”, coop
 val gt_eq_lt = store_thm("gt_eq_lt", “!(x y : int). x > y <=> y < x”, cooper_tac)
 val lt_eq_gt = store_thm("lt_eq_gt", “!(x y : int). x < y <=> y > x”, cooper_tac)
 
+Theorem int_add_minus_same_eq:
+  ∀ (i j : int). i + j - j = i
+Proof
+  int_tac
+QED
+
 (*
  * We generate and save an induction theorem for positive integers
  *)
diff --git a/backends/hol4/primitivesArithTheory.sig b/backends/hol4/primitivesArithTheory.sig
index e32b49d4..f7ecccab 100644
--- a/backends/hol4/primitivesArithTheory.sig
+++ b/backends/hol4/primitivesArithTheory.sig
@@ -7,6 +7,7 @@ sig
     val ge_eq_le : thm
     val gt_eq_lt : thm
     val int_add : thm
+    val int_add_minus_same_eq : thm
     val int_induction : thm
     val int_induction_ideal : thm
     val int_of_num_id : thm
@@ -48,6 +49,10 @@ sig
       
       ⊢ ∀m n. &(m + n) = &m + &n
    
+   [int_add_minus_same_eq]  Theorem
+      
+      ⊢ ∀i j. i + j − j = i
+   
    [int_induction]  Theorem
       
       ⊢ ∀P. (∀i. i < 0 ⇒ P i) ∧ P 0 ∧ (∀i. P i ⇒ P (i + 1)) ⇒ ∀i. P i
diff --git a/backends/hol4/primitivesBaseTacLib.sml b/backends/hol4/primitivesBaseTacLib.sml
index 0363ad41..1e874ad5 100644
--- a/backends/hol4/primitivesBaseTacLib.sml
+++ b/backends/hol4/primitivesBaseTacLib.sml
@@ -31,6 +31,7 @@ val map_first_tac = MAP_FIRST
 val fail_tac = FAIL_TAC
 val map_every_tac = MAP_EVERY
 
+(* TODO: rename assume to asm *)
 fun qspec_assume x th = qspec_then x assume_tac th
 fun qspecl_assume xl th = qspecl_then xl assume_tac th
 fun first_qspec_assume x = first_assum (qspec_assume x)
@@ -41,6 +42,11 @@ 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
 
+val pat_undisch_tac = Q.PAT_UNDISCH_TAC
+
+val equiv_is_imp = prove (“∀x y. ((x ⇒ y) ∧ (y ⇒ x)) ⇒ (x ⇔ y)”, metis_tac [])
+val equiv_tac = irule equiv_is_imp >> conj_tac
+
 (* Dependent rewrites *)
 val dep_pure_once_rewrite_tac = dep_rewrite.DEP_PURE_ONCE_REWRITE_TAC
 val dep_pure_rewrite_tac = dep_rewrite.DEP_PURE_REWRITE_TAC
@@ -493,6 +499,10 @@ fun filter_assums_tac (keep : term -> bool) : tactic =
   in
     ([(kept_asms, g)], valid)
   end
+  
+(* For debugging *)
+val dest_assums_conjs_th = ref sumTheory.EXISTS_SUM
+val dest_assums_conjs_goal = ref “T”
 
 (* Destruct the conjunctions in the assumptions *)
 val dest_assums_conjs_tac : tactic =
@@ -505,6 +515,8 @@ val dest_assums_conjs_tac : tactic =
       case thms of
         [th] =>
         let
+          (* Save the theorem for debugging *)
+          val _ = dest_assums_conjs_th := th
           (* Being a bit brutal - will optimize later *)
           val tac = ntac (length asms) strip_tac >>
             (* Small subtlety: we have to use the primitive irule here,
@@ -515,8 +527,13 @@ val dest_assums_conjs_tac : tactic =
             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)
+            pure_asm_rewrite_tac [] >> SIMP_TAC bool_ss [] >> 
+            (* We may need to finish the job with metis - TODO: there must be a better way *)
+            metis_tac []
+          (* Save the goal for debugging *)
+          val ng = list_mk_imp (asms, g)
+          val _ = dest_assums_conjs_goal := ng
+          val th = prove (ng, tac)
           val th = foldl (fn (_, th) => UNDISCH th) th asms
         in th end
       | _ => failwith "dest_assums_conjs: expected exactly one theorem"
@@ -538,7 +555,7 @@ val int_tac_pats = [
     “x: num >= y”,
     “x: num > y”
 ]
-val int_tac_ops = Redblackset.fromList Term.compare (map (fst o strip_comb) int_tac_pats)  
+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) =
@@ -560,7 +577,7 @@ fun int_tac (asms, g) =
  in
    (dest_assums_conjs_tac >>
     filter_assums_tac keep >>
-    first_tac [cooper_tac, exfalso >> cooper_tac]) (asms, g)
+    first_tac [cooper_tac, exfalso >- cooper_tac]) (asms, g)
  end
 
 (* Repeatedly destruct cases and return the last scrutinee we get *)
diff --git a/backends/hol4/testHashmapScript.sml b/backends/hol4/testHashmapScript.sml
index 7108776d..0e16ead3 100644
--- a/backends/hol4/testHashmapScript.sml
+++ b/backends/hol4/testHashmapScript.sml
@@ -111,6 +111,10 @@ Proof
   fs [lookup_def, lookup_raw_def, list_t_v_def]
 QED
 
+(*
+ * Invariant proof 1
+ *)
+
 Theorem distinct_keys_cons:
   ∀ k v ls.
   (∀ i. 0 ≤ i ⇒ i < len ls ⇒ FST (index i ls) ≠ k) ⇒
@@ -280,4 +284,138 @@ Proof
   metis_tac [distinct_keys_insert]
 QED
 
+(*
+ * Invariant proof 2: functional version of the invariant
+ *)
+val for_all_def = Define ‘
+  for_all p [] = T ∧
+  for_all p (x :: ls) = (p x ∧ for_all p ls)
+’
+
+val pairwise_rel_def = Define ‘
+  pairwise_rel p [] = T ∧
+  pairwise_rel p (x :: ls) = (for_all (p x) ls ∧ pairwise_rel p ls)
+’
+
+val distinct_keys_f_def = Define ‘
+  distinct_keys_f (ls : (u32 # 't) list) =
+    pairwise_rel (\x y. FST x ≠ FST y) ls
+’
+
+Theorem distinct_keys_f_insert_for_all:
+  ∀k v k1 ls0 ls1.
+  k1 ≠ k ⇒
+  for_all (λy. k1 ≠ FST y) (list_t_v ls0) ⇒
+  pairwise_rel (λx y. FST x ≠ FST y) (list_t_v ls0) ⇒
+  insert k v ls0 = Return ls1 ⇒
+  for_all (λy. k1 ≠ FST y) (list_t_v ls1)
+Proof
+  Induct_on ‘ls0’ >> rw [pairwise_rel_def] >~ [‘ListNil’] >>
+  gvs [list_t_v_def, pairwise_rel_def, for_all_def]
+  >-(gvs [MK_BOUNDED insert_def 1, bind_def, list_t_v_def, for_all_def]) >>
+  pat_undisch_tac ‘insert _ _ _ = _’ >>
+  simp [MK_BOUNDED insert_def 1, bind_def] >>
+  Cases_on ‘t’ >> rw [] >> gvs [list_t_v_def, pairwise_rel_def, for_all_def] >>
+  Cases_on ‘insert k v ls0’ >>
+  gvs [distinct_keys_f_def, list_t_v_def, pairwise_rel_def, for_all_def] >>
+  metis_tac []
+QED
+
+Theorem distinct_keys_f_insert:
+  ∀ k v ls0 ls1.
+  distinct_keys_f (list_t_v ls0) ⇒
+  insert k v ls0 = Return ls1 ⇒
+  distinct_keys_f (list_t_v ls1)
+Proof
+  Induct_on ‘ls0’ >> rw [distinct_keys_f_def] >~ [‘ListNil’]
+  >-(
+    fs [list_t_v_def, insert_def] >>
+    gvs [list_t_v_def, pairwise_rel_def, for_all_def]) >>
+  last_x_assum (qspecl_assume [‘k’, ‘v’]) >>
+  pat_undisch_tac ‘insert _ _ _ = _’ >>
+  simp [MK_BOUNDED insert_def 1, bind_def] >>
+  (* TODO: improve case_tac *)
+  Cases_on ‘t’ >> rw [] >> gvs [list_t_v_def, pairwise_rel_def, for_all_def] >>
+  Cases_on ‘insert k v ls0’ >>
+  gvs [distinct_keys_f_def, list_t_v_def, pairwise_rel_def, for_all_def] >>
+  metis_tac [distinct_keys_f_insert_for_all]
+QED
+
+(*
+ * Proving equivalence between the two version - exercise.
+ *)
+Theorem for_all_quant:
+  ∀p ls. for_all p ls ⇔ ∀i. 0 ≤ i ⇒ i < len ls ⇒ p (index i ls)
+Proof
+  strip_tac >> Induct_on ‘ls’
+  >-(rw [for_all_def, len_def] >> int_tac) >>
+  rw [for_all_def, len_def, index_eq] >>
+  equiv_tac
+  >-(
+    rw [] >>
+    Cases_on ‘i = 0’ >> fs [] >>
+    first_x_assum irule >>
+    int_tac) >>
+  rw []
+  >-(
+    first_x_assum (qspec_assume ‘0’) >> fs [] >>
+    first_x_assum irule >>
+    qspec_assume ‘ls’ len_pos >>
+    int_tac) >>
+  first_x_assum (qspec_assume ‘i + 1’) >>
+  fs [] >>
+  sg ‘i + 1 ≠ 0 ∧ i + 1 - 1 = i’ >- int_tac >> fs [] >>
+  first_x_assum irule >> int_tac
+QED
+
+Theorem pairwise_rel_quant:
+  ∀p ls. pairwise_rel p ls ⇔
+    (∀i j. 0 ≤ i ⇒ i < j ⇒ j < len ls ⇒ p (index i ls) (index j ls))
+Proof
+  strip_tac >> Induct_on ‘ls’
+  >-(rw [pairwise_rel_def, len_def] >> int_tac) >>
+  rw [pairwise_rel_def, len_def] >>
+  equiv_tac
+  >-(
+    (* ==> *)
+    rw [] >>
+    sg ‘0 < j’ >- int_tac >>
+    Cases_on ‘i = 0’
+    >-(
+      simp [index_eq] >>
+      qspecl_assume [‘p h’, ‘ls’] (iffLR for_all_quant) >>
+      first_x_assum irule >> fs [] >> int_tac
+    ) >>
+    rw [index_eq] >>
+    first_x_assum irule >> int_tac
+  ) >>
+  (* <== *)
+  rw []
+  >-(
+    rw [for_all_quant] >>
+    first_x_assum (qspecl_assume [‘0’, ‘i + 1’]) >>
+    sg ‘0 < i + 1 ∧ i + 1 - 1 = i’ >- int_tac >>
+    fs [index_eq] >>
+    first_x_assum irule >> int_tac
+  ) >>
+  sg ‘pairwise_rel p ls’
+  >-(
+    rw [pairwise_rel_def] >>
+    first_x_assum (qspecl_assume [‘i' + 1’, ‘j' + 1’]) >>
+    sg ‘0 < i' + 1 ∧ 0 < j' + 1’ >- int_tac >>
+    fs [index_eq, int_add_minus_same_eq] >>
+    first_x_assum irule >> int_tac
+  ) >>
+  fs []
+QED
+
+Theorem distinct_keys_f_eq_distinct_keys:
+  ∀ ls.
+  distinct_keys_f ls ⇔ distinct_keys ls
+Proof
+  rw [distinct_keys_def, distinct_keys_f_def] >>
+  qspecl_assume [‘(λx y. FST x ≠ FST y)’, ‘ls’] pairwise_rel_quant >>
+  fs []
+QED
+
 val _ = export_theory ()
diff --git a/backends/hol4/testHashmapTheory.sig b/backends/hol4/testHashmapTheory.sig
index 16031716..1d304723 100644
--- a/backends/hol4/testHashmapTheory.sig
+++ b/backends/hol4/testHashmapTheory.sig
@@ -7,18 +7,25 @@ sig
   
   (*  Definitions  *)
     val distinct_keys_def : thm
+    val distinct_keys_f_def : thm
+    val for_all_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
+    val pairwise_rel_def : thm
   
   (*  Theorems  *)
     val datatype_list_t : thm
     val distinct_keys_cons : thm
+    val distinct_keys_f_eq_distinct_keys : thm
+    val distinct_keys_f_insert : thm
+    val distinct_keys_f_insert_for_all : thm
     val distinct_keys_insert : thm
     val distinct_keys_insert_index_neq : thm
     val distinct_keys_tail : thm
+    val for_all_quant : thm
     val insert_index_neq : thm
     val insert_lem : thm
     val insert_lem_aux : thm
@@ -34,6 +41,7 @@ sig
     val nth_mut_fwd_def : thm
     val nth_mut_fwd_ind : thm
     val nth_mut_fwd_spec : thm
+    val pairwise_rel_quant : thm
   
   val testHashmap_grammars : type_grammar.grammar * term_grammar.grammar
 (*
@@ -63,6 +71,15 @@ sig
             j < len ls ⇒
             FST (index i ls) ≠ FST (index j ls)
    
+   [distinct_keys_f_def]  Definition
+      
+      ⊢ ∀ls. distinct_keys_f ls ⇔ pairwise_rel (λx y. FST x ≠ FST y) ls
+   
+   [for_all_def]  Definition
+      
+      ⊢ (∀p. for_all p [] ⇔ T) ∧
+        ∀p x ls. for_all p (x::ls) ⇔ p x ∧ for_all p ls
+   
    [list_t_TY_DEF]  Definition
       
       ⊢ ∃rep.
@@ -101,6 +118,12 @@ sig
       
       ⊢ ∀key ls. lookup key ls = lookup_raw key (list_t_v ls)
    
+   [pairwise_rel_def]  Definition
+      
+      ⊢ (∀p. pairwise_rel p [] ⇔ T) ∧
+        ∀p x ls.
+          pairwise_rel p (x::ls) ⇔ for_all (p x) ls ∧ pairwise_rel p ls
+   
    [datatype_list_t]  Theorem
       
       ⊢ DATATYPE (list_t ListCons ListNil)
@@ -112,6 +135,28 @@ sig
           distinct_keys ls ⇒
           distinct_keys ((k,v)::ls)
    
+   [distinct_keys_f_eq_distinct_keys]  Theorem
+      
+      ⊢ ∀ls. distinct_keys_f ls ⇔ distinct_keys ls
+   
+   [distinct_keys_f_insert]  Theorem
+      
+      [oracles: DISK_THM] [axioms: insert_def] []
+      ⊢ ∀k v ls0 ls1.
+          distinct_keys_f (list_t_v ls0) ⇒
+          insert k v ls0 = Return ls1 ⇒
+          distinct_keys_f (list_t_v ls1)
+   
+   [distinct_keys_f_insert_for_all]  Theorem
+      
+      [oracles: DISK_THM] [axioms: insert_def] []
+      ⊢ ∀k v k1 ls0 ls1.
+          k1 ≠ k ⇒
+          for_all (λy. k1 ≠ FST y) (list_t_v ls0) ⇒
+          pairwise_rel (λx y. FST x ≠ FST y) (list_t_v ls0) ⇒
+          insert k v ls0 = Return ls1 ⇒
+          for_all (λy. k1 ≠ FST y) (list_t_v ls1)
+   
    [distinct_keys_insert]  Theorem
       
       [oracles: DISK_THM] [axioms: insert_def] []
@@ -135,6 +180,10 @@ sig
       
       ⊢ ∀k v ls. distinct_keys ((k,v)::ls) ⇒ distinct_keys ls
    
+   [for_all_quant]  Theorem
+      
+      ⊢ ∀p ls. for_all p ls ⇔ ∀i. 0 ≤ i ⇒ i < len ls ⇒ p (index i ls)
+   
    [insert_index_neq]  Theorem
       
       [oracles: DISK_THM] [axioms: insert_def] []
@@ -245,6 +294,12 @@ sig
           | Fail v1 => F
           | Diverge => F
    
+   [pairwise_rel_quant]  Theorem
+      
+      ⊢ ∀p ls.
+          pairwise_rel p ls ⇔
+          ∀i j. 0 ≤ i ⇒ i < j ⇒ j < len ls ⇒ p (index i ls) (index j ls)
+   
    
 *)
 end