diff options
Diffstat (limited to '')
| -rw-r--r-- | backends/hol4/testHashmapScript.sml | 196 |
1 files changed, 178 insertions, 18 deletions
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 () |