diff options
author | Son Ho | 2023-05-09 21:22:57 +0200 |
---|---|---|
committer | Son HO | 2023-06-04 21:54:38 +0200 |
commit | 025f6b047a7a4c1d063aa5f72ac445de76e6d116 (patch) | |
tree | eb21309193fca0e22a996629af1a8dd0d8f6b081 | |
parent | 266bb06fea0a3ed22aad8b5862b502cb621714ac (diff) |
Update the hashmap proofs and fix some tactics
Diffstat (limited to '')
-rw-r--r-- | backends/hol4/ilistScript.sml | 8 | ||||
-rw-r--r-- | backends/hol4/ilistTheory.sig | 5 | ||||
-rw-r--r-- | backends/hol4/primitivesBaseTacLib.sml | 65 | ||||
-rw-r--r-- | backends/hol4/testHashmapScript.sml | 196 | ||||
-rw-r--r-- | backends/hol4/testHashmapTheory.sig | 72 |
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 |