summaryrefslogtreecommitdiff
path: root/backends
diff options
context:
space:
mode:
authorSon Ho2023-05-10 12:26:43 +0200
committerSon HO2023-06-04 21:54:38 +0200
commit4a84682195457d5b6d905b95bd7220ebacd30f91 (patch)
tree225c83fed0301b9501180422470a0a876d019a68 /backends
parent025f6b047a7a4c1d063aa5f72ac445de76e6d116 (diff)
Make more proofs about the hashmap proto
Diffstat (limited to '')
-rw-r--r--backends/hol4/primitivesArithScript.sml6
-rw-r--r--backends/hol4/primitivesArithTheory.sig5
-rw-r--r--backends/hol4/primitivesBaseTacLib.sml25
-rw-r--r--backends/hol4/testHashmapScript.sml138
-rw-r--r--backends/hol4/testHashmapTheory.sig55
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