cheated the last remaining theories

CakeML · Sep 8, 2023 · 2099095 · 2099095
1 parent ab6d4a8
commit 2099095
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 12 deletions.
diff --git a/compiler/backend/passes/proofs/thunk_case_d2bProofScript.sml b/compiler/backend/passes/proofs/thunk_case_d2bProofScript.sml
@@ -904,8 +904,8 @@ Proof
     >~ [‘Let (SOME s) x1 y1’] >- (
       strip_tac
       \\ rw [Once exp_rel_cases]
-      >- ((* D2B *)
-        pop_assum mp_tac
+      >- ((* D2B *) cheat
+(*        pop_assum mp_tac
         \\ simp [Once eval_to_def]
         \\ simp [Once eval_to_def, subst_def]
         \\ simp [Once eval_to_def]
@@ -1007,7 +1007,7 @@ Proof
         \\ Cases_on ‘eval_to (k - 2) X2’ \\ gs []
         \\ ‘eval_to (j1 + j2 + k) X1 = eval_to (j2 + k - 2) X1’
           suffices_by rw []
-        \\ irule eval_to_mono \\ gs [])
+        \\ irule eval_to_mono \\ gs []*))
       \\ ‘∀k. eval_to k x1 ≠ INL Type_error’
         by (qx_gen_tac ‘j’
             \\ strip_tac
@@ -1561,9 +1561,6 @@ Proof
   rw [rel_ok_def]
   >- ((* ∀x. f x ≠ Err from rel_ok prevents this case *)
     simp [d2b_apply_closure])
-  >- ((* Thunks go to Thunks or DoTicks *)
-    Cases_on ‘s’ \\ gs []
-    \\ gs [Once v_rel_cases])
   >- ((* Equal literals are related *)
     simp [exp_rel_Prim])
   >- ((* Equal 0-arity conses are related *)

diff --git a/compiler/backend/passes/proofs/thunk_case_inlProofScript.sml b/compiler/backend/passes/proofs/thunk_case_inlProofScript.sml
@@ -292,7 +292,7 @@ Theorem exp_rel_subst:
   ∀vs x ws y m.
     MAP FST vs = MAP FST ws ∧
     LIST_REL (λ(f,v) (g,w).
-      (* (f ∈ m ⇒ v_rel v (Thunk (INL w))) ∧ *)
+      (f ∈ m ⇒ v_rel v (Thunk (Value w))) ∧
       (f ∉ m ⇒ v_rel v w)) vs ws ∧
     exp_rel m x y ⇒
       exp_rel m (subst vs x) (subst ws y)
@@ -313,6 +313,7 @@ Proof
       \\ ‘k < LENGTH ws’ by gs [Abbr ‘k’]
       \\ first_x_assum (drule_then assume_tac)
       \\ rpt (pairarg_tac \\ gvs [])
+      \\ gs [Once exp_rel_cases]
       \\ irule exp_rel_Inline_Value
       \\ gs [])
         (* s ∉ m *)
@@ -478,7 +479,8 @@ Proof
   \\ rpt conj_tac \\ rpt gen_tac
   >~ [‘Value v’] >- (
     rw [Once exp_rel_cases]
-    \\ simp [eval_to_def])
+    \\ simp [eval_to_def]
+    \\ irule exp_rel_Value \\ simp [])
   >~ [‘App f x’] >- (
     strip_tac
     \\ rw [Once exp_rel_cases] \\ gs []
@@ -547,7 +549,8 @@ Proof
       \\ first_x_assum irule
       \\ simp [closed_subst]
       \\ irule_at Any exp_rel_subst \\ gs []
-      \\ first_assum (irule_at Any) \\ gs [])
+      \\ first_assum (irule_at Any) \\ gs []
+      \\ irule exp_rel_Value \\ gs [])
     \\ simp [eval_to_def]
     \\ IF_CASES_TAC \\ gs []
     \\ first_x_assum (drule_then assume_tac)
@@ -648,7 +651,6 @@ Proof
         \\ drule_then strip_assume_tac ALOOKUP_SOME_REVERSE_EL \\ gs []
         \\ first_x_assum (drule_then assume_tac)
         \\ gs [ELIM_UNCURRY, freevars_def])
-      \\ CASE_TAC \\ gs []
       \\ first_x_assum irule
       \\ simp [subst_funs_def, SF SFY_ss])
     \\ ‘∃y. dest_Tick w = SOME y’
@@ -850,8 +852,6 @@ Proof
   rw [rel_ok_def]
   >- ((* ∀x. f x ≠ Err from rel_ok prevents this case *)
     simp [inl_apply_closure])
-  >- ((* Thunks go to Thunks or DoTicks *)
-    Cases_on ‘s’ \\ gs [])
   >- (
     gs [Once v_rel_cases])
   >- ((* Equal literals are related *)

diff --git a/compiler/backend/passes/proofs/thunk_combine_Forcing_LambdasScript.sml b/compiler/backend/passes/proofs/thunk_combine_Forcing_LambdasScript.sml
@@ -1501,6 +1501,7 @@ Theorem combine_rel_eval_to:
     combine_rel x y ⇒
       ∃j. ($= +++ v_rel) (eval_to k x) (eval_to (j + k) y)
 Proof
+  cheat (*
   completeInduct_on ‘k’ \\ completeInduct_on ‘exp_size x’
   \\ Cases \\ gvs [PULL_FORALL, exp_size_def] \\ rw []
   >~ [‘Var m’] >- (
@@ -6520,6 +6521,7 @@ Proof
       \\ rpt (first_x_assum (drule_all_then assume_tac))
       \\ Cases_on ‘eval_to k (EL n xs)’
       \\ Cases_on ‘eval_to (j + k) (EL n ys)’ \\ gs [v_rel_def]))
+*)
 QED
 
 Theorem combine_rel_eval: