diff options
Diffstat (limited to 'backends')
| -rw-r--r-- | backends/hol4/primitivesArithScript.sml | 6 | ||||
| -rw-r--r-- | backends/hol4/primitivesArithTheory.sig | 5 | ||||
| -rw-r--r-- | backends/hol4/primitivesBaseTacLib.sml | 25 | ||||
| -rw-r--r-- | backends/hol4/testHashmapScript.sml | 138 | ||||
| -rw-r--r-- | backends/hol4/testHashmapTheory.sig | 55 |
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 |