diff options
| -rw-r--r-- | backends/hol4/Test.sml | 70 |
1 files changed, 69 insertions, 1 deletions
diff --git a/backends/hol4/Test.sml b/backends/hol4/Test.sml index 55915fbc..b16b67fb 100644 --- a/backends/hol4/Test.sml +++ b/backends/hol4/Test.sml @@ -1391,7 +1391,75 @@ Proof progress >> progress QED -(* *) +(* Example from the hashmap *) +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 = + case ls of + | ListCons (ckey, cvalue) tl => + if ckey = key + then Return (ListCons (ckey, value) tl) + else + do + tl0 <- insert key value tl; + Return (ListCons (ckey, cvalue) tl0) + od + | ListNil => Return (ListCons (key, value) ListNil) + ”) + +(* Property that keys are pairwise distinct *) +val distinct_keys_def = Define ‘ + distinct_keys (ls : (u32 # 't) list) = + !i j. + i < LENGTH ls ==> + j < LENGTH ls ==> + FST (EL i ls) = FST (EL j ls) ==> + i = j +’ + +val lookup_raw_def = Define ‘ + lookup_raw key [] = NONE /\ + lookup_raw key ((k, v) :: ls) = + if k = key then SOME v else lookup_raw key ls +’ + +val lookup_def = Define ‘ + lookup key ls = lookup_raw key (list_t_v ls) +’ + +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) + | Fail _ => F + | Loop => F +Proof + Induct_on ‘ls’ >> rw [list_t_v_def] >~ [‘ListNil’] >> + PURE_ONCE_REWRITE_TAC [insert_def] >> rw [] + >- (rw [lookup_def, lookup_raw_def, list_t_v_def]) + >- (rw [lookup_def, lookup_raw_def, list_t_v_def]) >> + CASE_TAC >> rw [] + >- (rw [lookup_def, lookup_raw_def, list_t_v_def]) + >- (rw [lookup_def, lookup_raw_def, list_t_v_def]) >> + progress + >- ( + fs [distinct_keys_def] >> + rpt strip_tac >> + first_assum (qspecl_then [‘SUC i’, ‘SUC j’] ASSUME_TAC) >> + fs [] + (* Alternative: *) + (* + PURE_ONCE_REWRITE_TAC [GSYM prim_recTheory.INV_SUC_EQ] >> + first_assum irule >> fs [] + *)) >> + fs [lookup_def, lookup_raw_def, list_t_v_def] +QED (*** * Example of how to get rid of the fuel in practice |