Fix breakage caused by change to sorted_map in HOL

CakeML · Jan 5, 2021 · 3c64959 · 3c64959
1 parent 8881f24
commit 3c64959
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 27 deletions.
diff --git a/compiler/backend/proofs/clos_numberProofScript.sml b/compiler/backend/proofs/clos_numberProofScript.sml
@@ -67,13 +67,14 @@ Proof
   res_tac
 QED
 
-val renumber_code_locs_distinct_lemma = Q.prove(
-  `(∀n es. SORTED $< (code_locs (SND (renumber_code_locs_list n es))) ∧
+Theorem renumber_code_locs_distinct_lemma[local]:
+   (∀n es. SORTED $< (code_locs (SND (renumber_code_locs_list n es))) ∧
             EVERY ($<= n) (code_locs (SND (renumber_code_locs_list n es))) ∧
             EVERY ($> (FST (renumber_code_locs_list n es))) (code_locs (SND (renumber_code_locs_list n es)))) ∧
     (∀n e. SORTED $< (code_locs [SND (renumber_code_locs n e)]) ∧
             EVERY ($<= n) (code_locs [SND (renumber_code_locs n e)]) ∧
-            EVERY ($> (FST (renumber_code_locs n e))) (code_locs [SND (renumber_code_locs n e)]))`,
+            EVERY ($> (FST (renumber_code_locs n e))) (code_locs [SND (renumber_code_locs n e)]))
+Proof
   ho_match_mp_tac renumber_code_locs_ind >>
   simp[renumber_code_locs_def,code_locs_def,pairTheory.UNCURRY] >>
   srw_tac[][] >> rpt (CHANGED_TAC tac >> full_simp_tac(srw_ss())[]) >> srw_tac[][] >>
@@ -107,8 +108,7 @@ val renumber_code_locs_distinct_lemma = Q.prove(
     imp_res_tac renumber_code_locs_imp_inc >>
     srw_tac[][] >> full_simp_tac(srw_ss())[EVERY_MEM] >> res_tac >> fsrw_tac[ARITH_ss][] >>
     NO_TAC) >>
-  fs[times_add_o,GSYM MAP_GENLIST,
-     MATCH_MP sorted_map transitive_LESS,
+  fs[times_add_o,GSYM MAP_GENLIST,sorted_map,
      SORTED_inv_image_LESS_PLUS,
      SORTED_GENLIST_TIMES] >>
   Cases_on `renumber_code_locs_list n (MAP SND fns)` >>
@@ -121,7 +121,8 @@ val renumber_code_locs_distinct_lemma = Q.prove(
   srw_tac[][] >> full_simp_tac(srw_ss())[EVERY_MEM] >> res_tac >> fsrw_tac[ARITH_ss][] >>
   srw_tac[][] >> full_simp_tac(srw_ss())[EVERY_MEM] >> res_tac >> fsrw_tac[ARITH_ss][MAP_ZIP] >>
   rev_full_simp_tac(srw_ss())[MAP_ZIP] >>
-  srw_tac[][] >> full_simp_tac(srw_ss())[EVERY_MEM] >> res_tac >> fsrw_tac[ARITH_ss][MAP_ZIP]);
+  srw_tac[][] >> full_simp_tac(srw_ss())[EVERY_MEM] >> res_tac >> fsrw_tac[ARITH_ss][MAP_ZIP]
+QED
 
 Theorem renumber_code_locs_distinct:
    ∀n e. ALL_DISTINCT (code_locs [SND (renumber_code_locs n e)]) ∧

diff --git a/compiler/backend/proofs/word_to_stackProofScript.sml b/compiler/backend/proofs/word_to_stackProofScript.sml
@@ -965,8 +965,8 @@ val env_to_list_K_I_IMP = Q.prove(
   \\ res_tac \\ fs [key_val_compare_def,LET_DEF]
   \\ pairarg_tac \\ fs [] \\ pairarg_tac \\ fs [])
 
-val evaluate_wLive = Q.prove(
-  `wLive names bs (k,f,f') = (wlive_prog,bs') /\
+Theorem evaluate_wLive[local]:
+   wLive names bs (k,f,f') = (wlive_prog,bs') /\
    (∀x. x ∈ domain names ⇒ EVEN x /\ k ≤ x DIV 2) /\
    state_rel k f f' (s:('a,'a word list # 'c,'ffi) wordSem$state) t lens /\ 1 <= f /\
    (cut_env names s.locals = SOME env) /\
@@ -976,7 +976,8 @@ val evaluate_wLive = Q.prove(
      state_rel k 0 0 (push_env env ^nn s with <|locals := LN; locals_size := SOME 0|>) t5 (f'::lens) /\
      state_rel k f f' s t5 lens /\
      LENGTH t5.stack = LENGTH t.stack /\ t5.stack_space = t.stack_space /\
-     !i. i ≠ k ==> get_var i t5 = get_var i t`,
+     !i. i ≠ k ==> get_var i t5 = get_var i t
+Proof
   fsrw_tac[] [wLive_def,LET_THM] \\ rpt strip_tac \\
   `f ≠ 0` by DECIDE_TAC \\ fsrw_tac[][] \\ pop_assum kall_tac
   \\ pairarg_tac \\ fsrw_tac[] [] \\ rpt var_eq_tac
@@ -1076,12 +1077,7 @@ val evaluate_wLive = Q.prove(
   \\ match_mp_tac SORTED_IMP_EQ_LISTS
   \\ conj_tac
   >- (
-    (sorted_map |> SPEC_ALL |> UNDISCH |> EQ_IMP_RULE |> snd
-    |> DISCH_ALL |> MP_CANON |> match_mp_tac) >>
-    REWRITE_TAC[GSYM inv_image_def] >>
-    conj_tac >-(
-      match_mp_tac transitive_inv_image >>
-      ACCEPT_TAC transitive_GT ) >>
+    REWRITE_TAC[GSYM inv_image_def,sorted_map] >>
     qmatch_abbrev_tac`SORTED R' (QSORT R ls)` >>
     `SORTED R (QSORT R ls)` by (
       match_mp_tac QSORT_SORTED >>
@@ -1100,21 +1096,13 @@ val evaluate_wLive = Q.prove(
       fsrw_tac[][EVEN_GT])
   \\ conj_tac
   >- (
-    (sorted_map |> SPEC_ALL |> UNDISCH |> EQ_IMP_RULE |> snd
-     |> DISCH_ALL |> MP_CANON |> match_mp_tac) >>
+    ONCE_REWRITE_TAC[sorted_map] >>
     REWRITE_TAC[GSYM inv_image_def] >>
-    conj_tac >-(
-      match_mp_tac transitive_inv_image >>
-      ACCEPT_TAC transitive_GT ) >>
     match_mp_tac (MP_CANON sorted_filter) >>
     conj_tac >- metis_tac[transitive_inv_image,transitive_GT] >>
-    (sorted_map |> SPEC_ALL |> UNDISCH |> EQ_IMP_RULE |> fst
-     |> DISCH_ALL |> MP_CANON |> match_mp_tac) >>
-    conj_tac >- metis_tac[transitive_inv_image,transitive_GT] >>
+    ONCE_REWRITE_TAC[GSYM sorted_map] >>
     simp[MAP_GENLIST,combinTheory.o_DEF] >>
-    (sorted_map |> SPEC_ALL |> UNDISCH |> EQ_IMP_RULE |> fst
-     |> DISCH_ALL |> MP_CANON |> match_mp_tac) >>
-    conj_tac >- ACCEPT_TAC transitive_GT>>
+    ONCE_REWRITE_TAC[GSYM sorted_map] >>
     simp[MAP_GENLIST,combinTheory.o_DEF] >>
     qmatch_abbrev_tac`SORTED R (GENLIST g m)` >>
     `GENLIST g m = GENLIST (λx. k + m - (x + 1)) m` by (
@@ -1168,7 +1156,8 @@ val evaluate_wLive = Q.prove(
   \\ ONCE_REWRITE_TAC[CONJ_COMM]
   \\ asm_exists_tac
   \\ simp[]
-  \\ simp_tac (srw_ss()) [MULT_COMM,MULT_DIV]);
+  \\ simp_tac (srw_ss()) [MULT_COMM,MULT_DIV]
+QED
 
 val push_env_set_store = Q.prove(
   `push_env env ^nn (set_store AllocSize (Word c) s) =