Try to fix compiler/backend/passes/proofs

After HOL changes in HOL-Theorem-Prover/HOL@8c4bb7e
CakeML · Feb 8, 2025 · cd3aee1 · cd3aee1
1 parent b560cb3
commit cd3aee1
Show file tree

Hide file tree

Showing 6 changed files with 15 additions and 7 deletions.
diff --git a/compiler/backend/passes/proofs/thunk_case_inlProofScript.sml b/compiler/backend/passes/proofs/thunk_case_inlProofScript.sml
@@ -703,6 +703,7 @@ Proof
         \\ first_x_assum (drule_all_then assume_tac) \\ gs []
         \\ first_x_assum (drule_all_then assume_tac) \\ gs []
         \\ first_x_assum (drule_all_then assume_tac) \\ gs []
+        \\ last_x_assum $ drule_all
         \\ Cases_on ‘eval_to k (EL n ys)’ \\ gs [])
       \\ rgs [Once (DECIDE “A ⇒ ¬B ⇔ B ⇒ ¬A”)]
       \\ IF_CASES_TAC \\ gs []

diff --git a/compiler/backend/passes/proofs/thunk_case_liftProofScript.sml b/compiler/backend/passes/proofs/thunk_case_liftProofScript.sml
@@ -487,6 +487,7 @@ Proof
         \\ first_x_assum (drule_then assume_tac) \\ gs []
         \\ first_x_assum (drule_all_then assume_tac) \\ gs []
         \\ first_x_assum (drule_all_then assume_tac) \\ gs []
+        \\ last_x_assum $ drule_all
         \\ Cases_on ‘eval_to k (EL n ys)’ \\ gs [])
       \\ rgs [Once (DECIDE “A ⇒ ¬B ⇔ B ⇒ ¬A”)]
       \\ IF_CASES_TAC \\ gs []

diff --git a/compiler/backend/passes/proofs/thunk_case_unboxProofScript.sml b/compiler/backend/passes/proofs/thunk_case_unboxProofScript.sml
@@ -458,6 +458,7 @@ Proof
         \\ first_x_assum (drule_then assume_tac) \\ gs []
         \\ first_x_assum (drule_all_then assume_tac) \\ gs []
         \\ first_x_assum (drule_all_then assume_tac) \\ gs []
+        \\ last_x_assum $ drule_all
         \\ Cases_on ‘eval_to k (EL n ys)’ \\ gs [])
       \\ rgs [Once (DECIDE “A ⇒ ¬B ⇔ B ⇒ ¬A”)]
       \\ IF_CASES_TAC \\ gs []

diff --git a/compiler/backend/passes/proofs/thunk_tickProofScript.sml b/compiler/backend/passes/proofs/thunk_tickProofScript.sml
@@ -903,8 +903,9 @@ Proof
         \\ Cases_on ‘eval_to k (EL n xs)’
         \\ Cases_on ‘eval_to (j + k) (EL n ys)’ \\ gvs []
         \\ rename1 ‘err ≠ Type_error’ \\ Cases_on ‘err’ \\ gs [])
-      \\ first_x_assum (drule_all_then assume_tac)
-      \\ Cases_on ‘eval_to k (EL n xs)’ \\ gs [])
+      \\ rpt $ first_x_assum (drule_all_then assume_tac)
+      \\ Cases_on ‘eval_to k (EL n xs)’ \\ gs []
+      )
     >- ((* IsEq *)
       IF_CASES_TAC \\ gvs [LENGTH_EQ_NUM_compute, DECIDE “∀n. n < 1 ⇔ n = 0”]
       \\ rename1 ‘exp_rel x y’

diff --git a/compiler/backend/passes/proofs/thunk_to_env_1ProofScript.sml b/compiler/backend/passes/proofs/thunk_to_env_1ProofScript.sml
@@ -443,14 +443,17 @@ Proof
         \\ rename1 ‘m < LENGTH ys’
         \\ first_x_assum (drule_all_then assume_tac)
         \\ first_x_assum (drule_all_then assume_tac)
-        \\ Cases_on ‘eval_to k (EL m xs)’ \\ gs [])
+        \\ last_x_assum $ drule_all
+        \\ Cases_on ‘eval_to k (EL m xs)’ \\ gs []
+        )
       \\ gs [DECIDE “A ⇒ ¬(B < C) ⇔ B < C ⇒ ¬A”]
       \\ IF_CASES_TAC \\ gs []
       >- (
         first_x_assum (drule_all_then assume_tac)
         \\ first_x_assum (drule_all_then assume_tac)
         \\ first_x_assum (drule_then assume_tac)
         \\ first_x_assum (drule_then assume_tac)
+        \\ pop_assum drule
         \\ Cases_on ‘eval_to k (EL n xs)’ \\ gs [])
       \\ gs [DECIDE “A ⇒ ¬(B < C) ⇔ B < C ⇒ ¬A”]
       \\ IF_CASES_TAC \\ gs []
@@ -459,6 +462,7 @@ Proof
         \\ first_x_assum (drule_all_then assume_tac)
         \\ first_x_assum (drule_then assume_tac)
         \\ first_x_assum (drule_then assume_tac)
+        \\ last_x_assum $ drule_all
         \\ Cases_on ‘eval_to k (EL n xs)’ \\ gs [])
       \\ gvs [DECIDE “A ⇒ ¬(B < C) ⇔ B < C ⇒ ¬A”, EVERY2_MAP, LIST_REL_EL_EQN]
       \\ rw []

diff --git a/compiler/backend/passes/proofs/thunk_untickProofScript.sml b/compiler/backend/passes/proofs/thunk_untickProofScript.sml
@@ -984,7 +984,7 @@ Proof
         \\ gs [result_map_def, CaseEq "bool", MEM_MAP]
         \\ gs [Once (DECIDE “A ⇒ ¬B ⇔ B ⇒ ¬A”)]
         \\ gvs [MEM_EL, PULL_EXISTS]
-        \\ first_x_assum (drule_all_then assume_tac)
+        \\ last_x_assum $ drule_then assume_tac
         \\ first_x_assum (drule_then drule)
         \\ disch_then (qx_choose_then ‘j’ assume_tac)
         \\ qexists_tac ‘j’
@@ -998,7 +998,7 @@ Proof
             \\ gvs [result_map_def, CaseEq "bool", MEM_MAP, Abbr ‘g’, MEM_EL]
             \\ rename1 ‘eval_to k (EL m ys) = INL Type_error’
             \\ ntac 2 (pop_assum kall_tac)
-            \\ first_x_assum (drule_all_then assume_tac)
+            \\ last_x_assum $ drule_then assume_tac
             \\ first_x_assum
               (drule_then (drule_then (qx_choose_then ‘j’ assume_tac)))
             \\ gs [Abbr ‘f’]
@@ -1197,13 +1197,13 @@ Proof
             \\ rename1 ‘m < LENGTH ys’
             \\ Cases_on ‘eval_to (k - 1) (EL m ys)’ \\ gvs []
             >- (
-              first_x_assum (drule_all_then assume_tac)
+              last_x_assum $ drule_then assume_tac
               \\ first_x_assum (drule_all_then (qx_choose_then ‘j’ assume_tac))
               \\ gs [Abbr ‘f’]
               \\ first_x_assum (drule_then assume_tac)
               \\ Cases_on ‘eval_to (j + k - 1) (EL m xs)’ \\ gs [])
             \\ fs [DECIDE “A ⇒ ¬B ⇔ B ⇒ ¬A”]
-            \\ first_x_assum (drule_all_then assume_tac)
+            \\ last_x_assum $ drule_then assume_tac
             \\ first_x_assum (drule_all_then (qx_choose_then ‘j’ assume_tac))
             \\ gs [Abbr ‘f’]
             \\ first_x_assum (drule_then assume_tac)