diff --git a/basis/Holmakefile b/basis/Holmakefile index ae036ef13b..31bfbf0884 100644 --- a/basis/Holmakefile +++ b/basis/Holmakefile @@ -1,7 +1,7 @@ INCLUDES = $(CAKEMLDIR)/developers $(CAKEMLDIR)/misc\ $(CAKEMLDIR)/semantics $(CAKEMLDIR)/characteristic\ $(CAKEMLDIR)/translator $(CAKEMLDIR)/translator/monadic\ - $(CAKEMLDIR)/compiler/printing pure + $(CAKEMLDIR)/compiler/printing pure monadic all: $(DEFAULT_TARGETS) README.md basis_ffi.o .PHONY: all diff --git a/basis/ListProgScript.sml b/basis/ListProgScript.sml index 109f43cf90..a20f56d9fc 100644 --- a/basis/ListProgScript.sml +++ b/basis/ListProgScript.sml @@ -6,6 +6,7 @@ Ancestors mergesort std_prelude mllist ml_translator OptionProg Libs preamble ml_translatorLib ml_progLib cfLib basisFunctionsLib + ml_monad_translator_interfaceLib val _ = translation_extends "OptionProg" @@ -339,6 +340,14 @@ val result = translate LUPDATE_eq; val _ = (next_ml_names := ["compare"]); val _ = translate mllistTheory.list_compare_def; +(* Translation of conventional merge-sort. + + * This is also List.sort, but is given the "mergesort" name too. + + * (The mergesort name was used in an experiment to allow the Candle kernel + * to specifically request this sort, and not an array-based alternative whose + * use of stateful features clashes with the Candle proofs.) + *) val _ = ml_prog_update open_local_block; val result = translate sort2_tail_def; @@ -347,6 +356,7 @@ val result = translate REV_DEF; val result = translate merge_tail_def; val result = translate DIV2_def; val result = translate DROP_def; + val result = translate_no_ind mergesortN_tail_def; Theorem mergesortn_tail_ind[local]: @@ -391,11 +401,15 @@ val result = translate mergesort_tail_def val _ = ml_prog_update open_local_in_block; +val _ = next_ml_names := ["mergesort"]; +val result = translate mergesort_def; + val _ = next_ml_names := ["sort"]; -val result = translate sort_def; +val sort_v_thm = mllistTheory.sort_thm |> translate; val _ = ml_prog_update close_local_blocks; + val _ = ml_prog_update (close_module NONE); (* finite maps -- depend on lists *) diff --git a/basis/README.md b/basis/README.md index 39a74be5fb..8d0b21e33a 100644 --- a/basis/README.md +++ b/basis/README.md @@ -149,6 +149,9 @@ Logical model of filesystem and I/O streams [mlbasicsProgScript.sml](mlbasicsProgScript.sml): Translates a variety of basic constructs. +[monadic](monadic): +Monadic definitions of stateful functions used in the basis + [pure](pure): HOL definitions of the pure functions used in the CakeML basis. diff --git a/basis/monadic/Holmakefile b/basis/monadic/Holmakefile new file mode 100644 index 0000000000..478702053b --- /dev/null +++ b/basis/monadic/Holmakefile @@ -0,0 +1,14 @@ +INCLUDES = $(CAKEMLDIR)/misc \ + $(CAKEMLDIR)/translator/monadic/ $(CAKEMLDIR)/translator/ + +all: $(DEFAULT_TARGETS) README.md +.PHONY: all + +README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax.sml) +DIRS = $(wildcard */) +README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES) + $(CAKEMLDIR)/developers/readme_gen $(README_SOURCES) + +ifdef POLY +HOLHEAP = $(CAKEMLDIR)/misc/cakeml-heap +endif diff --git a/basis/monadic/README.md b/basis/monadic/README.md new file mode 100644 index 0000000000..ffdf792519 --- /dev/null +++ b/basis/monadic/README.md @@ -0,0 +1,16 @@ +Monadic definitions of stateful functions used in the basis + +These functions are generated and verified using a monad type, and are then +translated to imperative CakeML code by the monadic translator. + +[heap_list_sort_monadicScript.sml](heap_list_sort_monadicScript.sml): +Monadic variants of the heap-list sort functions, and proofs of equivalence. + +[heap_list_sort_translationScript.sml](heap_list_sort_translationScript.sml): +Post-translation of heap_list_sort + +[merge_run_sort_monadicScript.sml](merge_run_sort_monadicScript.sml): +Monadic variants of the merge-run-sort functions, and proofs of equivalence. + +[merge_run_sort_translationScript.sml](merge_run_sort_translationScript.sml): +Post-translation of merge_run_sort diff --git a/basis/monadic/readmePrefix b/basis/monadic/readmePrefix new file mode 100644 index 0000000000..12720152a8 --- /dev/null +++ b/basis/monadic/readmePrefix @@ -0,0 +1,4 @@ +Monadic definitions of stateful functions used in the basis + +These functions are generated and verified using a monad type, and are then +translated to imperative CakeML code by the monadic translator. diff --git a/basis/pure/README.md b/basis/pure/README.md index e4f9eb8d1d..9b0e0c73ca 100644 --- a/basis/pure/README.md +++ b/basis/pure/README.md @@ -6,6 +6,12 @@ from these by the translator. [basis_cvScript.sml](basis_cvScript.sml): Translation of basis types and functions for use with cv_compute. +[heap_list_sortScript.sml](heap_list_sortScript.sml): +A heap-sort variant that builds a list of exactly-balanced heaps. + +[merge_run_sortScript.sml](merge_run_sortScript.sml): +Verified run-finding (natural) merge sort. + [mlintScript.sml](mlintScript.sml): Pure functions for the Int module. diff --git a/basis/pure/mllistScript.sml b/basis/pure/mllistScript.sml index 1ffad092a0..c3ff0b45f6 100644 --- a/basis/pure/mllistScript.sml +++ b/basis/pure/mllistScript.sml @@ -277,6 +277,10 @@ Proof QED (* ^^^^^ TO BE PORTED TO HOL ^^^^^ *) +Definition mergesort_def: + mergesort = mergesort$mergesort_tail +End + Definition sort_def: sort = mergesort$mergesort_tail End @@ -287,26 +291,31 @@ Proof rw[sort_def] QED -Theorem sort_SORTED: - !R L. transitive R ∧ total R ==> sorting$SORTED R (sort R L) +Theorem total_reflexive[local]: + total R ==> reflexive R Proof - simp[sort_def, mergesort_tail_def, mergesortN_correct, mergesortN_sorted] + simp [total_def, reflexive_def] + \\ metis_tac [] QED -Theorem sort_MEM[simp]: - !R L. MEM x (sort R L) ⇔ MEM x L +Theorem sort_SORTED: + !R L. transitive R ∧ total R ==> sorting$SORTED R (sort R L) Proof - simp[sort_def, mergesort_tail_MEM] + simp [mergesort_tail_correct, sort_def, mergesort_sorted] QED Theorem sort_PERM: !R L. sorting$PERM L (sort R L) Proof - simp[sort_def, mergesort_tail_def] - \\ rpt strip_tac - \\ `L = TAKE (LENGTH L) L` by rw[] - \\ pop_assum (fn x => pure_rewrite_tac [Once $ x]) - \\ rw[mergesortN_tail_PERM] + rw [sort_def, mergesort_tail_def] + \\ irule PERM_TRANS \\ irule_at Any mergesortN_tail_PERM + \\ simp [] +QED + +Theorem sort_MEM[simp]: + !R L. MEM x (sort R L) ⇔ MEM x L +Proof + metis_tac [sort_PERM, PERM_MEM_EQ] QED Theorem sort_LENGTH[simp]: diff --git a/candle/overloading/monadic/holKernelProofScript.sml b/candle/overloading/monadic/holKernelProofScript.sml index 3def9242e8..27872aa9fe 100644 --- a/candle/overloading/monadic/holKernelProofScript.sml +++ b/candle/overloading/monadic/holKernelProofScript.sml @@ -1684,31 +1684,50 @@ Proof \\ IMP_RES_TAC TERM_Var \\ FULL_SIMP_TAC std_ss [pred_setTheory.IN_UNION] QED -Theorem sort_type_vars_in_term: - (sort $<= (MAP explode (type_vars_in_term P)) = STRING_SORT (MAP explode (tvars P))) +Overload candle_sort[local] = ``mllist$mergesort`` + +Theorem string_le_ok[local]: + total string_le /\ antisymmetric string_le /\ transitive string_le Proof - REPEAT STRIP_TAC \\ - MATCH_MP_TAC (MP_CANON sortingTheory.SORTED_PERM_EQ) \\ - qexists_tac`$<=` >> - conj_asm1_tac >- ( - simp[relationTheory.transitive_def,relationTheory.antisymmetric_def,stringTheory.string_le_def] >> - METIS_TAC[stringTheory.string_lt_antisym,stringTheory.string_lt_trans] ) >> - conj_tac >- ( - MATCH_MP_TAC sort_SORTED >> - simp[relationTheory.total_def,stringTheory.string_le_def] >> - METIS_TAC[stringTheory.string_lt_cases] ) >> - conj_tac >- ( + simp[relationTheory.total_def, relationTheory.transitive_def, + relationTheory.antisymmetric_def, stringTheory.string_le_def] >> + METIS_TAC[stringTheory.string_lt_cases, stringTheory.string_lt_antisym, + stringTheory.string_lt_trans] +QED + +Theorem candle_sort_ok[local]: + SORTED string_le (candle_sort string_le xs) /\ + (PERM (candle_sort string_le xs) ys = PERM xs ys) +Proof + simp [mllistTheory.mergesort_def, mergesortTheory.mergesort_tail_correct, + string_le_ok, mergesortTheory.mergesort_sorted] + \\ metis_tac [mergesortTheory.mergesort_perm, sortingTheory.PERM_TRANS, + sortingTheory.PERM_SYM] +QED + +Theorem LENGTH_candle_sort[local]: + LENGTH (candle_sort string_le xs) = LENGTH xs +Proof + irule sortingTheory.PERM_LENGTH + \\ simp [candle_sort_ok] +QED + +Theorem candle_sort_type_vars_in_term[local]: + TERM defs P ==> + (candle_sort $<= (MAP explode (type_vars_in_term P)) = STRING_SORT (MAP explode (tvars P))) +Proof + rw [] + \\ irule sortingTheory.SORTED_PERM_EQ + \\ irule_at Any (hd (BODY_CONJUNCTS candle_sort_ok)) + \\ simp [string_le_ok, candle_sort_ok] + \\ reverse conj_tac >- ( MATCH_MP_TAC sortingTheory.SORTED_weaken >> qexists_tac`$<` >> simp[STRING_SORT_SORTED,stringTheory.string_le_def] ) >> - MATCH_MP_TAC (MP_CANON sortingTheory.PERM_ALL_DISTINCT) >> - conj_tac >- ( - METIS_TAC[sortingTheory.ALL_DISTINCT_PERM - ,sort_PERM - ,ALL_DISTINCT_type_vars_in_term - ,ALL_DISTINCT_MAP_explode] ) >> - simp[ALL_DISTINCT_STRING_SORT] >> - METIS_TAC[MEM_type_vars_in_term,MEM_MAP] + irule sortingTheory.PERM_ALL_DISTINCT + \\ simp [ALL_DISTINCT_MAP_explode, ALL_DISTINCT_type_vars_in_term] + \\ simp [MEM_MAP] + \\ metis_tac [MEM_type_vars_in_term] QED (* ------------------------------------------------------------------------- *) @@ -3545,7 +3564,7 @@ Proof impl_tac >- METIS_TAC[STATE_def,TERM_Comb,THM] >> simp[] >> disch_then kall_tac >> simp[Once st_ex_bind_def] >> - Q.PAT_ABBREV_TAC`vs:string list = sort R X` >> + Q.PAT_ABBREV_TAC`vs:string list = candle_sort R X` >> simp[add_type_def,can_def,otherwise_def,st_ex_return_def] >> ntac 2 (simp[Once st_ex_bind_def]) >> simp[Once st_ex_bind_def,get_the_type_constants_def] >> @@ -3556,6 +3575,7 @@ Proof `get_type_arity tyname s1 = (M_success (LENGTH vs), s1)` by ( simp[get_type_arity_def,st_ex_bind_def,Abbr`s1`] >> simp[Abbr`vs`]>> + simp[LENGTH_candle_sort]>> EVAL_TAC)>> simp[mk_type_def,try_def,otherwise_def,raise_Fail_def,st_ex_return_def,Once st_ex_bind_def] >> simp[mk_fun_ty_def] >> @@ -3601,12 +3621,10 @@ Proof rfs[TERM_def] >> METIS_TAC[]) >> imp_res_tac THM >> rfs[TERM_Comb] >> imp_res_tac THM_term_ok_bool >> - fs[term_ok_def,sort_type_vars_in_term] >> + fs[term_ok_def, candle_sort_type_vars_in_term] >> rfs[WELLTYPED] >> simp[Abbr`s2`,Abbr`s1`,Abbr`vs`,Abbr`l1`] >> - CONJ_TAC >- ( - qspec_then ‘P’ (mp_tac o Q.AP_TERM ‘LENGTH’) (GEN_ALL sort_type_vars_in_term) >> - simp[sort_LENGTH])>> + fsrw_tac [SFY_ss] [candle_sort_type_vars_in_term, sort_LENGTH] >> METIS_TAC[term_type]) >> qmatch_assum_abbrev_tac`Abbrev(l1 = [(absname,absty);(repname,repty)])` >> `mk_const (repname,[]) s2 = (M_success (Const repname repty), s2)` by ( @@ -3782,15 +3800,16 @@ Proof \\ conj_tac >- METIS_TAC[STATE_def,CONTEXT_def,extends_theory_ok,init_theory_ok] \\ simp [Abbr`s2`,conexts_of_upd_def] - \\ imp_res_tac sort_type_vars_in_term - \\ simp [equation_def,Abbr`vs`,MAP_MAP_o,combinTheory.o_DEF,ETA_AX,sort_type_vars_in_term]) + \\ imp_res_tac candle_sort_type_vars_in_term + \\ simp [equation_def,Abbr`vs`,MAP_MAP_o,combinTheory.o_DEF,ETA_AX]) \\ conj_tac >- (match_mp_tac (List.nth(CONJUNCTS proves_rules,9)) \\ conj_tac >- METIS_TAC[STATE_def,CONTEXT_def,extends_theory_ok,init_theory_ok] \\ simp [Abbr`s2`,conexts_of_upd_def] - \\ simp [sort_type_vars_in_term,equation_def,Abbr`vs`,MAP_MAP_o,combinTheory.o_DEF,ETA_AX]) + \\ fsrw_tac [SFY_ss] [candle_sort_type_vars_in_term] + \\ simp [equation_def,Abbr`vs`,MAP_MAP_o,combinTheory.o_DEF,ETA_AX]) \\ Cases \\ once_rewrite_tac [THM_def] \\ strip_tac diff --git a/candle/overloading/monadic/holKernelScript.sml b/candle/overloading/monadic/holKernelScript.sml index 161ef8bcd4..3caf91a74c 100644 --- a/candle/overloading/monadic/holKernelScript.sml +++ b/candle/overloading/monadic/holKernelScript.sml @@ -1347,7 +1347,7 @@ Definition new_basic_type_definition_def: do (P,x) <- try dest_comb c (strlit "new_basic_type_definition: Not a combination") ; if ~(freesin [] P) then failwith (strlit "new_basic_type_definition: Predicate is not closed") else - let tyvars = MAP Tyvar (MAP implode (sort string_le (MAP explode (type_vars_in_term P)))) in + let tyvars = MAP Tyvar (MAP implode (mergesort string_le (MAP explode (type_vars_in_term P)))) in do rty <- type_of x ; add_type (tyname, LENGTH tyvars) ; aty <- mk_type(tyname,tyvars) ; diff --git a/candle/prover/candle_kernel_permsScript.sml b/candle/prover/candle_kernel_permsScript.sml index 9ba3b2f817..f57d555027 100644 --- a/candle/prover/candle_kernel_permsScript.sml +++ b/candle/prover/candle_kernel_permsScript.sml @@ -133,10 +133,10 @@ Proof \\ rw[] QED -Theorem perms_ok_sort_v[simp]: - perms_ok ps ListProg$sort_v +Theorem perms_ok_mergesort_v[simp]: + perms_ok ps ListProg$mergesort_v Proof - rw[perms_ok_def, ListProgTheory.sort_v_def, astTheory.pat_bindings_def, perms_ok_env_def] + rw[perms_ok_def, ListProgTheory.mergesort_v_def, astTheory.pat_bindings_def, perms_ok_env_def] \\ pop_assum mp_tac \\ eval_nsLookup_tac \\ rw[] QED diff --git a/candle/standard/monadic/holKernelProofScript.sml b/candle/standard/monadic/holKernelProofScript.sml index e398c8d97a..f3de688047 100644 --- a/candle/standard/monadic/holKernelProofScript.sml +++ b/candle/standard/monadic/holKernelProofScript.sml @@ -1685,32 +1685,50 @@ Proof \\ IMP_RES_TAC TERM_Var \\ FULL_SIMP_TAC std_ss [pred_setTheory.IN_UNION] QED -Theorem sort_type_vars_in_term[local]: +Overload candle_sort[local] = ``mllist$mergesort`` + +Theorem string_le_ok[local]: + total string_le /\ antisymmetric string_le /\ transitive string_le +Proof + simp[relationTheory.total_def, relationTheory.transitive_def, + relationTheory.antisymmetric_def, stringTheory.string_le_def] >> + METIS_TAC[stringTheory.string_lt_cases, stringTheory.string_lt_antisym, + stringTheory.string_lt_trans] +QED + +Theorem candle_sort_ok[local]: + SORTED string_le (candle_sort string_le xs) /\ + (PERM (candle_sort string_le xs) ys = PERM xs ys) +Proof + simp [mllistTheory.mergesort_def, mergesortTheory.mergesort_tail_correct, + string_le_ok, mergesortTheory.mergesort_sorted] + \\ metis_tac [mergesortTheory.mergesort_perm, sortingTheory.PERM_TRANS, + sortingTheory.PERM_SYM] +QED + +Theorem LENGTH_candle_sort[local]: + LENGTH (candle_sort string_le xs) = LENGTH xs +Proof + irule sortingTheory.PERM_LENGTH + \\ simp [candle_sort_ok] +QED + +Theorem candle_sort_type_vars_in_term[local]: TERM defs P ==> - (sort $<= (MAP explode (type_vars_in_term P)) = STRING_SORT (MAP explode (tvars P))) + (candle_sort $<= (MAP explode (type_vars_in_term P)) = STRING_SORT (MAP explode (tvars P))) Proof - REPEAT STRIP_TAC \\ - MATCH_MP_TAC (MP_CANON sortingTheory.SORTED_PERM_EQ) \\ - qexists_tac`$<=` >> - conj_asm1_tac >- ( - simp[relationTheory.transitive_def,relationTheory.antisymmetric_def,stringTheory.string_le_def] >> - METIS_TAC[stringTheory.string_lt_antisym,stringTheory.string_lt_trans] ) >> - conj_tac >- ( - MATCH_MP_TAC sort_SORTED >> - simp[relationTheory.total_def,stringTheory.string_le_def] >> - METIS_TAC[stringTheory.string_lt_cases] ) >> - conj_tac >- ( + rw [] + \\ irule sortingTheory.SORTED_PERM_EQ + \\ irule_at Any (hd (BODY_CONJUNCTS candle_sort_ok)) + \\ simp [string_le_ok, candle_sort_ok] + \\ reverse conj_tac >- ( MATCH_MP_TAC sortingTheory.SORTED_weaken >> qexists_tac`$<` >> simp[STRING_SORT_SORTED,stringTheory.string_le_def] ) >> - MATCH_MP_TAC (MP_CANON sortingTheory.PERM_ALL_DISTINCT) >> - conj_tac >- ( - METIS_TAC[sortingTheory.ALL_DISTINCT_PERM - ,sort_PERM - ,ALL_DISTINCT_type_vars_in_term - ,ALL_DISTINCT_MAP_explode] ) >> - simp[ALL_DISTINCT_STRING_SORT] >> - METIS_TAC[MEM_type_vars_in_term,MEM_MAP] + irule sortingTheory.PERM_ALL_DISTINCT + \\ simp [ALL_DISTINCT_MAP_explode, ALL_DISTINCT_type_vars_in_term] + \\ simp [MEM_MAP] + \\ metis_tac [MEM_type_vars_in_term] QED (* ------------------------------------------------------------------------- *) @@ -2673,7 +2691,7 @@ Proof impl_tac >- METIS_TAC[STATE_def,TERM_Comb,THM] >> simp[] >> disch_then kall_tac >> simp[Once st_ex_bind_def] >> - Q.PAT_ABBREV_TAC`vs:string list = sort R X` >> + Q.PAT_ABBREV_TAC`vs:string list = candle_sort R X` >> simp[add_type_def,can_def,otherwise_def,st_ex_return_def] >> ntac 2 (simp[Once st_ex_bind_def]) >> simp[Once st_ex_bind_def,get_the_type_constants_def] >> @@ -2685,6 +2703,7 @@ Proof `get_type_arity tyname s1 = (M_success (LENGTH vs), s1)` by ( simp[get_type_arity_def,st_ex_bind_def,Abbr`s1`] >> simp[Abbr`vs`]>> + simp[LENGTH_candle_sort]>> EVAL_TAC)>> simp[mk_type_def,try_def,otherwise_def,raise_Failure_def,st_ex_return_def,Once st_ex_bind_def] >> @@ -2730,15 +2749,11 @@ Proof imp_res_tac freesin_IMP >> rfs[TERM_def] >> METIS_TAC[]) >> imp_res_tac THM >> rfs[TERM_Comb] >> - imp_res_tac sort_type_vars_in_term >> + imp_res_tac candle_sort_type_vars_in_term >> imp_res_tac THM_term_ok_bool >> fs[term_ok_def] >> rfs[WELLTYPED] >> simp[Abbr`s2`,Abbr`s1`,Abbr`vs`,Abbr`l1`] >> - CONJ_TAC >- ( - qpat_x_assum`_ = STRING_SORT _` (mp_tac o Q.AP_TERM`LENGTH`)>> - qpat_x_assum`_ = STRING_SORT _` (mp_tac o Q.AP_TERM`LENGTH`)>> - simp[LENGTH_QSORT,LENGTH_STRING_SORT,LENGTH_MAP,tvars_ALL_DISTINCT]) >> METIS_TAC[term_type]) >> qmatch_assum_abbrev_tac`Abbrev(l1 = [(absname,absty);(repname,repty)])` >> `mk_const (repname,[]) s2 = (M_success (Const repname repty), s2)` by ( @@ -2914,7 +2929,7 @@ Proof \\ conj_tac >- METIS_TAC[STATE_def,CONTEXT_def,extends_theory_ok,init_theory_ok] \\ simp [Abbr`s2`,conexts_of_upd_def] - \\ imp_res_tac sort_type_vars_in_term + \\ imp_res_tac candle_sort_type_vars_in_term \\ simp [equation_def,Abbr`vs`,MAP_MAP_o,combinTheory.o_DEF,ETA_AX]) \\ conj_tac >- @@ -2922,7 +2937,7 @@ Proof \\ conj_tac >- METIS_TAC[STATE_def,CONTEXT_def,extends_theory_ok,init_theory_ok] \\ simp [Abbr`s2`,conexts_of_upd_def] - \\ imp_res_tac sort_type_vars_in_term + \\ imp_res_tac candle_sort_type_vars_in_term \\ simp [equation_def,Abbr`vs`,MAP_MAP_o,combinTheory.o_DEF,ETA_AX]) \\ Cases \\ once_rewrite_tac [THM_def] diff --git a/candle/standard/monadic/holKernelScript.sml b/candle/standard/monadic/holKernelScript.sml index 747be946a5..c5c77e1554 100644 --- a/candle/standard/monadic/holKernelScript.sml +++ b/candle/standard/monadic/holKernelScript.sml @@ -1226,7 +1226,7 @@ Definition new_basic_type_definition_def: do (P,x) <- try dest_comb c (strlit "new_basic_type_definition: Not a combination") ; if ~(freesin [] P) then failwith (strlit "new_basic_type_definition: Predicate is not closed") else - let tyvars = MAP Tyvar (MAP implode (sort string_le (MAP explode (type_vars_in_term P)))) in + let tyvars = MAP Tyvar (MAP implode (mergesort string_le (MAP explode (type_vars_in_term P)))) in do rty <- type_of x ; add_type (tyname, LENGTH tyvars) ; aty <- mk_type(tyname,tyvars) ; diff --git a/compiler/backend/proofs/word_bignumProofScript.sml b/compiler/backend/proofs/word_bignumProofScript.sml index ad6ff6adb8..ae99ba47e5 100644 --- a/compiler/backend/proofs/word_bignumProofScript.sml +++ b/compiler/backend/proofs/word_bignumProofScript.sml @@ -353,14 +353,15 @@ Proof \\ rw [] QED +Theorem sort_singleton[local] = + sort_PERM |> Q.SPECL [`R`, `[x]`] + |> SIMP_RULE std_ss [sortingTheory.PERM_SING] + Theorem env_to_list_insert_0_LN[local]: env_to_list (insert 0 ret_val LN) p = ([0,ret_val],(\n. p (n+1))) Proof fs [env_to_list_def,toAList_def,Once insert_def,foldi_def] - \\ fs [sort_def, - mergesortTheory.mergesort_tail_def, - Once $ mergesortTheory.mergesortN_tail_def - ] + \\ simp [sort_singleton] \\ fs [list_rearrange_def] \\ rw [] \\ fs [BIJ_DEF,EVAL ``count 1``,INJ_DEF,SURJ_DEF] QED diff --git a/cv_translator/backend_cvScript.sml b/cv_translator/backend_cvScript.sml index 5bb42bc9a8..85cf2f06be 100644 --- a/cv_translator/backend_cvScript.sml +++ b/cv_translator/backend_cvScript.sml @@ -6,7 +6,7 @@ Libs preamble cv_transLib Ancestors mllist mergesort cv_std backend to_data_cv export unify_cv - infer_cv basis_cv + infer_cv basis_cv heap_list_sort val _ = cv_memLib.use_long_names := true; @@ -834,80 +834,23 @@ val _ = word_allocTheory.canonize_moves_aux_def |> cv_trans; val _ = word_allocTheory.heu_max_all_def |> cv_auto_trans; val _ = word_allocTheory.heu_merge_call_def |> cv_trans; -val tm = word_allocTheory.canonize_moves_def +(* A little detour to specialise the sort functions to this order relation. *) +val sort_rel = word_allocTheory.canonize_moves_def |> concl |> find_term (can (match_term “sort _”)) |> rand; Definition sort_canonize_def: sort_canonize ls = - sort ^tm ls + sort ^sort_rel ls End -Definition merge_tail_canonize_def: - merge_tail_canonize b ls accl accr = - merge_tail b ^tm ls accl accr -End - -val merge_tail_eq = merge_tail_def - |> CONJUNCTS |> map SPEC_ALL |> LIST_CONJ - |> Q.GEN ‘R’ |> ISPEC tm |> SRULE [GSYM merge_tail_canonize_def] - |> GEN_ALL |> SRULE [FORALL_PROD] |> SPEC_ALL - -val pre = cv_trans_pre "" merge_tail_eq; - -Theorem merge_tail_canonize_pre[cv_pre]: - ∀negate v0 v acc. merge_tail_canonize_pre negate v0 v acc -Proof - Induct_on`v` \\ rw[] - >- simp[Once pre] - \\ qid_spec_tac`acc` - \\ Induct_on`v0` \\ rw[] - >- simp[Once pre] - \\ simp[Once pre] - \\ rw[] - \\ metis_tac[] -QED - -Definition mergesortN_tail_canonize_def: - mergesortN_tail_canonize b n ls = - mergesortN_tail b ^tm n ls -End - -val mergesortN_tail_eq = mergesortN_tail_def - |> CONJUNCTS |> map SPEC_ALL |> LIST_CONJ - |> Q.GEN ‘R’ |> ISPEC tm |> SRULE [GSYM mergesortN_tail_canonize_def, GSYM merge_tail_canonize_def] - |> GEN_ALL |> SRULE [FORALL_PROD] |> SPEC_ALL; - -Theorem c2b_b2c[local]: - cv$c2b (b2c b) = b -Proof - fs[cvTheory.b2c_if,cvTheory.c2b_def] - \\ rw[] -QED - -val _ = cv_trans DIV2_def; - -val pre = cv_auto_trans_pre_rec "" mergesortN_tail_eq - (WF_REL_TAC ‘measure (cv_size o FST o SND)’ \\ rw [] - \\ rename1`_ < cv_size cvv` - \\ Cases_on`cvv` - \\ simp[GSYM (fetch "-" "cv_arithmetic_DIV2_thm")] - \\ rw[DIV2_def] - \\ cv_termination_tac - \\ fs[c2b_b2c] - \\ intLib.ARITH_TAC); - -Theorem mergesortN_tail_canonize_pre[cv_pre]: - ∀negate n l. mergesortN_tail_canonize_pre negate n l -Proof - completeInduct_on`n`>> - rw[Once pre,DIV2_def]>> - first_x_assum irule>> - intLib.ARITH_TAC -QED +val sort_metric_def = sort_canonize_def + |> REWRITE_RULE [sort_def, heap_list_sort_metric_eq] -val pre = cv_auto_trans (sort_canonize_def |> SRULE [sort_def,mergesort_tail_def,GSYM mergesortN_tail_canonize_def]); +val _ = sort_metric_def |> cv_auto_trans -val res = word_allocTheory.canonize_moves_def |> SRULE[GSYM sort_canonize_def] |> cv_auto_trans +val res = word_allocTheory.canonize_moves_def + |> REWRITE_RULE [GSYM sort_canonize_def] + |> cv_auto_trans val _ = cv_trans backendTheory.set_oracle_def; diff --git a/developers/build-sequence b/developers/build-sequence index 3ed8f687f1..ee1b21d944 100644 --- a/developers/build-sequence +++ b/developers/build-sequence @@ -33,6 +33,7 @@ translator/monadic/monad_base profiler # basis library +basis/monadic basis # compiler diff --git a/translator/monadic/examples/in_array_sorts/README.md b/translator/monadic/examples/in_array_sorts/README.md new file mode 100644 index 0000000000..aba5719085 --- /dev/null +++ b/translator/monadic/examples/in_array_sorts/README.md @@ -0,0 +1,24 @@ +Example applications of the monadic translator on in-array sort functions. + +These sort functions generally have a pure (datatype recursive) instance, a +monadic theory that provides an in-array version and proves that it simulates +the pure computation, and finally a translation theory that translates the +monadic code to CakeML AST. + +[heap_list_sortScript.sml](heap_list_sortScript.sml): +A heap-sort variant that builds a list of exactly-balanced heaps. + +[heap_list_sort_monadicScript.sml](heap_list_sort_monadicScript.sml): +Monadic variants of the heap-list sort functions, and proofs of equivalence. + +[heap_list_sort_translationScript.sml](heap_list_sort_translationScript.sml): +Post-translation of heap_list_sort + +[merge_run_sortScript.sml](merge_run_sortScript.sml): +Verified run-finding (natural) merge sort. + +[merge_run_sort_monadicScript.sml](merge_run_sort_monadicScript.sml): +Monadic variants of the merge-run-sort functions, and proofs of equivalence. + +[merge_run_sort_translationScript.sml](merge_run_sort_translationScript.sml): +Post-translation of merge_run_sort diff --git a/translator/monadic/examples/in_array_sorts/heap_list_sortScript.sml b/translator/monadic/examples/in_array_sorts/heap_list_sortScript.sml new file mode 100644 index 0000000000..4b13332655 --- /dev/null +++ b/translator/monadic/examples/in_array_sorts/heap_list_sortScript.sml @@ -0,0 +1,635 @@ +(* + + A heap-sort variant that builds a list of exactly-balanced heaps. + + This is prototyped and verified as a standard recursive functional program. + + It is also presented as an in-array algorithm, where the list of heaps are + placed in segments of an array. + + This allows the one algorithm to be evaluated either via its pure functional + instance or as an in-place algorithm in CakeML. + + The heap segments all point in the correct direction, so, unlike a standard + in-array heap-sort, sorting a sorted array requires linear-time comparisons + and no data moves. +*) + +Theory heap_list_sort +Ancestors + list rich_list sorting container bag + +Datatype: + simple_tree = Empty_Tree | Node 'a simple_tree simple_tree +End + +Definition tree_top_less_def: + tree_top_less R Empty_Tree y = T /\ + tree_top_less R (Node x _ _) y = R x y +End + +(* Invariant that a tree encodes a heap. *) +Definition heap_tree_inv_def: + (heap_tree_inv R n Empty_Tree = (n = 0)) /\ + (heap_tree_inv R n (Node y l r) = (n > 0 /\ + heap_tree_inv R (n - 1) l /\ tree_top_less R l y /\ + heap_tree_inv R (n - 1) r /\ tree_top_less R r y + )) +End + +Theorem heap_tree_inv_empty_eq_eq[local]: + heap_tree_inv R n t ==> ((t = Empty_Tree) = (n = 0)) +Proof + Cases_on `t` \\ simp [heap_tree_inv_def] +QED + +(* Invariant for a list of trees. *) +Definition heaps_tree_inv_def: + heaps_tree_inv R xs = (EVERY (\(t, n). heap_tree_inv R n t /\ n > 0) xs /\ + SORTED (\(t1, _) (t2, _). case t1 of Empty_Tree => F | Node x _ _ => + (case t2 of Empty_Tree => F | Node y _ _ => R y x)) xs + ) +End + +Theorem heaps_tree_inv_rec_def: + (heaps_tree_inv R [] = T) /\ + (heaps_tree_inv R (x :: xs) = (heap_tree_inv R (SND x) (FST x) /\ SND x > 0 /\ + ((xs <> []) ==> tree_top_less R (FST (HD xs)) (case x of (Node y _ _, _) => y)) /\ + heaps_tree_inv R xs)) +Proof + simp [heaps_tree_inv_def] + \\ Cases_on `x` \\ simp [] + \\ Cases_on `xs` \\ simp [] + \\ rpt (pairarg_tac \\ fs []) + \\ BasicProvers.EVERY_CASE_TAC \\ simp [] + \\ simp [hd (CONJUNCTS heap_tree_inv_def)] + \\ simp [tree_top_less_def] + \\ EQ_TAC \\ rw [] \\ simp [] +QED + +Definition tree_to_bag_def: + tree_to_bag Empty_Tree = {||} /\ + tree_to_bag (Node x l r) = BAG_INSERT x (BAG_UNION (tree_to_bag l) (tree_to_bag r)) +End + +(* Insert a value, replacing the top value of a balanced heap/tree, and moving + the new value down the heap as necessary to maintain the invariant. *) +Definition insert_tree_inv_def: + insert_tree_inv R Empty_Tree x = Empty_Tree /\ + insert_tree_inv R (Node _ l r) x = (case l of Empty_Tree => Node x l r + | Node lx _ _ => (case r of Empty_Tree => Node x l r + | Node rx _ _ => if R lx x /\ R rx x then Node x l r + else if R lx rx then Node rx l (insert_tree_inv R r x) + else Node lx (insert_tree_inv R l x) r + )) +End + +Theorem insert_tree_inv_size: + simple_tree_size (K 0) (insert_tree_inv R t x) = + simple_tree_size (K 0) t +Proof + Induct_on `t` + \\ simp [insert_tree_inv_def] + \\ BasicProvers.EVERY_CASE_TAC \\ simp [] +QED + +(* Insert similarly into a list of heap/trees. *) +Definition insert_trees_inv_def: + (insert_trees_inv R [] x = []) /\ + (insert_trees_inv R (tup :: ts) x = (case tup of (t1, n1) => (case ts of + | [] => [(insert_tree_inv R t1 x, n1)] + | (t2, n2) :: tl_ts => + (case t1 of Empty_Tree => + (* won't happen, leave list the same *) ((t1, n1) :: ts) + | Node _ l r => (case t2 of Empty_Tree => + (* won't happen, leave list the same *) ((t1, n1) :: ts) + | Node t2x _ _ => if ~ (R t2x x) /\ + ~ (case l of Empty_Tree => F | Node lx _ _ => R t2x lx) /\ + ~ (case r of Empty_Tree => F | Node rx _ _ => R t2x rx) + then (Node t2x l r, n1) :: insert_trees_inv R ts x + else (insert_tree_inv R t1 x, n1) :: ts + ))))) +End + +Theorem insert_trees_inv_size: + MAP (simple_tree_size (K 0) o FST) (insert_trees_inv R ts x) = + MAP (simple_tree_size (K 0) o FST) ts +Proof + measureInduct_on `LENGTH ts` + \\ Cases_on `ts` + \\ simp [insert_trees_inv_def] + \\ Cases_on `h` + \\ simp [insert_trees_inv_def] + \\ BasicProvers.EVERY_CASE_TAC \\ simp [] + \\ simp [insert_tree_inv_size] +QED + +Theorem insert_trees_inv_length = + Q.AP_TERM `LENGTH` insert_trees_inv_size |> REWRITE_RULE [LENGTH_MAP] + +(* Add a new value, assembling two heaps into a larger heap if needed. *) +Definition add_to_heaps_step1_def: + add_to_heaps_step1 ts x = (case ts of + (t1, n1) :: (t2, n2) :: ts2 => if n1 = n2 + then (Node x t2 t1, n1 + 1) :: ts2 + else (Node x Empty_Tree Empty_Tree, 1) :: ts + | _ => (Node x Empty_Tree Empty_Tree, 1) :: ts + ) +End + +Definition add_to_heaps_def: + add_to_heaps R ts x = insert_trees_inv R (add_to_heaps_step1 ts x) x +End + +Definition add_values_to_heaps_def: + add_values_to_heaps R ts [] = ts /\ + add_values_to_heaps R ts (x :: xs) = + add_values_to_heaps R (add_to_heaps R ts x) xs +End + +Definition add_heap_to_heaps_def: + add_heap_to_heaps R ts t n = (case t of + Empty_Tree => ts + | Node x l r => (let ord = (case ts of ((Node y _ _, _) :: _) => R y x | _ => T) + in if ord then (t, n) :: ts + else insert_trees_inv R ((t, n) :: ts) x + )) +End + +Theorem add_heap_to_heaps_size: + SUM (MAP (simple_tree_size (K 0) o FST) (add_heap_to_heaps R ts t n)) = + simple_tree_size (K 0) t + SUM (MAP (simple_tree_size (K 0) o FST) ts) +Proof + simp [add_heap_to_heaps_def] + \\ BasicProvers.EVERY_CASE_TAC \\ simp [] + \\ simp [insert_trees_inv_size] +QED + +(* This variant has a "fuel" parameter to make termination obvious, which + later helps with CV-translation of the sort function. *) +Definition heaps_to_list_metric_def: + heaps_to_list_metric R 0n ts acc = acc /\ + heaps_to_list_metric R n_bound orig_ts acc = (case orig_ts of + ((Node x l r, n) :: ts) => + let ts2 = add_heap_to_heaps R ts l (n - 1); + ts3 = add_heap_to_heaps R ts2 r (n - 1) + in heaps_to_list_metric R (n_bound - 1) ts3 (x :: acc) + | _ => acc) +End + +(* This variant doesn't have the fuel parameter. Defining one in terms of the + other seems to be too tricky. *) +Definition heaps_to_list_def: + heaps_to_list R [] acc = acc /\ + heaps_to_list R (tup :: ts) acc = (case tup of + (Node x l r, n) => + let ts2 = add_heap_to_heaps R ts l (n - 1); + ts3 = add_heap_to_heaps R ts2 r (n - 1) + in heaps_to_list R ts3 (x :: acc) + | _ => acc) +Termination + WF_REL_TAC `measure (\(_, ts, _). SUM (MAP (simple_tree_size (K 0) o FST) ts))` + \\ simp [REWRITE_RULE [combinTheory.o_DEF] add_heap_to_heaps_size] +End + +Theorem heaps_to_list_metric_eq: + !n acc. (SUM (MAP (simple_tree_size (K 0) o FST) ts)) <= n ==> + heaps_to_list_metric R n ts acc = heaps_to_list R ts acc +Proof + measureInduct_on `SUM (MAP (simple_tree_size (K 0) o FST) ts)` + \\ simp [] + \\ Cases + \\ rw [] + \\ simp [heaps_to_list_def] + \\ Cases_on `n` + \\ simp [heaps_to_list_metric_def] + \\ Cases_on `FST h` \\ Cases_on `h` \\ fs [] + \\ simp [add_heap_to_heaps_size] +QED + +Definition heap_list_sort_def: + heap_list_sort R xs = heaps_to_list R (add_values_to_heaps R [] xs) [] +End + +(* Equivalence of metric version. *) +Theorem add_values_to_heaps_size: + !xs hps. SUM (MAP (simple_tree_size (K 0) ∘ FST) (add_values_to_heaps R hps xs)) = + SUM (MAP (simple_tree_size (K 0) ∘ FST) hps) + LENGTH xs +Proof + Induct + \\ simp [add_values_to_heaps_def, add_to_heaps_def, + insert_trees_inv_size, add_to_heaps_step1_def] + \\ rw [] + \\ BasicProvers.EVERY_CASE_TAC \\ simp [] +QED + +Theorem heap_list_sort_metric_eq: + heap_list_sort R xs = heaps_to_list_metric R (LENGTH xs) + (add_values_to_heaps R [] xs) [] +Proof + simp [heap_list_sort_def] + \\ irule EQ_SYM + \\ irule heaps_to_list_metric_eq + \\ simp [add_values_to_heaps_size] +QED + +(* Invariant preservation. *) +Theorem insert_tree_inv_less[local]: + (case t of Node _ l r => tree_top_less R l y /\ tree_top_less R r y | _ => T) ==> + R x y ==> + transitive R ==> total R ==> + tree_top_less R (insert_tree_inv R t x) y +Proof + Cases_on `t` \\ simp [insert_tree_inv_def, tree_top_less_def] + \\ BasicProvers.EVERY_CASE_TAC \\ simp [] + \\ simp [tree_top_less_def] +QED + +Theorem total_lemma[local]: + total R ==> ~ R x y ==> R y x +Proof + metis_tac [relationTheory.total_def] +QED + +Theorem transitive_lemma[local] = hd (RES_CANON relationTheory.transitive_def) + +Theorem insert_tree_inv: + heap_tree_inv R n t ==> + transitive R ==> total R ==> + heap_tree_inv R n (insert_tree_inv R t x) +Proof + qid_spec_tac `n` + \\ Induct_on `t` + \\ rw [insert_tree_inv_def] + \\ BasicProvers.EVERY_CASE_TAC \\ simp [] + \\ gs [heap_tree_inv_def, tree_top_less_def] + \\ irule_at Any insert_tree_inv_less + \\ simp [] + \\ metis_tac [total_lemma, transitive_lemma] +QED + +Theorem insert_tree_inv_greater[local]: + R x y \/ (case l of Node ly _ _ => R x ly | _ => F) \/ + (case r of Node ry _ _ => R x ry | _ => F) ==> + transitive R ==> total R ==> + ((l = Empty_Tree) = (r = Empty_Tree)) ==> + R x (case insert_tree_inv R (Node x_old l r) y of + Empty_Tree => Anything | Node z _ _ => z) +Proof + simp [insert_tree_inv_def] + \\ BasicProvers.EVERY_CASE_TAC \\ simp [] + \\ simp [tree_top_less_def] + \\ metis_tac [transitive_lemma, total_lemma] +QED + +Theorem insert_tree_inv_contents: + tree_to_bag (insert_tree_inv R t x) = (case t of Empty_Tree => {||} + | Node _ l r => tree_to_bag (Node x l r)) +Proof + Induct_on `t` + \\ simp [insert_tree_inv_def, tree_to_bag_def] + \\ BasicProvers.EVERY_CASE_TAC \\ simp [] + \\ simp [tree_to_bag_def] + \\ simp [BAG_UNION_INSERT] + \\ simp [BAG_INSERT_commutes] +QED + +Theorem tree_top_less_mono: + tree_top_less R t x ==> R x y ==> + transitive R ==> + tree_top_less R t y +Proof + Cases_on `t` + \\ simp [tree_top_less_def] + \\ metis_tac [transitive_lemma] +QED + +Theorem tree_top_less_neg[local]: + (~ (case t of Empty_Tree => F | Node y _ _ => R x y)) ==> + total R ==> + tree_top_less R t x +Proof + BasicProvers.EVERY_CASE_TAC \\ simp [tree_top_less_def] + \\ metis_tac [total_lemma] +QED + +Theorem heap_tree_inv_mono: + heap_tree_inv R n (Node x l r) ==> + R x y ==> transitive R ==> + heap_tree_inv R n (Node y l r) +Proof + simp [heap_tree_inv_def] + \\ metis_tac [tree_top_less_mono] +QED + +Theorem insert_trees_inv_less[local]: + (case ts of [] => F | (Empty_Tree, _) :: _ => F | ((Node _ l r, _) :: ts2) => + tree_top_less R l y /\ tree_top_less R r y /\ + (ts2 <> [] ==> FST (HD (ts2)) <> Empty_Tree /\ + tree_top_less R (FST (HD ts2)) y)) ==> + R x y ==> + transitive R ==> total R ==> + tree_top_less R (FST (HD (insert_trees_inv R ts x))) y +Proof + BasicProvers.EVERY_CASE_TAC \\ simp [] + \\ simp [insert_trees_inv_def] + \\ BasicProvers.EVERY_CASE_TAC \\ simp [] + \\ rw [] + \\ fs [tree_top_less_def, insert_tree_inv_less] +QED + +Theorem insert_trees_inv: + heaps_tree_inv R ts ==> + transitive R ==> total R ==> + heaps_tree_inv R (insert_trees_inv R ts x) +Proof + Induct_on `ts` + \\ simp [insert_trees_inv_def, pairTheory.FORALL_PROD, heaps_tree_inv_rec_def] + \\ rpt gen_tac + \\ ntac 2 BasicProvers.TOP_CASE_TAC + \\ simp [insert_tree_inv, heaps_tree_inv_rec_def] + \\ ntac 2 BasicProvers.TOP_CASE_TAC + \\ simp [insert_tree_inv, heaps_tree_inv_rec_def] + \\ fs [hd (CONJUNCTS heap_tree_inv_def)] + \\ csimp [] + \\ rw [heaps_tree_inv_rec_def] + \\ simp [insert_tree_inv] + >- ( + fs [heap_tree_inv_def, tree_top_less_def] + \\ rpt (dxrule tree_top_less_neg) + \\ simp [] + ) + >- ( + irule insert_trees_inv_less + \\ fs [heap_tree_inv_def, tree_top_less_def] + \\ fsrw_tac [SFY_ss] [total_lemma] + \\ rpt strip_tac + \\ Cases_on `t` \\ fs [] + \\ fs [heaps_tree_inv_rec_def, heap_tree_inv_def] + ) + >- ( + simp [tree_top_less_def] + \\ irule insert_tree_inv_greater + \\ fs [heap_tree_inv_def] + \\ rpt (dxrule heap_tree_inv_empty_eq_eq) + \\ simp [] + ) +QED + +Theorem insert_trees_inv_contents: + EVERY (\p. FST p <> Empty_Tree) ts ==> + (FOLDR BAG_UNION {||} (MAP (tree_to_bag o FST) (insert_trees_inv R ts x)) = + (case ts of [] => {||} + | (Node _ l r, _) :: ts => BAG_UNION (tree_to_bag (Node x l r)) + (FOLDR BAG_UNION {||} (MAP (tree_to_bag o FST) ts))) + ) +Proof + Induct_on `ts` + \\ simp [pairTheory.FORALL_PROD, insert_trees_inv_def, tree_to_bag_def] + \\ rw [] + \\ BasicProvers.EVERY_CASE_TAC \\ simp [] + \\ fs [heaps_tree_inv_rec_def, heap_tree_inv_def] + \\ gs [] + \\ simp [insert_tree_inv_contents, tree_to_bag_def] + \\ simp [BAG_UNION_INSERT] + \\ simp [BAG_INSERT_commutes] +QED + +Theorem insert_trees_non_empty: + EVERY (\p. FST p <> Empty_Tree) ts ==> + EVERY (\p. FST p <> Empty_Tree) (insert_trees_inv R ts x) +Proof + Induct_on `ts` + \\ simp [pairTheory.FORALL_PROD, insert_trees_inv_def] + \\ rw [] + \\ BasicProvers.EVERY_CASE_TAC \\ simp [] + \\ gs [] + \\ rw [insert_tree_inv_def] +QED + +Theorem add_values_to_heaps_contents: + EVERY (\p. FST p <> Empty_Tree) ts ==> + FOLDR BAG_UNION {||} (MAP (tree_to_bag o FST) (add_values_to_heaps R ts xs)) = + BAG_UNION (LIST_TO_BAG xs) (FOLDR BAG_UNION {||} (MAP (tree_to_bag o FST) ts)) /\ + EVERY (\p. FST p <> Empty_Tree) (add_values_to_heaps R ts xs) +Proof + qid_spec_tac `ts` + \\ Induct_on `xs` + \\ rw [add_values_to_heaps_def] + \\ simp [add_to_heaps_def, add_to_heaps_step1_def] + \\ BasicProvers.EVERY_CASE_TAC \\ simp [] + \\ fs [] + \\ simp [insert_trees_inv_contents, insert_trees_non_empty, tree_to_bag_def] + \\ simp [BAG_UNION_INSERT] + \\ simp [BAG_INSERT_commutes, ASSOC_BAG_UNION, COMM_BAG_UNION] +QED + +Theorem insert_tree_inv_adj[local]: + insert_tree_inv R (Node x_dc l r) x = + insert_tree_inv R (Node y_dc l r) x +Proof + simp [insert_tree_inv_def] +QED + +Theorem insert_tree_adj_inv[local]: + heap_tree_inv R n (insert_tree_inv R (Node x l r) x) + ==> + heap_tree_inv R n (insert_tree_inv R (Node x_dc l r) x) +Proof + simp [insert_tree_inv_def] +QED + +Theorem insert_trees_adj_inv1[local]: + heaps_tree_inv R (insert_trees_inv R ((Node x_dc l r, n) :: ts) x) ==> + heaps_tree_inv R (insert_trees_inv R ((Node y_dc l r, n) :: ts) x) +Proof + simp [insert_trees_inv_def] + \\ BasicProvers.EVERY_CASE_TAC \\ simp [] + \\ simp [insert_tree_inv_def] + \\ csimp [heaps_tree_inv_rec_def, heap_tree_inv_def] +QED + +Theorem insert_trees_adj_inv2[local]: + heaps_tree_inv R ts ==> + heap_tree_inv R n (Node x_dc l r) ==> + transitive R ==> total R ==> reflexive R ==> + heaps_tree_inv R (insert_trees_inv R ((Node x_dc l r, n) :: ts) x) +Proof + Cases_on `heaps_tree_inv R ((Node x_dc l r, n) :: ts)` + \\ simp [insert_trees_inv] + \\ rw [] + \\ irule insert_trees_adj_inv1 + \\ qexists_tac `case HD ts of (Node x _ _, _) => x` + \\ irule insert_trees_inv + \\ fs [heaps_tree_inv_rec_def, heap_tree_inv_def] + \\ Cases_on `FST (HD ts)` \\ Cases_on `HD ts` \\ Cases_on `ts` \\ fs [] + \\ fs [tree_top_less_def] + \\ simp [heaps_tree_inv_rec_def, heap_tree_inv_def, tree_top_less_def] + \\ fs [relationTheory.reflexive_def] + \\ rw [] + \\ drule_then irule tree_top_less_mono + \\ simp [] + \\ metis_tac [total_lemma] +QED + +Theorem insert_trees_adj_inv3[local]: + heaps_tree_inv R ts ==> + heap_tree_inv R (n - 1) l ==> + heap_tree_inv R (n - 1) r ==> + n > 0 ==> + transitive R ==> total R ==> reflexive R ==> + heaps_tree_inv R (insert_trees_inv R ((Node x_dc l r, n) :: ts) x) +Proof + Cases_on `heap_tree_inv R n (Node (case l of Node y _ _ => y) l r) \/ + heap_tree_inv R n (Node (case r of Node y _ _ => y) l r)` + >- ( + rw [] \\ fs [] + \\ irule insert_trees_adj_inv1 + \\ irule_at Any insert_trees_adj_inv2 + \\ simp [] + \\ first_x_assum (irule_at Any) + ) + >- ( + rw [] \\ fs [] + \\ fs [heaps_tree_inv_rec_def, heap_tree_inv_def] + \\ BasicProvers.EVERY_CASE_TAC \\ fs [tree_top_less_def] + \\ gs [relationTheory.reflexive_def] + \\ irule insert_trees_adj_inv1 + \\ irule_at Any insert_trees_adj_inv2 + \\ simp [heap_tree_inv_def, relationTheory.reflexive_def, tree_top_less_def] + \\ metis_tac [total_lemma] + ) +QED + +Theorem add_values_to_heaps_inv: + heaps_tree_inv R ts ==> + transitive R ==> total R ==> reflexive R ==> + heaps_tree_inv R (add_values_to_heaps R ts xs) +Proof + qid_spec_tac `ts` + \\ Induct_on `xs` + \\ rw [add_values_to_heaps_def] + \\ simp [add_to_heaps_def, add_to_heaps_step1_def] + \\ BasicProvers.EVERY_CASE_TAC \\ simp [] + \\ simp [] + \\ first_x_assum irule + \\ simp [] + \\ irule insert_trees_adj_inv3 + \\ fs [heaps_tree_inv_rec_def, heap_tree_inv_def, tree_top_less_def] +QED + +Theorem add_heap_to_heaps_contents[local]: + EVERY (\p. FST p <> Empty_Tree) ts ==> + FOLDR BAG_UNION {||} (MAP (tree_to_bag o FST) (add_heap_to_heaps R ts t n)) = + BAG_UNION (tree_to_bag t) (FOLDR BAG_UNION {||} (MAP (tree_to_bag o FST) ts)) +Proof + simp [add_heap_to_heaps_def] + \\ BasicProvers.EVERY_CASE_TAC \\ simp [] + \\ simp [tree_to_bag_def] + \\ simp [insert_trees_inv_contents, insert_trees_non_empty, tree_to_bag_def] +QED + +Theorem add_heap_to_heaps_not_empty[local]: + EVERY (\p. FST p <> Empty_Tree) ts ==> + EVERY (\p. FST p <> Empty_Tree) (add_heap_to_heaps R ts t n) +Proof + simp [add_heap_to_heaps_def] + \\ BasicProvers.EVERY_CASE_TAC \\ simp [] + \\ simp [insert_trees_non_empty] +QED + +Theorem add_heap_to_heaps_inv[local]: + (t <> Empty_Tree ==> heap_tree_inv R n t) ==> + heaps_tree_inv R ts ==> + total R /\ transitive R /\ reflexive R ==> + heaps_tree_inv R (add_heap_to_heaps R ts t n) +Proof + simp [add_heap_to_heaps_def] + \\ BasicProvers.EVERY_CASE_TAC \\ simp [] + \\ csimp [heaps_tree_inv_rec_def, heap_tree_inv_def, tree_top_less_def] + \\ rw [] + \\ irule insert_trees_adj_inv3 + \\ fs [heaps_tree_inv_rec_def, heap_tree_inv_def] +QED + +Theorem add_heap_to_heaps_less[local]: + (ts <> [] ==> tree_top_less R (FST (HD ts)) x) ==> + tree_top_less R t x ==> + total R ==> transitive R ==> + (add_heap_to_heaps R ts t n <> []) ==> + heaps_tree_inv R ts ==> + heap_tree_inv R n t ==> + tree_top_less R (FST (HD (add_heap_to_heaps R ts t n))) x +Proof + simp [add_heap_to_heaps_def] + \\ BasicProvers.EVERY_CASE_TAC \\ simp [] + \\ rw [] + \\ irule insert_trees_inv_less + \\ fs [tree_top_less_def] + \\ fs [heaps_tree_inv_rec_def, heap_tree_inv_def] + \\ fsrw_tac [SFY_ss] [tree_top_less_mono] + \\ CCONTR_TAC + \\ Cases_on `ts` + \\ gs [heaps_tree_inv_rec_def, heap_tree_inv_def] +QED + +Theorem heaps_to_list_contents: + ! R ts acc. EVERY (\p. FST p <> Empty_Tree) ts ==> + LIST_TO_BAG (heaps_to_list R ts acc) = + BAG_UNION (FOLDR BAG_UNION {||} (MAP (tree_to_bag o FST) ts)) (LIST_TO_BAG acc) +Proof + recInduct heaps_to_list_ind + \\ simp [heaps_to_list_def] + \\ rw [] + \\ BasicProvers.EVERY_CASE_TAC \\ fs [] + \\ simp [add_heap_to_heaps_contents, add_heap_to_heaps_not_empty] + \\ simp [tree_to_bag_def] + \\ simp [BAG_UNION_INSERT] + \\ simp [BAG_INSERT_commutes, ASSOC_BAG_UNION, COMM_BAG_UNION] +QED + +Theorem heaps_to_list_sorted: + ! R ts acc. heaps_tree_inv R ts ==> + transitive R ==> total R ==> reflexive R ==> + SORTED R acc ==> + ((ts <> []) ==> (acc <> []) ==> tree_top_less R (FST (HD ts)) (HD acc)) ==> + SORTED R (heaps_to_list R ts acc) +Proof + recInduct heaps_to_list_ind + \\ simp [heaps_to_list_def] + \\ rw [] + \\ BasicProvers.EVERY_CASE_TAC \\ fs [] + \\ fs [heaps_tree_inv_rec_def, heap_tree_inv_def, tree_top_less_def] + \\ gs [] + \\ first_x_assum irule + \\ simp [add_heap_to_heaps_inv] + \\ rw [] + \\ simp [add_heap_to_heaps_less, add_heap_to_heaps_inv] + \\ Cases_on `acc` + \\ fs [] +QED + +Theorem heap_list_sort_sorted: + reflexive R ==> transitive R ==> total R ==> + SORTED R (heap_list_sort R xs) +Proof + rw [heap_list_sort_def] + \\ irule heaps_to_list_sorted + \\ simp [] + \\ irule add_values_to_heaps_inv + \\ simp [heaps_tree_inv_def] +QED + +Theorem heap_list_sort_contents: + LIST_TO_BAG (heap_list_sort R xs) = LIST_TO_BAG xs +Proof + rw [heap_list_sort_def] + \\ simp [heaps_to_list_contents, add_values_to_heaps_contents] +QED + +Theorem heap_list_sort_PERM: + PERM (heap_list_sort R xs) xs +Proof + simp [GSYM PERM_LIST_TO_BAG, heap_list_sort_contents] +QED + diff --git a/translator/monadic/examples/in_array_sorts/heap_list_sort_monadicScript.sml b/translator/monadic/examples/in_array_sorts/heap_list_sort_monadicScript.sml new file mode 100644 index 0000000000..df33035f9f --- /dev/null +++ b/translator/monadic/examples/in_array_sorts/heap_list_sort_monadicScript.sml @@ -0,0 +1,1150 @@ +(* + Monadic variants of the heap-list sort functions, and proofs of equivalence. +*) + +Theory heap_list_sort_monadic +Ancestors + heap_list_sort ml_monadBase +Libs + preamble ml_monadBaseLib + +(* Part 1: Setup of types and infrastructure. *) + +(* The data type of the state. *) +Datatype: + heap_list_state = <| + heap_array : ( 'a ) list; + sz_array : num list; + |> +End + +(* Equivalent to unit, but we need to construct a type so that the translation + can construct a new exception type. *) +Datatype: + heap_list_subscript_exn = Heap_List_Subscript +End + +(* Setup to use monad translator constants and monad syntax. *) +val acc_fun_defs = define_monad_access_funs ``: 'a heap_list_state`` + +val mr_manip_funs = define_MRarray_manip_funs acc_fun_defs + ``Heap_List_Subscript`` ``Heap_List_Subscript`` + +val _ = ParseExtras.temp_tight_equality (); +val _ = monadsyntax.temp_add_monadsyntax (); + +Overload "monad_bind"[local] = ``st_ex_bind`` +Overload "monad_unitbind"[local] = ``st_ex_ignore_bind`` +Overload "monad_ignore_bind"[local] = ``st_ex_ignore_bind`` +Overload "return"[local] = ``st_ex_return`` + +(* Part 2: Definition of heap-list sort via "suffix encoded" balanced trees. + Every heap/tree is of power-of-two-minus-one size, with the largest element + at the end, and two equal-sized smaller trees before it. *) + +(* Positions of the left child in a suffix encoded balanced tree + of height ht. *) +Definition sfx_heap_left_def: + sfx_heap_left i ht = (i - (2 EXP (ht - 1))) +End + +(* Insert a value into a balanced suffix heap of height ht, replacing the + current top element which is at index i. *) +Definition insert_into_sfx_heap_def: + insert_into_sfx_heap R i ht x = if ht <= 1 + then update_heap_array i x + else do + l <- return (sfx_heap_left i ht); + r <- return (i - 1); + lx <- heap_array_sub l; + rx <- heap_array_sub r; + if R lx x /\ R rx x + then update_heap_array i x + else if R lx rx + then do + update_heap_array i rx; + insert_into_sfx_heap R r (ht - 1) x + od + else do + update_heap_array i lx; + insert_into_sfx_heap R l (ht - 1) x + od + od +End + +(* Insert a value into a sequence of balanced suffix heaps, heights stored + in positions [0 ..< j] of the sz_array. Replace the top elements of the + final heap, which is at index i. *) +Definition insert_into_sfx_heap_list_def: + insert_into_sfx_heap_list R i j x = + if j <= 1 then do + ht <- sz_array_sub (j - 1); + insert_into_sfx_heap R i ht x + od + else do + ht <- sz_array_sub (j - 1); + i2 <- return ((i + 1) - (2 EXP ht)); + t2x <- heap_array_sub i2; + cond1 <- return (~ R t2x x); + cond <- if cond1 /\ (1 < ht) + then do + l <- return (sfx_heap_left i ht); + r <- return (i - 1); + lx <- heap_array_sub l; + rx <- heap_array_sub r; + return (~ R t2x lx /\ ~ R t2x rx) + od + else return cond1; + if cond + then do + update_heap_array i t2x; + insert_into_sfx_heap_list R i2 (j - 1) x + od + else insert_into_sfx_heap R i ht x + od +End + +(* Expand the total size of a sequence of balanced suffix heaps from i to + i + 1 total elements, starting with j total heaps. *) +Definition add_to_sfx_heaps_step1_def: + add_to_sfx_heaps_step1 j = do + merge <- if j <= 1 + then return F + else do + n1 <- sz_array_sub (j - 1); + n2 <- sz_array_sub (j - 2); + return (n1 = n2); + od; + if merge + then do + n <- sz_array_sub (j - 2); + update_sz_array (j - 2) (n + 1); + return (j - 1); + od + else do + update_sz_array j 1; + return (j + 1); + od + od +End + +(* Expand from i to i + 1 elements, set the new element, and preserve the heap + invariants. *) +Definition add_to_sfx_heaps_def: + add_to_sfx_heaps R i j x = do + j' <- add_to_sfx_heaps_step1 j; + insert_into_sfx_heap_list R i j' x; + return j' + od +End + +(* Extend a list of suffix heaps by a list of values. *) +Definition add_all_to_sfx_heaps_def: + (add_all_to_sfx_heaps R i j [] = return (i, j)) /\ + (add_all_to_sfx_heaps R i j (x :: xs) = do + j <- add_to_sfx_heaps R i j x; + add_all_to_sfx_heaps R (i + 1) j xs; + od) +End + +(* Take an intact heap in the correct position and add it to the heap sequence, + i.e. ensure its top element is the overall top element. *) +Definition reinsert_tree_def: + reinsert_tree R i j ht = + do + update_sz_array j ht; + x <- heap_array_sub (i - 1); + upd <- if 0 < j then do + i2 <- return (i - (2 EXP ht)); + t2x <- heap_array_sub i2; + return (~ (R t2x x)) + od else return F; + if upd + then insert_into_sfx_heap_list R (i - 1) (j + 1) x + else return (); + od +End + +(* Reduce a sequence of suffix-encoded heaps to a list. *) +Definition sfx_trees_to_list_def: + sfx_trees_to_list R i j acc = + if i = 0 then return acc + else do + ht <- sz_array_sub (j - 1); + x <- heap_array_sub (i - 1); + if ht <= 1 then sfx_trees_to_list R (i - 1) (j - 1) (x :: acc) + else do + l <- return (sfx_heap_left i ht); + reinsert_tree R l (j - 1) (ht - 1); + reinsert_tree R (i - 1) j (ht - 1); + sfx_trees_to_list R (i - 1) (j + 1) (x :: acc) + od + od +End + +(* Compute an overapproximation of the base-2 logarithm of v *) +Definition above_log2_def: + above_log2 i v n = if n = 0n \/ v <= n + then i + else above_log2 (i + 1n) v (n * 2) +Termination + WF_REL_TAC `measure (\(i, v, n). (v - n))` +End + +(* Top-level sort function for now. This is then given a functional interface + by a "run" wrapper once more monadic translation apparatus is in place. *) +Definition sort_via_sfx_trees_worker_def: + sort_via_sfx_trees_worker R x xs = do + sz <- return (LENGTH xs); + alloc_heap_array (sz + 1) x; + sz_log <- return (above_log2 0 (sz + 1) 1); + alloc_sz_array (sz_log + 5) 0; + (i, j) <- add_all_to_sfx_heaps R 0 0 xs; + sfx_trees_to_list R i j [] + od +End + +(* Part 3. Proof that this monadic encoding computes the same as the pure heap + list sort implementation. *) + +(* 3.1: More setup *) + +Definition bs_tree_to_list_def: + (bs_tree_to_list 0 t = []) /\ + (bs_tree_to_list (SUC ht) t = + bs_tree_to_list ht (case t of Node _ l r => l | _ => t) ++ + bs_tree_to_list ht (case t of Node _ l r => r | _ => t) ++ + [case t of Node x l r => x] + ) +End + +Theorem bs_tree_to_list_tree_rec[local]: + (i = 0 ==> bs_tree_to_list i Empty_Tree = []) /\ + (0 < i ==> bs_tree_to_list i (Node x l r) = + bs_tree_to_list (i - 1) l ++ + bs_tree_to_list (i - 1) r ++ + [x]) +Proof + Cases_on `i` \\ simp [bs_tree_to_list_def] +QED + +Definition two_exp_min_1_def: + two_exp_min_1 i = (2n EXP i) - 1 +End + +Theorem two_exp_min_1_less_rec[local]: + 0 < i ==> two_exp_min_1 i = two_exp_min_1 (i - 1) + two_exp_min_1 (i - 1) + 1 +Proof + Cases_on `i` + \\ fs [two_exp_min_1_def, EXP] + \\ rw [SUB_RIGHT_ADD] +QED + +Theorem two_exp_min_1_rec[local]: + two_exp_min_1 0 = 0 /\ + two_exp_min_1 (SUC i) = two_exp_min_1 i + two_exp_min_1 i + 1 +Proof + simp [two_exp_min_1_less_rec] \\ simp [two_exp_min_1_def] +QED + +Theorem to_two_exp_min_1[local]: + (2n EXP i) = (two_exp_min_1 i + 1) +Proof + rw [two_exp_min_1_def, SUB_RIGHT_ADD] +QED + +Theorem LENGTH_bs_tree_to_list[local]: + ! i t. LENGTH (bs_tree_to_list i t) = two_exp_min_1 i +Proof + Induct + \\ simp [bs_tree_to_list_def, two_exp_min_1_rec] +QED + +Theorem LAST_bs_tree_to_list[local]: + 0 < ht ==> LAST (bs_tree_to_list ht t) = ( + case t of Node x _ _ => x) +Proof + Cases_on `ht` \\ simp [bs_tree_to_list_def, two_exp_min_1_rec] +QED + +Definition tree_balanced_height_def: + (tree_balanced_height i Empty_Tree = (i = 0n)) /\ + (tree_balanced_height i (Node x l r) = ( + (i > 0) /\ tree_balanced_height (i - 1) l /\ + tree_balanced_height (i - 1) r) + ) +End + +Theorem tree_balanced_height_0[local]: + (tree_balanced_height 0 t = (t = Empty_Tree)) +Proof + Cases_on `t` \\ simp [tree_balanced_height_def] +QED + +Theorem tree_balanced_height_eq_0[local]: + ht = 0 ==> (tree_balanced_height ht t = (t = Empty_Tree)) +Proof + Cases_on `t` \\ simp [tree_balanced_height_def] +QED + +Theorem tree_balanced_height_pos[local]: + 0 < ht ==> tree_balanced_height ht t = + (?x l r. t = Node x l r /\ tree_balanced_height (ht - 1) l /\ + tree_balanced_height (ht - 1) r) +Proof + Cases_on `t` \\ simp [tree_balanced_height_def] +QED + +Definition bs_tree_list_to_list_def: + bs_tree_list_to_list ts = + FLAT (MAP (\(t, i). bs_tree_to_list i t) (REVERSE ts)) +End + +Theorem bs_tree_list_to_list_rec[local]: + bs_tree_list_to_list (t_i :: ts) = ( + bs_tree_list_to_list ts ++ bs_tree_to_list (SND t_i) (FST t_i) + ) /\ + bs_tree_list_to_list [] = [] +Proof + simp [bs_tree_list_to_list_def] + \\ rpt (pairarg_tac \\ fs[]) +QED + +Theorem st_ex_ignore_bind_simp[local]: + st_ex_ignore_bind f g = st_ex_bind f (\_. g) +Proof + simp [ml_monadBaseTheory.st_ex_bind_def, ml_monadBaseTheory.st_ex_ignore_bind_def] +QED + +(* +Theorem monad_simps[local] = LIST_CONJ + [fetch "-" "update_heap_array_def", fetch "-" "heap_array_sub_def", + ml_monadBaseTheory.monad_eqs, st_ex_ignore_bind_simp, + fetch "-" "update_sz_array_def", fetch "-" "sz_array_sub_def"] + +Theorem tree_len_simps_no_less[local] = LIST_CONJ + [tree_balanced_height_def, tree_balanced_height_0, + two_exp_min_1_rec, + LENGTH_bs_tree_to_list, bs_tree_to_list_def, + bs_tree_to_list_tree_rec, bs_tree_list_to_list_rec] + +Theorem tree_len_simps[local] = LIST_CONJ [tree_len_simps_no_less, + two_exp_min_1_less_rec] + +Theorem TAKE_DROP_eq_imp[local]: + !xs i j. TAKE i (DROP j xs) = ys ==> + i <= LENGTH ys ==> + ys = [] \/ (?xs_pre xs_post. xs = xs_pre ++ ys ++ xs_post /\ + j = LENGTH xs_pre /\ i = LENGTH ys) +Proof + Cases_on `ys = []` \\ simp [] + \\ rw [] + \\ qexists_tac `TAKE j xs` + \\ qexists_tac `DROP (i + j) xs` + \\ fs [GSYM TAKE_SUM] + \\ fs [LENGTH_TAKE_EQ] +QED + +Theorem TAKE_DROP_last_eq_imp[local]: + TAKE l (DROP ((i + 1) - l) xs) = ys /\ + i + 1 <= LENGTH xs /\ l <= i + 1 /\ + l <= LENGTH ys /\ 0 < l ==> + ?xs_pre xs_post. xs = xs_pre ++ ys ++ xs_post /\ + l = LENGTH ys /\ i = LENGTH xs_pre + (LENGTH ys - 1) +Proof + rpt strip_tac + \\ dxrule TAKE_DROP_eq_imp + \\ Cases_on `ys = []` \\ fs [] + \\ rw [] + \\ irule_at Any EQ_REFL + \\ simp [] +QED +*) + +Theorem two_exp_min_1_pos[local]: + (0 < two_exp_min_1 r) = (0 < r) +Proof + Cases_on `r` \\ simp [two_exp_min_1_rec] +QED + +Theorem MAP_SND_insert_trees_inv[local]: + !ts. MAP SND (insert_trees_inv R ts x) = MAP SND ts +Proof + Induct \\ simp [pairTheory.FORALL_PROD, insert_trees_inv_def] + \\ rw [] + \\ rpt (TOP_CASE_TAC \\ simp []) + \\ simp [] +QED + +Theorem MAP_LENGTH_insert_trees_inv[local]: + MAP (LENGTH o (\(t, n). bs_tree_to_list n t)) + (insert_trees_inv R ts x) = + MAP (LENGTH o (\(t, n). bs_tree_to_list n t)) ts +Proof + qspec_then `ts` (mp_tac o Q.AP_TERM `MAP two_exp_min_1`) MAP_SND_insert_trees_inv + \\ simp [MAP_MAP_o, o_DEF, UNCURRY, bs_tree_list_to_list_rec, LENGTH_bs_tree_to_list] +QED + +Theorem LENGTH_insert_trees_inv[local] = + Q.AP_TERM `LENGTH` (SPEC_ALL MAP_LENGTH_insert_trees_inv) + |> REWRITE_RULE [LENGTH_MAP] + +Theorem LENGTH_list_of_insert_trees[local]: + LENGTH (bs_tree_list_to_list (insert_trees_inv R ts x)) = + LENGTH (bs_tree_list_to_list ts) +Proof + simp [bs_tree_list_to_list_def, LENGTH_FLAT, MAP_MAP_o, MAP_REVERSE] + \\ simp [MAP_LENGTH_insert_trees_inv] +QED + +Theorem tree_to_list_unfold = LIST_CONJ [ + bs_tree_list_to_list_rec, bs_tree_to_list_tree_rec] + +Theorem LENGTH_add_to_heaps_step1_facts[local]: + 0 < LENGTH (add_to_heaps_step1 ts x) /\ + LENGTH (bs_tree_list_to_list (add_to_heaps_step1 ts x)) = + LENGTH (bs_tree_list_to_list ts) + 1 /\ + LENGTH (add_to_heaps_step1 ts x) <= LENGTH ts + 1 /\ + (MAP SND (add_to_heaps_step1 ts x) = MAP SND (add_to_heaps_step1 ts y)) = T /\ + (LENGTH (add_to_heaps_step1 ts x) = LENGTH (add_to_heaps_step1 ts y)) = T +Proof + simp [add_to_heaps_step1_def] + \\ rpt (TOP_CASE_TAC \\ fs [tree_to_list_unfold]) +QED + +Theorem inv_add_tree_step1[local]: + (EVERY (\(t,n). 0 < n /\ tree_balanced_height n t) ts ==> + EVERY (\(t,n). 0 < n /\ tree_balanced_height n t) (add_to_heaps_step1 ts x) + ) /\ + (EVERY (\(t,n). 0 < n /\ tree_balanced_height n t) ts /\ + SORTED ($<=) (TAKE 2 (MAP SND ts)) /\ SORTED ($<) (MAP SND (DROP 1 ts)) ==> + SORTED ($<=) (TAKE 2 (MAP SND (add_to_heaps_step1 ts x))) /\ + SORTED ($<) (MAP SND (DROP 1 (add_to_heaps_step1 ts x))) + ) +Proof + simp [add_to_heaps_step1_def] + \\ rpt (TOP_CASE_TAC \\ fs [tree_balanced_height_def]) + \\ rpt (pairarg_tac \\ fs []) + \\ rw [] + \\ fs [] + \\ imp_res_tac SORTED_TL \\ fs [] + \\ Cases_on `t'` \\ fs [] +QED + +Theorem insert_trees_adj_with_inv[local]: + EVERY (\(t,n). 0 < n /\ tree_balanced_height n t) ts ==> + insert_trees_inv R ((Node x_dc l r, n) :: ts) x = + insert_trees_inv R ((Node y_dc l r, n) :: ts) x +Proof + simp [insert_trees_inv_def] + \\ rpt (TOP_CASE_TAC \\ fs []) \\ rw [] \\ fs [tree_balanced_height_def] + \\ simp [insert_tree_inv_def] +QED + +Theorem insert_trees_adj_step1[local]: + EVERY (\(t,n). 0 < n /\ tree_balanced_height n t) ts ==> + insert_trees_inv R (add_to_heaps_step1 ts x_dc) x = + insert_trees_inv R (add_to_heaps_step1 ts y_dc) x +Proof + simp [add_to_heaps_step1_def] + \\ rpt (TOP_CASE_TAC \\ fs [tree_balanced_height_def]) + \\ rw [] + \\ irule insert_trees_adj_with_inv + \\ simp [] +QED + +Theorem LENGTH_to_list_add_to_heaps[local]: + LENGTH (bs_tree_list_to_list (add_to_heaps R ts x)) = + LENGTH (bs_tree_list_to_list ts) + 1 +Proof + simp [add_to_heaps_def, LENGTH_list_of_insert_trees, + LENGTH_add_to_heaps_step1_facts] +QED + +Theorem insert_tree_inv_balance_inv[local]: + !t ht. tree_balanced_height ht t ==> + tree_balanced_height ht (insert_tree_inv R t x) +Proof + Induct \\ simp [insert_tree_inv_def] + \\ rpt (TOP_CASE_TAC \\ fs [tree_balanced_height_def]) +QED + +Theorem insert_trees_inv_balance_inv[local]: + !ts x. EVERY (\(t,n). 0 < n /\ tree_balanced_height n t) ts ==> + EVERY (\(t,n). 0 < n /\ tree_balanced_height n t) (insert_trees_inv R ts x) +Proof + Induct \\ simp [pairTheory.FORALL_PROD, insert_trees_inv_def] + \\ rw [] + \\ rpt (TOP_CASE_TAC \\ fs [tree_balanced_height_def, insert_tree_inv_balance_inv]) +QED + +Theorem inv_add_to_heaps[local]: + (EVERY (\(t,n). 0 < n /\ tree_balanced_height n t) ts ==> + EVERY (\(t,n). 0 < n /\ tree_balanced_height n t) (add_to_heaps R ts x) + ) /\ + (EVERY (\(t,n). 0 < n /\ tree_balanced_height n t) ts /\ + SORTED ($<=) (TAKE 2 (MAP SND ts)) /\ SORTED ($<) (MAP SND (DROP 1 ts)) ==> + SORTED ($<=) (TAKE 2 (MAP SND (add_to_heaps R ts x))) /\ + SORTED ($<) (MAP SND (DROP 1 (add_to_heaps R ts x))) + ) +Proof + simp [add_to_heaps_def, MAP_SND_insert_trees_inv, MAP_DROP] + \\ simp [GSYM MAP_DROP, inv_add_tree_step1, insert_trees_inv_balance_inv] +QED + +Theorem sum_lengths_greater_equal_exp[local]: + ! ts n. EVERY (\(t,n). 0 < n /\ tree_balanced_height n t) ts /\ + SORTED $< (MAP SND ts) /\ + ts <> [] /\ n <= SND (HD ts) /\ 1 <= n ==> + ((2 EXP (LENGTH ts + (n - 1))) - 1) <= LENGTH (bs_tree_list_to_list ts) +Proof + Induct \\ rw [] + \\ fs [tree_to_list_unfold, LENGTH_bs_tree_to_list] + \\ pairarg_tac \\ fs [] + \\ first_x_assum (qspec_then `SUC n` mp_tac) + \\ imp_res_tac SORTED_TL + \\ simp [EXP] + \\ Cases_on `ts` \\ fs [] + >- ( + simp [tree_to_list_unfold] + \\ simp [two_exp_min_1_def, LEFT_SUB_DISTRIB] + \\ simp [GSYM EXP, ADD1] + \\ rw [SUB_RIGHT_ADD] + ) + >- ( + rw [] + \\ gs [ADD1] + ) +QED + +Theorem inv_trees_less_via_exp[local]: + EVERY (\(t,n). 0 < n /\ tree_balanced_height n t) ts /\ + SORTED $< (DROP 1 (MAP SND ts)) /\ + LENGTH (bs_tree_list_to_list ts) < 2 ** lg /\ + lg + i + 2 <= bd ==> + LENGTH ts + i < bd +Proof + rw [] + \\ fs [GSYM MAP_DROP] + \\ drule_at (Pat `SORTED _ _`) sum_lengths_greater_equal_exp + \\ simp [EVERY_DROP] + \\ disch_then (qspec_then `1` mp_tac) + \\ Cases_on `LENGTH ts <= 1` \\ fs [] + \\ impl_tac + >- ( + fs [HD_DROP, EVERY_EL, UNCURRY] + \\ first_x_assum (qspec_then `1` mp_tac) + \\ simp [] + ) + \\ disch_tac + \\ subgoal `2n ** (LENGTH ts - 1) < 2 ** lg` + >- ( + drule_then irule LESS_EQ_LESS_TRANS + \\ Cases_on `ts` \\ fs [tree_to_list_unfold] + \\ pairarg_tac \\ fs [] + \\ gs [tree_balanced_height_pos, tree_to_list_unfold] + ) + \\ fs [] +QED + +Theorem LENGTH_add_heap_to_heaps_facts[local]: + tree_balanced_height ht t /\ 0 < ht ==> + LENGTH (add_heap_to_heaps R ts t ht) = LENGTH ts + 1 + /\ + MAP SND (add_heap_to_heaps R ts t ht) = ht :: MAP SND ts + /\ + LENGTH (bs_tree_list_to_list (add_heap_to_heaps R ts t ht)) = + LENGTH (bs_tree_list_to_list ts) + LENGTH (bs_tree_to_list ht t) /\ + (EVERY (\(t, n). 0 < n /\ tree_balanced_height n t) ts ==> + EVERY (\(t, n). 0 < n /\ tree_balanced_height n t) (add_heap_to_heaps R ts t ht) + ) +Proof + rw [add_heap_to_heaps_def] + \\ fs [tree_to_list_unfold, tree_balanced_height_pos] + \\ BasicProvers.EVERY_CASE_TAC \\ fs [] + \\ simp [LENGTH_insert_trees_inv, MAP_SND_insert_trees_inv, + LENGTH_list_of_insert_trees, tree_to_list_unfold, tree_balanced_height_def, + insert_trees_inv_balance_inv] +QED + +Theorem above_log2_is_above_ind[local]: + ! i v n. n = 2 EXP i ==> v <= 2 ** (above_log2 i v n) +Proof + recInduct above_log2_ind + \\ rw [] \\ fs [] + \\ ONCE_REWRITE_TAC [above_log2_def] + \\ rw [] \\ fs [EXP_ADD] +QED + +Theorem add_values_to_heaps_facts[local]: + !xs ts. + EVERY (\(t, n). 0 < n /\ tree_balanced_height n t) ts ==> + LENGTH (bs_tree_list_to_list (add_values_to_heaps R ts xs)) = + LENGTH (bs_tree_list_to_list ts) + LENGTH xs /\ + EVERY (\(t, n). 0 < n /\ tree_balanced_height n t) (add_values_to_heaps R ts xs) /\ + (SORTED $< (MAP SND (DROP 1 ts)) /\ SORTED $<= (TAKE 2 (MAP SND ts)) ==> + SORTED $< (MAP SND (DROP 1 (add_values_to_heaps R ts xs))) /\ + SORTED $<= (TAKE 2 (MAP SND (add_values_to_heaps R ts xs)))) +Proof + Induct \\ simp [tree_to_list_unfold, add_values_to_heaps_def] + \\ rw [] + \\ simp [inv_add_to_heaps, LENGTH_to_list_add_to_heaps] + \\ fs [IMP_CONJ_THM, FORALL_AND_THM] +QED + +(* 3.2: State/Heap-list equivalence setup. *) + +Definition mk_st_def: + mk_st hps szs = + (<| + sz_array := REVERSE (FST szs) ++ SND szs; + heap_array := bs_tree_list_to_list (FST hps) ++ SND hps + |>) +End + +Definition is_last_ix_def: + is_last_ix szs i = (SUM (MAP two_exp_min_1 szs) = i + 1) +End + +Theorem is_last_ix_eq_min_1: + is_last_ix szs i ==> i = SUM (MAP two_exp_min_1 szs) - 1 +Proof + simp [is_last_ix_def] +QED + +Theorem bind_success_eqI: + m st = (M_success v, st2) /\ f v st2 = rhs ==> + st_ex_bind m f st = rhs +Proof + simp [ml_monadBaseTheory.st_ex_bind_def] +QED + +Theorem bind_success_rdonly_eqI = + Q.INST [`st2` |-> `st`] bind_success_eqI + +Theorem mk_st_node_split_r: + 0 < ht ==> + mk_st ((Node x l r, ht) :: hps, oths) szs = + mk_st ((r, ht - 1) :: (l, ht - 1) :: hps, x :: oths) szs +Proof + simp [mk_st_def, tree_to_list_unfold] +QED + +Theorem mk_st_node_split_l: + 0 < ht ==> + mk_st ((Node x l r, ht) :: hps, oths) szs = + mk_st ((l, ht - 1) :: hps, bs_tree_to_list (ht - 1) r ++ x :: oths) szs +Proof + simp [mk_st_def, tree_to_list_unfold] +QED + +Theorem mk_st_move_others: + mk_st ((t, ht) :: hps, oths) szs_pair = + mk_st (hps, bs_tree_to_list ht t ++ oths) szs_pair /\ + mk_st hps_pair (n :: szs, sz_oths) = + mk_st hps_pair (szs, n :: sz_oths) +Proof + simp [mk_st_def, tree_to_list_unfold] +QED + +Theorem LENGTH_bs_tree_list_to_list_eq_SUM[local]: + LENGTH (bs_tree_list_to_list ts) = SUM (MAP two_exp_min_1 (MAP SND ts)) +Proof + simp [bs_tree_list_to_list_def, LENGTH_FLAT, MAP_MAP_o, o_DEF] + \\ simp [UNCURRY, LENGTH_bs_tree_to_list, MAP_REVERSE, SUM_REVERSE] +QED + +Theorem heap_array_sub_curr_bind_eq: + is_last_ix (ht :: MAP SND hps) i /\ 0 < ht ==> + st_ex_bind (heap_array_sub i) f + (mk_st ((Node x l r, ht) :: hps, oths) szs) = + f x (mk_st ((Node x l r, ht) :: hps, oths) szs) +Proof + rw [] + \\ irule bind_success_eqI + \\ simp [fetch "-" "heap_array_sub_def", ml_monadBaseTheory.monad_eqs] + \\ simp [mk_st_def, tree_to_list_unfold, LENGTH_bs_tree_to_list] + \\ fs [is_last_ix_def, LENGTH_bs_tree_list_to_list_eq_SUM, two_exp_min_1_less_rec, + EL_APPEND1, EL_APPEND2, LENGTH_bs_tree_to_list, EL_CONS_IF] +QED + +Theorem is_last_ix_imps: + is_last_ix (ht :: hts) i ==> + (1 < ht ==> is_last_ix (ht - 1 :: hts) (sfx_heap_left i ht)) /\ + (1 < ht ==> is_last_ix (ht - 1 :: ht - 1 :: hts) (i - 1)) /\ + (0 < LENGTH hts /\ 0 < HD hts ==> is_last_ix hts (i - two_exp_min_1 ht)) +Proof + fs [is_last_ix_def] + \\ rw [] + \\ fs [sfx_heap_left_def, to_two_exp_min_1, two_exp_min_1_less_rec] + \\ Cases_on `hts` \\ fs [] + \\ fs [sfx_heap_left_def, to_two_exp_min_1, two_exp_min_1_less_rec] +QED + +Theorem heap_array_sub_left_bind_eq: + is_last_ix (ht :: MAP SND hps) i /\ 1 < ht ==> + st_ex_bind (heap_array_sub (sfx_heap_left i ht)) f + (mk_st ((Node x (Node lx ll lr) r, ht) :: hps, oths) szs) = + f lx (mk_st ((Node x (Node lx ll lr) r, ht) :: hps, oths) szs) +Proof + rw [] + \\ imp_res_tac is_last_ix_imps + \\ fs [] + \\ simp [Once mk_st_node_split_l] + \\ simp [heap_array_sub_curr_bind_eq] + \\ simp [mk_st_node_split_l] +QED + +Theorem heap_array_sub_right_bind_eq: + is_last_ix (ht :: MAP SND hps) i /\ 1 < ht ==> + st_ex_bind (heap_array_sub (i - 1)) f + (mk_st ((Node x l (Node rx rl rr), ht) :: hps, oths) szs) = + f rx (mk_st ((Node x l (Node rx rl rr), ht) :: hps, oths) szs) +Proof + rw [] + \\ imp_res_tac is_last_ix_imps + \\ fs [] + \\ simp [Once mk_st_node_split_r] + \\ simp [heap_array_sub_curr_bind_eq] + \\ simp [mk_st_node_split_r] +QED + +Theorem heap_array_sub_prev_bind_eq: + is_last_ix (ht :: MAP SND hps) i /\ 0 < LENGTH hps /\ + EVERY (\(t, n). 0 < n /\ tree_balanced_height n t) hps ==> + st_ex_bind (heap_array_sub (i - two_exp_min_1 ht)) f + (mk_st ((t, ht) :: hps, oths) szs) = + f (case hps of (Node x _ _, _) :: _ => x) (mk_st ((t, ht) :: hps, oths) szs) +Proof + rw [] + \\ imp_res_tac is_last_ix_imps + \\ fs [] + \\ simp [mk_st_move_others] + \\ Cases_on `HD hps` \\ Cases_on `hps` \\ fs [] + \\ gs [tree_balanced_height_pos] + \\ simp [heap_array_sub_curr_bind_eq] +QED + +Theorem update_heap_array_mk_st_eq: + is_last_ix (ht :: MAP SND hps) i /\ 0 < ht ==> + update_heap_array i x (mk_st ((Node x_dc l r, ht) :: hps, oths) szs) = + (M_success (), mk_st ((Node x l r, ht) :: hps, oths) szs) +Proof + simp [fetch "-" "update_heap_array_def", ml_monadBaseTheory.monad_eqs] + \\ rw [is_last_ix_def, mk_st_def] + \\ fs [tree_to_list_unfold, LENGTH_bs_tree_to_list, + LENGTH_bs_tree_list_to_list_eq_SUM, LUPDATE_APPEND, + two_exp_min_1_less_rec, LUPDATE_DEF] +QED + +Theorem return_bind_eq: + st_ex_bind (return v) f = f v +Proof + simp [ml_monadBaseTheory.st_ex_bind_def, ml_monadBaseTheory.st_ex_return_def, FUN_EQ_THM] +QED + +Theorem sz_array_sub_bind_eq: + i < LENGTH szs ==> + st_ex_bind (sz_array_sub i) f (mk_st hps (szs, oths)) = + f (EL (LENGTH szs - (i + 1)) szs) (mk_st hps (szs, oths)) +Proof + rw [] + \\ irule bind_success_eqI + \\ simp [fetch "-" "sz_array_sub_def", ml_monadBaseTheory.monad_eqs] + \\ simp [mk_st_def, EL_APPEND1, EL_REVERSE, PRE_SUB1] +QED + +Theorem update_sz_array_eq: + i < LENGTH szs ==> + update_sz_array i x (mk_st hps (szs, oths)) = + (M_success (), mk_st hps (LUPDATE x (LENGTH szs - (i + 1)) szs, oths)) +Proof + rw [] + \\ simp [fetch "-" "update_sz_array_def", ml_monadBaseTheory.monad_eqs] + \\ simp [mk_st_def] + \\ qspecl_then [`REVERSE szs`, `i`] mp_tac LESS_LENGTH + \\ simp [listTheory.SWAP_REVERSE_SYM] + \\ rw [] + \\ simp [LUPDATE_APPEND1, LUPDATE_APPEND2, LUPDATE_DEF] +QED + +(* 3.3: Proofs of equivalence *) + +Theorem insert_into_sfx_heap_eq: + ! ht hps oths t R i x st. + is_last_ix (ht :: MAP SND hps) i /\ ht > 0 /\ + tree_balanced_height ht t ==> + insert_into_sfx_heap R i ht x (mk_st ((t, ht) :: hps, oths) szs) = + (M_success (), (mk_st ((insert_tree_inv R t x, ht) :: hps, oths) szs)) +Proof + Induct + \\ simp [ADD1] + \\ ONCE_REWRITE_TAC [insert_into_sfx_heap_def] + \\ simp [tree_balanced_height_pos] + \\ rw [] + >- ( + Cases_on `ht` \\ fs [tree_balanced_height_0] + \\ simp [insert_tree_inv_def, update_heap_array_mk_st_eq] + ) + >- ( + simp [return_bind_eq] + \\ gs [tree_balanced_height_pos] + \\ ONCE_REWRITE_TAC [insert_tree_inv_def] + \\ drule_then assume_tac is_last_ix_imps + \\ gs [] + \\ simp [heap_array_sub_left_bind_eq, heap_array_sub_right_bind_eq] + \\ rpt TOP_CASE_TAC + \\ simp [update_heap_array_mk_st_eq, st_ex_ignore_bind_simp] + >- ( + simp [st_ex_ignore_bind_simp] + \\ irule bind_success_eqI + \\ simp [update_heap_array_mk_st_eq] + \\ simp [Once mk_st_node_split_r] + \\ simp [mk_st_node_split_r] + ) + >- ( + simp [st_ex_ignore_bind_simp] + \\ irule bind_success_eqI + \\ simp [update_heap_array_mk_st_eq] + \\ simp [Once mk_st_node_split_l] + \\ simp [mk_st_node_split_l] + ) + ) +QED + +Theorem insert_into_sfx_heap_list_eq: + ! j ts R i x oths szs. + j = LENGTH ts /\ + is_last_ix (MAP SND ts) i /\ + 0 < j /\ EVERY (\(t, n). 0 < n /\ tree_balanced_height n t) ts ==> + insert_into_sfx_heap_list R i j x (mk_st (ts, oths) (MAP SND ts, szs)) = + (M_success (), mk_st (insert_trees_inv R ts x, oths) (MAP SND ts, szs)) +Proof + Induct + \\ simp [] + \\ ONCE_REWRITE_TAC [insert_into_sfx_heap_list_def] + \\ rpt strip_tac + \\ Cases_on `HD ts` \\ Cases_on `ts` \\ fs [] + \\ gs [ADD1, TAKE_SUM] + \\ simp [insert_trees_inv_def] + \\ rw [] + >- ( + Cases_on `t` \\ fs [] + \\ simp [sz_array_sub_bind_eq, return_bind_eq] + \\ simp [insert_into_sfx_heap_eq] + ) + \\ simp [sz_array_sub_bind_eq, return_bind_eq] + \\ simp [ADD1] + \\ simp [to_two_exp_min_1, heap_array_sub_prev_bind_eq] + \\ irule bind_success_rdonly_eqI + \\ qexists_tac `case t of ((Node t2x _ _, _) :: _) => + ~ R t2x x /\ ~ (case q of Node _ (Node lx _ _) _ => R t2x lx | _ => F) /\ + ~ (case q of Node _ _ (Node rx _ _) => R t2x rx | _ => F) | _ => F` + \\ conj_tac + >- ( + Cases_on `HD t` \\ Cases_on `t` \\ fs [] + \\ rw [] + >- ( + gs [tree_balanced_height_pos] + \\ simp [heap_array_sub_left_bind_eq, heap_array_sub_right_bind_eq] + \\ simp [ml_monadBaseTheory.monad_eqs] + ) + >- ( + simp [ml_monadBaseTheory.monad_eqs] + \\ gs [tree_balanced_height_pos, tree_balanced_height_eq_0] + ) + ) + \\ simp [] + \\ TOP_CASE_TAC + >- ( + gs [tree_balanced_height_pos] + \\ simp [st_ex_ignore_bind_simp] + \\ irule bind_success_eqI + \\ simp [update_heap_array_mk_st_eq] + \\ simp [mk_st_move_others] + \\ drule_then assume_tac is_last_ix_imps + \\ gs [] + \\ Cases_on `HD t` \\ Cases_on `t` \\ fs [] + \\ gs [tree_balanced_height_pos] + \\ simp [insert_trees_inv_def, mk_st_move_others] + ) + >- ( + simp [insert_into_sfx_heap_eq] + \\ Cases_on `HD t` \\ Cases_on `t` \\ fs [] + \\ gs [tree_balanced_height_pos] + ) +QED + +Theorem add_to_sfx_heaps_step1_eq: + j = LENGTH ts /\ + EVERY (\(t, n). 0 < n /\ tree_balanced_height n t) ts /\ + 0 < LENGTH oth_szs ==> + ? oth_szs2. + let ts2 = add_to_heaps_step1 ts x in + add_to_sfx_heaps_step1 j (mk_st (ts, x :: oths) (MAP SND ts, oth_szs)) = + (M_success (LENGTH ts2), mk_st (ts2, oths) (MAP SND ts2, oth_szs2)) /\ + LENGTH ts2 + LENGTH oth_szs2 = LENGTH ts + LENGTH oth_szs +Proof + rw [] + \\ simp [add_to_sfx_heaps_step1_def, add_to_heaps_step1_def] + \\ irule_at Any bind_success_rdonly_eqI + \\ qexists_tac `case ts of (_, n1) :: (_, n2) :: _ => n1 = n2 | _ => F` + \\ simp [GSYM PULL_EXISTS] + \\ conj_tac + >- ( + every_case_tac \\ fs [] + \\ simp [sz_array_sub_bind_eq, ADD1] + \\ simp [ml_monadBaseTheory.monad_eqs] + ) + \\ TOP_CASE_TAC + >- ( + every_case_tac \\ fs [] + \\ simp [sz_array_sub_bind_eq, ADD1, st_ex_ignore_bind_simp] + \\ irule_at Any bind_success_eqI + \\ simp [update_sz_array_eq, ml_monadBaseTheory.monad_eqs] + \\ simp [ADD1, LUPDATE_DEF] + \\ simp [mk_st_node_split_r, mk_st_move_others] + \\ irule_at Any EQ_REFL + \\ simp [] + ) + >- ( + simp [st_ex_ignore_bind_simp] + \\ irule_at Any bind_success_eqI + \\ Cases_on `oth_szs` \\ fs [] + \\ simp [GSYM mk_st_move_others] + \\ simp [update_sz_array_eq, ml_monadBaseTheory.monad_eqs] + \\ simp [ADD1, LUPDATE_DEF] + \\ every_case_tac \\ fs [] + \\ simp [mk_st_move_others, bs_tree_to_list_tree_rec] + \\ REWRITE_TAC [GSYM APPEND_ASSOC, APPEND] + \\ irule_at Any EQ_REFL + \\ simp [] + ) +QED + +Theorem add_to_sfx_heaps_eq: + j = LENGTH ts /\ i = LENGTH (bs_tree_list_to_list ts) /\ + EVERY (\(t, n). 0 < n /\ tree_balanced_height n t) ts /\ + 0 < LENGTH oth_szs /\ 0 < LENGTH oths ==> + let ts2 = add_to_heaps R ts x in + ? oth_szs2. + add_to_sfx_heaps R i j x (mk_st (ts, oths) (MAP SND ts, oth_szs)) = + (M_success (LENGTH ts2), mk_st (ts2, TL oths) (MAP SND ts2, oth_szs2)) /\ + LENGTH ts2 + LENGTH oth_szs2 = LENGTH ts + LENGTH oth_szs +Proof + rpt strip_tac + \\ qspecl_then [`HD oths`, `TL oths`] mp_tac (Q.GENL [`x`, `oths`] add_to_sfx_heaps_step1_eq) + \\ Cases_on `oths` \\ fs [] + \\ rw [] + \\ simp [add_to_sfx_heaps_def, add_to_heaps_def] + \\ irule_at Any bind_success_eqI + \\ simp [st_ex_ignore_bind_simp] + \\ irule_at Any bind_success_eqI + \\ simp [ml_monadBaseTheory.monad_eqs, LENGTH_insert_trees_inv] + \\ dep_rewrite.DEP_REWRITE_TAC [insert_into_sfx_heap_list_eq] + \\ simp [LENGTH_add_to_heaps_step1_facts, inv_add_tree_step1, is_last_ix_def, + GSYM LENGTH_bs_tree_list_to_list_eq_SUM] + \\ simp [MAP_SND_insert_trees_inv] + \\ irule_at Any (Q.prove (`a = b /\ c = d ==> mk_st a c = mk_st b d`, simp [])) + \\ simp [] + \\ metis_tac [insert_trees_adj_step1, LENGTH_add_to_heaps_step1_facts] +QED + +Theorem add_all_to_sfx_heaps_eq: + !xs i j ts oths oth_szs. + j = LENGTH ts /\ i = LENGTH (bs_tree_list_to_list ts) /\ + EVERY (\(t, n). 0 < n /\ tree_balanced_height n t) ts /\ + SORTED ($<=) (TAKE 2 (MAP SND ts)) /\ SORTED ($<) (MAP SND (DROP 1 ts)) /\ + lg + 3 <= LENGTH ts + LENGTH oth_szs /\ + i + LENGTH xs < 2 EXP lg ==> + LENGTH xs <= LENGTH oths ==> + let ts2 = add_values_to_heaps R ts xs in + ? oth_szs2. + add_all_to_sfx_heaps R i j xs (mk_st (ts, oths) (MAP SND ts, oth_szs)) = + (M_success (LENGTH (bs_tree_list_to_list ts2), LENGTH ts2), + mk_st (ts2, DROP (LENGTH xs) oths) (MAP SND ts2, oth_szs2)) /\ + LENGTH ts2 + LENGTH oth_szs2 = LENGTH ts + LENGTH oth_szs +Proof + Induct + \\ simp [add_all_to_sfx_heaps_def, add_values_to_heaps_def] + >- ( + simp [ml_monadBaseTheory.monad_eqs] + \\ metis_tac [] + ) + \\ rpt strip_tac + \\ irule_at Any bind_success_eqI + \\ qmatch_goalsub_abbrev_tac `add_to_sfx_heaps R i j x` + \\ mp_tac add_to_sfx_heaps_eq + \\ fs [markerTheory.Abbrev_def] + \\ impl_keep_tac + >- ( + (* exponential argument that there is space in szs array *) + drule inv_trees_less_via_exp + \\ disch_then (qspecl_then [`lg`, `1`] mp_tac) + \\ simp [GSYM MAP_DROP] + \\ disch_then dxrule + \\ simp [] + ) + \\ rw [] \\ simp [] + \\ qmatch_goalsub_abbrev_tac `mk_st (ts2, _)` + \\ first_x_assum (qspecl_then [`ts2`, `TL oths`, `oth_szs2`] mp_tac) + \\ fs [markerTheory.Abbrev_def] + \\ simp [LENGTH_to_list_add_to_heaps, inv_add_to_heaps] + \\ rw [] \\ simp [] + \\ Cases_on `oths` \\ fs [] + \\ irule_at Any EQ_REFL + \\ simp [] +QED + +Theorem reinsert_tree_eq: + j = LENGTH ts /\ i = LENGTH (bs_tree_list_to_list ((t, ht) :: ts)) /\ + EVERY (\(t, n). 0 < n /\ tree_balanced_height n t) ts /\ + SORTED ($<=) (TAKE 2 (MAP SND ts)) /\ SORTED ($<) (MAP SND (DROP 1 ts)) /\ + 0 < ht /\ tree_balanced_height ht t ==> + reinsert_tree R i j ht (mk_st ((t, ht) :: ts, oths) (dc :: MAP SND ts, oth_szs)) = + (let ts2 = add_heap_to_heaps R ts t ht in + (M_success (), mk_st (ts2, oths) (MAP SND ts2, oth_szs))) +Proof + simp [reinsert_tree_def, add_heap_to_heaps_def] + \\ rw [] + \\ gs [tree_balanced_height_pos] + \\ qmatch_goalsub_abbrev_tac `mk_st (COND tree_cond _ _, _)` + \\ simp [st_ex_ignore_bind_simp] + \\ irule_at Any bind_success_eqI + \\ simp [update_sz_array_eq] + \\ dep_rewrite.DEP_REWRITE_TAC [heap_array_sub_curr_bind_eq] + \\ conj_asm1_tac + >- ( + fs [markerTheory.Abbrev_def] + \\ simp [is_last_ix_def, LENGTH_bs_tree_list_to_list_eq_SUM] + \\ fs [two_exp_min_1_less_rec] + ) + \\ irule_at Any bind_success_rdonly_eqI + \\ qexists_tac `~ tree_cond` + \\ conj_tac + >- ( + rw [] + \\ simp [return_bind_eq, to_two_exp_min_1] + \\ simp [heap_array_sub_prev_bind_eq |> Q.GEN `i` |> Q.SPEC `i - 1` + |> SIMP_RULE (srw_ss ()) [GSYM SUB_PLUS, ADD_COMM]] + \\ simp [ml_monadBaseTheory.monad_eqs] + \\ every_case_tac \\ fs [markerTheory.Abbrev_def] + \\ gs [tree_balanced_height_pos] + ) + \\ rw [] + >- ( + simp [ADD1, LUPDATE_DEF] + \\ qmatch_goalsub_abbrev_tac `mk_st (tt :: ts, _)` + \\ qspecl_then [`j`, `tt :: ts`] (mp_tac o Q.GEN `j`) insert_into_sfx_heap_list_eq + \\ fs [markerTheory.Abbrev_def, tree_balanced_height_def, ADD1] + \\ simp [MAP_SND_insert_trees_inv] + ) + \\ simp [ml_monadBaseTheory.monad_eqs] + \\ simp [ADD1, LUPDATE_DEF] +QED + +Theorem sfx_trees_to_list_eq: + !i j acc ts oths oth_szs. + EVERY (\(t, n). 0 < n /\ tree_balanced_height n t) ts /\ + SORTED ($<=) (TAKE 2 (MAP SND ts)) /\ SORTED ($<) (MAP SND (DROP 1 ts)) /\ + LENGTH ts = j /\ LENGTH (bs_tree_list_to_list ts) = i /\ + lg + 4 <= LENGTH ts + LENGTH oth_szs /\ + i < 2 EXP lg ==> + ?st'. sfx_trees_to_list R i j acc (mk_st (ts, oths) (MAP SND ts, oth_szs)) = + (M_success (heaps_to_list R ts acc), st') +Proof + Induct + \\ REWRITE_TAC [] + \\ ONCE_REWRITE_TAC [sfx_trees_to_list_def] + >- ( + rw [] + \\ Cases_on `ts` \\ fs [] + \\ simp [ml_monadBaseTheory.monad_eqs, heaps_to_list_def] + \\ rpt (pairarg_tac \\ fs []) \\ gs [tree_to_list_unfold, tree_balanced_height_pos] + ) + \\ rw [] + \\ subgoal `is_last_ix (MAP SND ts) i` + >- ( + fs [is_last_ix_def, ADD1] + \\ fs [LENGTH_bs_tree_list_to_list_eq_SUM] + ) + \\ Cases_on `HD ts` \\ Cases_on `ts` \\ fs [bs_tree_list_to_list_rec] + \\ simp [sz_array_sub_bind_eq, ADD1] + \\ gs [tree_balanced_height_pos, bs_tree_to_list_tree_rec, ADD1] + \\ simp [heap_array_sub_curr_bind_eq] +(* + \\ drule inv_trees_less_via_exp + \\ simp [GSYM MAP_DROP] + \\ disch_then (qspecl_then [`lg`, `2`] mp_tac) +*) + \\ subgoal `SORTED $<= (TAKE 2 (MAP SND t)) ∧ SORTED $< (DROP 1 (MAP SND t))` + >- ( + Cases_on `TL t` \\ Cases_on `t` \\ fs [] + ) + \\ rw [] + >- ( + gs [tree_balanced_height_eq_0] + \\ simp [mk_st_move_others, bs_tree_to_list_tree_rec, heaps_to_list_def, + add_heap_to_heaps_def] + \\ first_x_assum irule + \\ fs [bs_tree_to_list_tree_rec, MAP_DROP] + ) + >- ( + simp [st_ex_ignore_bind_simp, return_bind_eq] + \\ simp [mk_st_node_split_l] + \\ simp [ml_monadBaseTheory.monad_eqs] + \\ dep_rewrite.DEP_REWRITE_TAC [reinsert_tree_eq] + \\ qpat_x_assum `_ = _ + 1n` (assume_tac o GSYM) + \\ simp [MAP_DROP, sfx_heap_left_def, bs_tree_list_to_list_rec, + LENGTH_bs_tree_to_list, to_two_exp_min_1] + \\ Cases_on `oth_szs` + >- ( + (* log/exp proof there is still a spare sz slot *) + gs [] + \\ drule inv_trees_less_via_exp + \\ disch_then (qspecl_then [`lg`, `2`] mp_tac) + \\ simp [] + \\ disch_then drule + \\ simp [] + ) + \\ simp [GSYM mk_st_move_others] + \\ dep_rewrite.DEP_REWRITE_TAC [reinsert_tree_eq] + \\ simp [LENGTH_add_heap_to_heaps_facts, MAP_DROP, bs_tree_list_to_list_rec] + \\ conj_tac + >- ( + Cases_on `t` \\ fs [] + ) + \\ qmatch_goalsub_abbrev_tac `sfx_trees_to_list _ _ _ acc2 (mk_st (ts, oths2) (_, oth_szs2))` + \\ first_x_assum (qspecl_then [`acc2`, `ts`, `oths2`, `oth_szs2`] mp_tac) + \\ fs [markerTheory.Abbrev_def, LENGTH_add_heap_to_heaps_facts, ADD1, MAP_DROP] + \\ impl_tac + >- ( + Cases_on `t` \\ fs [] + ) + \\ rw [] \\ simp [] + \\ simp [heaps_to_list_def] + ) +QED + +Theorem sort_via_sfx_trees_worker_eq: + FST (sort_via_sfx_trees_worker R x xs st) = M_success (heap_list_sort R xs) +Proof + simp [sort_via_sfx_trees_worker_def] + \\ simp [FST_EQ_EQUIV, st_ex_ignore_bind_simp, return_bind_eq] + \\ simp [fetch "-" "alloc_heap_array_def", fetch "-" "alloc_sz_array_def", + ml_monadBaseTheory.monad_eqs, st_ex_ignore_bind_simp] + \\ qmatch_goalsub_abbrev_tac `add_all_to_sfx_heaps _ _ _ xs st` + \\ qspecl_then [`above_log2 0 (LENGTH xs + 1) 1`, `xs`, + `0`, `0`, `[]`, `st.heap_array`, `st.sz_array`] + mp_tac (add_all_to_sfx_heaps_eq |> Q.GEN `lg`) + \\ qspecl_then [`0`, `LENGTH xs + 1`, `1`] assume_tac above_log2_is_above_ind + \\ gs [markerTheory.Abbrev_def, bs_tree_list_to_list_rec, ADD1] + \\ simp [mk_st_def |> Q.SPEC `([], x)`, bs_tree_list_to_list_rec] + \\ rw [] \\ simp [] + \\ simp [heap_list_sort_def] + \\ irule sfx_trees_to_list_eq + \\ simp [add_values_to_heaps_facts] + \\ drule_at_then Any (irule_at Any) LESS_LESS_EQ_TRANS + \\ simp [tree_to_list_unfold] +QED + diff --git a/translator/monadic/examples/in_array_sorts/heap_list_sort_translationScript.sml b/translator/monadic/examples/in_array_sorts/heap_list_sort_translationScript.sml new file mode 100644 index 0000000000..c3a00ca180 --- /dev/null +++ b/translator/monadic/examples/in_array_sorts/heap_list_sort_translationScript.sml @@ -0,0 +1,163 @@ +(* + Post-translation of heap_list_sort +*) +Theory heap_list_sort_translation +Ancestors + mergesort std_prelude mllist ml_translator heap_list_sort_monadic +Libs + preamble ml_translatorLib ml_progLib + ml_monad_translator_interfaceLib + +val _ = ml_prog_update (open_module "Sort_Post_Translation"); + +val () = generate_sigs := true; + +(* Little bits of List translation that might be needed. *) + +val r = translate NULL; + +val _ = ml_prog_update open_local_block; +val res = translate LENGTH_AUX_def; +val _ = ml_prog_update open_local_in_block; + +val result = next_ml_names := ["length"] +val res = translate LENGTH_AUX_THM; + +val _ = ml_prog_update close_local_block; + +val _ = ml_prog_update open_local_block; + +(* Config to use monadic translator temporarily. *) +val _ = ml_translatorLib.use_sub_check true; + +val tvar = ``: 'el``; + +val state_type = ``: ( ^tvar ) heap_list_state``; + +val subs = ``Heap_List_Subscript`` + +val exn_type = type_of subs; + +val config = local_state_config |> + with_state state_type |> + with_exception exn_type |> + with_resizeable_arrays [ + ("heap_array", listSyntax.mk_list ([], tvar), subs, subs), + ("sz_array", ``[] : num list``, subs, subs) + ]; + +val _ = start_translation config; + +(* Some clunking around to translate the accessors as auto-defined in + heap_list_sort_monadicTheory using their counterparts auto-defined above. *) +val heap_list_acc_def_names = ["heap_array_sub_def", "update_heap_array_def", + "alloc_heap_array_def", "sz_array_sub_def", "update_sz_array_def", + "alloc_sz_array_def"] + +val configured_acc_defs = map (fetch "-") heap_list_acc_def_names; +val previous_acc_defs = map (fetch "heap_list_sort_monadic") heap_list_acc_def_names; +val redefs = previous_acc_defs + |> map (REWRITE_RULE (map GSYM configured_acc_defs)) +val do_redef = REWRITE_RULE redefs + +Definition comp_exp_def: + comp_exp m x 0 = x /\ + comp_exp (m : num) x (SUC i) = comp_exp m (x * m) i +End + +Theorem comp_exp_eq_ind[local]: + !i x. comp_exp m x i = x * (m EXP i) +Proof + Induct \\ simp [comp_exp_def, EXP] +QED + +Theorem use_comp_exp: + (m EXP i) = comp_exp m 1 i +Proof + simp [comp_exp_eq_ind] +QED + +val comp_exp_v_thm = comp_exp_def |> translate; + +val sfx_heap_left_v_thm = sfx_heap_left_def + |> REWRITE_RULE [use_comp_exp] |> translate; + +val insert_into_sfx_heap_v_thm = insert_into_sfx_heap_def + |> do_redef |> m_translate; + +val insert_into_sfx_heap_list_v_thm = insert_into_sfx_heap_list_def + |> REWRITE_RULE [use_comp_exp] + |> do_redef |> m_translate; + +Theorem bind_assoc[local]: + (st_ex_bind (st_ex_bind f g) h) = + (st_ex_bind f (\x. st_ex_bind (g x) h)) +Proof + rw [ml_monadBaseTheory.st_ex_bind_def, FUN_EQ_THM] + \\ rpt (TOP_CASE_TAC \\ fs []) +QED + +val add_to_sfx_heaps_v_thm = add_to_sfx_heaps_def + |> SIMP_RULE bool_ss [add_to_sfx_heaps_step1_def, bind_assoc] + |> do_redef |> m_translate; + +val add_all_to_sfx_heaps_v_thm = add_all_to_sfx_heaps_def + |> do_redef |> m_translate; + +val reinsert_tree_v_thm = reinsert_tree_def + |> REWRITE_RULE [use_comp_exp] + |> do_redef |> m_translate; + +val sfx_trees_to_list_v_thm = sfx_trees_to_list_def + |> do_redef |> m_translate; + +val above_log2_v_thm = above_log2_def |> translate; + +val sort_via_sfx_trees_worker_v_thm = sort_via_sfx_trees_worker_def + |> do_redef |> m_translate; + +val run_init_heap_list_state_def = define_run state_type [] "init_heap_list_state"; + +Definition sort_via_sfx_trees_run_worker_def: + sort_via_sfx_trees_run_worker R x xs = + run_init_heap_list_state (sort_via_sfx_trees_worker R x xs) + (init_heap_list_state [] []) +End + +val run_init_heap_list_state_v_thm = sort_via_sfx_trees_run_worker_def + |> m_translate_run; + +Definition sort_via_sfx_trees_def: + sort_via_sfx_trees R xs = (case xs of [] => [] + | x :: _ => (case sort_via_sfx_trees_run_worker R x xs of + M_success ys => ys + | _ => []) + ) +End + +val sort_via_sfx_trees_v_thm = sort_via_sfx_trees_def |> translate; + +(* Done monadic translation. *) + +val _ = ml_translatorLib.use_sub_check false; + +Theorem heap_list_sort_eq_sort_via_sfx_trees: + heap_list_sort R xs = sort_via_sfx_trees R xs +Proof + simp [sort_via_sfx_trees_def] + \\ Cases_on `xs` \\ simp [EVAL ``(heap_list_sort R [])``] + \\ simp [sort_via_sfx_trees_run_worker_def, + run_init_heap_list_state_def, ml_monadBaseTheory.run_def] + \\ simp [heap_list_sort_monadicTheory.sort_via_sfx_trees_worker_eq] +QED + +val _ = ml_prog_update open_local_in_block; + +val heap_list_sort_v_thm = heap_list_sort_eq_sort_via_sfx_trees |> translate; + +val _ = next_ml_names := ["heap_list_sort"]; + +val _ = ml_prog_update close_local_blocks; + + + diff --git a/translator/monadic/examples/in_array_sorts/merge_run_sortScript.sml b/translator/monadic/examples/in_array_sorts/merge_run_sortScript.sml new file mode 100644 index 0000000000..06bf359b63 --- /dev/null +++ b/translator/monadic/examples/in_array_sorts/merge_run_sortScript.sml @@ -0,0 +1,958 @@ +(* + Verified run-finding (natural) merge sort. + + This is a bottom-up adaptive merge sort that: + 1. Finds natural ascending/descending runs in the input + 2. Merges adjacent pairs of runs, prioritising merges of similar-sized lists. + + Proven to be a permutation, to sort and to be stable. +*) + +Theory merge_run_sort +Ancestors + pred_set arithmetic list rich_list option pair relation sorting mergesort + +Libs + BasicProvers permLib + +val every_case_tac = BasicProvers.EVERY_CASE_TAC; + +(* ======== Section 1: find_run and its helpers ======== *) + +Definition find_run_desc_def: + find_run_desc R prev [] acc = (prev::acc, []) /\ + find_run_desc R prev (h::t) acc = + if ~ R prev h then find_run_desc R h t (prev::acc) + else (prev::acc, h::t) +End + +Definition find_run_asc_def: + find_run_asc R prev [] acc = (REVERSE (prev::acc), []) /\ + find_run_asc R prev (h::t) acc = + if R prev h + then find_run_asc R h t (prev::acc) + else (REVERSE (prev::acc), h::t) +End + +Definition find_run_def: + find_run R [] = ([], []) /\ + find_run R [x] = ([x], []) /\ + find_run R (a::b::rest) = + if ~ R a b then find_run_desc R b rest [a] + else find_run_asc R b rest [a] +End + +(* -- Helper -- *) + +Theorem PERM_cons_REVERSE[local]: + !x l. PERM (x::l) (REVERSE l ++ [x]) +Proof + rpt gen_tac + \\ once_rewrite_tac [GSYM REVERSE_DEF] + \\ rw [PERM_REVERSE] +QED + +(* -- find_run_desc lemmas -- *) + +Theorem find_run_desc_perm: + !R prev tl acc run rest. + find_run_desc R prev tl acc = (run, rest) ==> + PERM (run ++ rest) (REVERSE acc ++ [prev] ++ tl) +Proof + Induct_on `tl` + \\ simp [Once find_run_desc_def] + >- rw [PERM_cons_REVERSE] + \\ rpt gen_tac \\ strip_tac + \\ every_case_tac \\ gvs [] + >- ( + first_x_assum drule + \\ simp [] + \\ rewrite_tac [GSYM APPEND_ASSOC, APPEND] + ) + >- ( + ONCE_REWRITE_TAC [GSYM APPEND] + \\ rewrite_tac [APPEND_ASSOC] + \\ irule PERM_CONG + \\ simp [] + \\ irule PERM_TRANS + \\ irule_at Any PERM_REVERSE + \\ rewrite_tac [REVERSE_DEF] + \\ simp [] + ) +QED + +Theorem find_run_desc_length: + !R prev tl acc run rest. + find_run_desc R prev tl acc = (run, rest) ==> + LENGTH rest <= LENGTH tl +Proof + Induct_on `tl` + \\ simp [Once find_run_desc_def] + \\ rpt gen_tac \\ strip_tac + \\ every_case_tac \\ gvs [] + \\ Q.PAT_X_ASSUM `!R prev acc run rest. _` + (mp_tac o Q.SPECL [`R`, `h`, `prev::acc`, `run`, `rest`]) + \\ simp [] +QED + +Theorem sorted_cons_lemma[local]: + SORTED R xs /\ (xs <> [] ==> R x (HD xs)) ==> SORTED R (x :: xs) +Proof + Cases_on `xs` \\ fs [SORTED_DEF] +QED + +Theorem find_run_desc_strict_sorted: + !R prev tl acc run rest. + find_run_desc R prev tl acc = (run, rest) /\ + transitive R /\ + SORTED (\x y. ~ R y x) acc /\ (acc <> [] ==> ~ R (HD acc) prev) ==> + SORTED (\x y. ~ R y x) run +Proof + Induct_on `tl` + \\ simp [Once find_run_desc_def] + \\ simp [sorted_cons_lemma] + \\ rw [] + \\ simp [sorted_cons_lemma] + \\ first_x_assum (drule_then irule) + \\ simp [sorted_cons_lemma] + \\ fs [total_def] + \\ metis_tac [] +QED + +Theorem find_run_desc_sorted: + !R prev tl acc run rest. + find_run_desc R prev tl acc = (run, rest) /\ + transitive R /\ total R /\ + SORTED (\x y. ~ R y x) acc /\ (acc <> [] ==> ~ R (HD acc) prev) ==> + SORTED R run +Proof + rw [] + \\ irule SORTED_weaken + \\ drule_then (irule_at Any) find_run_desc_strict_sorted + \\ fs [total_def] + \\ metis_tac [] +QED + +Theorem mem_sorted_append[local]: + !R l1 l2 x y. + transitive R /\ SORTED R (l1 ++ l2) /\ MEM x l1 /\ MEM y l2 ==> R x y +Proof + Induct_on `l1` \\ rw [] + \\ imp_res_tac SORTED_EQ + >- (first_x_assum irule \\ simp [MEM_APPEND]) + \\ first_x_assum irule \\ fs [SORTED_EQ] + \\ qexists_tac `l2` \\ simp [] +QED + +(* -- find_run_asc lemmas -- *) + +Theorem find_run_asc_partition: + !R prev tl acc run rest. + find_run_asc R prev tl acc = (run, rest) ==> + run ++ rest = REVERSE acc ++ [prev] ++ tl +Proof + Induct_on `tl` + \\ simp [Once find_run_asc_def] + \\ rpt gen_tac \\ strip_tac + \\ every_case_tac \\ gvs [] + \\ Q.PAT_X_ASSUM `!R prev acc run rest. _` + (mp_tac o Q.SPECL [`R`, `h`, `prev::acc`, `run`, `rest`]) + \\ simp [Once REVERSE_DEF] +QED + +Theorem find_run_asc_length: + !R prev tl acc run rest. + find_run_asc R prev tl acc = (run, rest) ==> + LENGTH rest <= LENGTH tl +Proof + Induct_on `tl` + \\ simp [Once find_run_asc_def] + \\ rpt gen_tac \\ strip_tac + \\ every_case_tac \\ gvs [] + \\ TRY ( + Q.PAT_X_ASSUM `!R prev acc run rest. _` + (mp_tac o Q.SPECL [`R`, `h`, `prev::acc`, `run`, `rest`]) + \\ simp [] \\ NO_TAC) +QED + +Theorem find_run_asc_sorted: + !R prev tl acc run rest. + transitive R /\ total R /\ + SORTED R (REVERSE (prev::acc)) /\ + find_run_asc R prev tl acc = (run, rest) ==> + SORTED R run +Proof + Induct_on `tl` + \\ simp [Once find_run_asc_def] + \\ rpt gen_tac \\ strip_tac + \\ every_case_tac \\ gvs [] + \\ Q.PAT_X_ASSUM `!R prev acc run rest. _` + (mp_tac o Q.SPECL [`R`, `h`, `prev::acc`, `run`, `rest`]) + \\ impl_tac + >- ( + rw [] \\ once_rewrite_tac [REVERSE_DEF] \\ rw [] + \\ irule SORTED_APPEND_IMP + \\ fs [SORTED_DEF] + \\ `R prev h` by metis_tac [relationTheory.total_def] + \\ `!x. MEM x acc ==> R x prev` by + metis_tac [mem_sorted_append, MEM_REVERSE, MEM] + \\ rw [] \\ metis_tac [relationTheory.transitive_def] + ) + \\ simp [] +QED + +(* -- find_run lemmas -- *) + +Theorem find_run_perm: + !R l run rest. + find_run R l = (run, rest) ==> PERM (run ++ rest) l +Proof + rpt gen_tac \\ strip_tac + \\ Cases_on `l` \\ gvs [Once find_run_def] + \\ Cases_on `t` \\ gvs [Once find_run_def] + \\ every_case_tac \\ gvs [] + >- (imp_res_tac find_run_desc_perm + \\ rewrite_tac [GSYM APPEND_ASSOC, APPEND] \\ fs []) + \\ imp_res_tac find_run_asc_partition + \\ rewrite_tac [GSYM APPEND_ASSOC, APPEND] \\ fs [] +QED + +Theorem find_run_length: + !R l run rest. + find_run R l = (run, rest) /\ l <> [] ==> LENGTH rest < LENGTH l +Proof + rpt gen_tac \\ strip_tac + \\ Cases_on `l` \\ gvs [] + \\ Cases_on `t` \\ gvs [Once find_run_def] + \\ every_case_tac \\ gvs [] + \\ imp_res_tac find_run_desc_length + \\ imp_res_tac find_run_asc_length + \\ fs [] +QED + +Theorem find_run_sorted: + !R l run rest. + total R /\ transitive R /\ find_run R l = (run, rest) ==> SORTED R run +Proof + rpt gen_tac \\ strip_tac + \\ Cases_on `l` \\ gvs [Once find_run_def, SORTED_DEF] + \\ Cases_on `t` \\ gvs [Once find_run_def, SORTED_DEF] + \\ every_case_tac \\ gvs [] + >- (match_mp_tac find_run_desc_sorted + \\ qexists_tac `h'` \\ qexists_tac `t'` + \\ qexists_tac `[h]` \\ qexists_tac `rest` + \\ simp [SORTED_DEF]) + \\ match_mp_tac find_run_asc_sorted + \\ qexists_tac `h'` \\ qexists_tac `t'` + \\ qexists_tac `[h]` \\ qexists_tac `rest` + \\ simp [SORTED_DEF] + \\ metis_tac [relationTheory.total_def] +QED + +(* An alternative (used in the monadic variant). *) + +Definition count_while_2_def: + count_while_2 P [] = 0n /\ + count_while_2 P [x] = 1 /\ + count_while_2 P (x :: y :: zs) = if P x y + then count_while_2 P (y :: zs) + 1 + else 1 +End + +Theorem find_run_asc_eq_count: + !R x xs acc. + find_run_asc R x xs acc = + let n = count_while_2 R (x :: xs) + in (REVERSE acc ++ TAKE n (x :: xs), DROP n (x :: xs)) +Proof + Induct_on `xs` + \\ simp [find_run_asc_def, count_while_2_def] + \\ rw [] +QED + +Theorem find_run_desc_eq_count: + !R x xs acc. + find_run_desc R x xs acc = + let n = count_while_2 (\x y. ~ R x y) (x :: xs) + in (REVERSE (TAKE n (x :: xs)) ++ acc, DROP n (x :: xs)) +Proof + Induct_on `xs` + \\ simp [find_run_desc_def, count_while_2_def] + \\ rw [] +QED + +Theorem find_run_eq_count: + find_run R (x :: y :: zs) = + let n = count_while_2 (\x' y'. R x' y' = R x y) (y :: zs) in + ((if R x y then I else REVERSE) (x :: TAKE n (y :: zs)), DROP n (y :: zs)) +Proof + simp [find_run_def, find_run_asc_eq_count, find_run_desc_eq_count] + \\ rw [] \\ fs [] + \\ srw_tac [ETA_ss] [] +QED + +Theorem count_while_2_length: + ! R xs. + count_while_2 R xs <= LENGTH xs /\ + (0 < LENGTH xs ==> 0 < count_while_2 R xs) +Proof + recInduct count_while_2_ind + \\ rw [count_while_2_def] +QED + +Theorem find_run_length_fst: + ! R xs. + LENGTH (FST (find_run R xs)) <= LENGTH xs +Proof + rw [] + \\ Cases_on `TL xs` \\ Cases_on `xs` \\ fs [] + \\ simp [find_run_eq_count] + \\ simp [find_run_def] + \\ rw [LENGTH_TAKE_EQ] +QED + +Theorem find_run_length_eq_sub: + LENGTH (SND (find_run R xs)) = LENGTH xs - LENGTH (FST (find_run R xs)) +Proof + Cases_on `TL xs` \\ Cases_on `xs` \\ fs [] + \\ simp [find_run_eq_count] + \\ simp [find_run_def] + \\ rw [LENGTH_TAKE_EQ] +QED + +(* ======== Section 2: find_runs (depends on find_run_length) ======== *) + +Definition find_runs_def: + find_runs R [] = [] /\ + find_runs R l = + let (run, rest) = find_run R l in + run :: find_runs R rest +Termination + WF_REL_TAC `measure (LENGTH o SND)` + \\ metis_tac [find_run_length, listTheory.NOT_NIL_CONS, PAIR_EQ] +End + +Theorem find_runs_perm: + !R l. PERM l (FLAT (find_runs R l)) +Proof + ho_match_mp_tac find_runs_ind + \\ rw [Once find_runs_def] + \\ Cases_on `find_run R (v2::v3)` \\ gvs [] + \\ imp_res_tac find_run_perm + \\ TRY (irule PERM_TRANS + \\ qexists_tac `q ++ r` + \\ conj_tac >- metis_tac [PERM_SYM] + \\ irule PERM_CONG \\ simp [] \\ NO_TAC) + \\ simp [Once find_runs_def] +QED + +Theorem find_runs_every_sorted: + !R l. + total R /\ transitive R ==> + EVERY (SORTED R) (find_runs R l) +Proof + ho_match_mp_tac find_runs_ind + \\ rw [Once find_runs_def] + \\ Cases_on `find_run R (v2::v3)` \\ gvs [] + >- simp [Once find_runs_def] + \\ metis_tac [find_run_sorted] +QED + +(* ======== Section 3: merging into sized runs ======== *) + +Definition merge_sizes_def: + merge_sizes do_merge R [] sz_run = [sz_run] /\ + merge_sizes do_merge R (sz_run2 :: acc) sz_run = ( + if do_merge (FST sz_run) (FST sz_run2) + then merge_sizes do_merge R acc + (let (sz, run) = sz_run; (sz2, run2) = sz_run2 + in (sz + sz2, merge R run2 run)) + else sz_run :: sz_run2 :: acc + ) +End + +(* +Definition merge_sizes_def: + merge_sizes R acc run = (case acc of + [] => [(LENGTH run, run)] + | (x :: xs) => let + l = LENGTH run; + (l2, run2) = x in + if l * 2 < l2 + then (l, run) :: x :: xs + else (l + l2, merge R run2 run) :: xs + ) +End +*) + +(* When merging in a new run, of length l, perform two kinds of merge. + Firstly, merge smaller existing runs until their length reaches l. + Secondly, merge in this run repeatedly unless there would be an + "unbalanced" merge with a much longer run. This will preserve the invariant + that the run lengths are at least exponential, and avoid unbalanced merges + where possible. *) +Definition merge_in_run_def: + merge_in_run R xs run = + let l = LENGTH run in + if l = 0 then xs + else let ys = (case xs of (t1 :: t2 :: ts) => if FST t2 < l + then merge_sizes (\sz sz2. sz2 < l) R (t2 :: ts) t1 + else xs + | _ => xs) in + merge_sizes (\sz sz2. ~ (sz * 2 < sz2)) R ys (l, run) +End + +Definition first_pass_def: + first_pass R xs = FOLDL (merge_in_run R) [] (find_runs R xs) +End + +Theorem merge_sizes_perm[local]: + !xs run. PERM (FLAT (MAP SND (merge_sizes f R xs run))) + (FLAT (MAP SND xs) ++ SND run) +Proof + Induct + \\ rw [merge_sizes_def] + \\ rpt (pairarg_tac \\ fs []) + >- ( + irule PERM_TRANS + \\ first_x_assum (irule_at Any) + \\ simp [] + \\ REWRITE_TAC [GSYM APPEND_ASSOC, sortingTheory.PERM_TO_APPEND_SIMPS] + \\ ONCE_REWRITE_TAC [PERM_SYM] + \\ irule PERM_TRANS \\ irule_at (Pat `PERM _ (merge _ _ _)`) merge_perm + \\ simp [PERM_APPEND] + ) + \\ metis_tac [PERM_APPEND, APPEND_ASSOC] +QED + +Theorem merge_in_run_perm: + !run acc. PERM (FLAT (MAP SND (merge_in_run R acc run))) + (FLAT (MAP SND acc) ++ run) +Proof + rw [merge_in_run_def] + \\ irule PERM_TRANS \\ irule_at Any merge_sizes_perm + \\ simp [] + \\ irule PERM_CONG + \\ simp [] + \\ every_case_tac \\ simp [] + \\ irule PERM_TRANS \\ irule_at Any merge_sizes_perm + \\ simp [] + \\ irule PERM_TRANS \\ irule_at Any PERM_APPEND + \\ simp [] +QED + +Theorem FOLDL_merge_in_run_perm[local]: + !rs acc. PERM (FLAT (MAP SND (FOLDL (merge_in_run R) acc rs))) + (FLAT (MAP SND acc ++ rs)) +Proof + Induct + \\ rw [] + \\ irule PERM_TRANS \\ pop_assum (irule_at Any) + \\ simp [] + \\ irule PERM_CONG + \\ simp [] + \\ irule merge_in_run_perm +QED + +Theorem first_pass_perm: + !R xs. PERM (FLAT (MAP SND (first_pass R xs))) xs +Proof + rw [first_pass_def] + \\ irule PERM_TRANS \\ irule_at Any FOLDL_merge_in_run_perm + \\ simp [] + \\ ONCE_REWRITE_TAC [PERM_SYM] + \\ irule find_runs_perm +QED + +Theorem merge_sizes_every_sorted[local]: + !sz_run acc. + total R /\ transitive R /\ + EVERY (SORTED R) (MAP SND acc) /\ SORTED R (SND sz_run) ==> + EVERY (SORTED R) (MAP SND (merge_sizes f R acc sz_run)) +Proof + Induct_on `acc` + \\ rw [merge_sizes_def] + \\ first_x_assum irule + \\ simp [] + \\ rpt (pairarg_tac \\ fs []) + \\ rw [merge_sorted] +QED + +Theorem merge_in_run_every_sorted[local]: + !run acc. + total R /\ transitive R /\ + EVERY (SORTED R) (MAP SND acc) /\ SORTED R run ==> + EVERY (SORTED R) (MAP SND (merge_in_run R acc run)) +Proof + rw [merge_in_run_def] + \\ every_case_tac \\ fs [] + \\ simp [merge_sizes_every_sorted] +QED + +Theorem FOLDL_merge_in_run_every_sorted[local]: + !rs acc. + total R /\ transitive R /\ + EVERY (SORTED R) (MAP SND acc) /\ EVERY (SORTED R) rs ==> + EVERY (SORTED R) (MAP SND (FOLDL (merge_in_run R) acc rs)) +Proof + Induct + \\ rw [] + \\ first_x_assum irule + \\ simp [merge_in_run_every_sorted] +QED + +Theorem first_pass_every_sorted: + !R xs. + total R /\ transitive R ==> + EVERY (SORTED R) (MAP SND (first_pass R xs)) +Proof + rw [first_pass_def] + \\ irule FOLDL_merge_in_run_every_sorted + \\ simp [find_runs_every_sorted] +QED + +Theorem merge_sizes_neq_nil[local]: + !acc sz_run. merge_sizes f R acc sz_run <> [] +Proof + Induct + \\ rw [merge_sizes_def] +QED + +Theorem merge_sizes_eq_cons_lemma[local]: + !acc sz_run. + merge_sizes f R acc sz_run = hd :: tl ==> + ?n. tl = DROP n acc /\ + (tl <> [] ==> ~ f (FST hd) (FST (HD tl))) +Proof + Induct + \\ rw [merge_sizes_def] + >- ( + first_x_assum drule + \\ rw [] + \\ qexists_tac `n + 1` + \\ simp [] + ) + >- ( + qexists_tac `0` + \\ simp [] + ) +QED + +Theorem merge_length[local]: + LENGTH (merge R xs ys) = LENGTH xs + LENGTH ys +Proof + qspecl_then [`R`, `xs`, `ys`] mp_tac merge_perm + \\ rw [] + \\ imp_res_tac PERM_LENGTH + \\ fs [] +QED + +Theorem merge_sizes_eq_length_inv: + ! acc sz_run. + EVERY (\(sz, xs). sz = LENGTH xs /\ ~ NULL xs) acc /\ + FST sz_run = LENGTH (SND sz_run) /\ ~ NULL (SND sz_run) ==> + EVERY (\(sz, xs). sz = LENGTH xs /\ ~ NULL xs) (merge_sizes f R acc sz_run) +Proof + Induct_on `acc` + \\ simp [merge_sizes_def, FORALL_PROD] + \\ rw [] + \\ first_x_assum irule + \\ fs [merge_length, GSYM rich_listTheory.LENGTH_NOT_NULL] +QED + +Theorem merge_in_run_eq_length_inv: + EVERY (\(sz, xs). sz = LENGTH xs /\ ~ NULL xs) acc ==> + EVERY (\(sz, xs). sz = LENGTH xs /\ ~ NULL xs) (merge_in_run R acc r) +Proof + rw [merge_in_run_def] + \\ Cases_on `HD acc` \\ Cases_on `acc` + \\ fs [merge_sizes_def, merge_empty, GSYM NULL_EQ] + \\ irule merge_sizes_eq_length_inv + \\ simp [] + \\ every_case_tac \\ fs [] + \\ irule merge_sizes_eq_length_inv + \\ simp [] + \\ rpt (pairarg_tac \\ fs []) + \\ fs [merge_length, GSYM rich_listTheory.LENGTH_NOT_NULL] +QED + +Theorem SORTED_DROP_IMP[local]: + !n xs. SORTED R xs ==> SORTED R (DROP n xs) +Proof + Induct + \\ simp [] + \\ Cases \\ simp [] + \\ metis_tac [SORTED_TL] +QED + +Theorem SORTED_merge_sizes_lemma[local]: + SORTED R2 acc /\ (!sz r sz2 r2. ~ f sz sz2 ==> R2 (sz, r) (sz2, r2)) ==> + SORTED R2 (merge_sizes f R acc sz_run) +Proof + rw [] + \\ subgoal `!t t2. ~ f (FST t) (FST t2) ==> R2 t t2` + >- simp [FORALL_PROD] + \\ Cases_on `merge_sizes f R acc sz_run` \\ simp [] + \\ drule merge_sizes_eq_cons_lemma + \\ rw [] + \\ irule sorted_cons_lemma + \\ fs [SORTED_DROP_IMP] +QED + +Theorem neq_nil_IMP: + x <> [] ==> (?y ys. x = y :: ys) +Proof + Cases_on `x` \\ simp [] +QED + +(* The interesting case of the size invariant proof. The existing + sizes go up in at-least-exponential strides, and are to be merged. + The initial two are less than 'n'. The first may already have been + merged, so it is merely less than the second. Merging continues until + 'n' is passed, and we need to know it does not overshoot so far that + it would not itself be merged in the next pass. *) +Theorem merge_sizes_hd_lim[local]: + !xs sz_run. + merge_sizes (\sz sz2. sz2 < n) R xs sz_run = hd :: tl /\ + tl <> [] /\ FST sz_run < 2 * n /\ + SORTED (\sz sz2. sz * 2 < sz2) (MAP FST xs) /\ + (xs <> [] ==> FST sz_run < FST (HD xs)) ==> + FST hd < 2 * n +Proof + Induct + \\ simp [merge_sizes_def] + \\ rw [] + \\ imp_res_tac SORTED_TL + \\ simp [] + \\ first_x_assum (drule_then irule) + \\ simp [] + \\ rpt (pairarg_tac \\ fs []) + \\ rw [] + \\ imp_res_tac neq_nil_IMP \\ fs [] +QED + +(* Not strictly needed for the verification of this variant. *) +Theorem merge_in_run_size_invariant: + SORTED (\sz sz2. sz * 2 < sz2) (MAP FST acc) /\ + EVERY (\(sz, xs). sz = LENGTH xs /\ ~ NULL xs) acc ==> + SORTED (\sz sz2. sz * 2 < sz2) (MAP FST (merge_in_run R acc r_add)) +Proof + strip_tac + \\ rw [merge_in_run_def] + \\ fs [sorted_map] + \\ Cases_on `HD acc` \\ Cases_on `acc` + \\ simp [merge_sizes_def, merge_empty] + \\ fs [] + \\ imp_res_tac SORTED_TL + \\ rw [] \\ fs [] + \\ every_case_tac \\ fs [] + \\ simp [SORTED_merge_sizes_lemma, sorted_map] + (* The tricky case that remains is the one where the invariant + might not hold at the head of the intermediate constructed list. *) + \\ rpt (pairarg_tac \\ fs []) + \\ qmatch_asmsub_rename_tac `EVERY _ xs` + \\ qmatch_goalsub_abbrev_tac `SORTED _ (merge_sizes _ _ merge1 _)` + \\ Cases_on `merge1` + \\ fs [merge_sizes_neq_nil] + \\ imp_res_tac merge_sizes_eq_cons_lemma + \\ imp_res_tac SORTED_TL + \\ rw [merge_sizes_def] + >- ( + rpt (pairarg_tac \\ fs []) + \\ simp [SORTED_merge_sizes_lemma, SORTED_DROP_IMP] + ) + >- ( + irule sorted_cons_lemma + \\ simp [SORTED_DROP_IMP] + \\ rw [] + \\ gs [] + \\ drule merge_sizes_hd_lim + \\ simp [sorted_map] + \\ rw [] + \\ imp_res_tac neq_nil_IMP \\ fs [] + ) +QED + +(* Not strictly needed for the verification of this variant. *) +Theorem FOLDL_merge_in_run_size_invariant: + !rs acc. + SORTED (\sz sz2. sz * 2 < sz2) (MAP FST acc) /\ + EVERY (\(sz, xs). sz = LENGTH xs /\ ~ NULL xs) acc ==> + SORTED (\sz sz2. sz * 2 < sz2) + (MAP FST (FOLDL (merge_in_run R) acc rs)) /\ + EVERY (\(sz, xs). sz = LENGTH xs /\ ~ NULL xs) + (FOLDL (merge_in_run R) acc rs) +Proof + Induct + \\ simp [] + \\ rpt gen_tac + \\ strip_tac + \\ fs [] + \\ first_x_assum irule + \\ simp [merge_in_run_eq_length_inv, + SIMP_RULE arith_ss [] merge_in_run_size_invariant] +QED + +Theorem first_pass_size_invariant: + SORTED (\sz sz2. sz * 2 < sz2) + (MAP FST (first_pass R xs)) /\ + EVERY (\(sz, xs). sz = LENGTH xs /\ ~ NULL xs) + (first_pass R xs) +Proof + REWRITE_TAC [first_pass_def] + \\ irule FOLDL_merge_in_run_size_invariant + \\ simp [] +QED + +(* ======== Section 4: merge_run_sort (top-level) ======== *) + +Definition merge_run_sort_def: + merge_run_sort R xs = FLAT (MAP SND (merge_sizes (\_ _. T) R + (first_pass R xs) (0, []))) +End + +(* +Theorem PERM_FLAT_MAP_REVERSE: + !xs. PERM (FLAT (MAP REVERSE xs)) (FLAT xs) +Proof + Induct \\ simp [] + \\ simp [PERM_CONG] +QED +*) + +Theorem merge_run_sort_perm: + !R l. PERM l (merge_run_sort R l) +Proof + rw [merge_run_sort_def] + \\ ONCE_REWRITE_TAC [PERM_SYM] + \\ irule PERM_TRANS \\ irule_at Any merge_sizes_perm + \\ simp [first_pass_perm] +QED + +Theorem SORTED_FLAT_1_lemma[local]: + LENGTH xs <= 1 /\ EVERY (SORTED R) xs ==> + SORTED R (FLAT xs) +Proof + Cases_on `TL xs` \\ Cases_on `xs` \\ fs [ADD1] +QED + +Theorem merge_sizes_T_length[local]: + !acc sz_run. (!sz sz2. f sz sz2) ==> + LENGTH (merge_sizes f R acc sz_run) <= 1 +Proof + Induct + \\ simp [merge_sizes_def] +QED + +Theorem merge_run_sort_sorted: + !R l. total R /\ transitive R ==> SORTED R (merge_run_sort R l) +Proof + rw [merge_run_sort_def] + \\ irule SORTED_FLAT_1_lemma + \\ simp [merge_sizes_every_sorted, first_pass_every_sorted] + \\ simp [merge_sizes_T_length] +QED + +Theorem merge_run_sort_SORTS: + !R. total R /\ transitive R ==> SORTS merge_run_sort R +Proof + rw [SORTS_DEF] \\ metis_tac [merge_run_sort_perm, merge_run_sort_sorted] +QED + +(* ======== Section 5: Stability ======== *) + +(* Stability for find_run_asc is easy. For find_run_desc, which reverses, + this will be OK because each strictly descending run can have at most + one element that satisfies the special predicate p. *) + +Theorem find_run_asc_append_eq[local]: + !R prev tl acc run rest. + find_run_asc R prev tl acc = (run, rest) ==> + REVERSE acc ++ [prev] ++ tl = run ++ rest +Proof + Induct_on `tl` + \\ simp [Once find_run_asc_def] + \\ rw [] + \\ simp [] + \\ res_tac + \\ fs [] +QED + +Theorem find_run_desc_append_eq[local]: + !R prev tl acc run rest. + find_run_desc R prev tl acc = (run, rest) ==> + REVERSE acc ++ [prev] ++ tl = REVERSE run ++ rest +Proof + Induct_on `tl` + \\ simp [Once find_run_desc_def] + \\ rw [] + \\ simp [] + \\ res_tac + \\ fs [] +QED + +Theorem find_run_append_eq[local]: + !R xs run rest. + find_run R xs = (run, rest) ==> + run ++ rest = xs \/ REVERSE run ++ rest = xs +Proof + recInduct find_run_ind + \\ simp [find_run_def] + \\ rw [] + \\ imp_res_tac find_run_desc_append_eq + \\ imp_res_tac find_run_asc_append_eq + \\ fs [] +QED + +Theorem stable_refl[local] = stable_def |> Q.SPECL [`R`, `xs`, `xs`] + |> REWRITE_RULE [] + +Theorem not_R_transitive[local]: + transitive R /\ total R ==> + transitive (\x y. ~ R y x) +Proof + simp [transitive_def, total_def] + \\ metis_tac [] +QED + +Theorem strict_desc_stable_reverse_lemma[local]: + !xs. + transitive R /\ total R /\ SORTED (\x y. ~ R y x) xs /\ + (!x y. p x /\ p y ==> R x y) ==> + FILTER p (REVERSE xs) = FILTER p xs +Proof + Induct + \\ rw [] + \\ imp_res_tac SORTED_TL + \\ simp [FILTER_APPEND] + \\ Cases_on `FILTER p xs = []` + \\ fs [FILTER_NEQ_NIL] + \\ gs [SORTED_EQ, not_R_transitive] + \\ metis_tac [] +QED + +Theorem find_run_stable: + !R l run rest. + transitive R /\ total R /\ + find_run R l = (run, rest) ==> + stable R l (run ++ rest) +Proof + recInduct find_run_ind + \\ simp [find_run_def] + \\ rw [stable_refl] + \\ imp_res_tac find_run_desc_append_eq + \\ imp_res_tac find_run_asc_append_eq + \\ fs [stable_refl] + \\ irule stable_cong + \\ rw [stable_def] + \\ drule_then irule strict_desc_stable_reverse_lemma + \\ simp [] + \\ drule_then irule find_run_desc_strict_sorted + \\ simp [] +QED + +Theorem find_runs_stable: + !R l. + transitive R /\ total R ==> + stable R l (FLAT (find_runs R l)) +Proof + ho_match_mp_tac find_runs_ind + \\ rw [Once find_runs_def] + >- simp [Once find_runs_def, stable_def] + \\ Cases_on `find_run R (v2::v3)` \\ gvs [] + \\ irule stable_trans + \\ qexists_tac `q ++ FLAT (find_runs R r)` + \\ conj_tac + >- (irule stable_trans + \\ qexists_tac `q ++ r` + \\ conj_tac >- metis_tac [find_run_stable] + \\ irule stable_cong \\ rw [stable_def]) + \\ rewrite_tac [GSYM APPEND_ASSOC] + \\ irule stable_cong \\ rw [stable_def] +QED + +Theorem merge_sizes_stable[local]: + !acc sz_run. transitive R /\ EVERY (SORTED R) (MAP SND acc) ==> + stable R (FLAT (REVERSE (MAP SND acc)) ++ SND sz_run) + (FLAT (REVERSE (MAP SND (merge_sizes f R acc sz_run)))) +Proof + Induct + \\ rw [merge_sizes_def, stable_refl] + \\ irule stable_trans + \\ first_x_assum (irule_at Any) + \\ rpt (pairarg_tac \\ fs []) + \\ REWRITE_TAC [GSYM APPEND_ASSOC] + \\ irule stable_cong + \\ simp [stable_refl, merge_stable] +QED + +Theorem merge_in_run_stable[local]: + !acc sz_run. transitive R /\ total R /\ EVERY (SORTED R) (MAP SND acc) ==> + stable R (FLAT (REVERSE (MAP SND acc)) ++ r) + (FLAT (REVERSE (MAP SND (merge_in_run R acc r)))) +Proof + rw [merge_in_run_def, stable_refl] + \\ irule stable_trans + \\ irule_at (Pat `stable _ _ (FLAT _)`) merge_sizes_stable + \\ simp [] + \\ every_case_tac \\ simp [stable_refl] + \\ fs [merge_sizes_every_sorted] + \\ irule stable_cong + \\ simp [stable_refl] + \\ irule stable_trans + \\ irule_at (Pat `stable _ _ (FLAT _)`) merge_sizes_stable + \\ simp [stable_refl] +QED + +Theorem FOLDL_merge_in_run_stable[local]: + !rs acc. total R /\ transitive R /\ + EVERY (SORTED R) (MAP SND acc) /\ EVERY (SORTED R) rs ==> + stable R (FLAT (REVERSE (MAP SND acc) ++ rs)) + (FLAT (REVERSE (MAP SND (FOLDL (merge_in_run R) acc rs)))) +Proof + Induct + \\ simp [stable_refl] + \\ rw [] + \\ irule stable_trans + \\ first_x_assum (irule_at Any) + \\ simp [merge_in_run_every_sorted] + \\ irule stable_cong + \\ simp [stable_refl, merge_in_run_stable] +QED + +Theorem first_pass_stable: + !R rs. + total R /\ transitive R ==> + stable R rs (FLAT (REVERSE (MAP SND (first_pass R rs)))) +Proof + rw [first_pass_def] + \\ irule stable_trans + \\ irule_at Any FOLDL_merge_in_run_stable + \\ simp [find_runs_every_sorted, find_runs_stable] +QED + +Theorem stable_FLAT_1_lemma[local]: + stable R l (FLAT (REVERSE xs)) /\ LENGTH xs <= 1 ==> + stable R l (FLAT xs) +Proof + Cases_on `TL xs` \\ Cases_on `xs` \\ fs [] +QED + +Theorem merge_run_sort_stable: + !R l. total R /\ transitive R ==> stable R l (merge_run_sort R l) +Proof + rw [merge_run_sort_def] + \\ irule stable_FLAT_1_lemma + \\ simp [merge_sizes_T_length] + \\ irule stable_trans + \\ irule_at Any (merge_sizes_stable) + \\ simp [MAP_REVERSE, first_pass_every_sorted, first_pass_stable] +QED + +Theorem merge_run_sort_STABLE_SORT: + !R. transitive R /\ total R ==> STABLE merge_run_sort R +Proof + rw [STABLE_DEF] + \\ metis_tac [merge_run_sort_SORTS, merge_run_sort_stable, stable_def] +QED + diff --git a/translator/monadic/examples/in_array_sorts/merge_run_sort_monadicScript.sml b/translator/monadic/examples/in_array_sorts/merge_run_sort_monadicScript.sml new file mode 100644 index 0000000000..38225079d1 --- /dev/null +++ b/translator/monadic/examples/in_array_sorts/merge_run_sort_monadicScript.sml @@ -0,0 +1,1277 @@ +(* + Monadic variants of the merge-run-sort functions, and proofs of equivalence. +*) + +Theory merge_run_sort_monadic +Ancestors + merge_run_sort ml_monadBase mergesort +Libs + preamble ml_monadBaseLib + +(* Part 1: Setup of types and infrastructure. *) + +(* The data type of the state. *) +Datatype: + merge_run_state = <| + main_array : ( 'a ) list; + copy_array : ( 'a ) list; + sz_array : num list; + |> +End + +(* Equivalent to unit, but we need to construct a type so that the translation + can construct a new exception type. *) +Datatype: + heap_list_subscript_exn = MR_Subscript +End + +(* Setup to use monad translator constants and monad syntax. *) +val acc_fun_defs = define_monad_access_funs ``: 'a merge_run_state`` + +val mr_manip_funs = define_MRarray_manip_funs acc_fun_defs + ``MR_Subscript`` ``MR_Subscript`` + +val _ = ParseExtras.temp_tight_equality (); +val _ = monadsyntax.temp_add_monadsyntax (); + +Overload "monad_bind"[local] = ``st_ex_bind`` +Overload "monad_unitbind"[local] = ``st_ex_ignore_bind`` +Overload "monad_ignore_bind"[local] = ``st_ex_ignore_bind`` +Overload "return"[local] = ``st_ex_return`` + +(* Part 2: Definition of sort functions with runs held in an array. *) + +Definition merge_runs_def: + merge_runs R xi xlen yi ylen base = if xi >= xlen + then (* no more xs, ys are in correct place *) + return () + else if yi >= ylen + then do (* no more ys, copy xs to correct place *) + x <- copy_array_sub xi; + update_main_array (base + yi + xi) x; + merge_runs R (xi + 1) xlen yi ylen base + od + else do + x <- copy_array_sub xi; + y <- main_array_sub (base + xlen + yi); + b <- return (R x y); + update_main_array (base + yi + xi) (if b then x else y); + merge_runs R (xi + (if b then 1 else 0)) xlen + (yi + (if b then 0 else 1)) ylen base + od +Termination + WF_REL_TAC `measure (\(R, xi, xlen, yi, ylen, base). (xlen - xi) + (ylen - yi))` +End + +Definition copy_to_copy_def: + copy_to_copy base xi xlen = if xi >= xlen + then return () + else do + x <- main_array_sub (base + xi); + update_copy_array xi x; + copy_to_copy base (xi + 1) xlen + od +Termination + WF_REL_TAC `measure (\(base, xi, xlen). (xlen - xi))` +End + +Definition do_merge_array_def: + do_merge_array R ri arri = do + xsz <- sz_array_sub (ri + 1); + ysz <- sz_array_sub ri; + update_sz_array (ri + 1) (xsz + ysz); + base <- return (arri - (xsz + ysz)); + copy_to_copy base 0 xsz; + merge_runs R 0 xsz 0 ysz base + od +End + +Definition merge_sizes_gen_array_def: + merge_sizes_gen_array R f ri rlen arri = + if ri + 1 >= rlen + then return ri + else do + sz <- sz_array_sub ri; + sz2 <- sz_array_sub (ri + 1); + if f sz sz2 + then do + do_merge_array R ri arri; + merge_sizes_gen_array R f (ri + 1) rlen arri + od + else return ri + od +Termination + WF_REL_TAC `measure (\(R, f, ri, rlen, arri). (rlen - ri))` +End + +Definition merge_smaller_array_def: + merge_smaller_array R n ri rlen arri = + if ri + 1 >= rlen + then return ri + else do + sz2 <- sz_array_sub (ri + 1); + if sz2 < n + then do + do_merge_array R ri arri; + merge_smaller_array R n (ri + 1) rlen arri + od + else return ri + od +Termination + WF_REL_TAC `measure (\(R, n, ri, rlen, arri). (rlen - ri))` +End + +Definition merge_similar_array_def: + merge_similar_array R ri rlen arri = + if ri + 1 >= rlen + then return ri + else do + sz <- sz_array_sub ri; + sz2 <- sz_array_sub (ri + 1); + if sz * 2 < sz2 + then return ri + else do + do_merge_array R ri arri; + merge_similar_array R (ri + 1) rlen arri + od + od +Termination + WF_REL_TAC `measure (\(R, ri, rlen, arri). (rlen - ri))` +End + +Definition merge_every_array_def: + merge_every_array R ri rlen arri = + if ri + 1 >= rlen + then return ri + else do + do_merge_array R ri arri; + merge_every_array R (ri + 1) rlen arri + od +Termination + WF_REL_TAC `measure (\(R, ri, rlen, arri). (rlen - ri))` +End + +Definition merge_in_run_array_def: + merge_in_run_array R ri rlen arri l = do + ri2 <- if ri + 1 < rlen + then do + l2 <- sz_array_sub (ri + 1); + if l2 < l then merge_smaller_array R l ri rlen arri + else return ri + od else return ri; + ri3 <- return (ri2 - 1); + update_sz_array ri3 l; + merge_similar_array R ri3 rlen (arri + l) + od +End + +Definition find_known_run_array_def: + find_known_run_array R x b n i arrlen = if i >= arrlen then return n + else do + y <- main_array_sub i; + if R x y = b + then find_known_run_array R y b (n + 1n) (i + 1n) arrlen + else return n + od +Termination + WF_REL_TAC `measure (\(R, x, b, n, i, arrlen). arrlen - i)` +End + +Definition reverse_run_def: + reverse_run i l = if l < 2 + then return () + else let l2 = l - 2 in do + x <- main_array_sub i; + j <- return (i + l2 + 1); + y <- main_array_sub j; + update_main_array i y; + update_main_array j x; + reverse_run (i + 1) l2 + od +End + +Definition find_run_array_def: + find_run_array R i arrlen = if i + 1 >= arrlen + then return (arrlen - i) + else do + x <- main_array_sub i; + y <- main_array_sub (i + 1); + b <- return (R x y); + l <- find_known_run_array R y b 2 (i + 2) arrlen; + if ~ b + then reverse_run i l + else return (); + return l + od +End + +Definition first_pass_array_def: + first_pass_array R ri rlen i arrlen = + if i >= arrlen + then return ri + else do + l <- find_run_array R i arrlen; + ri2 <- merge_in_run_array R ri rlen i l; + first_pass_array R ri2 rlen (i + (if l = 0 then 1n else l)) arrlen + od +Termination + WF_REL_TAC `measure (\(R, ri, rlen, i, arrlen). arrlen - i)` +End + +(* Top-level of the monadic worker. Needs to be wrapped in a "run" function + that sets up the array and fetches the final list again. *) +Definition merge_run_sort_monadic_def: + merge_run_sort_monadic R rlen arrlen = do + ri <- first_pass_array R rlen rlen 0 arrlen; + merge_every_array R ri rlen arrlen; + return () + od +End + +(* Compute an overapproximation of the base-2 logarithm of v *) +Definition above_log2_def: + above_log2 i v n = if n = 0n \/ v <= n + then i + else above_log2 (i + 1n) v (n * 2) +Termination + WF_REL_TAC `measure (\(i, v, n). (v - n))` +End + +Definition copy_into_array_def: + copy_into_array i [] = return () + /\ + copy_into_array i (x :: xs) = do + update_main_array i x; + copy_into_array (i + 1) xs + od +End + +Definition copy_from_array_def: + copy_from_array i acc = if i = 0 + then return acc + else let j = i - 1 in do + x <- main_array_sub j; + copy_from_array j (x :: acc) + od +End + +Definition merge_run_sort_worker_def: + merge_run_sort_worker R x xs = do + l <- return (LENGTH xs); + sz_log <- return (above_log2 0 (l + 1) 1 + 2); + alloc_main_array l x; + alloc_copy_array l x; + alloc_sz_array sz_log 0; + copy_into_array 0 xs; + merge_run_sort_monadic R sz_log l; + copy_from_array l []; + od +End + +(* Get straight to the key proof. Can we show that do_merge_array is merge + and that merge_smaller_array is merge_sizes? *) + +Definition mk_st_def: + mk_st xs sz_junk junk copy = + (<| + sz_array := sz_junk ++ (MAP LENGTH xs); + main_array := FLAT (REVERSE xs) ++ junk; + copy_array := copy + |>) +End + +Theorem return_bind_eq[local]: + st_ex_bind (return v) f = f v +Proof + simp [ml_monadBaseTheory.st_ex_bind_def, ml_monadBaseTheory.st_ex_return_def, FUN_EQ_THM] +QED + +Theorem st_ex_ignore_bind_simp[local]: + st_ex_ignore_bind f g = st_ex_bind f (\_. g) +Proof + simp [ml_monadBaseTheory.st_ex_bind_def, ml_monadBaseTheory.st_ex_ignore_bind_def] +QED + +Theorem bind_success_eqI: + m st = (M_success v, st2) /\ f v st2 = rhs ==> + st_ex_bind m f st = rhs +Proof + simp [ml_monadBaseTheory.st_ex_bind_def] +QED + +Theorem copy_array_sub_eq[local]: + i < LENGTH c ==> + st_ex_bind (copy_array_sub i) f + (mk_st xs szj j c) = + f (EL i c) (mk_st xs szj j c) +Proof + rw [] + \\ irule bind_success_eqI + \\ simp [fetch "-" "copy_array_sub_def", ml_monadBaseTheory.monad_eqs] + \\ simp [mk_st_def] +QED + +Theorem update_copy_array_eq[local]: + i < LENGTH c ==> + st_ex_bind (update_copy_array i x) f (mk_st xss szj j c) = + f () (mk_st xss szj j (LUPDATE x i c)) +Proof + rw [] + \\ irule bind_success_eqI + \\ simp [fetch "-" "update_copy_array_def", ml_monadBaseTheory.monad_eqs] + \\ simp [mk_st_def] +QED + +Theorem main_array_sub_hd_app_cons_eq[local]: + i = LENGTH xs + SUM (MAP LENGTH pre) ==> + st_ex_bind (main_array_sub i) f + (mk_st ((xs ++ y :: ys) :: pre) szj j c) = + f y (mk_st ((xs ++ y :: ys) :: pre) szj j c) +Proof + rw [] + \\ irule bind_success_eqI + \\ simp [fetch "-" "main_array_sub_def", ml_monadBaseTheory.monad_eqs] + \\ simp [mk_st_def, LENGTH_FLAT, MAP_REVERSE, SUM_REVERSE, + EL_APPEND1, EL_APPEND2] +QED + +Theorem main_array_sub_extra_EL[local]: + SUM (MAP LENGTH pre) <= i /\ i < LENGTH ys + SUM (MAP LENGTH pre) ==> + st_ex_bind (main_array_sub i) f + (mk_st pre szj ys c) = + f (EL (i - SUM (MAP LENGTH pre)) ys) (mk_st pre szj ys c) +Proof + rw [] + \\ irule bind_success_eqI + \\ simp [fetch "-" "main_array_sub_def", ml_monadBaseTheory.monad_eqs] + \\ simp [mk_st_def, LENGTH_FLAT, MAP_REVERSE, SUM_REVERSE, + EL_APPEND1, EL_APPEND2] +QED + +Theorem main_array_sub_extra[local]: + !xs. i = LENGTH xs + SUM (MAP LENGTH pre) ==> + st_ex_bind (main_array_sub i) f + (mk_st pre szj (xs ++ y :: ys) c) = + f y (mk_st pre szj (xs ++ y :: ys) c) +Proof + simp [main_array_sub_extra_EL, EL_APPEND2] +QED + +Theorem update_main_array_hd_app_cons_eq[local]: + i = LENGTH xs + SUM (MAP LENGTH pre) ==> + st_ex_bind (update_main_array i x) f + (mk_st ((xs ++ y :: ys) :: pre) szj j c) = + f () (mk_st ((xs ++ x :: ys) :: pre) szj j c) +Proof + rw [] + \\ irule bind_success_eqI + \\ simp [fetch "-" "update_main_array_def", ml_monadBaseTheory.monad_eqs] + \\ simp [mk_st_def, LENGTH_FLAT, MAP_REVERSE, SUM_REVERSE, + LUPDATE_APPEND1, LUPDATE_APPEND2, LUPDATE_DEF] +QED + +Theorem update_main_array_extra_LUPDATE[local]: + SUM (MAP LENGTH pre) <= i /\ i < LENGTH ys + SUM (MAP LENGTH pre) ==> + st_ex_bind (update_main_array i x) f + (mk_st pre szj ys c) = + f () (mk_st pre szj (LUPDATE x (i - SUM (MAP LENGTH pre)) ys) c) +Proof + rw [] + \\ irule bind_success_eqI + \\ simp [fetch "-" "update_main_array_def", ml_monadBaseTheory.monad_eqs] + \\ simp [mk_st_def, LENGTH_FLAT, MAP_REVERSE, SUM_REVERSE, + LUPDATE_APPEND1, LUPDATE_APPEND2, LUPDATE_DEF] +QED + +Definition mk_st_eq_def: + mk_st_eq xs szs j cxs st = (st = mk_st xs szs j cxs) +End + +val mk_st_unfold = qpat_x_assum `mk_st_eq _ _ _ _ _` + (assume_tac o REWRITE_RULE [mk_st_eq_def]) + \\ full_simp_tac bool_ss [] + +Theorem mk_st_eqI[local]: + xs = xs2 /\ szs = szs2 /\ j = j2 /\ cxs = cxs2 ==> + mk_st_eq xs szs j cxs (mk_st xs2 szs2 j2 cxs2) +Proof + simp [mk_st_eq_def] +QED + +Theorem mk_st_eq_mk_stI[local] = + REWRITE_RULE [mk_st_eq_def] mk_st_eqI + +Theorem merge_runs_empty_ys_eq_lemma: + ! xs xi csp sp fin st. + xi + LENGTH xs = xlen /\ + base = SUM (MAP LENGTH pre) /\ LENGTH sp = LENGTH xs /\ + xi = LENGTH csp /\ LENGTH fin = ylen + xi /\ + mk_st_eq ((fin ++ sp) :: pre) szj j (csp ++ xs ++ j2) st ==> + merge_runs R xi xlen ylen ylen base st = + (M_success (), (mk_st ((fin ++ xs) :: pre) szj j + (csp ++ xs ++ j2))) +Proof + Induct + \\ ONCE_REWRITE_TAC [merge_runs_def] + \\ rw [st_ex_ignore_bind_simp] + \\ mk_st_unfold + >- ( + simp [merge_empty, ml_monadBaseTheory.st_ex_return_def] + ) + >- ( + simp [copy_array_sub_eq, EL_APPEND1, EL_APPEND2] + \\ Cases_on `sp` \\ fs [] + \\ simp [update_main_array_hd_app_cons_eq] + \\ first_x_assum (qspec_then `spc ++ [x]` (assume_tac o Q.GENL [`spc`, `x`])) + \\ fs [] + \\ irule EQ_TRANS + \\ first_x_assum (irule_at Any) + \\ simp [] + \\ irule_at Any mk_st_eqI + \\ irule_at Any mk_st_eq_mk_stI + \\ simp [] + ) +QED + +Theorem merge_runs_eq: + ! R xs ys xi yi csp sp fin st. + xi + LENGTH xs = xlen /\ yi + LENGTH ys = ylen /\ + base = SUM (MAP LENGTH pre) /\ LENGTH sp = LENGTH xs /\ + LENGTH csp = xi /\ LENGTH fin = xi + yi /\ + mk_st_eq ((fin ++ sp ++ ys) :: pre) szj j (csp ++ xs ++ j2) st ==> + merge_runs R xi xlen yi ylen base st = + (M_success (), (mk_st ((fin ++ merge R xs ys) :: pre) szj j + (csp ++ xs ++ j2))) +Proof + recInduct merge_ind + \\ rw [] + \\ mk_st_unfold + >- ( + ONCE_REWRITE_TAC [merge_runs_def] + \\ simp [merge_empty, ml_monadBaseTheory.st_ex_return_def] + ) + >- ( + simp [SIMP_RULE bool_ss [mk_st_eq_def] merge_runs_empty_ys_eq_lemma] + \\ simp [merge_empty] + ) + >- ( + ONCE_REWRITE_TAC [merge_runs_def] + \\ simp [merge_empty, ml_monadBaseTheory.st_ex_return_def] + ) + >- ( + ONCE_REWRITE_TAC [merge_runs_def] + \\ simp [copy_array_sub_eq, EL_APPEND1, EL_APPEND2] + \\ simp [st_ex_ignore_bind_simp, return_bind_eq] + \\ simp [main_array_sub_hd_app_cons_eq] + \\ Cases_on `sp` \\ fs [] + \\ REWRITE_TAC [GSYM APPEND_ASSOC, APPEND] + \\ simp [update_main_array_hd_app_cons_eq] + \\ TOP_CASE_TAC \\ fs [] + >- ( + first_x_assum (qspec_then `spc_z ++ [x_z]` + (assume_tac o Q.GENL [`spc_z`, `x_z`])) + \\ fs [] + \\ irule EQ_TRANS \\ first_x_assum (irule_at Any) + \\ simp [] + \\ irule_at Any mk_st_eqI + \\ irule_at Any mk_st_eq_mk_stI + \\ simp [merge_def] + ) + >- ( + irule EQ_TRANS \\ first_x_assum (irule_at Any) + \\ simp [] + \\ irule_at Any mk_st_eqI + \\ irule_at Any mk_st_eq_mk_stI + \\ simp [merge_def] + ) + ) +QED + +Theorem copy_to_copy_eq: + ! xs xi copied j2 st. + xi + LENGTH xs = xlen /\ + base = SUM (MAP LENGTH pre) /\ + LENGTH copied = xi /\ + LENGTH xs <= LENGTH j2 /\ + mk_st_eq ((copied ++ xs ++ oth) :: pre) szj j (copied ++ j2) st ==> + copy_to_copy base xi xlen st = + (M_success (), (mk_st ((copied ++ xs ++ oth) :: pre) szj j + (copied ++ xs ++ DROP (LENGTH xs) j2))) +Proof + Induct + \\ rw [] + \\ ONCE_REWRITE_TAC [copy_to_copy_def] + \\ rw [] + \\ mk_st_unfold + >- ( + simp [ml_monadBaseTheory.st_ex_return_def] + ) + >- ( + simp [st_ex_ignore_bind_simp, return_bind_eq] + \\ REWRITE_TAC [GSYM APPEND_ASSOC, APPEND] + \\ simp [main_array_sub_hd_app_cons_eq] + \\ simp [update_copy_array_eq] + \\ Cases_on `j2` \\ fs [] + \\ first_x_assum (qspec_then `spc ++ [x]` (assume_tac o Q.GENL [`spc`, `x`])) + \\ fs [] + \\ irule EQ_TRANS \\ first_x_assum (irule_at Any) + \\ simp [] + \\ irule_at Any mk_st_eqI + \\ irule_at Any mk_st_eq_mk_stI + \\ simp [] + ) +QED + +Theorem sz_array_sub_bind_eq: + LENGTH szj <= i /\ i - LENGTH szj < LENGTH xss ==> + st_ex_bind (sz_array_sub i) f (mk_st xss szj j c) = + f (LENGTH (EL (i - LENGTH szj) xss)) (mk_st xss szj j c) +Proof + rw [] + \\ irule bind_success_eqI + \\ simp [fetch "-" "sz_array_sub_def", ml_monadBaseTheory.monad_eqs] + \\ simp [mk_st_def, EL_APPEND2, EL_MAP] +QED + +Theorem update_sz_array_append_eq: + i = LENGTH szj + 1 /\ n = LENGTH xs + LENGTH ys ==> + update_sz_array i n (mk_st (ys :: xs :: pre) szj j c) = + (M_success (), mk_st ((xs ++ ys) :: pre) (szj ++ [LENGTH ys]) j c) +Proof + rw [] + \\ simp [fetch "-" "update_sz_array_def", ml_monadBaseTheory.monad_eqs] + \\ simp [mk_st_def, LUPDATE_APPEND1, LUPDATE_APPEND2, LUPDATE_DEF] +QED + +Theorem update_sz_array_append_bind_eq: + i = LENGTH szj + 1 /\ n = LENGTH xs + LENGTH ys ==> + st_ex_bind (update_sz_array i n) f (mk_st (ys :: xs :: pre) szj j c) = + f () (mk_st ((xs ++ ys) :: pre) (szj ++ [LENGTH ys]) j c) +Proof + rw [] + \\ irule bind_success_eqI + \\ simp [update_sz_array_append_eq] +QED + +Theorem update_sz_array_extend_eq: + i + 1 = LENGTH szj /\ n = LENGTH xs ==> + update_sz_array i n (mk_st xss szj (xs ++ j) c) = + (M_success (), mk_st (xs :: xss) (TAKE i szj) j c) +Proof + rw [] + \\ simp [fetch "-" "update_sz_array_def", ml_monadBaseTheory.monad_eqs] + \\ simp [mk_st_def, LUPDATE_APPEND1, LUPDATE_APPEND2, LUPDATE_DEF] + \\ irule LIST_EQ + \\ simp [EL_APPEND, EL_LUPDATE] + \\ rw [] + \\ simp [EL_TAKE] +QED + +Theorem update_sz_array_extend_bind_eq: + i + 1 = LENGTH szj /\ n = LENGTH xs ==> + st_ex_bind (update_sz_array i n) f (mk_st xss szj (xs ++ j) c) = + f () (mk_st (xs :: xss) (TAKE i szj) j c) +Proof + rw [] + \\ irule bind_success_eqI + \\ simp [update_sz_array_extend_eq] +QED + +Theorem do_merge_array_eq: + ri = LENGTH szj /\ + arri = LENGTH xs + LENGTH ys + SUM (MAP LENGTH pre) /\ + LENGTH xs <= LENGTH c ==> + do_merge_array R ri arri (mk_st (ys :: xs :: pre) szj j c) = + (M_success (), (mk_st (merge R xs ys :: pre) (szj ++ [LENGTH ys]) j + (xs ++ DROP (LENGTH xs) c))) +Proof + rw [do_merge_array_def] + \\ simp [st_ex_ignore_bind_simp, return_bind_eq] + \\ simp [sz_array_sub_bind_eq] + \\ simp [update_sz_array_append_bind_eq] + \\ irule bind_success_eqI + \\ irule_at Any copy_to_copy_eq + \\ irule_at Any mk_st_eqI + \\ csimp [APPEND_11_LENGTH] + \\ irule EQ_TRANS + \\ irule_at Any merge_runs_eq + \\ irule_at Any mk_st_eqI + \\ csimp [APPEND_11_LENGTH] +QED + +Definition add_lengths_def: + add_lengths xss = MAP (\xs. (LENGTH xs, xs)) xss +End + +Theorem add_lengths_simps[local]: + add_lengths [] = [] /\ + add_lengths (xs :: xss) = (LENGTH xs, xs) :: add_lengths xss /\ + MAP SND (add_lengths xss) = xss /\ + LENGTH (add_lengths xss) = LENGTH xss +Proof + simp [add_lengths_def, MAP_MAP_o, combinTheory.o_DEF] +QED + +Theorem add_lengths_MAP_SND_eq[local]: + EVERY (\(sz, xs). sz = LENGTH xs) xss ==> + add_lengths (MAP SND xss) = xss +Proof + rw [add_lengths_def, MAP_MAP_o] + \\ irule EQ_TRANS + \\ irule_at Any MAP_CONG + \\ simp [] + \\ qexists_tac `I` + \\ fs [EVERY_MEM, FORALL_PROD] +QED + +Definition is_eq_def: + is_eq x y = (x = y) +End + +Theorem is_eq_bind_successD: + is_eq (st_ex_bind f g st) r ==> + (?r'. is_eq (f st) r' /\ + (!x s. r' = (M_success x, s) ==> is_eq (g x s) r)) +Proof + rw [is_eq_def] + \\ simp [bind_success_eqI] +QED + +Theorem is_eq_bind_success_real_eqD: + is_eq (st_ex_bind f g st) r ==> + (!x s. f st = (M_success x, s) ==> is_eq (g x s) r) +Proof + rw [is_eq_def] + \\ simp [bind_success_eqI] +QED + +Theorem merge_length[local]: + LENGTH (merge R xs ys) = LENGTH xs + LENGTH ys +Proof + qspecl_then [`R`, `xs`, `ys`] mp_tac merge_perm + \\ rw [] + \\ imp_res_tac PERM_LENGTH + \\ fs [] +QED + +Theorem merge_sizes_gen_array_eq: + ! R f ri rlen arri xs xss szj j c r. + is_eq (merge_sizes_gen_array R f ri rlen arri + (mk_st (xs :: xss) szj j c)) r /\ + ri = LENGTH szj /\ ri + LENGTH xss + 1 = rlen /\ + arri = LENGTH xs + SUM (MAP LENGTH xss) /\ + arri <= LENGTH c ==> + ?szj2 c2. + let ys = merge_sizes f R (add_lengths xss) (LENGTH xs, xs) + in + r = (M_success (rlen - LENGTH ys), mk_st (MAP SND ys) (szj ++ szj2) j c2) /\ + LENGTH szj + LENGTH szj2 + LENGTH ys = rlen /\ LENGTH c2 = LENGTH c +Proof + recInduct merge_sizes_gen_array_ind + \\ rpt gen_tac \\ disch_tac + \\ ONCE_REWRITE_TAC [merge_sizes_gen_array_def] + \\ rw [] + >- ( + Cases_on `xss` \\ fs [] + \\ fs [is_eq_def, ml_monadBaseTheory.st_ex_return_def] + \\ rw [merge_sizes_def, add_lengths_simps] + \\ irule_at Any mk_st_eq_mk_stI + \\ simp [] + ) + >- ( + Cases_on `xss` \\ fs [] + \\ fs [st_ex_ignore_bind_simp, return_bind_eq] + \\ fs [sz_array_sub_bind_eq] + \\ simp [merge_sizes_def, add_lengths_simps] + \\ rw [] \\ fs [] + >- ( + dxrule is_eq_bind_success_real_eqD + \\ simp [do_merge_array_eq] + \\ rw [] + \\ first_x_assum (drule_then drule) + \\ simp [merge_length] + \\ rw [] + \\ irule_at Any mk_st_eq_mk_stI + \\ simp [] + ) + >- ( + fs [is_eq_def, ml_monadBaseTheory.st_ex_return_def] + \\ rw [] + \\ irule_at Any mk_st_eq_mk_stI + \\ simp [merge_sizes_def, add_lengths_simps] + ) + ) +QED + +Theorem merge_smaller_array_eq: + ! R n ri rlen arri. + merge_smaller_array R n ri rlen arri = + merge_sizes_gen_array R (\sz sz2. sz2 < n) ri rlen arri +Proof + recInduct merge_smaller_array_ind + \\ rw [] + \\ ONCE_REWRITE_TAC [merge_smaller_array_def] + \\ ONCE_REWRITE_TAC [merge_sizes_gen_array_def] + \\ rw [] + \\ rw [FUN_EQ_THM] + \\ simp [st_ex_bind_def |> Q.ISPEC `sz_array_sub i`] + \\ every_case_tac + \\ fs [fetch "-" "sz_array_sub_def", ml_monadBaseTheory.monad_eqs] + \\ res_tac + \\ simp [] +QED + +Theorem merge_similar_array_eq: + ! R ri rlen arri. + merge_similar_array R ri rlen arri = + merge_sizes_gen_array R (\sz sz2. ~ (sz * 2 < sz2)) ri rlen arri +Proof + recInduct merge_similar_array_ind + \\ rw [] + \\ ONCE_REWRITE_TAC [merge_similar_array_def] + \\ ONCE_REWRITE_TAC [merge_sizes_gen_array_def] + \\ rw [FUN_EQ_THM] + \\ simp [st_ex_bind_def |> Q.ISPEC `sz_array_sub i`] + \\ every_case_tac +QED + +Theorem merge_every_array_eq: + ! R ri rlen arri. + merge_every_array R ri rlen arri = + merge_sizes_gen_array R (\sz sz2. T) ri rlen arri +Proof + recInduct merge_every_array_ind + \\ rw [] + \\ ONCE_REWRITE_TAC [merge_every_array_def] + \\ ONCE_REWRITE_TAC [merge_sizes_gen_array_def] + \\ rw [FUN_EQ_THM] + \\ simp [st_ex_bind_def |> Q.ISPEC `sz_array_sub i`] + \\ every_case_tac + \\ fs [fetch "-" "sz_array_sub_def", ml_monadBaseTheory.monad_eqs] + \\ simp [do_merge_array_def] + \\ simp [st_ex_ignore_bind_simp, st_ex_bind_def] + \\ every_case_tac + \\ fs [fetch "-" "sz_array_sub_def", ml_monadBaseTheory.monad_eqs] +QED + +Overload mk_st_ret_xs[local] = + ``\xss szj j c rlen. (M_success (rlen - LENGTH xss), + mk_st xss szj j c)`` + +Theorem merge_sizes_same_length: + !xss sz_run. + SUM (MAP LENGTH (MAP SND (merge_sizes f R xss sz_run))) = + LENGTH (SND sz_run) + SUM (MAP LENGTH (MAP SND xss)) +Proof + Induct + \\ simp [merge_sizes_def] + \\ rw [] + \\ rpt (pairarg_tac \\ fs[]) + \\ simp [merge_length] +QED + +Theorem merge_in_run_array_eq: + is_eq (merge_in_run_array R ri rlen arri l + (mk_st xss szj (xs ++ j) c)) r /\ + ri = LENGTH szj /\ ri + LENGTH xss = rlen /\ + arri = SUM (MAP LENGTH xss) /\ + arri + LENGTH xs <= LENGTH c /\ l = LENGTH xs /\ + EVERY ($~ o NULL) xss /\ + 0 < ri /\ 0 < l + ==> + ?szj2 c2. + r = mk_st_ret_xs (MAP SND (merge_in_run R (add_lengths xss) xs)) + szj2 j c2 rlen /\ + LENGTH szj2 + LENGTH (merge_in_run R (add_lengths xss) xs) = rlen /\ + LENGTH c2 = LENGTH c +Proof + rpt strip_tac + \\ fs [merge_in_run_array_def, merge_in_run_def] + \\ Cases_on `xs = []` \\ fs [] + \\ qmatch_goalsub_abbrev_tac `merge_sizes _ _ merge_smaller_step` + \\ subgoal `SUM (MAP LENGTH (MAP SND merge_smaller_step)) = + SUM (MAP LENGTH xss) /\ + add_lengths (MAP SND merge_smaller_step) = merge_smaller_step` + >- ( + fs [markerTheory.Abbrev_def] + \\ Cases_on `TL xss` \\ Cases_on `xss` \\ fs [add_lengths_simps] + \\ rw [] \\ fs [add_lengths_simps] + \\ simp [merge_sizes_same_length, add_lengths_simps] + \\ irule add_lengths_MAP_SND_eq + \\ irule MONO_EVERY + \\ irule_at Any (merge_sizes_eq_length_inv) + \\ simp [FORALL_PROD] + \\ simp [add_lengths_def, EVERY_MAP] + \\ fs [combinTheory.o_DEF] + ) + \\ dxrule is_eq_bind_successD + \\ strip_tac + \\ subgoal `?szj3 c3. r' = mk_st_ret_xs (MAP SND merge_smaller_step) + szj3 (xs ++ j) c3 rlen /\ + LENGTH szj3 + LENGTH merge_smaller_step = rlen /\ + 0 < LENGTH szj3 /\ LENGTH c3 = LENGTH c` + >- ( + Cases_on `LENGTH xss < 2 \/ LENGTH (EL 1 xss) >= LENGTH xs` + >- ( + Cases_on `TL xss` \\ Cases_on `xss` \\ fs [] + \\ fs [markerTheory.Abbrev_def] + \\ gs [add_lengths_simps, is_eq_def, ml_monadBaseTheory.st_ex_return_def] + \\ rw [] + \\ simp [sz_array_sub_bind_eq] + \\ irule_at Any mk_st_eq_mk_stI + \\ simp [] + ) + \\ Cases_on `TL xss` \\ Cases_on `xss` \\ fs [] + \\ fs [markerTheory.Abbrev_def] + \\ gs [add_lengths_simps, sz_array_sub_bind_eq] + \\ fs [merge_smaller_array_eq] + \\ dxrule merge_sizes_gen_array_eq + \\ rw [] + \\ irule_at Any mk_st_eq_mk_stI + \\ gs [add_lengths_simps] + ) + \\ fs [] + \\ qpat_x_assum `is_eq _ (M_success _, _)` kall_tac + \\ qpat_x_assum `is_eq _ _` mp_tac + \\ simp [st_ex_ignore_bind_simp, return_bind_eq] + \\ simp [update_sz_array_extend_bind_eq] + \\ simp [merge_similar_array_eq] + \\ disch_tac \\ dxrule merge_sizes_gen_array_eq + \\ simp [add_lengths_simps] + \\ rw [] + \\ irule_at Any mk_st_eq_mk_stI + \\ gs [add_lengths_simps] +QED + +Theorem find_known_run_array_eq: + ! R x b n i arrlen xs xss szj ys c st. + n = LENGTH xs /\ i = LENGTH xs + SUM (MAP LENGTH xss) /\ + i + LENGTH ys = arrlen /\ + mk_st_eq xss szj (REVERSE xs ++ ys) c st ==> + find_known_run_array R x b n i arrlen st = + (M_success (n + count_while_2 (\x y. R x y = b) (x :: ys) - 1), + mk_st xss szj (REVERSE xs ++ ys) c) +Proof + recInduct find_known_run_array_ind + \\ rw [] + \\ ONCE_REWRITE_TAC [find_known_run_array_def] + \\ mk_st_unfold + \\ Cases_on `ys` \\ fs [] + >- ( + simp [ml_monadBaseTheory.st_ex_return_def] + \\ simp [count_while_2_def] + ) + >- ( + simp [main_array_sub_extra] + \\ TOP_CASE_TAC + >- ( + first_x_assum drule + \\ disch_then (qspec_then `z :: zs` (mp_tac o Q.GENL [`z`, `zs`])) + \\ simp [ADD1] + \\ disch_tac + \\ irule EQ_TRANS + \\ pop_assum (irule_at Any) + \\ simp [] + \\ irule_at Any mk_st_eqI + \\ simp [count_while_2_def] + \\ REWRITE_TAC [GSYM APPEND_ASSOC, APPEND] + ) + >- ( + simp [ml_monadBaseTheory.st_ex_return_def] + \\ simp [count_while_2_def] + ) + ) +QED + +Theorem find_known_run_array_eq_2[local] = + find_known_run_array_eq |> SPEC_ALL |> Q.GEN `xs` + |> Q.SPEC `[x; y]` |> GEN_ALL + +Theorem reverse_run_eq: + !i l xs ys st. + i = SUM (MAP LENGTH xss) + LENGTH xs /\ + l <= LENGTH ys /\ + mk_st_eq xss szj (xs ++ ys) c st ==> + reverse_run i l st = + (M_success (), mk_st xss szj (xs ++ REVERSE (TAKE l ys) ++ DROP l ys) c) +Proof + recInduct reverse_run_ind + \\ rw [] + \\ ONCE_REWRITE_TAC [reverse_run_def] + \\ mk_st_unfold + \\ rw [] + >- ( + simp [ml_monadBaseTheory.st_ex_return_def] + \\ irule mk_st_eq_mk_stI + \\ simp [] + \\ subgoal `REVERSE (TAKE l ys) = TAKE l ys` \\ simp [] + \\ Cases_on `TL ys` \\ Cases_on `ys` \\ fs [] + \\ rw [TAKE_def] + ) + >- ( + qspecl_then [`ys`, `l - 1`] mp_tac LESS_LENGTH + \\ rw [] + \\ simp [main_array_sub_extra_EL, return_bind_eq, EL_APPEND2, EL_APPEND1] + \\ simp [TAKE_APPEND1, DROP_APPEND2, TAKE_LENGTH_TOO_LONG, REVERSE_APPEND] + \\ Cases_on `ys1` \\ fs [] + \\ simp [st_ex_ignore_bind_simp] + \\ simp [update_main_array_extra_LUPDATE, LUPDATE_APPEND1, + LUPDATE_APPEND2, LUPDATE_DEF] + \\ first_x_assum (qspec_then `zs ++ [z]` (mp_tac o Q.GENL [`z`, `zs`])) + \\ rw [ADD1] + \\ irule EQ_TRANS \\ first_x_assum (irule_at Any) + \\ simp [] + \\ irule_at Any mk_st_eqI + \\ irule_at Any mk_st_eq_mk_stI + \\ simp [DROP_APPEND1, TAKE_APPEND1, TAKE_LENGTH_TOO_LONG] + ) +QED + +Theorem count_while_2_length_trans[local]: + LENGTH xs <= n ==> + count_while_2 R xs <= n +Proof + metis_tac [count_while_2_length, LE_TRANS] +QED + +Theorem find_run_array_eq: + i = SUM (MAP LENGTH xss) /\ + i + LENGTH ys = arrlen /\ + mk_st_eq xss szj ys c st ==> + find_run_array R i arrlen st = + (M_success (LENGTH (FST (find_run R ys))), + mk_st xss szj (FST (find_run R ys) ++ SND (find_run R ys)) c) +Proof + rw [find_run_array_def] + \\ mk_st_unfold + >- ( + simp [ml_monadBaseTheory.st_ex_return_def] + \\ Cases_on `TL ys` \\ Cases_on `ys` \\ fs [ADD1] + \\ simp [find_run_def] + ) + \\ Cases_on `TL ys` \\ Cases_on `ys` \\ fs [ADD1] + \\ simp [main_array_sub_extra |> Q.SPEC `[]` |> SIMP_RULE list_ss [], + main_array_sub_extra |> Q.SPEC `[x]` |> SIMP_RULE list_ss []] + \\ simp [st_ex_ignore_bind_simp, return_bind_eq] + \\ irule bind_success_eqI + \\ irule_at Any find_known_run_array_eq_2 + \\ simp [] + \\ irule_at Any mk_st_eqI + \\ simp [] + \\ rw [] + >- ( + irule bind_success_eqI + \\ irule_at Any reverse_run_eq + \\ simp [ml_monadBaseTheory.st_ex_return_def] + \\ irule_at Any mk_st_eqI + \\ simp [] + \\ simp [find_run_eq_count, ADD1, LENGTH_TAKE_EQ] + \\ csimp [] + \\ simp [count_while_2_length_trans] + ) + >- ( + simp [return_bind_eq] + \\ simp [ml_monadBaseTheory.st_ex_return_def] + \\ simp [find_run_eq_count, ADD1, LENGTH_TAKE_EQ] + \\ simp [count_while_2_length_trans] + ) +QED + +Theorem FST_find_run_neq_nil[local]: + xs <> [] ==> FST (find_run R xs) <> [] +Proof + Cases_on `TL xs` \\ Cases_on `xs` \\ fs [] + \\ simp [find_run_eq_count] + \\ simp [find_run_def] + \\ rw [] +QED + +Theorem merge_in_run_total_length: + SUM (MAP (LENGTH o SND) (merge_in_run R xs r)) = + SUM (MAP (LENGTH o SND) xs) + LENGTH r +Proof + qspecl_then [`R`, `r`, `xs`] mp_tac (GEN_ALL merge_in_run_perm) + \\ rw [] + \\ imp_res_tac PERM_LENGTH + \\ fs [LENGTH_FLAT, MAP_MAP_o] +QED + +Theorem merge_in_run_MAP_SND_invs[local]: + EVERY ($¬ ∘ NULL) xss /\ SORTED (\a b. 2 * LENGTH a < LENGTH b) xss ==> + EVERY ($¬ ∘ NULL) (MAP SND (merge_in_run R (add_lengths xss) r)) /\ + SORTED (\a b. 2 * LENGTH a < LENGTH b) + (MAP SND (merge_in_run R (add_lengths xss) r)) +Proof + strip_tac + \\ qspecl_then [`r`, `add_lengths xss`, `R`] mp_tac + (GEN_ALL merge_in_run_eq_length_inv) + \\ impl_tac + >- ( + fs [add_lengths_def, EVERY_MAP, FORALL_PROD, o_DEF] + ) + \\ rw [] + >- ( + fs [EVERY_MEM, MEM_MAP, FORALL_PROD, EXISTS_PROD] + ) + >- ( + simp [sorted_map] + \\ irule SORTED_weaken + \\ irule_at Any (REWRITE_RULE [sorted_map] merge_in_run_size_invariant) + \\ simp [FORALL_PROD, EVERY_MAP, add_lengths_def, sorted_map, inv_image_def] + \\ fs [o_DEF] + \\ rw [] + \\ fs [EVERY_MEM, FORALL_PROD, add_lengths_def] + \\ res_tac + \\ simp [] + ) +QED + +Theorem find_runs_neq_nil_def[local]: + xs <> [] ==> + find_runs R xs = FST (find_run R xs) :: find_runs R (SND (find_run R xs)) +Proof + Cases_on `xs` + \\ simp [find_runs_def] + \\ pairarg_tac \\ simp [] +QED + +Theorem size_invariant_imp_sum_ineq: + SORTED (λa b. 2 * LENGTH a < LENGTH b) xss /\ + xss <> [] /\ HD xss <> [] ==> + 2 ** (LENGTH xss - 1) <= SUM (MAP LENGTH xss) +Proof + rw [] + \\ subgoal `!n. n < LENGTH xss ==> LENGTH (EL n xss) >= (2 ** n) * LENGTH (HD xss)` + >- ( + Induct + \\ rw [] + \\ fs [] + \\ imp_res_tac SORTED_EL_SUC + \\ fs [EXP] + ) + \\ qspec_then `xss` mp_tac SNOC_CASES + \\ first_x_assum (qspec_then `LENGTH xss - 1` mp_tac) + \\ Cases_on `HD xss` + \\ rw [] + \\ fs [MAP_SNOC, SUM_SNOC, EL_LENGTH_SNOC, ADD1] +QED + +Theorem first_pass_array_eq: + ! R ri rlen i_param arrlen i xss szj ys c r. + is_eq (first_pass_array R ri rlen i arrlen (mk_st xss szj ys c)) r /\ + is_eq ri (LENGTH szj) /\ is_eq (ri + LENGTH xss) rlen /\ + is_eq i (SUM (MAP LENGTH xss)) /\ + is_eq i_param i /\ + is_eq (i + LENGTH ys) arrlen /\ + LENGTH c = arrlen /\ + EVERY ($~ o NULL) xss /\ + SORTED (\a b. LENGTH a * 2 < LENGTH b) xss /\ + arrlen < 2 ** (rlen - 1) + ==> + ?szj2 c2. + r = mk_st_ret_xs (MAP SND (FOLDL (merge_in_run R) (add_lengths xss) (find_runs R ys))) + szj2 [] c2 rlen /\ + LENGTH szj2 + LENGTH (FOLDL (merge_in_run R) (add_lengths xss) (find_runs R ys)) = rlen /\ + LENGTH c2 = arrlen +Proof + recInduct first_pass_array_ind + \\ rpt gen_tac \\ disch_tac + \\ ONCE_REWRITE_TAC [first_pass_array_def] + \\ rw [] \\ fs [] + >- ( + fs [is_eq_def, ml_monadBaseTheory.st_ex_return_def] + \\ rw [] + \\ Cases_on `ys` \\ fs [] + \\ simp [find_runs_def, add_lengths_simps] + \\ irule_at Any mk_st_eq_mk_stI + \\ simp [] + ) + \\ dxrule is_eq_bind_success_real_eqD + \\ rpt (qpat_x_assum `is_eq _ _` (assume_tac o REWRITE_RULE [is_eq_def])) + \\ dep_rewrite.DEP_REWRITE_TAC [find_run_array_eq] + \\ simp [mk_st_eqI] + \\ strip_tac + \\ dxrule is_eq_bind_successD + \\ strip_tac + \\ dxrule merge_in_run_array_eq + \\ simp [LENGTH_NOT_NULL, NULL_EQ, FST_find_run_neq_nil] + \\ Cases_on `ys = []` \\ fs [] + \\ impl_tac + >- ( + qspecl_then [`R`, `ys`] mp_tac find_run_length_fst + \\ rw [FST_find_run_neq_nil] + \\ CCONTR_TAC \\ fs [] + \\ gs [] + \\ imp_res_tac size_invariant_imp_sum_ineq + \\ Cases_on `xss` \\ fs [] + \\ gs [NULL_EQ] + ) + \\ strip_tac + \\ simp [find_runs_neq_nil_def] + \\ fs [] + \\ first_x_assum drule + \\ simp [is_eq_def, FST_find_run_neq_nil] + \\ disch_then (qspec_then `LENGTH (FST (find_run R ys))` mp_tac) + \\ simp [FST_find_run_neq_nil] + \\ impl_tac + >- ( + simp [merge_in_run_total_length, MAP_MAP_o] + \\ simp [GSYM MAP_MAP_o, add_lengths_simps] + \\ simp [merge_in_run_MAP_SND_invs] + \\ qspecl_then [`R`, `ys`] mp_tac find_run_length_fst + \\ simp [find_run_length_eq_sub] + ) + \\ rw [] + \\ simp [add_lengths_simps, add_lengths_MAP_SND_eq] + \\ dep_rewrite.DEP_REWRITE_TAC [add_lengths_MAP_SND_eq] + \\ conj_asm1_tac + >- ( + irule MONO_EVERY + \\ irule_at Any merge_in_run_eq_length_inv + \\ simp [FORALL_PROD] + \\ simp [add_lengths_def, EVERY_MAP] + \\ fs [o_DEF] + ) + \\ irule_at Any mk_st_eq_mk_stI + \\ fs [add_lengths_MAP_SND_eq] +QED + +Theorem merge_sizes_T_eq_sing[local]: + !xss sz_run. ?x. merge_sizes (\_ _. T) R xss sz_run = [x] +Proof + Induct + \\ simp [merge_sizes_def] +QED + +Theorem merge_run_sort_monadic_eq: + arrlen = LENGTH ys /\ rlen = LENGTH szj /\ LENGTH c = arrlen /\ + ys <> [] /\ LENGTH ys < 2 ** (LENGTH szj − 1) ==> + ?szj2 c2. + merge_run_sort_monadic R rlen arrlen + (mk_st [] szj ys c) = + (M_success (), mk_st [merge_run_sort R ys] szj2 [] c2) +Proof + rw [] + \\ qmatch_goalsub_abbrev_tac `res = (_, _)` + \\ subgoal `?r. is_eq res r` + >- ( + simp [is_eq_def] + ) + \\ first_assum (simp o single o REWRITE_RULE [is_eq_def]) + \\ gs [markerTheory.Abbrev_def] + \\ fs [merge_run_sort_monadic_def] + \\ dxrule is_eq_bind_successD + \\ rw [] + \\ dxrule first_pass_array_eq + \\ simp [is_eq_def] + \\ rw [] + \\ fs [st_ex_ignore_bind_simp, merge_every_array_eq] + \\ dxrule is_eq_bind_successD + \\ rw [] + \\ fs [add_lengths_simps] + \\ qspecl_then [`ys`, `R`] mp_tac (GEN_ALL first_pass_size_invariant) + \\ Cases_on `first_pass R ys` + >- ( + qspecl_then [`R`, `ys`] mp_tac first_pass_perm + \\ simp [first_pass_def] + ) + \\ fs [first_pass_def] + \\ rw [] + \\ dxrule merge_sizes_gen_array_eq + \\ simp [] + \\ impl_tac + >- ( + qspecl_then [`R`, `ys`] mp_tac first_pass_perm + \\ rw [first_pass_def] + \\ drule PERM_LENGTH + \\ simp [LENGTH_FLAT] + ) + \\ rw [] + \\ fs [is_eq_def, ml_monadBaseTheory.st_ex_return_def] + \\ rw [] + \\ irule_at Any mk_st_eq_mk_stI + \\ simp [merge_run_sort_def, first_pass_def, merge_sizes_def] + \\ dep_rewrite.DEP_REWRITE_TAC [add_lengths_MAP_SND_eq] + \\ simp [merge_empty] + \\ pairarg_tac \\ fs [] + \\ csimp [] + \\ drule_at_then Any (irule_at Any) MONO_EVERY + \\ simp [FORALL_PROD, merge_sizes_T_eq_sing] +QED + +Theorem copy_into_array_eq: + !xs i ys. + i + LENGTH xs = LENGTH ys ==> + copy_into_array i xs (mk_st [] szj ys c) = + (M_success (), mk_st [] szj (TAKE i ys ++ xs) c) +Proof + Induct + \\ simp [copy_into_array_def, ml_monadBaseTheory.st_ex_return_def] + \\ simp [st_ex_ignore_bind_simp] + \\ rw [] + \\ fs [ADD1] + \\ qspecl_then [`ys`, `i`] mp_tac LESS_LENGTH + \\ rw [] + \\ fs [] + \\ simp [update_main_array_extra_LUPDATE, LUPDATE_APPEND1, + LUPDATE_APPEND2, LUPDATE_DEF, TAKE_APPEND1, TAKE_APPEND2] + \\ irule mk_st_eq_mk_stI + \\ simp [] +QED + +Theorem copy_from_array_eq: + !i xs ys. + i <= LENGTH st.main_array ==> + copy_from_array i xs st = + (M_success (TAKE i st.main_array ++ xs), st) +Proof + recInduct copy_from_array_ind + \\ rw [] + \\ ONCE_REWRITE_TAC [copy_from_array_def] + \\ rw [] + \\ simp [ml_monadBaseTheory.st_ex_return_def] + \\ simp [fetch "-" "main_array_sub_def", ml_monadBaseTheory.monad_eqs] + \\ Cases_on `i` \\ fs [] + \\ simp [ADD1, TAKE_EL_SNOC] +QED + +Theorem above_log2_is_above_ind[local]: + ! i v n. n = 2 EXP i ==> v <= 2 ** (above_log2 i v n) +Proof + recInduct above_log2_ind + \\ rw [] \\ fs [] + \\ ONCE_REWRITE_TAC [above_log2_def] + \\ rw [] \\ fs [EXP_ADD] +QED + +Theorem merge_run_sort_worker_eq: + xs <> [] ==> + ?szj2 c2. + merge_run_sort_worker R x xs st = + (M_success (merge_run_sort R xs), mk_st [merge_run_sort R xs] szj2 [] c2) +Proof + rw [merge_run_sort_worker_def] + \\ simp [st_ex_ignore_bind_simp, return_bind_eq] + \\ simp [fetch "-" "alloc_main_array_def", fetch "-" "alloc_sz_array_def", + fetch "-" "alloc_copy_array_def", ml_monadBaseTheory.monad_eqs] + \\ simp [GSYM (mk_st_def |> Q.SPEC `[]` |> SIMP_RULE (srw_ss ()) [])] + \\ simp [copy_into_array_eq] + \\ qmatch_goalsub_abbrev_tac + `merge_run_sort_monadic R rlen arrlen (mk_st _ szj _ c)` + \\ qspec_then `xs` mp_tac (Q.GEN `ys` merge_run_sort_monadic_eq) + \\ fs [markerTheory.Abbrev_def] + \\ impl_tac + >- ( + qspecl_then [`0`, `LENGTH xs + 1`, `1`] assume_tac above_log2_is_above_ind + \\ fs [REWRITE_RULE [ADD1] EXP] + ) + \\ rw [] + \\ subgoal `LENGTH xs = LENGTH (merge_run_sort R xs)` + >- ( + irule PERM_LENGTH + \\ irule merge_run_sort_perm + ) + \\ simp [copy_from_array_eq, mk_st_def] +QED + + diff --git a/translator/monadic/examples/in_array_sorts/merge_run_sort_translationScript.sml b/translator/monadic/examples/in_array_sorts/merge_run_sort_translationScript.sml new file mode 100644 index 0000000000..5789d60dab --- /dev/null +++ b/translator/monadic/examples/in_array_sorts/merge_run_sort_translationScript.sml @@ -0,0 +1,169 @@ +(* + Post-translation of merge_run_sort +*) +Theory merge_run_sort_translation +Ancestors + mergesort std_prelude mllist ml_translator merge_run_sort_monadic +Libs + preamble ml_translatorLib ml_progLib + ml_monad_translator_interfaceLib + +val _ = ml_prog_update (open_module "Sort_Post_Translation"); + +val () = generate_sigs := true; + +(* Little bits of List translation that might be needed. *) + +val r = translate NULL; + +val _ = ml_prog_update open_local_block; +val res = translate LENGTH_AUX_def; +val _ = ml_prog_update open_local_in_block; + +val result = next_ml_names := ["length"] +val res = translate LENGTH_AUX_THM; + +val _ = ml_prog_update close_local_block; + +val _ = ml_prog_update open_local_block; + +val tvar = ``: 'el``; + +val state_type = ``: ( ^tvar ) merge_run_state``; + +val subs = ``MR_Subscript`` + +val exn_type = type_of subs; + +val config = local_state_config |> + with_state state_type |> + with_exception exn_type |> + with_resizeable_arrays [ + ("main_array", listSyntax.mk_list ([], tvar), subs, subs), + ("copy_array", listSyntax.mk_list ([], tvar), subs, subs), + ("sz_array", ``[] : num list``, subs, subs) + ]; + +val _ = start_translation config; + +(* Some clunking around to translate the accessors as auto-defined in + heap_list_sort_monadicTheory using their counterparts auto-defined above. *) +val heap_list_acc_def_names = ["main_array_sub_def", "update_main_array_def", + "alloc_main_array_def", "sz_array_sub_def", "update_sz_array_def", + "alloc_sz_array_def", "copy_array_sub_def", "update_copy_array_def", + "alloc_copy_array_def"] + +val configured_acc_defs = map (fetch "-") heap_list_acc_def_names; +val previous_acc_defs = map (fetch "merge_run_sort_monadic") heap_list_acc_def_names; +val redefs = previous_acc_defs + |> map (REWRITE_RULE (map GSYM configured_acc_defs)) +val do_redef = REWRITE_RULE redefs + +(* Translate all monadic defs. *) + +val merge_runs_v_thm = merge_runs_def + |> do_redef |> m_translate; + +val copy_to_copy_v_thm = copy_to_copy_def + |> do_redef |> m_translate; + +(* Include a check in the translation of the subtraction in do_merge_array. + There is an invariant (arri = SUM (DROP ri) st.sz_array) that proves the + subtraction is safe, but that invariant would have to be maintained + through all the other functions here. *) +val _ = (ml_translatorLib.use_sub_check true); +val do_merge_array_v_thm = do_merge_array_def + |> do_redef |> m_translate; +val _ = (ml_translatorLib.use_sub_check false); + +val merge_smaller_array_v_thm = merge_smaller_array_def + |> do_redef |> m_translate; + +val merge_similar_array_v_thm = merge_similar_array_def + |> do_redef |> m_translate; + +val merge_every_array_v_thm = merge_every_array_def + |> do_redef |> m_translate; + +val merge_in_run_array_v_thm = merge_in_run_array_def + |> do_redef |> m_translate; + +val find_known_run_array_v_thm = find_known_run_array_def + |> do_redef |> m_translate; + +val reverse_run_v_thm = reverse_run_def + |> do_redef |> m_translate; + +val find_run_array_v_thm = find_run_array_def + |> do_redef |> m_translate; + +val first_pass_array_v_thm = first_pass_array_def + |> do_redef |> m_translate; + +val merge_run_sort_monadic_v_thm = merge_run_sort_monadic_def + |> do_redef |> m_translate; + +val above_log2_v_thm = above_log2_def + |> translate; + +val copy_into_array_v_thm = copy_into_array_def + |> do_redef |> m_translate; + +val copy_from_array_v_thm = copy_from_array_def + |> do_redef |> m_translate; + +val merge_run_sort_worker_v_thm = merge_run_sort_worker_def + |> do_redef |> m_translate; + +(* Set up the "run" mechanism. *) +val run_init_merge_run_state_def = + define_run state_type [] "init_merge_run_state"; + +Definition sort_via_merge_run_sort_worker_def: + sort_via_merge_run_sort_worker R x xs = + run_init_merge_run_state (merge_run_sort_worker R x xs) + (init_merge_run_state [] [] []) +End + +val run_v_thm = sort_via_merge_run_sort_worker_def + |> m_translate_run; + +Definition sort_via_array_merge_def: + sort_via_array_merge R xs = (case xs of [] => [] + | x :: _ => (case sort_via_merge_run_sort_worker R x xs of + M_success ys => ys + | _ => []) + ) +End + +val sort_via_array_merge_v_thm = sort_via_array_merge_def |> translate; + +(* Done monadic translation. *) + +val _ = ml_translatorLib.use_sub_check false; + +Theorem merge_run_sort_worker_eq_FST[local]: + xs <> [] ==> + FST (merge_run_sort_worker R x xs st) = + (M_success (merge_run_sort R xs)) +Proof + mp_tac merge_run_sort_worker_eq + \\ rw [] \\ fs [] +QED + +Theorem merge_run_sort_eq_sort_via_array_merge: + merge_run_sort R xs = sort_via_array_merge R xs +Proof + simp [sort_via_array_merge_def] + \\ Cases_on `xs` \\ simp [EVAL ``(merge_run_sort R [])``] + \\ simp [sort_via_merge_run_sort_worker_def, + run_init_merge_run_state_def, ml_monadBaseTheory.run_def] + \\ simp [merge_run_sort_worker_eq_FST] +QED + +val _ = ml_prog_update open_local_in_block; + +val merge_run_sort_v_thm = merge_run_sort_eq_sort_via_array_merge |> translate; + +val _ = ml_prog_update close_local_block; + diff --git a/translator/monadic/examples/in_array_sorts/readmePrefix b/translator/monadic/examples/in_array_sorts/readmePrefix new file mode 100644 index 0000000000..59d119d672 --- /dev/null +++ b/translator/monadic/examples/in_array_sorts/readmePrefix @@ -0,0 +1,6 @@ +Example applications of the monadic translator on in-array sort functions. + +These sort functions generally have a pure (datatype recursive) instance, a +monadic theory that provides an in-array version and proves that it simulates +the pure computation, and finally a translation theory that translates the +monadic code to CakeML AST. diff --git a/translator/monadic/ml_monadStoreLib.sml b/translator/monadic/ml_monadStoreLib.sml index 21d8719186..b93577bd43 100644 --- a/translator/monadic/ml_monadStoreLib.sml +++ b/translator/monadic/ml_monadStoreLib.sml @@ -114,7 +114,14 @@ fun mk_get_refs state = let val get_refs = mk_comb(get_refs, state) |> BETA_CONV |> concl |> rand in get_refs end - +(* wrap ISPECL to give more detailed error. *) +fun ISPECL terms thm = Drule.ISPECL terms thm + handle HOL_ERR err => ( + print "ISPECL failed:\n"; + List.app print_term terms; + print_thm thm; + Drule.ISPECL terms thm + ) fun mk_REF_REL TYPE r x = ISPECL [TYPE, r, x] REF_REL_def |> concl |> dest_eq |> fst @@ -1008,6 +1015,8 @@ fun prove_store_access_specs refs_manip_list in (eval_th, true) end handle HOL_ERR _ => (TRUTH, false) + (* Handle annoying situations where ``\st. st with <| arr := xs |>`` + gets type ``: 'a state => 'b state``. FIXME: same fix for farray? *) val set_subst = let val set_type = type_of set_arr |> dom_rng |> snd |> dom_rng in match_type (snd set_type) (fst set_type) end @@ -1024,7 +1033,7 @@ fun prove_store_access_specs refs_manip_list in rewrite_thm th end else let val th = - ISPECL[name_v,loc,TYPE,EXN_TYPE,H_part,get_arr,set_arr, + ISPECL[name_v,loc,TYPE,EXN_TYPE,H_part,get_arr,set_arr', update_exn,update_rexp] EvalM_R_Marray_update_handle val th = SPEC_ALL th |> UNDISCH |> UNDISCH val th = remove_assumption th |> remove_assumption diff --git a/translator/monadic/ml_monad_translatorLib.sml b/translator/monadic/ml_monad_translatorLib.sml index 21489094b1..30995985da 100644 --- a/translator/monadic/ml_monad_translatorLib.sml +++ b/translator/monadic/ml_monad_translatorLib.sml @@ -2938,53 +2938,39 @@ fun abbrev_code (fname,ml_fname,def,th,v) = let (* Some definitions might have polymorphic state and exceptions: those types need to be instantiated before translation *) -fun instantiate_monadic_types def = let - val original_def = def - (* Retrieve the state and exceptions types *) - val def = List.hd (CONJUNCTS def) - val ty = concl def |> strip_forall |> snd |> rhs |> type_of - val state_ty = dest_type ty |> snd |> List.hd - val exn_ty = dest_type ty |> snd |> List.last |> dest_type |> snd |> - List.hd |> dest_type |> snd |> List.last - (* Instantiate them to the proper types *) - val def = - if is_vartype state_ty then - let - val def = Thm.INST_TYPE[state_ty |-> !(#refs_type translator_state)] - original_def - in - print "Instantiated polymorphic monadic state\n"; - def - end - else original_def - - val def = - if is_vartype exn_ty then - let - val def = Thm.INST_TYPE [exn_ty |-> !(#exn_type translator_state)] def - in - print "Instantiated polymorphic monadic exceptions\n"; - def - end - else def -in def end; - fun get_monadic_types_inst tm = let (* Retrieve the state and exceptions types *) val ty = type_of tm val state_ty = dest_type ty |> snd |> List.hd val exn_ty = dest_type ty |> snd |> List.last |> dest_type |> snd |> List.hd |> dest_type |> snd |> List.last - (* Instantiate them to the proper types *) - val tys = - if is_vartype state_ty then - [state_ty |-> !(#refs_type translator_state)] - else [] - val tys = - if is_vartype exn_ty - then (exn_ty |-> !(#exn_type translator_state)) :: tys - else tys -in tys end; + + fun print_inst inst = let + val strs = commafy (map (fn i => type_to_string (#redex i) ^ + " |-> " ^ type_to_string (#residue i)) inst) + in print (String.concat (strs @ ["\n"])) end + + val ref_state_ty = !(#refs_type translator_state) + val inst1 = case total (match_type state_ty) ref_state_ty of + SOME [] => [] + | SOME inst => (print "Instantiating polymorphic monadic state\n"; print_inst inst; inst) + | NONE => (print "Warning: no match on state type\n"; []) + + val ref_exn_ty = !(#exn_type translator_state) + val inst2 = case total (match_type exn_ty) ref_exn_ty of + SOME [] => [] + | SOME inst => (print "Instantiating polymorphic exception state\n"; print_inst inst; inst) + | NONE => (print "Warning: no match on exception type\n"; []) +in inst1 @ inst2 end; + +fun instantiate_monadic_types def = let + val original_def = def + + val def = List.hd (CONJUNCTS def) + val tm = concl def |> strip_forall |> snd |> rhs + val inst = get_monadic_types_inst tm + +in Thm.INST_TYPE inst original_def end; (****************************************************************************** diff --git a/translator/monadic/ml_monad_translator_interfaceLib.sig b/translator/monadic/ml_monad_translator_interfaceLib.sig index 7d9b8a6c03..5fe5af92df 100644 --- a/translator/monadic/ml_monad_translator_interfaceLib.sig +++ b/translator/monadic/ml_monad_translator_interfaceLib.sig @@ -47,6 +47,9 @@ signature ml_monad_translator_interfaceLib = sig + (* Sets up monadic syntax, Less invasive than the full version. *) + val minimal_set_up_monadic_translator : unit -> unit + val set_up_monadic_translator : unit -> unit type term = Term.term diff --git a/translator/monadic/ml_monad_translator_interfaceLib.sml b/translator/monadic/ml_monad_translator_interfaceLib.sml index 307d7a575d..a7669c24ef 100644 --- a/translator/monadic/ml_monad_translator_interfaceLib.sml +++ b/translator/monadic/ml_monad_translator_interfaceLib.sml @@ -15,9 +15,13 @@ open preamble ml_monadBaseLib ml_monadStoreLib ml_monad_translatorLib ******************************************************************************) -fun set_up_monadic_translator () = let +(* Sidestep setting up "syntax" libraries, fetch const from def. *) +fun left_const thm = concl thm + |> strip_conj |> hd |> strip_forall |> snd |> lhs + |> strip_comb |> fst + +fun minimal_set_up_monadic_translator () = let (* Add monadic syntax: do x <- f y; ... od *) - val _ = ParseExtras.temp_loose_equality(); val _ = monadsyntax.temp_add_monadsyntax() (* Parser overloadings *) @@ -25,6 +29,15 @@ fun set_up_monadic_translator () = let val _ = Parse.temp_overload_on("monad_unitbind",ml_monadBaseSyntax.st_ex_ignore_bind_tm); val _ = Parse.temp_overload_on("monad_ignore_bind",ml_monadBaseSyntax.st_ex_ignore_bind_tm); val _ = Parse.temp_overload_on("return",ml_monadBaseSyntax.st_ex_return_tm); + val _ = Parse.temp_overload_on("monad_ignore_bind", ign_c); + val _ = Parse.temp_overload_on("return", left_const st_ex_return_def); +in () end + +fun set_up_monadic_translator () = let + (* Take all steps taken by a previous version. *) + val _ = ParseExtras.temp_loose_equality(); + + val _ = minimal_set_up_monadic_translator(); (* Hide "state" due to semanticPrimitives *) val _ = hide "state"; @@ -39,7 +52,7 @@ in () end ******************************************************************************) -fun toUppers(str) = String.implode (map Char.toUpper (String.explode str)); +val unit_ty = type_of (left_const oneTheory.one_DEF); val unit_ty = oneSyntax.one_ty; @@ -56,8 +69,6 @@ datatype translator_mode = GLOBAL | LOCAL; type state = { state_access_funs : (string * thm * thm) list ref, (* (name, get, set) *) - store_invariant_name : string ref, - store_exn_invariant_name : string ref, exn_type_def : thm ref, additional_type_theories : string list ref, hprop_field_names : (term * string) list ref, @@ -71,8 +82,6 @@ type state = { (* Initial internal state *) val internal_state : state = { state_access_funs = ref [], - store_invariant_name = ref "STATE_STORE", - store_exn_invariant_name = ref "STATE_EXN", exn_type_def = ref ml_translatorTheory.UNIT_TYPE_def, additional_type_theories = ref [], hprop_field_names = ref [], @@ -139,27 +148,27 @@ fun with_state state_type (translator_config : config) = let val accessors = define_monad_access_funs state_type in #state_type internal_state := state_type; - #store_invariant_name internal_state := - (state_type |> dest_type |> fst |> toUppers); #state_access_funs internal_state := accessors; translator_config end; +(* This hack also used in ml_translatorLib. *) +fun guess_const_def tm = let + val stuff = dest_thy_const tm + in DB.fetch (#Thy stuff) (#Name stuff ^ "_def") end + (* * Register the exception type and return the type definition *) fun register_exception_type exn_type = - let val exn_name = (exn_type |> dest_type |> fst |> toUppers) - val exn_type_def_name = exn_name ^ "_TYPE_def" - in ( + ( register_type oneSyntax.one_ty; register_type (pairSyntax.mk_prod(alpha,beta)); register_type (listSyntax.mk_list_type alpha); register_type (optionSyntax.mk_option alpha); register_exn_type exn_type; - #store_exn_invariant_name internal_state := exn_name; - theorem exn_type_def_name - ) end; + guess_const_def (get_type_inv exn_type) + ); (* * Set the exception type, and get monadic exception functions @@ -342,10 +351,28 @@ fun extract_rarrays_manip_funs (name, init, get, set, len, sub, upd, alloc) = fun extract_farrays_manip_funs (name, init, get, set, len, sub, upd) = (name, get, set, len, sub, upd); +fun get_store_inv_name state_type = let + val _ = is_type state_type orelse (print_type state_type; + failwith ("get_store_inv_name: not a type constructor") + ) + val (nm, _) = dest_type state_type + in + nm ^ "_STORE_INV" + end + +fun get_store_inv state_type = let + val nm = get_store_inv_name state_type + (* This is a bit of a hack. The call to start_translation will call to the + store library (ml_monadStoreLib) to define the store inv. We then fetch + it back via naming scheme to do follow-up proofs. *) + val def_thm = DB.fetch "-" (nm ^ "_def") + val const = left_const def_thm + in (const, def_thm) end + local val IMP_STAR_GC = Q.prove( - `(STAR a x) s ∧ (y = GC) ⇒ (STAR a y) s`, + `(STAR a x) s ∧ (y = cfHeapsBase$GC) ⇒ (STAR a y) s`, fs [set_sepTheory.STAR_def] >> rw [] >> asm_exists_tac >> fs [] >> EVAL_TAC >> @@ -357,13 +384,20 @@ local in fun add_field_access_patterns (hprop_comb, field_name) = let - val store_inv_name = ( !(#store_invariant_name internal_state) ) val state_ty = ( !(#state_type internal_state) ) - val state_predicate = - if state_ty = unit_ty then ml_translatorSyntax.UNIT_TYPE - else Term [QUOTE store_inv_name] - val field = Term [QUOTE field_name] - val st_field = Term [QUOTE "st.", QUOTE field_name] + val (store_inv, store_inv_def) = get_store_inv state_ty + + val liftM_const = left_const ml_monadBaseTheory.liftM_def + val field_gen = Term [QUOTE field_name] + val _ = same_const liftM_const (fst (strip_comb field_gen)) + orelse failwith ("add_field_access_patterns: " ^ + "syntax conflict with liftM: " ^ field_name) + + val st_var = mk_var ("st", state_ty) + val f_var = mk_var ("f", fst (dom_rng (type_of field_gen))) + val field = mk_icomb (mk_comb (field_gen, f_var), st_var) |> rator |> rator + val st_field = case strip_comb field of (_, [acc, _]) => mk_comb (acc, st_var) + | _ => failwith ("add_field_access_patterns: field format issue") val HPROP_COMB_STAR_COMM = Q.prove( `∀ p q . p * ^(hprop_comb) q = ^(hprop_comb) q * p`, @@ -377,13 +411,13 @@ in ⇒ (∀st. EvalM ro env st exp (MONAD ret_ty exc_ty (^field f)) - (^state_predicate, p:'ffi ffi_proj))`, + (^store_inv, p:'ffi ffi_proj))`, fs [ml_monad_translatorTheory.EvalM_def] >> rw [] >> first_x_assum (qspecl_then [`^st_field`,`s`] mp_tac) >> impl_tac >- ( fs [ml_monad_translatorBaseTheory.REFS_PRED_def] >> - fs [fetch "-" (store_inv_name ^ "_def")] >> + fs [store_inv_def] >> qabbrev_tac `a = ^hprop_comb ^st_field` >> qabbrev_tac `b = GC` >> fs [AC set_sepTheory.STAR_ASSOC set_sepTheory.STAR_COMM] >> @@ -398,18 +432,16 @@ in Cases_on `f ^st_field` >> fs [] >> EVERY_CASE_TAC >> rveq >> fs [] >> - fs [fetch "-" (store_inv_name ^ "_def")] >> + fs [store_inv_def] >> fs [ml_monadBaseTheory.liftM_def] >> rw [] >> rfs[] >> fs[HPROP_COMB_STAR_COMM, set_sepTheory.STAR_ASSOC] >> metis_tac[set_sepTheory.STAR_ASSOC] ) - val state_exn_name = ( !(#store_exn_invariant_name internal_state) ) + val state_exn_ty = ( !(#exn_type internal_state) ) - val state_exn_predicate = - if state_exn_ty = unit_ty then ml_translatorSyntax.UNIT_TYPE - else Term [QUOTE state_exn_name, QUOTE "_TYPE"] + val state_exn_predicate = get_type_inv state_exn_ty val access_thm_list = mapfilter (fn ((_, name), (thm, Thm, _)) => (name^"_"^field_name, thm) @@ -465,7 +497,7 @@ fun start_translation (translator_config : config) = ((!(#refs c) ) |> map from_named_tuple_refs) ((!(#resizeable_arrays c) ) |> map from_named_tuple_rarray) ((!(#fixed_arrays c) ) |> map from_named_tuple_farray) - ( !(#store_invariant_name s) ) + ((!(#state_type c) ) |> get_store_inv_name) ( !(#state_type c) ) ( !(#exn_type_def s) ) ((!(#exn_access_funs c) ) |> map from_named_tuple_exn) @@ -486,7 +518,7 @@ fun start_translation (translator_config : config) = map extract_rarrays_manip_funs) ((!(#fixed_arrays c) ) |> map from_named_tuple_farray |> map extract_farrays_manip_funs) - ( !(#store_invariant_name s) ) + ((!(#state_type c) ) |> get_store_inv_name) ( !(#state_type c) ) ( !(#exn_type_def s) ) ((!(#exn_access_funs c) ) |> map from_named_tuple_exn)