From 1ecbf6cd33e8e4a785a024c402aa9309ec0f4675 Mon Sep 17 00:00:00 2001 From: tanyongkiam Date: Fri, 19 Dec 2025 16:58:01 +0800 Subject: [PATCH 1/9] add non-failing assumption to force-delay --- .../passes/proofs/thunk_force_delayScript.sml | 57 +++++++++++++++---- 1 file changed, 45 insertions(+), 12 deletions(-) diff --git a/compiler/backend/passes/proofs/thunk_force_delayScript.sml b/compiler/backend/passes/proofs/thunk_force_delayScript.sml index a3ef8549..3e500ce4 100644 --- a/compiler/backend/passes/proofs/thunk_force_delayScript.sml +++ b/compiler/backend/passes/proofs/thunk_force_delayScript.sml @@ -1,5 +1,5 @@ (* - Simplify occurences of `Force (Delay e)` to `e` + Simplify occurrences of `Force (Delay e)` to `e` This proof is retired and not maintained because it's not used as a part of the compiler definition. @@ -12,7 +12,6 @@ Ancestors Libs term_tactic monadsyntax dep_rewrite - Inductive force_delay_rel: [~Var:] (∀n. force_delay_rel (Var n) (Var n)) @@ -332,7 +331,8 @@ QED Theorem exp_rel_eval_to[local]: ∀x y. - exp_rel x y ⇒ + exp_rel x y ∧ + eval_to k x ≠ INL Type_error ⇒ ($= +++ v_rel) (eval_to k x) (eval_to k y) Proof completeInduct_on ‘k’ @@ -401,7 +401,8 @@ Proof rw [Once exp_rel_cases] \\ gs [eval_to_def, v_rel_def]) >~ [‘Let NONE x y’] >- ( - rw [exp_rel_def] \\ gs [] + cheat + \\ rw [exp_rel_def] \\ gs [] \\ simp [eval_to_def] \\ IF_CASES_TAC \\ gs [] \\ rename1 ‘exp_rel x x2’ \\ rename1 ‘exp_rel y y2’ @@ -412,7 +413,8 @@ Proof \\ Cases_on ‘eval_to (k - 1) x2’ \\ Cases_on ‘eval_to (k - 1) x’ \\ gs []) >~ [‘Let (SOME n) x y’] >- ( - rw [exp_rel_def] \\ gs [] + cheat + \\ rw [exp_rel_def] \\ gs [] \\ simp [eval_to_def] \\ IF_CASES_TAC \\ gs [] \\ rename1 ‘exp_rel x x2’ \\ rename1 ‘exp_rel y y2’ @@ -425,7 +427,8 @@ Proof \\ last_x_assum irule \\ irule exp_rel_subst \\ gs []) >~ [‘Letrec f x’] >- ( - rw [exp_rel_def] \\ gs [] + cheat + \\ rw [exp_rel_def] \\ gs [] \\ simp [eval_to_def] \\ IF_CASES_TAC \\ gs [] \\ last_x_assum $ qspecl_then [‘k - 1’] assume_tac \\ gvs [] @@ -445,7 +448,8 @@ Proof rw []) \\ gs [] \\ first_x_assum $ dxrule_then assume_tac \\ gvs []) >~ [‘If x1 y1 z1’] >- ( - rw [exp_rel_def, eval_to_def] \\ gs [eval_to_def] + cheat + (* \\ rw [exp_rel_def, eval_to_def] \\ gs [eval_to_def] \\ rename1 ‘exp_rel x1 x2’ \\ rename1 ‘exp_rel y1 y2’ \\ rename1 ‘exp_rel z1 z2’ \\ last_x_assum $ qspecl_then [‘k - 1’] assume_tac \\ gvs [] @@ -460,14 +464,35 @@ Proof \\ IF_CASES_TAC \\ gs [] >- (Cases_on ‘v1’ \\ gs [v_rel_def]) \\ IF_CASES_TAC \\ gvs [] - >- (Cases_on ‘v1’ \\ gs [v_rel_def])) - >~ [‘Force x’] >- cheat (* + >- (Cases_on ‘v1’ \\ gs [v_rel_def])*) ) + >~ [‘Force x’] >- ( rw [exp_rel_def] \\ gs [] >~[‘Force (Delay x)’] >- ( once_rewrite_tac [eval_to_def] \\ IF_CASES_TAC \\ simp [] \\ simp [Once eval_to_def, dest_anyThunk_def] - \\ simp [subst_funs_def, subst_empty]) + \\ simp [subst_funs_def, subst_empty] + \\ first_x_assum $ drule_at $ Pos $ el 2 + \\ disch_then (qspec_then `k-1` mp_tac) + \\ impl_tac >- ( + simp[]>> + CCONTR_TAC>> + qpat_x_assum` _ ≠ INL Type_error` mp_tac>> + fs[]>> + simp[Once eval_to_def]>> + simp [Once eval_to_def, dest_anyThunk_def]>> + simp [subst_funs_def, subst_empty]) + \\ strip_tac + \\ rfs[] + \\ Cases_on ‘eval_to (k - 1) x’ + \\ rw[] >> + qpat_x_assum` _ ≠ INL Type_error` mp_tac>> + fs[]>> + simp[Once eval_to_def]>> + simp [Once eval_to_def, dest_anyThunk_def]>> + simp [subst_funs_def, subst_empty])>> + cheat ) + (* \\ rename1 ‘exp_rel x y’ \\ once_rewrite_tac [eval_to_def] \\ IF_CASES_TAC \\ gs [] @@ -517,9 +542,16 @@ Proof rw [exp_rel_def] \\ gs [] \\ simp [eval_to_def] \\ rename1 ‘exp_rel x y’ - \\ first_x_assum $ drule_then assume_tac + \\ first_x_assum $ drule_then mp_tac + \\ impl_tac >- ( + CCONTR_TAC>> + qpat_x_assum`_ ≠ _` mp_tac>> + simp[eval_to_def]>> + fs[]) \\ Cases_on ‘eval_to k y’ \\ Cases_on ‘eval_to k x’ \\ gs [v_rel_def]) >~ [‘Prim op xs’] >- ( + cheat + (* rw [] \\ gvs [Once exp_rel_def, eval_to_def] \\ gvs [MEM_EL, PULL_EXISTS, LIST_REL_EL_EQN] @@ -671,12 +703,13 @@ Proof \\ gen_tac \\ strip_tac \\ rename1 ‘n < _’ \\ rpt $ first_x_assum $ qspec_then ‘n’ assume_tac \\ gs [] \\ Cases_on ‘eval_to k (EL n xs)’ \\ gs [] - \\ CASE_TAC \\ gs [v_rel_def])) + \\ CASE_TAC \\ gs [v_rel_def])*)) >~ [‘Monad mop xs’] >- ( rw [Once exp_rel_cases] \\ gs [] \\ simp [eval_to_def, v_rel_def]) QED +(* TODO: broken under here *) Theorem exp_rel_eval: exp_rel x y ⇒ ($= +++ v_rel) (eval x) (eval y) From 05748965eebd2cfc1608acb86e536e3306f0ceec Mon Sep 17 00:00:00 2001 From: artisanbk Date: Sat, 20 Dec 2025 14:12:24 +0800 Subject: [PATCH 2/9] some progress --- .../passes/proofs/thunk_force_delayScript.sml | 76 +++++++++++-------- 1 file changed, 45 insertions(+), 31 deletions(-) diff --git a/compiler/backend/passes/proofs/thunk_force_delayScript.sml b/compiler/backend/passes/proofs/thunk_force_delayScript.sml index 3e500ce4..2adbfac7 100644 --- a/compiler/backend/passes/proofs/thunk_force_delayScript.sml +++ b/compiler/backend/passes/proofs/thunk_force_delayScript.sml @@ -4,6 +4,7 @@ This proof is retired and not maintained because it's not used as a part of the compiler definition. *) + Theory thunk_force_delay Ancestors string option sum pair list alist finite_map pred_set rich_list @@ -401,8 +402,7 @@ Proof rw [Once exp_rel_cases] \\ gs [eval_to_def, v_rel_def]) >~ [‘Let NONE x y’] >- ( - cheat - \\ rw [exp_rel_def] \\ gs [] + rw [exp_rel_def] \\ gs [] \\ simp [eval_to_def] \\ IF_CASES_TAC \\ gs [] \\ rename1 ‘exp_rel x x2’ \\ rename1 ‘exp_rel y y2’ @@ -411,10 +411,10 @@ Proof \\ last_assum $ dxrule_then assume_tac \\ last_x_assum $ dxrule_then assume_tac \\ Cases_on ‘eval_to (k - 1) x2’ - \\ Cases_on ‘eval_to (k - 1) x’ \\ gs []) + \\ Cases_on ‘eval_to (k - 1) x’ \\ gs [] + \\ fs[eval_to_def]) >~ [‘Let (SOME n) x y’] >- ( - cheat - \\ rw [exp_rel_def] \\ gs [] + rw [exp_rel_def] \\ gs [] \\ simp [eval_to_def] \\ IF_CASES_TAC \\ gs [] \\ rename1 ‘exp_rel x x2’ \\ rename1 ‘exp_rel y y2’ @@ -424,32 +424,39 @@ Proof \\ last_assum $ dxrule_then assume_tac \\ Cases_on ‘eval_to (k - 1) x2’ \\ Cases_on ‘eval_to (k - 1) x’ \\ gs [] - \\ last_x_assum irule - \\ irule exp_rel_subst \\ gs []) + \\ fs[eval_to_def, exp_rel_subst]) + >~ [‘Letrec f x’] >- ( - cheat - \\ rw [exp_rel_def] \\ gs [] + rw [exp_rel_def] \\ gs [] \\ simp [eval_to_def] \\ IF_CASES_TAC \\ gs [] \\ last_x_assum $ qspecl_then [‘k - 1’] assume_tac \\ gvs [] \\ first_x_assum irule \\ simp [subst_funs_def, closed_subst, MAP_MAP_o, combinTheory.o_DEF, LAMBDA_PROD, GSYM FST_THM] - \\ irule exp_rel_subst - \\ gvs [MAP_MAP_o, combinTheory.o_DEF, LAMBDA_PROD, GSYM FST_THM, LIST_REL_EL_EQN, EL_MAP] - \\ rw [] \\ pairarg_tac \\ gs [] \\ pairarg_tac \\ gs [v_rel_def, LIST_REL_EL_EQN, EL_MAP] - \\ rename1 ‘MAP FST f = MAP FST g’ - \\ ‘∀i. i < LENGTH f ⇒ FST (EL i f) = FST (EL i g)’ - by (rw [] >> - ‘i < LENGTH f’ by gs [] >> - dxrule_then (qspecl_then [‘FST’] assume_tac) $ GSYM EL_MAP >> - ‘i < LENGTH g’ by gs [] >> - dxrule_then (qspecl_then [‘FST’] assume_tac) $ GSYM EL_MAP >> - rw []) - \\ gs [] \\ first_x_assum $ dxrule_then assume_tac \\ gvs []) + \\ strip_tac + >- ( + CCONTR_TAC + \\ fs[eval_to_def] + \\ metis_tac[subst_def, subst_funs_def] + ) + >- ( + irule exp_rel_subst + \\ gvs [MAP_MAP_o, combinTheory.o_DEF, LAMBDA_PROD, GSYM FST_THM, LIST_REL_EL_EQN, EL_MAP] + \\ rw [] \\ pairarg_tac \\ gs [] \\ pairarg_tac \\ gs [v_rel_def, LIST_REL_EL_EQN, EL_MAP] + \\ rename1 ‘MAP FST f = MAP FST g’ + \\ ‘∀i. i < LENGTH f ⇒ FST (EL i f) = FST (EL i g)’ + by (rw [] >> + ‘i < LENGTH f’ by gs [] >> + dxrule_then (qspecl_then [‘FST’] assume_tac) $ GSYM EL_MAP >> + ‘i < LENGTH g’ by gs [] >> + dxrule_then (qspecl_then [‘FST’] assume_tac) $ GSYM EL_MAP >> + rw []) + \\ gs [] \\ first_x_assum $ dxrule_then assume_tac \\ gvs [])) + >~ [‘If x1 y1 z1’] >- ( - cheat - (* \\ rw [exp_rel_def, eval_to_def] \\ gs [eval_to_def] + cheat (* + \\ rw [exp_rel_def, eval_to_def] \\ gs [eval_to_def] \\ rename1 ‘exp_rel x1 x2’ \\ rename1 ‘exp_rel y1 y2’ \\ rename1 ‘exp_rel z1 z2’ \\ last_x_assum $ qspecl_then [‘k - 1’] assume_tac \\ gvs [] @@ -464,7 +471,10 @@ Proof \\ IF_CASES_TAC \\ gs [] >- (Cases_on ‘v1’ \\ gs [v_rel_def]) \\ IF_CASES_TAC \\ gvs [] - >- (Cases_on ‘v1’ \\ gs [v_rel_def])*) ) + >- (Cases_on ‘v1’ \\ gs [v_rel_def]) + *) +) + >~ [‘Force x’] >- ( rw [exp_rel_def] \\ gs [] >~[‘Force (Delay x)’] >- ( @@ -485,13 +495,17 @@ Proof \\ strip_tac \\ rfs[] \\ Cases_on ‘eval_to (k - 1) x’ - \\ rw[] >> - qpat_x_assum` _ ≠ INL Type_error` mp_tac>> - fs[]>> - simp[Once eval_to_def]>> - simp [Once eval_to_def, dest_anyThunk_def]>> - simp [subst_funs_def, subst_empty])>> - cheat ) + \\ rw[] + \\ qpat_x_assum` _ ≠ INL Type_error` mp_tac + \\ fs[] + \\ simp[Once eval_to_def] + \\ simp [Once eval_to_def, dest_anyThunk_def] + \\ simp [subst_funs_def, subst_empty]) + + >~[`Force x`] >-( + cheat + )) + (* \\ rename1 ‘exp_rel x y’ \\ once_rewrite_tac [eval_to_def] From c985528b3e6f239779d5d59411f65d9ff3b24464 Mon Sep 17 00:00:00 2001 From: artisanbk Date: Tue, 23 Dec 2025 14:09:49 +0800 Subject: [PATCH 3/9] dest_Tick y' case --- .../passes/proofs/thunk_force_delayScript.sml | 211 ++++++++++-------- 1 file changed, 122 insertions(+), 89 deletions(-) diff --git a/compiler/backend/passes/proofs/thunk_force_delayScript.sml b/compiler/backend/passes/proofs/thunk_force_delayScript.sml index 2adbfac7..9d8f8087 100644 --- a/compiler/backend/passes/proofs/thunk_force_delayScript.sml +++ b/compiler/backend/passes/proofs/thunk_force_delayScript.sml @@ -341,9 +341,11 @@ Proof >~ [‘Var v’] >- ( rw [Once exp_rel_cases] \\ simp [eval_to_def]) + >~ [‘Value v’] >- ( rw [Once exp_rel_cases] \\ simp [eval_to_def]) + >~ [‘App g y’] >- ( gvs [Once exp_rel_def, eval_to_def, PULL_EXISTS] \\ rw [] \\ rename1 ‘exp_rel y x’ \\ rename1 ‘exp_rel g f’ @@ -398,9 +400,11 @@ Proof \\ rename1 ‘n < _’ \\ ‘EL n (MAP FST xs) = EL n (MAP FST ys)’ by simp [] \\ gs [EL_MAP]) + >~ [‘Lam s x’] >- ( rw [Once exp_rel_cases] \\ gs [eval_to_def, v_rel_def]) + >~ [‘Let NONE x y’] >- ( rw [exp_rel_def] \\ gs [] \\ simp [eval_to_def] @@ -413,6 +417,7 @@ Proof \\ Cases_on ‘eval_to (k - 1) x2’ \\ Cases_on ‘eval_to (k - 1) x’ \\ gs [] \\ fs[eval_to_def]) + >~ [‘Let (SOME n) x y’] >- ( rw [exp_rel_def] \\ gs [] \\ simp [eval_to_def] @@ -455,12 +460,10 @@ Proof \\ gs [] \\ first_x_assum $ dxrule_then assume_tac \\ gvs [])) >~ [‘If x1 y1 z1’] >- ( - cheat (* - \\ rw [exp_rel_def, eval_to_def] \\ gs [eval_to_def] + rw [exp_rel_def, eval_to_def] \\ gs [eval_to_def] \\ rename1 ‘exp_rel x1 x2’ \\ rename1 ‘exp_rel y1 y2’ \\ rename1 ‘exp_rel z1 z2’ \\ last_x_assum $ qspecl_then [‘k - 1’] assume_tac \\ gvs [] - \\ last_x_assum kall_tac \\ last_x_assum kall_tac \\ last_x_assum kall_tac \\ rpt $ first_assum $ dxrule_then assume_tac \\ last_x_assum kall_tac \\ last_x_assum kall_tac \\ gvs [] \\ Cases_on ‘eval_to (k - 1) x2’ @@ -468,103 +471,131 @@ Proof \\ rename1 ‘v_rel v1 w1’ \\ IF_CASES_TAC \\ gvs [v_rel_def] \\ IF_CASES_TAC \\ gvs [v_rel_def] - \\ IF_CASES_TAC \\ gs [] - >- (Cases_on ‘v1’ \\ gs [v_rel_def]) - \\ IF_CASES_TAC \\ gvs [] - >- (Cases_on ‘v1’ \\ gs [v_rel_def]) - *) -) + \\ IF_CASES_TAC \\ gs []) >~ [‘Force x’] >- ( rw [exp_rel_def] \\ gs [] - >~[‘Force (Delay x)’] >- ( + >~[‘Force (Delay x)’] >-( once_rewrite_tac [eval_to_def] \\ IF_CASES_TAC \\ simp [] \\ simp [Once eval_to_def, dest_anyThunk_def] \\ simp [subst_funs_def, subst_empty] - \\ first_x_assum $ drule_at $ Pos $ el 2 + \\ first_assum $ drule_at $ Pos $ el 2 \\ disch_then (qspec_then `k-1` mp_tac) - \\ impl_tac >- ( - simp[]>> - CCONTR_TAC>> - qpat_x_assum` _ ≠ INL Type_error` mp_tac>> - fs[]>> - simp[Once eval_to_def]>> - simp [Once eval_to_def, dest_anyThunk_def]>> - simp [subst_funs_def, subst_empty]) - \\ strip_tac - \\ rfs[] - \\ Cases_on ‘eval_to (k - 1) x’ - \\ rw[] - \\ qpat_x_assum` _ ≠ INL Type_error` mp_tac - \\ fs[] - \\ simp[Once eval_to_def] - \\ simp [Once eval_to_def, dest_anyThunk_def] - \\ simp [subst_funs_def, subst_empty]) - + \\ impl_tac + >-( + simp[] + \\ CCONTR_TAC + \\ qpat_x_assum` _ ≠ INL Type_error` mp_tac + \\ fs[] + \\ simp[Once eval_to_def] + \\ simp [Once eval_to_def, dest_anyThunk_def] + \\ simp [subst_funs_def, subst_empty]) + >-( + strip_tac + \\ Cases_on ‘eval_to (k - 1) x'’ + \\ rw[] + \\ qpat_x_assum` _ ≠ INL Type_error` mp_tac + \\ simp[Once eval_to_def] + \\ simp [Once eval_to_def, dest_anyThunk_def] + \\ simp [subst_funs_def, subst_empty])) >~[`Force x`] >-( - cheat - )) + rename1 ‘exp_rel x y’ + \\ once_rewrite_tac [eval_to_def] + \\ IF_CASES_TAC \\ gs [] + \\ last_assum $ qspecl_then [‘k - 1’] assume_tac \\ gvs [] + \\ last_assum $ drule_then assume_tac + \\ Cases_on ‘eval_to k y’ \\ Cases_on ‘eval_to k x’ \\ gvs [] + >~[`x''=x'`] >-( + `x'' ≠ Type_error` suffices_by fs[] + \\ CCONTR_TAC + \\ qpat_x_assum `eval_to k x = INL x''` MP_TAC + \\ fs[Once $ eval_to_def, exp_rel_def, v_rel_def] + \\ Cases_on `eval_to k x` \\ gvs[]) + >~[`dest_Tick y'`] >-( + `dest_Tick y' = NONE` by (Cases_on `y` \\ Cases_on `y'` \\ gs[Once $ eval_to_def]) + \\ gs[subst_funs_def, Once $ eval_to_def]) + + >~[`dest_Tick y''`] >-( + Cases_on `dest_Tick y''` \\ Cases_on `dest_Tick y'` + \\ gs [v_rel_def, exp_rel_def, PULL_EXISTS, dest_Tick_def] + >- ( + (*dest_Tick y'' = NONE ∧ dest_Tick y' = NONE*) + cheat + ) + >- ( + (*dest_Tick y'' = NONE ∧ dest_Tick y' = SOME*) + cheat + ) + >- ( + (*dest_Tick y'' = SOME ∧ dest_Tick y' = NONE*) + cheat + ) + >- ( + (*dest_Tick y'' = SOME ∧ dest_Tick y' = SOME*) + cheat + ) + ) + ) + + (* + ‘dest_Tick v = NONE’ + by (Cases_on ‘v’ \\ Cases_on ‘w’ \\ gs [] + \\ gs [Once v_rel_def]) + \\ gs [] + \\ Cases_on ‘v’ \\ gvs [dest_anyThunk_def, v_rel_def] + >~[‘Recclosure _ _’] + >- (rename1 ‘LIST_REL _ (MAP SND xs) (MAP SND ys)’ + \\ ‘OPTREL exp_rel + (ALOOKUP (REVERSE xs) s) + (ALOOKUP (REVERSE ys) s)’ + by (irule LIST_REL_OPTREL + \\ gvs [LIST_REL_EL_EQN, ELIM_UNCURRY, EL_MAP, LIST_EQ_REWRITE]) + \\ gs [OPTREL_def] + \\ rename1 ‘exp_rel x0 y0’ + \\ ‘MEM (s, x0) xs’ by (rpt $ dxrule_then assume_tac ALOOKUP_MEM \\ gvs []) + \\ gvs [EVERY_MEM, MEM_MAP, PULL_EXISTS] + \\ first_assum $ dxrule_then assume_tac + \\ Cases_on ‘x0’ \\ gvs [ok_bind_def, exp_rel_def] + >~[‘subst_funs ys e2’] + >- (last_x_assum irule \\ simp [subst_funs_def] + \\ irule exp_rel_subst \\ simp [] + \\ gs [FORALL_PROD] + \\ gvs [MAP_MAP_o, combinTheory.o_DEF, LAMBDA_PROD, GSYM FST_THM, LIST_REL_EL_EQN, EL_MAP] + \\ rw [] \\ pairarg_tac \\ gs [] \\ pairarg_tac \\ gs [v_rel_def, LIST_REL_EL_EQN, EL_MAP] + \\ gs [EVERY_MEM, MEM_MAP, PULL_EXISTS, FORALL_PROD] + \\ rw [] + >- ( + rename [‘n < _’, ‘MAP FST xs = MAP FST ys’] + \\ ‘EL n (MAP FST xs) = EL n (MAP FST ys)’ by gs [] + \\ gvs [EL_MAP]) + \\ last_x_assum $ drule_then irule)) + \\ gs [subst_funs_def, subst_empty]) + >~[`dest_Tick y''`] >-( + rename1 ‘v_rel v w’ + \\ Cases_on ‘dest_Tick w’ \\ gs [] + \\ Cases_on ‘v’ \\ gs [v_rel_def, exp_rel_def, PULL_EXISTS, dest_Tick_def]) + >~ [‘Delay x’] >- ( + rw [Once exp_rel_cases] \\ gs [] + \\ simp [eval_to_def, v_rel_def]) + >~ [‘MkTick x’] >- ( + rw [exp_rel_def] \\ gs [] + \\ simp [eval_to_def] + \\ rename1 ‘exp_rel x y’ + \\ first_x_assum $ drule_then mp_tac + \\ impl_tac >- ( + CCONTR_TAC>> + qpat_x_assum`_ ≠ _` mp_tac>> + simp[eval_to_def]>> + fs[]) + \\ Cases_on ‘eval_to k y’ \\ Cases_on ‘eval_to k x’ \\ gs [v_rel_def]) + )) + ) + *) - (* - \\ rename1 ‘exp_rel x y’ - \\ once_rewrite_tac [eval_to_def] - \\ IF_CASES_TAC \\ gs [] - \\ last_x_assum $ qspecl_then [‘k - 1’] assume_tac \\ gvs [] - \\ last_x_assum $ dxrule_then assume_tac - \\ Cases_on ‘eval_to k y’ \\ Cases_on ‘eval_to k x’ \\ gs [] - \\ rename1 ‘v_rel v w’ - \\ Cases_on ‘dest_Tick w’ \\ gs [] - >- ( - ‘dest_Tick v = NONE’ - by (Cases_on ‘v’ \\ Cases_on ‘w’ \\ gs [] - \\ gs [Once v_rel_def]) - \\ gs [] - \\ Cases_on ‘v’ \\ gvs [dest_anyThunk_def, v_rel_def] - >~[‘Recclosure _ _’] - >- (rename1 ‘LIST_REL _ (MAP SND xs) (MAP SND ys)’ - \\ ‘OPTREL exp_rel - (ALOOKUP (REVERSE xs) s) - (ALOOKUP (REVERSE ys) s)’ - by (irule LIST_REL_OPTREL - \\ gvs [LIST_REL_EL_EQN, ELIM_UNCURRY, EL_MAP, LIST_EQ_REWRITE]) - \\ gs [OPTREL_def] - \\ rename1 ‘exp_rel x0 y0’ - \\ ‘MEM (s, x0) xs’ by (rpt $ dxrule_then assume_tac ALOOKUP_MEM \\ gvs []) - \\ gvs [EVERY_MEM, MEM_MAP, PULL_EXISTS] - \\ first_assum $ dxrule_then assume_tac - \\ Cases_on ‘x0’ \\ gvs [ok_bind_def, exp_rel_def] - >~[‘subst_funs ys e2’] - >- (last_x_assum irule \\ simp [subst_funs_def] - \\ irule exp_rel_subst \\ simp [] - \\ gs [FORALL_PROD] - \\ gvs [MAP_MAP_o, combinTheory.o_DEF, LAMBDA_PROD, GSYM FST_THM, LIST_REL_EL_EQN, EL_MAP] - \\ rw [] \\ pairarg_tac \\ gs [] \\ pairarg_tac \\ gs [v_rel_def, LIST_REL_EL_EQN, EL_MAP] - \\ gs [EVERY_MEM, MEM_MAP, PULL_EXISTS, FORALL_PROD] - \\ rw [] - >- ( - rename [‘n < _’, ‘MAP FST xs = MAP FST ys’] - \\ ‘EL n (MAP FST xs) = EL n (MAP FST ys)’ by gs [] - \\ gvs [EL_MAP]) - \\ last_x_assum $ drule_then irule)) - \\ gs [subst_funs_def, subst_empty]) - \\ Cases_on ‘v’ \\ gs [v_rel_def, exp_rel_def, PULL_EXISTS, dest_Tick_def]*) - >~ [‘Delay x’] >- ( - rw [Once exp_rel_cases] \\ gs [] - \\ simp [eval_to_def, v_rel_def]) - >~ [‘MkTick x’] >- ( - rw [exp_rel_def] \\ gs [] - \\ simp [eval_to_def] - \\ rename1 ‘exp_rel x y’ - \\ first_x_assum $ drule_then mp_tac - \\ impl_tac >- ( - CCONTR_TAC>> - qpat_x_assum`_ ≠ _` mp_tac>> - simp[eval_to_def]>> - fs[]) - \\ Cases_on ‘eval_to k y’ \\ Cases_on ‘eval_to k x’ \\ gs [v_rel_def]) >~ [‘Prim op xs’] >- ( cheat + (* rw [] \\ gvs [Once exp_rel_def, eval_to_def] @@ -717,7 +748,9 @@ Proof \\ gen_tac \\ strip_tac \\ rename1 ‘n < _’ \\ rpt $ first_x_assum $ qspec_then ‘n’ assume_tac \\ gs [] \\ Cases_on ‘eval_to k (EL n xs)’ \\ gs [] - \\ CASE_TAC \\ gs [v_rel_def])*)) + \\ CASE_TAC \\ gs [v_rel_def])*) + ) + >~ [‘Monad mop xs’] >- ( rw [Once exp_rel_cases] \\ gs [] \\ simp [eval_to_def, v_rel_def]) From c586dfa7a3ccfc6eab074ea4d77557d9ebaf6823 Mon Sep 17 00:00:00 2001 From: artisanbk Date: Mon, 29 Dec 2025 18:12:47 +0800 Subject: [PATCH 4/9] some progress --- .../passes/proofs/thunk_force_delayScript.sml | 612 ++++++++++-------- 1 file changed, 340 insertions(+), 272 deletions(-) diff --git a/compiler/backend/passes/proofs/thunk_force_delayScript.sml b/compiler/backend/passes/proofs/thunk_force_delayScript.sml index 9d8f8087..ef1fb5ef 100644 --- a/compiler/backend/passes/proofs/thunk_force_delayScript.sml +++ b/compiler/backend/passes/proofs/thunk_force_delayScript.sml @@ -10,6 +10,7 @@ Ancestors string option sum pair list alist finite_map pred_set rich_list thunkLang thunkLang_primitives wellorder arithmetic pure_misc thunkLangProps thunk_semantics thunk_remove_unuseful_bindings + combin bool Libs term_tactic monadsyntax dep_rewrite @@ -338,277 +339,23 @@ Theorem exp_rel_eval_to[local]: Proof completeInduct_on ‘k’ \\ Induct using freevars_ind \\ rpt gen_tac - >~ [‘Var v’] >- ( - rw [Once exp_rel_cases] - \\ simp [eval_to_def]) - >~ [‘Value v’] >- ( + >~ [‘Var n’] >- ( rw [Once exp_rel_cases] \\ simp [eval_to_def]) - >~ [‘App g y’] >- ( - gvs [Once exp_rel_def, eval_to_def, PULL_EXISTS] \\ rw [] - \\ rename1 ‘exp_rel y x’ \\ rename1 ‘exp_rel g f’ - \\ first_x_assum $ drule_then assume_tac \\ gs [] - \\ Cases_on ‘eval_to k x’ \\ gs [] - \\ Cases_on ‘eval_to k y’ \\ gs [] - \\ rename1 ‘v_rel w1 v1’ - \\ first_x_assum $ drule_then assume_tac \\ gs [] - \\ Cases_on ‘eval_to k f’ - \\ Cases_on ‘eval_to k g’ \\ gs [] - \\ rename1 ‘v_rel w2 v2’ - \\ Cases_on ‘dest_anyClosure v2’ \\ gs [] - >- ( - Cases_on ‘v2’ \\ Cases_on ‘w2’ \\ gs [dest_anyClosure_def, v_rel_def] - \\ rename1 ‘LIST_REL _ (MAP SND xs) (MAP SND ys)’ - \\ ‘OPTREL exp_rel (ALOOKUP (REVERSE xs) s) (ALOOKUP (REVERSE ys) s)’ - by (irule LIST_REL_OPTREL - \\ gvs [LIST_REL_EL_EQN, ELIM_UNCURRY, LIST_EQ_REWRITE, EL_MAP]) - \\ gvs [OPTREL_def] - \\ rpt $ dxrule_then assume_tac ALOOKUP_MEM \\ gvs [EVERY_MEM, MEM_MAP, PULL_EXISTS, FORALL_PROD] - \\ last_x_assum $ dxrule_then assume_tac - \\ qpat_x_assum ‘exp_rel x0 _’ mp_tac - \\ rw [Once exp_rel_cases] \\ gs [ok_bind_def]) - \\ pairarg_tac \\ gvs [] - \\ ‘∃body' binds'. dest_anyClosure w2 = INR (s,body',binds')’ - by (Cases_on ‘v2’ \\ Cases_on ‘w2’ \\ gs [dest_anyClosure_def, v_rel_def] - >- (rename [‘LIST_REL _ (MAP SND xs) (MAP SND ys)’, ‘ALOOKUP _ s’] - \\ ‘OPTREL exp_rel (ALOOKUP (REVERSE xs) s) (ALOOKUP (REVERSE ys) s)’ - by (irule LIST_REL_OPTREL - \\ gvs [LIST_REL_EL_EQN, ELIM_UNCURRY, LIST_EQ_REWRITE, EL_MAP]) - \\ gvs [OPTREL_def] - \\ rpt $ dxrule_then assume_tac ALOOKUP_MEM \\ gvs [EVERY_MEM, MEM_MAP, PULL_EXISTS] - \\ last_x_assum $ dxrule_then assume_tac - \\ qpat_x_assum ‘exp_rel x0 _’ mp_tac - \\ rw [Once exp_rel_cases] \\ gvs [CaseEqs ["option", "exp"], ok_bind_def])) - \\ IF_CASES_TAC \\ gs [] - \\ last_x_assum $ qspec_then ‘k - 1’ irule \\ gs [] - \\ irule exp_rel_subst - \\ Cases_on ‘w2’ - \\ gvs [dest_anyClosure_def, v_rel_def, subst_APPEND] - \\ rename [‘LIST_REL _ (MAP SND xs) (MAP SND ys)’, ‘ALOOKUP _ s’] - \\ ‘OPTREL exp_rel (ALOOKUP (REVERSE xs) s) (ALOOKUP (REVERSE ys) s)’ - by (irule LIST_REL_OPTREL - \\ gvs [LIST_REL_EL_EQN, ELIM_UNCURRY, LIST_EQ_REWRITE, EL_MAP]) - \\ gvs [OPTREL_def] - \\ rename1 ‘exp_rel x' y'’ \\ Cases_on ‘x'’ \\ gvs [exp_rel_def] - \\ simp [MAP_MAP_o, combinTheory.o_DEF, LAMBDA_PROD, GSYM FST_THM] - \\ gs [LIST_REL_EL_EQN, EL_MAP] - \\ gen_tac \\ strip_tac - \\ pairarg_tac \\ fs [] - \\ pairarg_tac \\ fs [v_rel_def, LIST_REL_EL_EQN, EL_MAP] - \\ rename1 ‘n < _’ - \\ ‘EL n (MAP FST xs) = EL n (MAP FST ys)’ by simp [] - \\ gs [EL_MAP]) - - >~ [‘Lam s x’] >- ( - rw [Once exp_rel_cases] - \\ gs [eval_to_def, v_rel_def]) - - >~ [‘Let NONE x y’] >- ( - rw [exp_rel_def] \\ gs [] - \\ simp [eval_to_def] - \\ IF_CASES_TAC \\ gs [] - \\ rename1 ‘exp_rel x x2’ \\ rename1 ‘exp_rel y y2’ - \\ last_x_assum $ qspecl_then [‘k - 1’] assume_tac - \\ last_x_assum kall_tac \\ last_x_assum kall_tac \\ gvs [] - \\ last_assum $ dxrule_then assume_tac - \\ last_x_assum $ dxrule_then assume_tac - \\ Cases_on ‘eval_to (k - 1) x2’ - \\ Cases_on ‘eval_to (k - 1) x’ \\ gs [] - \\ fs[eval_to_def]) - - >~ [‘Let (SOME n) x y’] >- ( - rw [exp_rel_def] \\ gs [] - \\ simp [eval_to_def] - \\ IF_CASES_TAC \\ gs [] - \\ rename1 ‘exp_rel x x2’ \\ rename1 ‘exp_rel y y2’ - \\ last_x_assum $ qspecl_then [‘k - 1’] assume_tac - \\ last_x_assum kall_tac \\ last_x_assum kall_tac \\ gvs [] - \\ last_x_assum assume_tac - \\ last_assum $ dxrule_then assume_tac - \\ Cases_on ‘eval_to (k - 1) x2’ - \\ Cases_on ‘eval_to (k - 1) x’ \\ gs [] - \\ fs[eval_to_def, exp_rel_subst]) - - >~ [‘Letrec f x’] >- ( - rw [exp_rel_def] \\ gs [] - \\ simp [eval_to_def] - \\ IF_CASES_TAC \\ gs [] - \\ last_x_assum $ qspecl_then [‘k - 1’] assume_tac \\ gvs [] - \\ first_x_assum irule - \\ simp [subst_funs_def, closed_subst, MAP_MAP_o, combinTheory.o_DEF, - LAMBDA_PROD, GSYM FST_THM] - \\ strip_tac - >- ( - CCONTR_TAC - \\ fs[eval_to_def] - \\ metis_tac[subst_def, subst_funs_def] - ) - >- ( - irule exp_rel_subst - \\ gvs [MAP_MAP_o, combinTheory.o_DEF, LAMBDA_PROD, GSYM FST_THM, LIST_REL_EL_EQN, EL_MAP] - \\ rw [] \\ pairarg_tac \\ gs [] \\ pairarg_tac \\ gs [v_rel_def, LIST_REL_EL_EQN, EL_MAP] - \\ rename1 ‘MAP FST f = MAP FST g’ - \\ ‘∀i. i < LENGTH f ⇒ FST (EL i f) = FST (EL i g)’ - by (rw [] >> - ‘i < LENGTH f’ by gs [] >> - dxrule_then (qspecl_then [‘FST’] assume_tac) $ GSYM EL_MAP >> - ‘i < LENGTH g’ by gs [] >> - dxrule_then (qspecl_then [‘FST’] assume_tac) $ GSYM EL_MAP >> - rw []) - \\ gs [] \\ first_x_assum $ dxrule_then assume_tac \\ gvs [])) - - >~ [‘If x1 y1 z1’] >- ( - rw [exp_rel_def, eval_to_def] \\ gs [eval_to_def] - \\ rename1 ‘exp_rel x1 x2’ - \\ rename1 ‘exp_rel y1 y2’ \\ rename1 ‘exp_rel z1 z2’ - \\ last_x_assum $ qspecl_then [‘k - 1’] assume_tac \\ gvs [] - \\ rpt $ first_assum $ dxrule_then assume_tac - \\ last_x_assum kall_tac \\ last_x_assum kall_tac \\ gvs [] - \\ Cases_on ‘eval_to (k - 1) x2’ - \\ Cases_on ‘eval_to (k - 1) x1’ \\ gs [] - \\ rename1 ‘v_rel v1 w1’ - \\ IF_CASES_TAC \\ gvs [v_rel_def] - \\ IF_CASES_TAC \\ gvs [v_rel_def] - \\ IF_CASES_TAC \\ gs []) - - >~ [‘Force x’] >- ( - rw [exp_rel_def] \\ gs [] - >~[‘Force (Delay x)’] >-( - once_rewrite_tac [eval_to_def] - \\ IF_CASES_TAC \\ simp [] - \\ simp [Once eval_to_def, dest_anyThunk_def] - \\ simp [subst_funs_def, subst_empty] - \\ first_assum $ drule_at $ Pos $ el 2 - \\ disch_then (qspec_then `k-1` mp_tac) - \\ impl_tac - >-( - simp[] - \\ CCONTR_TAC - \\ qpat_x_assum` _ ≠ INL Type_error` mp_tac - \\ fs[] - \\ simp[Once eval_to_def] - \\ simp [Once eval_to_def, dest_anyThunk_def] - \\ simp [subst_funs_def, subst_empty]) - >-( - strip_tac - \\ Cases_on ‘eval_to (k - 1) x'’ - \\ rw[] - \\ qpat_x_assum` _ ≠ INL Type_error` mp_tac - \\ simp[Once eval_to_def] - \\ simp [Once eval_to_def, dest_anyThunk_def] - \\ simp [subst_funs_def, subst_empty])) - >~[`Force x`] >-( - rename1 ‘exp_rel x y’ - \\ once_rewrite_tac [eval_to_def] - \\ IF_CASES_TAC \\ gs [] - \\ last_assum $ qspecl_then [‘k - 1’] assume_tac \\ gvs [] - \\ last_assum $ drule_then assume_tac - \\ Cases_on ‘eval_to k y’ \\ Cases_on ‘eval_to k x’ \\ gvs [] - >~[`x''=x'`] >-( - `x'' ≠ Type_error` suffices_by fs[] - \\ CCONTR_TAC - \\ qpat_x_assum `eval_to k x = INL x''` MP_TAC - \\ fs[Once $ eval_to_def, exp_rel_def, v_rel_def] - \\ Cases_on `eval_to k x` \\ gvs[]) - >~[`dest_Tick y'`] >-( - `dest_Tick y' = NONE` by (Cases_on `y` \\ Cases_on `y'` \\ gs[Once $ eval_to_def]) - \\ gs[subst_funs_def, Once $ eval_to_def]) - - >~[`dest_Tick y''`] >-( - Cases_on `dest_Tick y''` \\ Cases_on `dest_Tick y'` - \\ gs [v_rel_def, exp_rel_def, PULL_EXISTS, dest_Tick_def] - >- ( - (*dest_Tick y'' = NONE ∧ dest_Tick y' = NONE*) - cheat - ) - >- ( - (*dest_Tick y'' = NONE ∧ dest_Tick y' = SOME*) - cheat - ) - >- ( - (*dest_Tick y'' = SOME ∧ dest_Tick y' = NONE*) - cheat - ) - >- ( - (*dest_Tick y'' = SOME ∧ dest_Tick y' = SOME*) - cheat - ) - ) - ) - - (* - ‘dest_Tick v = NONE’ - by (Cases_on ‘v’ \\ Cases_on ‘w’ \\ gs [] - \\ gs [Once v_rel_def]) - \\ gs [] - \\ Cases_on ‘v’ \\ gvs [dest_anyThunk_def, v_rel_def] - >~[‘Recclosure _ _’] - >- (rename1 ‘LIST_REL _ (MAP SND xs) (MAP SND ys)’ - \\ ‘OPTREL exp_rel - (ALOOKUP (REVERSE xs) s) - (ALOOKUP (REVERSE ys) s)’ - by (irule LIST_REL_OPTREL - \\ gvs [LIST_REL_EL_EQN, ELIM_UNCURRY, EL_MAP, LIST_EQ_REWRITE]) - \\ gs [OPTREL_def] - \\ rename1 ‘exp_rel x0 y0’ - \\ ‘MEM (s, x0) xs’ by (rpt $ dxrule_then assume_tac ALOOKUP_MEM \\ gvs []) - \\ gvs [EVERY_MEM, MEM_MAP, PULL_EXISTS] - \\ first_assum $ dxrule_then assume_tac - \\ Cases_on ‘x0’ \\ gvs [ok_bind_def, exp_rel_def] - >~[‘subst_funs ys e2’] - >- (last_x_assum irule \\ simp [subst_funs_def] - \\ irule exp_rel_subst \\ simp [] - \\ gs [FORALL_PROD] - \\ gvs [MAP_MAP_o, combinTheory.o_DEF, LAMBDA_PROD, GSYM FST_THM, LIST_REL_EL_EQN, EL_MAP] - \\ rw [] \\ pairarg_tac \\ gs [] \\ pairarg_tac \\ gs [v_rel_def, LIST_REL_EL_EQN, EL_MAP] - \\ gs [EVERY_MEM, MEM_MAP, PULL_EXISTS, FORALL_PROD] - \\ rw [] - >- ( - rename [‘n < _’, ‘MAP FST xs = MAP FST ys’] - \\ ‘EL n (MAP FST xs) = EL n (MAP FST ys)’ by gs [] - \\ gvs [EL_MAP]) - \\ last_x_assum $ drule_then irule)) - \\ gs [subst_funs_def, subst_empty]) - >~[`dest_Tick y''`] >-( - rename1 ‘v_rel v w’ - \\ Cases_on ‘dest_Tick w’ \\ gs [] - \\ Cases_on ‘v’ \\ gs [v_rel_def, exp_rel_def, PULL_EXISTS, dest_Tick_def]) - >~ [‘Delay x’] >- ( - rw [Once exp_rel_cases] \\ gs [] - \\ simp [eval_to_def, v_rel_def]) - >~ [‘MkTick x’] >- ( - rw [exp_rel_def] \\ gs [] - \\ simp [eval_to_def] - \\ rename1 ‘exp_rel x y’ - \\ first_x_assum $ drule_then mp_tac - \\ impl_tac >- ( - CCONTR_TAC>> - qpat_x_assum`_ ≠ _` mp_tac>> - simp[eval_to_def]>> - fs[]) - \\ Cases_on ‘eval_to k y’ \\ Cases_on ‘eval_to k x’ \\ gs [v_rel_def]) - )) - ) - *) - >~ [‘Prim op xs’] >- ( cheat - - (* - rw [] - \\ gvs [Once exp_rel_def, eval_to_def] - \\ gvs [MEM_EL, PULL_EXISTS, LIST_REL_EL_EQN] + \\ rpt strip_tac + \\ gvs [Once exp_rel_def, eval_to_def, MEM_EL, PULL_EXISTS, LIST_REL_EL_EQN] \\ Cases_on ‘op’ \\ gs [] - >- cheat (*(* Cons *) - last_x_assum kall_tac - \\ ‘($= +++ LIST_REL v_rel) (result_map (eval_to k) xs) - (result_map (eval_to k) ys)’ - suffices_by ( - strip_tac \\ gs [SF ETA_ss] + >~[`Cons _`] >-( (*stuck*) + qsuff_tac ‘($= +++ LIST_REL v_rel) (result_map (eval_to k) xs) (result_map (eval_to k) ys) ∧ (result_map (eval_to k) xs ≠ INL Type_error)’ + >- ( + cheat (* broken *) + \\ strip_tac \\ gs [SF ETA_ss] \\ Cases_on ‘result_map (eval_to k) ys’ - \\ Cases_on ‘result_map (eval_to k) xs’ \\ gs [v_rel_def]) + \\ Cases_on ‘result_map (eval_to k) xs’ \\ gs [v_rel_def, o_DEF, ETA_AX]) \\ gvs [result_map_def, MEM_EL, PULL_EXISTS, EL_MAP, SF CONJ_ss] \\ IF_CASES_TAC \\ gs [] >- ( @@ -646,8 +393,9 @@ Proof \\ first_x_assum (drule_all_then assume_tac) \\ Cases_on ‘eval_to k (EL n ys)’ \\ Cases_on ‘eval_to k (EL n xs)’ \\ gvs [] - \\ rename1 ‘INL err’ \\ Cases_on ‘err’ \\ gs [])*) - >- ((* IsEq *) + \\ rename1 ‘INL err’ \\ Cases_on ‘err’ \\ gs [])) + + >~ [`IsEq _ _ _`] >-( IF_CASES_TAC \\ gvs [LENGTH_EQ_NUM_compute] \\ rename1 ‘exp_rel x y’ \\ IF_CASES_TAC \\ gs [] @@ -659,7 +407,8 @@ Proof \\ Cases_on ‘v’ \\ Cases_on ‘w’ \\ gvs [LIST_REL_EL_EQN, v_rel_def] \\ IF_CASES_TAC \\ gs [] \\ rw [v_rel_def]) - >- ((* Proj *) + + >~[`Proj _ _`] >-( IF_CASES_TAC \\ gvs [LENGTH_EQ_NUM_compute] \\ rename1 ‘exp_rel x y’ \\ IF_CASES_TAC \\ gs [] @@ -670,7 +419,8 @@ Proof \\ rename1 ‘v_rel v w’ \\ Cases_on ‘v’ \\ Cases_on ‘w’ \\ gvs [LIST_REL_EL_EQN, v_rel_def] \\ IF_CASES_TAC \\ gs []) - >- ((* AtomOp *) + + >~[`AtomOp _`] >-( (*stuck*) Cases_on ‘k = 0’ \\ gs [] >- ( rw [result_map_def, MEM_MAP, MEM_EL, PULL_EXISTS] @@ -748,12 +498,329 @@ Proof \\ gen_tac \\ strip_tac \\ rename1 ‘n < _’ \\ rpt $ first_x_assum $ qspec_then ‘n’ assume_tac \\ gs [] \\ Cases_on ‘eval_to k (EL n xs)’ \\ gs [] - \\ CASE_TAC \\ gs [v_rel_def])*) - ) + \\ CASE_TAC \\ gs [v_rel_def]) + ) - >~ [‘Monad mop xs’] >- ( - rw [Once exp_rel_cases] \\ gs [] - \\ simp [eval_to_def, v_rel_def]) + >~ [‘Monad mop xs’] >- ( + rw [Once exp_rel_cases] \\ gs [] + \\ simp [eval_to_def, v_rel_def]) + + >~ [‘If x x' x''’] >- ( + rename1 `(If x1 y1 z1)` + \\ rw [exp_rel_def, eval_to_def] \\ gs [eval_to_def] + \\ rename1 ‘exp_rel x1 x2’ + \\ rename1 ‘exp_rel y1 y2’ \\ rename1 ‘exp_rel z1 z2’ + \\ last_x_assum $ qspecl_then [‘k - 1’] assume_tac \\ gvs [] + \\ rpt $ first_assum $ dxrule_then assume_tac + \\ last_x_assum kall_tac \\ last_x_assum kall_tac \\ gvs [] + \\ Cases_on ‘eval_to (k - 1) x2’ + \\ Cases_on ‘eval_to (k - 1) x1’ \\ gs [] + \\ rename1 ‘v_rel v1 w1’ + \\ IF_CASES_TAC \\ gvs [v_rel_def] + \\ IF_CASES_TAC \\ gvs [v_rel_def] + \\ IF_CASES_TAC \\ gs []) + + >~ [‘App x x'’] >- ( + rename [`App g y`] + \\ gvs [Once exp_rel_def, eval_to_def, PULL_EXISTS] \\ rw [] + \\ rename1 ‘exp_rel y x’ \\ rename1 ‘exp_rel g f’ + \\ first_x_assum $ drule_then assume_tac \\ gs [] + \\ Cases_on ‘eval_to k x’ \\ gs [] + \\ Cases_on ‘eval_to k y’ \\ gs [] + \\ rename1 ‘v_rel w1 v1’ + \\ first_x_assum $ drule_then assume_tac \\ gs [] + \\ Cases_on ‘eval_to k f’ + \\ Cases_on ‘eval_to k g’ \\ gs [] + \\ rename1 ‘v_rel w2 v2’ + \\ Cases_on ‘dest_anyClosure v2’ \\ gs [] + >- ( + Cases_on ‘v2’ \\ Cases_on ‘w2’ \\ gs [dest_anyClosure_def, v_rel_def] + \\ rename1 ‘LIST_REL _ (MAP SND xs) (MAP SND ys)’ + \\ ‘OPTREL exp_rel (ALOOKUP (REVERSE xs) s) (ALOOKUP (REVERSE ys) s)’ + by (irule LIST_REL_OPTREL + \\ gvs [LIST_REL_EL_EQN, ELIM_UNCURRY, LIST_EQ_REWRITE, EL_MAP]) + \\ gvs [OPTREL_def] + \\ rpt $ dxrule_then assume_tac ALOOKUP_MEM \\ gvs [EVERY_MEM, MEM_MAP, PULL_EXISTS, FORALL_PROD] + \\ last_x_assum $ dxrule_then assume_tac + \\ qpat_x_assum ‘exp_rel x0 _’ mp_tac + \\ rw [Once exp_rel_cases] \\ gs [ok_bind_def]) + \\ pairarg_tac \\ gvs [] + \\ ‘∃body' binds'. dest_anyClosure w2 = INR (s,body',binds')’ + by (Cases_on ‘v2’ \\ Cases_on ‘w2’ \\ gs [dest_anyClosure_def, v_rel_def] + >- (rename [‘LIST_REL _ (MAP SND xs) (MAP SND ys)’, ‘ALOOKUP _ s’] + \\ ‘OPTREL exp_rel (ALOOKUP (REVERSE xs) s) (ALOOKUP (REVERSE ys) s)’ + by (irule LIST_REL_OPTREL + \\ gvs [LIST_REL_EL_EQN, ELIM_UNCURRY, LIST_EQ_REWRITE, EL_MAP]) + \\ gvs [OPTREL_def] + \\ rpt $ dxrule_then assume_tac ALOOKUP_MEM \\ gvs [EVERY_MEM, MEM_MAP, PULL_EXISTS] + \\ last_x_assum $ dxrule_then assume_tac + \\ qpat_x_assum ‘exp_rel x0 _’ mp_tac + \\ rw [Once exp_rel_cases] \\ gvs [CaseEqs ["option", "exp"], ok_bind_def])) + \\ IF_CASES_TAC \\ gs [] + \\ last_x_assum $ qspec_then ‘k - 1’ irule \\ gs [] + \\ irule exp_rel_subst + \\ Cases_on ‘w2’ + \\ gvs [dest_anyClosure_def, v_rel_def, subst_APPEND] + \\ rename [‘LIST_REL _ (MAP SND xs) (MAP SND ys)’, ‘ALOOKUP _ s’] + \\ ‘OPTREL exp_rel (ALOOKUP (REVERSE xs) s) (ALOOKUP (REVERSE ys) s)’ + by (irule LIST_REL_OPTREL + \\ gvs [LIST_REL_EL_EQN, ELIM_UNCURRY, LIST_EQ_REWRITE, EL_MAP]) + \\ gvs [OPTREL_def] + \\ rename1 ‘exp_rel x' y'’ \\ Cases_on ‘x'’ \\ gvs [exp_rel_def] + \\ simp [MAP_MAP_o, combinTheory.o_DEF, LAMBDA_PROD, GSYM FST_THM] + \\ gs [LIST_REL_EL_EQN, EL_MAP] + \\ gen_tac \\ strip_tac + \\ pairarg_tac \\ fs [] + \\ pairarg_tac \\ fs [v_rel_def, LIST_REL_EL_EQN, EL_MAP] + \\ rename1 ‘n < _’ + \\ ‘EL n (MAP FST xs) = EL n (MAP FST ys)’ by simp [] + \\ gs [EL_MAP]) + + >~ [‘Lam s x’] >-( + rw [Once exp_rel_cases] + \\ gs [eval_to_def, v_rel_def]) + + >~ [‘Let NONE x x'’] >-( + rw [exp_rel_def] \\ gs [] + \\ simp [eval_to_def] + \\ IF_CASES_TAC \\ gs [] + \\ rename1 ‘exp_rel x x2’ \\ rename1 ‘exp_rel y y2’ + \\ last_x_assum $ qspecl_then [‘k - 1’] assume_tac + \\ last_x_assum kall_tac \\ last_x_assum kall_tac \\ gvs [] + \\ last_assum $ dxrule_then assume_tac + \\ last_x_assum $ dxrule_then assume_tac + \\ Cases_on ‘eval_to (k - 1) x2’ + \\ Cases_on ‘eval_to (k - 1) x’ \\ gs [] + \\ fs[eval_to_def]) + + >~ [‘Let (SOME s) x x'’] >- ( + rw [exp_rel_def] \\ gs [] + \\ simp [eval_to_def] + \\ IF_CASES_TAC \\ gs [] + \\ rename1 ‘exp_rel x x2’ \\ rename1 ‘exp_rel y y2’ + \\ last_x_assum $ qspecl_then [‘k - 1’] assume_tac + \\ last_x_assum kall_tac \\ last_x_assum kall_tac \\ gvs [] + \\ last_x_assum assume_tac + \\ last_assum $ dxrule_then assume_tac + \\ Cases_on ‘eval_to (k - 1) x2’ + \\ Cases_on ‘eval_to (k - 1) x’ \\ gs [] + \\ fs[eval_to_def, exp_rel_subst]) + + >~ [‘Letrec f x’] >- ( + rw [exp_rel_def] \\ gs [] + \\ simp [eval_to_def] + \\ IF_CASES_TAC \\ gs [] + \\ last_x_assum $ qspecl_then [‘k - 1’] assume_tac \\ gvs [] + \\ first_x_assum irule + \\ simp [subst_funs_def, closed_subst, MAP_MAP_o, combinTheory.o_DEF, + LAMBDA_PROD, GSYM FST_THM] + \\ strip_tac + >- ( + CCONTR_TAC + \\ fs[eval_to_def] + \\ metis_tac[subst_def, subst_funs_def] + ) + >- ( + irule exp_rel_subst + \\ gvs [MAP_MAP_o, combinTheory.o_DEF, LAMBDA_PROD, GSYM FST_THM, LIST_REL_EL_EQN, EL_MAP] + \\ rw [] \\ pairarg_tac \\ gs [] \\ pairarg_tac \\ gs [v_rel_def, LIST_REL_EL_EQN, EL_MAP] + \\ rename1 ‘MAP FST f = MAP FST g’ + \\ ‘∀i. i < LENGTH f ⇒ FST (EL i f) = FST (EL i g)’ + by (rw [] >> + ‘i < LENGTH f’ by gs [] >> + dxrule_then (qspecl_then [‘FST’] assume_tac) $ GSYM EL_MAP >> + ‘i < LENGTH g’ by gs [] >> + dxrule_then (qspecl_then [‘FST’] assume_tac) $ GSYM EL_MAP >> + rw []) + \\ gs [] \\ first_x_assum $ dxrule_then assume_tac \\ gvs [])) + + >~ [‘Delay x’] >- ( + rw [Once exp_rel_cases] \\ gs [] + \\ simp [eval_to_def, v_rel_def]) + + >~ [‘Force x’] >- ( + rw [exp_rel_def] \\ gs [] + >~[‘Force (Delay _)’] >-( + once_rewrite_tac [eval_to_def] + \\ IF_CASES_TAC \\ simp [] + \\ simp [Once eval_to_def, dest_anyThunk_def] + \\ simp [subst_funs_def, subst_empty] + \\ first_assum $ drule_at $ Pos $ el 2 + \\ disch_then (qspec_then `k-1` mp_tac) + \\ impl_tac + >-( + simp[] + \\ CCONTR_TAC + \\ qpat_x_assum` _ ≠ INL Type_error` mp_tac + \\ fs[] + \\ simp[Once eval_to_def] + \\ simp [Once eval_to_def, dest_anyThunk_def] + \\ simp [subst_funs_def, subst_empty]) + \\ strip_tac + \\ rfs[] + \\ Cases_on ‘eval_to (k - 1) x'’ + \\ rw[] + \\ qpat_x_assum` _ ≠ INL Type_error` mp_tac + \\ fs[] + \\ simp [Once eval_to_def] + \\ simp [Once eval_to_def, dest_anyThunk_def] + \\ simp [subst_funs_def, subst_empty]) + + >~[`Force _`] >-( + rename1 ‘exp_rel x y’ + \\ once_rewrite_tac [eval_to_def] + \\ IF_CASES_TAC \\ gs [] + \\ last_x_assum $ drule + \\ impl_tac + >- (CCONTR_TAC \\ fs[Once $ eval_to_def]) + \\ strip_tac + \\ Cases_on ‘eval_to k y’ \\ Cases_on ‘eval_to k x’ \\ gvs [] + \\ rename1 ‘v_rel v w’ + \\ Cases_on ‘dest_Tick w’ \\ gs [] + >~[`dest_Tick w = NONE`] >-( + ‘dest_Tick v = NONE’ by (Cases_on ‘v’ \\ Cases_on ‘w’ \\ gs [Once v_rel_def]) + \\ Cases_on ‘v’ \\ gvs [dest_anyThunk_def, v_rel_def] + + >~[‘Recclosure _ _’] >-( + rename1 ‘LIST_REL _ (MAP SND xs) (MAP SND ys)’ + \\ ‘OPTREL exp_rel (ALOOKUP (REVERSE xs) s) (ALOOKUP (REVERSE ys) s)’ + by (irule LIST_REL_OPTREL \\ gvs [LIST_REL_EL_EQN, ELIM_UNCURRY, EL_MAP, LIST_EQ_REWRITE]) + \\ gs [OPTREL_def] + \\rename1 `exp_rel x0 y0` + \\ ‘MEM (s, x0) xs’ by (rpt $ dxrule_then assume_tac ALOOKUP_MEM \\ gvs []) + \\ gvs [EVERY_MEM, MEM_MAP, PULL_EXISTS] + \\ Cases_on ‘x0’ \\ gs [ok_bind_def, exp_rel_def] + \\ qsuff_tac `($= +++ v_rel) (eval_to (k − 1) (subst_funs xs e)) (eval_to (k − 1) (subst_funs ys y'))` + >~[`($= +++ v_rel) _ _ ⇒ ($= +++ v_rel) _ _`] >-( + \\ rpt strip_tac + (* stuck on last case *) + \\ Cases_on `eval_to (k-1) (subst_funs xs e)` + \\ Cases_on `eval_to (k-1) (subst_funs ys y')` + \\ gs[SUM_REL_THM, is_anyThunk_def] + `is_anyThunk y'' <=> is_anyThunk y'''` by ( + cheat + ) + \\ rw[is_anyThunk_def]) + + >~[`($= +++ v_rel) _ _`] >-( + last_x_assum $ irule + \\ conj_tac + >- (cheat) + >- ( + simp[subst_funs_def] + \\ irule exp_rel_subst \\ simp[] + \\ gs [FORALL_PROD] + \\ gvs [MAP_MAP_o, o_DEF, LAMBDA_PROD, GSYM FST_THM, LIST_REL_EL_EQN, EL_MAP] + \\ rw [] \\ pairarg_tac \\ gs [] \\ pairarg_tac \\ gs [v_rel_def, LIST_REL_EL_EQN, EL_MAP] + \\ gs [EVERY_MEM, MEM_MAP, PULL_EXISTS, FORALL_PROD] + \\ rw [] + >- ( + rename [‘n < _’, ‘MAP FST xs = MAP FST ys’] + \\ ‘EL n (MAP FST xs) = EL n (MAP FST ys)’ by gs [] + \\ gvs [EL_MAP]) + \\ last_x_assum $ drule_then irule))) + + >~[`Thunk _ _`] >-( + simp[subst_funs_def] + \\ `k-1 < k` by fs[] + \\ res_tac + \\ `eval_to (k-1) e ≠ INL Type_error ∧ eval_to (k-1) x ≠ INL Type_error` by ( + CONJ_TAC + >- ( + cheat + ) + >- ( + CCONTR_TAC + \\ qpat_x_assum `eval_to k (Force x) ≠ INL Type_error` mp_tac + \\ simp[] + \\ `eval_to k x = INL Type_error` by ( + qspecl_then [`k-1`, `x`, `k`] assume_tac eval_to_mono \\ fs[]) + \\ fs[Once $ eval_to_def])) + \\ Cases_on `eval_to (k-1) e` \\ Cases_on `eval_to (k-1) y'` \\ gs[] + \\ Cases_on `is_anyThunk y''` \\ Cases_on `is_anyThunk y'''` \\ gs[SUM_REL_THM] + >- ( + cheat \\ + qpat_x_assum `¬is_anyThunk y'''` mp_tac \\ fs[] + \\ qspecl_then [`y''`, `y'''`] mp_tac v_rel_anyThunk + \\ fs[] + \\ impl_tac + \\ fs[] (*????*)) + >- (cheat) + ) + ) + + >~[`dest_Tick w = SOME _`] >-( + Cases_on ‘v’ \\ gs [v_rel_def, dest_Tick_def] + \\ `k-1 < k` by simp [] + \\ first_x_assum $ drule \\ strip_tac + \\ first_assum $ drule + \\ impl_tac + >- ( + CCONTR_TAC + \\ qpat_x_assum `_ = INR (DoTick v')` mp_tac \\ fs[Once $ eval_to_def] + \\ `eval_to (k-1) x = eval_to k x` by simp[eval_to_mono] \\ fs[]) + >- ( + cheat \\ + strip_tac + \\ last_assum $ irule + \\ conj_tac \\ simp[exp_rel_def, Once $ eval_to_def] + \\ IF_CASES_TAC \\ gs[] + (*stuck*))) + ) + + (*old proof -- Force case *) + (* + ‘dest_Tick v = NONE’ + by (Cases_on ‘v’ \\ Cases_on ‘w’ \\ gs [] + \\ gs [Once v_rel_def]) + \\ gs [] + \\ Cases_on ‘v’ \\ gvs [dest_anyThunk_def, v_rel_def] + >~[‘Recclosure _ _’] + >- (rename1 ‘LIST_REL _ (MAP SND xs) (MAP SND ys)’ + \\ ‘OPTREL exp_rel + (ALOOKUP (REVERSE xs) s) + (ALOOKUP (REVERSE ys) s)’ + by (irule LIST_REL_OPTREL + \\ gvs [LIST_REL_EL_EQN, ELIM_UNCURRY, EL_MAP, LIST_EQ_REWRITE]) + \\ gs [OPTREL_def] + \\ rename1 ‘exp_rel x0 y0’ + \\ ‘MEM (s, x0) xs’ by (rpt $ dxrule_then assume_tac ALOOKUP_MEM \\ gvs []) + \\ gvs [EVERY_MEM, MEM_MAP, PULL_EXISTS] + + \\ first_assum $ dxrule_then assume_tac + \\ Cases_on ‘x0’ \\ gvs [ok_bind_def, exp_rel_def] + >~[‘subst_funs ys e2’] + + >- ( + last_x_assum irule \\ simp [subst_funs_def] + \\ irule exp_rel_subst \\ simp [] + \\ gs [FORALL_PROD] + \\ gvs [MAP_MAP_o, combinTheory.o_DEF, LAMBDA_PROD, GSYM FST_THM, LIST_REL_EL_EQN, EL_MAP] + \\ rw [] \\ pairarg_tac \\ gs [] \\ pairarg_tac \\ gs [v_rel_def, LIST_REL_EL_EQN, EL_MAP] + \\ gs [EVERY_MEM, MEM_MAP, PULL_EXISTS, FORALL_PROD] + \\ rw [] + >- ( + rename [‘n < _’, ‘MAP FST xs = MAP FST ys’] + \\ ‘EL n (MAP FST xs) = EL n (MAP FST ys)’ by gs [] + \\ gvs [EL_MAP]) + \\ last_x_assum $ drule_then irule)) + \\ gs [subst_funs_def, subst_empty]) *) + + >~ [‘Value v’] >- ( + rw [Once exp_rel_cases] + \\ simp [eval_to_def]) + + >~ [‘MkTick x’] >- ( + rw [exp_rel_def] \\ gs [] + \\ simp [eval_to_def] + \\ rename1 ‘exp_rel x y’ + \\ first_x_assum $ drule_then mp_tac + \\ impl_tac >- ( + CCONTR_TAC>> + qpat_x_assum`_ ≠ _` mp_tac>> + simp[eval_to_def]>> + fs[]) + \\ Cases_on ‘eval_to k y’ \\ Cases_on ‘eval_to k x’ \\ gs [v_rel_def]) QED (* TODO: broken under here *) @@ -900,3 +967,4 @@ Proof \\ gs [closed_def] QED + From 97cfc4b7c9b7be9e3b982c1f671ae23317e210e5 Mon Sep 17 00:00:00 2001 From: tanyongkiam Date: Tue, 30 Dec 2025 16:06:54 +0800 Subject: [PATCH 5/9] fix some cheats --- .../passes/proofs/thunk_force_delayScript.sml | 93 ++++++++++++++----- 1 file changed, 72 insertions(+), 21 deletions(-) diff --git a/compiler/backend/passes/proofs/thunk_force_delayScript.sml b/compiler/backend/passes/proofs/thunk_force_delayScript.sml index ef1fb5ef..9930f9c9 100644 --- a/compiler/backend/passes/proofs/thunk_force_delayScript.sml +++ b/compiler/backend/passes/proofs/thunk_force_delayScript.sml @@ -331,6 +331,45 @@ Proof \\ gs [exp_rel_MkTick]) QED +Theorem bind_not_error: + monad_bind f g ≠ INL Type_error + ⇒ + f ≠ INL Type_error +Proof + CCONTR_TAC>>gs[] +QED + +Theorem v_rel_anyThunk: + (∀x y. exp_rel x y ⇒ T) ∧ + (∀v w. v_rel v w ⇒ (is_anyThunk v ⇔ is_anyThunk w)) +Proof + ho_match_mp_tac exp_rel_strongind + \\ rw[] \\ gvs [SF ETA_ss] + \\ rw [is_anyThunk_def, dest_anyThunk_def] + \\ simp[AllCaseEqs(),PULL_EXISTS] + \\ + `OPTREL exp_rel + (ALOOKUP (REVERSE f) n) + (ALOOKUP (REVERSE g) n)` by ( + irule LIST_REL_OPTREL >> + fs[LIST_REL_MAP,MAP_EQ_EVERY2]>> + gvs[LIST_REL_EL_EQN]>>rw[]>> + rpt (pairarg_tac>>gvs[])>> + metis_tac[FST,SND])>> + eq_tac>>rw[]>> + gvs[OPTREL_SOME,Once exp_rel_cases] +QED + +Theorem LIST_REL_EVERY_EVERY: + LIST_REL R xs ys ∧ + EVERY P xs ∧ + (∀x y. R x y ∧ P x ⇒ Q y) ⇒ + EVERY Q ys +Proof + rw[EVERY_EL,LIST_REL_EL_EQN]>> + metis_tac[] +QED + Theorem exp_rel_eval_to[local]: ∀x y. exp_rel x y ∧ @@ -345,17 +384,28 @@ Proof \\ simp [eval_to_def]) >~ [‘Prim op xs’] >- ( - cheat - \\ rpt strip_tac + rpt strip_tac \\ gvs [Once exp_rel_def, eval_to_def, MEM_EL, PULL_EXISTS, LIST_REL_EL_EQN] \\ Cases_on ‘op’ \\ gs [] - >~[`Cons _`] >-( (*stuck*) - qsuff_tac ‘($= +++ LIST_REL v_rel) (result_map (eval_to k) xs) (result_map (eval_to k) ys) ∧ (result_map (eval_to k) xs ≠ INL Type_error)’ + >- ( (* op = Cons *) + drule_then assume_tac bind_not_error>> + qsuff_tac ‘ + ($= +++ LIST_REL v_rel) + (result_map (eval_to k) xs) + (result_map (eval_to k) ys)’ >- ( - cheat (* broken *) - \\ strip_tac \\ gs [SF ETA_ss] - \\ Cases_on ‘result_map (eval_to k) ys’ - \\ Cases_on ‘result_map (eval_to k) xs’ \\ gs [v_rel_def, o_DEF, ETA_AX]) + strip_tac \\ gs [SF ETA_ss] + \\ Cases_on ‘result_map (eval_to k) ys’ + \\ Cases_on ‘result_map (eval_to k) xs’ + \\ gs[o_DEF,SF ETA_ss] + \\ IF_CASES_TAC + >- gs[v_rel_def] + \\ `F` by + (pop_assum mp_tac + \\ fs[] + \\ drule_at_then Any irule LIST_REL_EVERY_EVERY + \\ first_x_assum (irule_at Any) + \\ metis_tac[v_rel_anyThunk]) ) \\ gvs [result_map_def, MEM_EL, PULL_EXISTS, EL_MAP, SF CONJ_ss] \\ IF_CASES_TAC \\ gs [] >- ( @@ -395,7 +445,7 @@ Proof \\ Cases_on ‘eval_to k (EL n xs)’ \\ gvs [] \\ rename1 ‘INL err’ \\ Cases_on ‘err’ \\ gs [])) - >~ [`IsEq _ _ _`] >-( + >- ( (* IsEq *) IF_CASES_TAC \\ gvs [LENGTH_EQ_NUM_compute] \\ rename1 ‘exp_rel x y’ \\ IF_CASES_TAC \\ gs [] @@ -408,7 +458,7 @@ Proof \\ IF_CASES_TAC \\ gs [] \\ rw [v_rel_def]) - >~[`Proj _ _`] >-( + >- ( (* Proj *) IF_CASES_TAC \\ gvs [LENGTH_EQ_NUM_compute] \\ rename1 ‘exp_rel x y’ \\ IF_CASES_TAC \\ gs [] @@ -420,7 +470,7 @@ Proof \\ Cases_on ‘v’ \\ Cases_on ‘w’ \\ gvs [LIST_REL_EL_EQN, v_rel_def] \\ IF_CASES_TAC \\ gs []) - >~[`AtomOp _`] >-( (*stuck*) + >- ( (* AtomOp *) Cases_on ‘k = 0’ \\ gs [] >- ( rw [result_map_def, MEM_MAP, MEM_EL, PULL_EXISTS] @@ -519,7 +569,7 @@ Proof \\ IF_CASES_TAC \\ gvs [v_rel_def] \\ IF_CASES_TAC \\ gvs [v_rel_def] \\ IF_CASES_TAC \\ gs []) - + >~ [‘App x x'’] >- ( rename [`App g y`] \\ gvs [Once exp_rel_def, eval_to_def, PULL_EXISTS] \\ rw [] @@ -605,7 +655,7 @@ Proof \\ Cases_on ‘eval_to (k - 1) x2’ \\ Cases_on ‘eval_to (k - 1) x’ \\ gs [] \\ fs[eval_to_def, exp_rel_subst]) - + >~ [‘Letrec f x’] >- ( rw [exp_rel_def] \\ gs [] \\ simp [eval_to_def] @@ -696,16 +746,16 @@ Proof (* stuck on last case *) \\ Cases_on `eval_to (k-1) (subst_funs xs e)` \\ Cases_on `eval_to (k-1) (subst_funs ys y')` - \\ gs[SUM_REL_THM, is_anyThunk_def] - `is_anyThunk y'' <=> is_anyThunk y'''` by ( - cheat - ) - \\ rw[is_anyThunk_def]) + \\ gs[SUM_REL_THM] + \\ drule (cj 2 v_rel_anyThunk) + \\ rw[]) >~[`($= +++ v_rel) _ _`] >-( last_x_assum $ irule \\ conj_tac - >- (cheat) + >- ( + gs[Once eval_to_def,dest_anyThunk_def] + \\ metis_tac[bind_not_error]) >- ( simp[subst_funs_def] \\ irule exp_rel_subst \\ simp[] @@ -724,7 +774,8 @@ Proof simp[subst_funs_def] \\ `k-1 < k` by fs[] \\ res_tac - \\ `eval_to (k-1) e ≠ INL Type_error ∧ eval_to (k-1) x ≠ INL Type_error` by ( + \\ `eval_to (k-1) e ≠ INL Type_error ∧ + eval_to (k-1) x ≠ INL Type_error` by ( CONJ_TAC >- ( cheat @@ -756,7 +807,7 @@ Proof \\ first_assum $ drule \\ impl_tac >- ( - CCONTR_TAC + CCONTR_TAC \\ qpat_x_assum `_ = INR (DoTick v')` mp_tac \\ fs[Once $ eval_to_def] \\ `eval_to (k-1) x = eval_to k x` by simp[eval_to_mono] \\ fs[]) >- ( From 7bb624c8196dfbec6706abd71f2e66ac22a368b1 Mon Sep 17 00:00:00 2001 From: artisanbk Date: Fri, 2 Jan 2026 00:58:55 +0800 Subject: [PATCH 6/9] some progress --- .../passes/proofs/thunk_force_delayScript.sml | 136 ++++++++++++------ 1 file changed, 90 insertions(+), 46 deletions(-) diff --git a/compiler/backend/passes/proofs/thunk_force_delayScript.sml b/compiler/backend/passes/proofs/thunk_force_delayScript.sml index 9930f9c9..7d71d2db 100644 --- a/compiler/backend/passes/proofs/thunk_force_delayScript.sml +++ b/compiler/backend/passes/proofs/thunk_force_delayScript.sml @@ -383,9 +383,9 @@ Proof rw [Once exp_rel_cases] \\ simp [eval_to_def]) - >~ [‘Prim op xs’] >- ( + >~ [‘Prim op xs’] >-( rpt strip_tac - \\ gvs [Once exp_rel_def, eval_to_def, MEM_EL, PULL_EXISTS, LIST_REL_EL_EQN] + \\ gs [Once exp_rel_def, eval_to_def, MEM_EL, PULL_EXISTS, LIST_REL_EL_EQN] \\ Cases_on ‘op’ \\ gs [] >- ( (* op = Cons *) drule_then assume_tac bind_not_error>> @@ -400,18 +400,53 @@ Proof \\ gs[o_DEF,SF ETA_ss] \\ IF_CASES_TAC >- gs[v_rel_def] - \\ `F` by - (pop_assum mp_tac + \\ `F` by ( + pop_assum mp_tac \\ fs[] \\ drule_at_then Any irule LIST_REL_EVERY_EVERY \\ first_x_assum (irule_at Any) - \\ metis_tac[v_rel_anyThunk]) ) - \\ gvs [result_map_def, MEM_EL, PULL_EXISTS, EL_MAP, SF CONJ_ss] - \\ IF_CASES_TAC \\ gs [] - >- ( - first_x_assum (drule_all_then assume_tac) + \\ metis_tac[v_rel_anyThunk])) + \\ gs [result_map_def, MEM_EL, PULL_EXISTS, EL_MAP, SF CONJ_ss, bind_not_error] + \\ IF_CASES_TAC \\ gs [bind_not_error] \\ IF_CASES_TAC + >- ( (* LHS = INL Diverge *) + first_x_assum mp_tac \\ strip_tac + \\ `($= +++ v_rel) (eval_to k (EL n xs)) (eval_to k (EL n ys))` by fs[] + \\ Cases_on ‘eval_to k (EL n ys)’ + >- ( (*eval_to k (EL n ys) = INL x*) + Cases_on `x` + >- ( (* x = Type_error *) + CCONTR_TAC + \\ qpat_x_assum `($= +++ v_rel) (eval_to k (EL n xs)) (INL _)` mp_tac + \\ fs[]) + >- ( (* x = Diverge *) + IF_CASES_TAC + >- ( + fs[] + \\ res_tac + \\ qpat_x_assum `eval_to k (EL n' xs) ≠ INL Type_error ⇒ + ($= +++ v_rel) (eval_to k (EL n' xs)) (eval_to k (EL n' ys))` mp_tac + \\ `eval_to k (EL n' xs) ≠ INL Type_error` by ( + qpat_x_assum `!n. _ ⇒ ¬(n < LENGTH ys)` (fn thm => qspec_then `n'` assume_tac thm) + \\ `n' < LENGTH ys ⇒ ¬(eval_to k (EL n' xs) = INL Type_error)` + by simp[Once $ MONO_NOT_EQ] + \\ fs[]) + \\ strip_tac + \\ `($= +++ v_rel) (eval_to k (EL n' xs)) (eval_to k (EL n' ys))` by fs[] + \\ qpat_x_assum `($= +++ v_rel) (eval_to k (EL n' xs)) (eval_to k (EL n' ys))` mp_tac + \\ qpat_x_assum `eval_to k (EL n' ys) = _` (fn thm => pure_rewrite_tac [thm]) + \\ Cases_on `eval_to k (EL n' xs)` \\ fs[]) + >- ( + IF_CASES_TAC \\ simp[] + \\ qpat_x_assum `n < LENGTH ys` mp_tac \\ fs[]))) + >- ((*eval_to k (EL n ys) = INR x*) + IF_CASES_TAC \\ gs[])) + >-((*LHS = INR _ *) + cheat)) + + + (* \\ first_x_assum $ drule_all_then assume_tac - \\ Cases_on ‘eval_to k (EL n ys)’ \\ gvs [] + \\ Cases_on ‘eval_to k (EL n ys)’ \\ gs [] \\ rw [] \\ gs [SF SFY_ss]) \\ ‘∀n. n < LENGTH ys ⇒ ($= +++ v_rel) (eval_to k (EL n xs)) @@ -444,8 +479,9 @@ Proof \\ Cases_on ‘eval_to k (EL n ys)’ \\ Cases_on ‘eval_to k (EL n xs)’ \\ gvs [] \\ rename1 ‘INL err’ \\ Cases_on ‘err’ \\ gs [])) + *) - >- ( (* IsEq *) + >-( (* IsEq *) IF_CASES_TAC \\ gvs [LENGTH_EQ_NUM_compute] \\ rename1 ‘exp_rel x y’ \\ IF_CASES_TAC \\ gs [] @@ -458,7 +494,7 @@ Proof \\ IF_CASES_TAC \\ gs [] \\ rw [v_rel_def]) - >- ( (* Proj *) + >-( (* Proj *) IF_CASES_TAC \\ gvs [LENGTH_EQ_NUM_compute] \\ rename1 ‘exp_rel x y’ \\ IF_CASES_TAC \\ gs [] @@ -470,9 +506,9 @@ Proof \\ Cases_on ‘v’ \\ Cases_on ‘w’ \\ gvs [LIST_REL_EL_EQN, v_rel_def] \\ IF_CASES_TAC \\ gs []) - >- ( (* AtomOp *) + >-( (* AtomOp *) Cases_on ‘k = 0’ \\ gs [] - >- ( + >- ( (*k = 0*) rw [result_map_def, MEM_MAP, MEM_EL, PULL_EXISTS] \\ Cases_on ‘ys = []’ \\ gs [] >- ( @@ -480,9 +516,10 @@ Proof \\ CASE_TAC \\ gs [v_rel_def]) \\ ‘xs ≠ []’ by (strip_tac \\ gs []) \\ first_x_assum (qspec_then ‘0’ assume_tac) \\ gs []) + (* k ≠ 0 *) \\ qmatch_goalsub_abbrev_tac ‘result_map f ys’ \\ last_x_assum $ qspecl_then [‘k - 1’] assume_tac - \\ last_x_assum kall_tac \\ gvs [] + \\ last_x_assum kall_tac \\ gvs [bind_not_error] \\ ‘result_map f xs = result_map f ys’ suffices_by ( strip_tac \\ gs [SF ETA_ss] @@ -494,10 +531,8 @@ Proof \\ Cases_on ‘k’ \\ gs [arithmeticTheory.ADD1] \\ rename1 ‘eval_to k’ \\ ‘∀n. n < LENGTH ys ⇒ - ($= +++ v_rel) (eval_to k (EL n xs)) - (eval_to k (EL n ys))’ - by rw [] - \\ qpat_x_assum ‘∀x y. exp_rel _ _ ⇒ _’ kall_tac + ($= +++ v_rel) (eval_to k (EL n xs)) (eval_to k (EL n ys))’ by (cheat) (*rest of proof works*) + (*\\ qpat_x_assum ‘∀x y. exp_rel _ _ ⇒ _’ kall_tac*) \\ IF_CASES_TAC \\ gs [] >- ( rename1 ‘m < LENGTH ys’ @@ -548,8 +583,8 @@ Proof \\ gen_tac \\ strip_tac \\ rename1 ‘n < _’ \\ rpt $ first_x_assum $ qspec_then ‘n’ assume_tac \\ gs [] \\ Cases_on ‘eval_to k (EL n xs)’ \\ gs [] - \\ CASE_TAC \\ gs [v_rel_def]) - ) + \\ CASE_TAC \\ gs [v_rel_def] + \\ Cases_on `y` \\ gs[v_rel_def])) >~ [‘Monad mop xs’] >- ( rw [Once exp_rel_cases] \\ gs [] @@ -730,7 +765,6 @@ Proof >~[`dest_Tick w = NONE`] >-( ‘dest_Tick v = NONE’ by (Cases_on ‘v’ \\ Cases_on ‘w’ \\ gs [Once v_rel_def]) \\ Cases_on ‘v’ \\ gvs [dest_anyThunk_def, v_rel_def] - >~[‘Recclosure _ _’] >-( rename1 ‘LIST_REL _ (MAP SND xs) (MAP SND ys)’ \\ ‘OPTREL exp_rel (ALOOKUP (REVERSE xs) s) (ALOOKUP (REVERSE ys) s)’ @@ -742,14 +776,13 @@ Proof \\ Cases_on ‘x0’ \\ gs [ok_bind_def, exp_rel_def] \\ qsuff_tac `($= +++ v_rel) (eval_to (k − 1) (subst_funs xs e)) (eval_to (k − 1) (subst_funs ys y'))` >~[`($= +++ v_rel) _ _ ⇒ ($= +++ v_rel) _ _`] >-( - \\ rpt strip_tac + rpt strip_tac (* stuck on last case *) \\ Cases_on `eval_to (k-1) (subst_funs xs e)` \\ Cases_on `eval_to (k-1) (subst_funs ys y')` \\ gs[SUM_REL_THM] \\ drule (cj 2 v_rel_anyThunk) \\ rw[]) - >~[`($= +++ v_rel) _ _`] >-( last_x_assum $ irule \\ conj_tac @@ -772,31 +805,39 @@ Proof >~[`Thunk _ _`] >-( simp[subst_funs_def] - \\ `k-1 < k` by fs[] - \\ res_tac - \\ `eval_to (k-1) e ≠ INL Type_error ∧ - eval_to (k-1) x ≠ INL Type_error` by ( - CONJ_TAC - >- ( - cheat - ) - >- ( + \\ last_x_assum $ qspec_then `k-1` assume_tac + \\ `eval_to (k-1) x ≠ INL Type_error` by ( CCONTR_TAC \\ qpat_x_assum `eval_to k (Force x) ≠ INL Type_error` mp_tac \\ simp[] \\ `eval_to k x = INL Type_error` by ( qspecl_then [`k-1`, `x`, `k`] assume_tac eval_to_mono \\ fs[]) - \\ fs[Once $ eval_to_def])) - \\ Cases_on `eval_to (k-1) e` \\ Cases_on `eval_to (k-1) y'` \\ gs[] - \\ Cases_on `is_anyThunk y''` \\ Cases_on `is_anyThunk y'''` \\ gs[SUM_REL_THM] - >- ( - cheat \\ - qpat_x_assum `¬is_anyThunk y'''` mp_tac \\ fs[] - \\ qspecl_then [`y''`, `y'''`] mp_tac v_rel_anyThunk - \\ fs[] - \\ impl_tac - \\ fs[] (*????*)) + \\ fs[Once $ eval_to_def]) + \\ `k-1 < k` by fs[] + \\ Cases_on `eval_to (k-1) e` \\ Cases_on `eval_to (k-1) y'` \\ gs[bind_not_error] >- (cheat) + >- ( + qsuff_tac `is_anyThunk y''` + >- (strip_tac \\ fs[]) + >- ( + Cases_on `y''` \\ simp[is_anyThunk_def, dest_anyThunk_def, dest_Thunk_def, v_rel_anyThunk] + \\ cheat + ) + ) + >- ( + Cases_on `is_anyThunk y''` \\ Cases_on `is_anyThunk y'''` \\ gs[] + >- ( + qpat_x_assum `¬ is_anyThunk y'''` mp_tac \\ fs[] + \\ mp_tac v_rel_anyThunk \\ strip_tac + \\ `is_anyThunk y'' ⇔ is_anyThunk y'''` by ( + first_x_assum irule \\ fs[]) + \\ fs[]) + >- ( + qpat_x_assum `¬ is_anyThunk y''` mp_tac \\ fs[] + \\ mp_tac v_rel_anyThunk \\ strip_tac + `is_anyThunk y'' ⇔ is_anyThunk y'''` by ( + first_x_assum irule \\ fs[]) + \\ fs[]))) ) ) @@ -811,11 +852,14 @@ Proof \\ qpat_x_assum `_ = INR (DoTick v')` mp_tac \\ fs[Once $ eval_to_def] \\ `eval_to (k-1) x = eval_to k x` by simp[eval_to_mono] \\ fs[]) >- ( - cheat \\ strip_tac \\ last_assum $ irule - \\ conj_tac \\ simp[exp_rel_def, Once $ eval_to_def] - \\ IF_CASES_TAC \\ gs[] + \\ conj_tac \\ fs[exp_rel_def] + \\ simp[Once $ eval_to_def] \\ IF_CASES_TAC \\ fs[] + \\ simp[Once $ eval_to_def] + \\ CASE_TAC \\ gs[bind_not_error] + \\ Cases_on `v'` \\ gs[dest_anyThunk_def] + cheat (*stuck*))) ) From 9da8899fa3c7f4bbeaef04cb2957a55940d1f4c0 Mon Sep 17 00:00:00 2001 From: artisanbk Date: Mon, 5 Jan 2026 23:04:29 +0800 Subject: [PATCH 7/9] exp_rel_eval_to proof --- .../passes/proofs/thunk_force_delayScript.sml | 195 +++++++----------- 1 file changed, 80 insertions(+), 115 deletions(-) diff --git a/compiler/backend/passes/proofs/thunk_force_delayScript.sml b/compiler/backend/passes/proofs/thunk_force_delayScript.sml index 7d71d2db..67db0ada 100644 --- a/compiler/backend/passes/proofs/thunk_force_delayScript.sml +++ b/compiler/backend/passes/proofs/thunk_force_delayScript.sml @@ -370,6 +370,7 @@ Proof metis_tac[] QED + Theorem exp_rel_eval_to[local]: ∀x y. exp_rel x y ∧ @@ -441,46 +442,45 @@ Proof >- ((*eval_to k (EL n ys) = INR x*) IF_CASES_TAC \\ gs[])) >-((*LHS = INR _ *) - cheat)) - - - (* - \\ first_x_assum $ drule_all_then assume_tac - \\ Cases_on ‘eval_to k (EL n ys)’ \\ gs [] - \\ rw [] \\ gs [SF SFY_ss]) - \\ ‘∀n. n < LENGTH ys ⇒ - ($= +++ v_rel) (eval_to k (EL n xs)) - (eval_to k (EL n ys))’ - by rw [] - \\ last_x_assum kall_tac - \\ IF_CASES_TAC \\ gs [] - >- ( - IF_CASES_TAC \\ gs [] - >- ( - first_x_assum $ drule_then assume_tac - \\ last_x_assum $ drule_then assume_tac - \\ rename1 ‘eval_to _ (EL m ys) = INL Type_error’ - \\ Cases_on ‘eval_to k (EL m xs)’ \\ gs []) - \\ first_x_assum (drule_then assume_tac) - \\ Cases_on ‘eval_to k (EL n ys)’ \\ gs [] - \\ IF_CASES_TAC \\ gvs []) - \\ rw [] \\ gs [SF SFY_ss] - >- ( - first_x_assum $ drule_then assume_tac \\ gs [] - \\ rename1 ‘n < _’ - \\ Cases_on ‘eval_to k (EL n xs)’ \\ gs []) - >- ( - first_x_assum $ drule_then assume_tac \\ gs [] - \\ rename1 ‘n < _’ - \\ Cases_on ‘eval_to k (EL n xs)’ \\ gs []) - >- ( - gvs [EVERY2_MAP, LIST_REL_EL_EQN] \\ rw [] - \\ first_x_assum (drule_all_then assume_tac) - \\ Cases_on ‘eval_to k (EL n ys)’ - \\ Cases_on ‘eval_to k (EL n xs)’ \\ gvs [] - \\ rename1 ‘INL err’ \\ Cases_on ‘err’ \\ gs [])) - *) - + IF_CASES_TAC \\ gs[o_DEF] + >-( + Cases_on `eval_to k (EL n xs)` + >- ( + Cases_on `x` + >- ( + qpat_x_assum `∀n. eval_to k (EL n xs) = INL Type_error ⇒ ¬(n < LENGTH ys)` mp_tac \\ fs[] + \\ qexists `n` \\ fs[]) + >- ( + qpat_x_assum `∀n. eval_to k (EL n xs) = INL Diverge ⇒ ¬(n < LENGTH ys)` mp_tac \\ fs[] + \\ qexists `n` \\ fs[])) + >- ( + `eval_to k (EL n xs) ≠ INL Type_error` by fs[] + \\ res_tac \\ metis_tac[SUM_REL_THM]) + ) + >-( + IF_CASES_TAC \\ gs[] + >-( + `exp_rel (EL n xs) (EL n ys)` by res_tac + \\ rpt $ first_x_assum $ qspec_then `n` assume_tac + \\ gvs[] + \\ res_tac + \\ qpat_x_assum `eval_to k (EL n ys) = INL Diverge` assume_tac + \\ fs[] + \\ Cases_on `eval_to k (EL n xs)` \\ fs[] + ) + >-( + simp[MAP_MAP_o] + \\ simp[LIST_REL_MAP] + \\ simp[LIST_REL_EL_EQN] + \\ rw[] + \\ rpt $ first_x_assum $ qspec_then `n` assume_tac + \\ gvs[] + \\ res_tac + \\ Cases_on `eval_to k (EL n xs)` \\ fs[] + >-(Cases_on `x` \\ fs[]) + \\ Cases_on `eval_to k (EL n ys)` \\ fs[]) + ) + )) >-( (* IsEq *) IF_CASES_TAC \\ gvs [LENGTH_EQ_NUM_compute] \\ rename1 ‘exp_rel x y’ @@ -493,7 +493,6 @@ Proof \\ Cases_on ‘v’ \\ Cases_on ‘w’ \\ gvs [LIST_REL_EL_EQN, v_rel_def] \\ IF_CASES_TAC \\ gs [] \\ rw [v_rel_def]) - >-( (* Proj *) IF_CASES_TAC \\ gvs [LENGTH_EQ_NUM_compute] \\ rename1 ‘exp_rel x y’ @@ -505,7 +504,6 @@ Proof \\ rename1 ‘v_rel v w’ \\ Cases_on ‘v’ \\ Cases_on ‘w’ \\ gvs [LIST_REL_EL_EQN, v_rel_def] \\ IF_CASES_TAC \\ gs []) - >-( (* AtomOp *) Cases_on ‘k = 0’ \\ gs [] >- ( (*k = 0*) @@ -531,7 +529,15 @@ Proof \\ Cases_on ‘k’ \\ gs [arithmeticTheory.ADD1] \\ rename1 ‘eval_to k’ \\ ‘∀n. n < LENGTH ys ⇒ - ($= +++ v_rel) (eval_to k (EL n xs)) (eval_to k (EL n ys))’ by (cheat) (*rest of proof works*) + ($= +++ v_rel) (eval_to k (EL n xs)) (eval_to k (EL n ys))’ by ( + rpt strip_tac + \\ res_tac + \\ first_x_assum irule \\ fs[] + \\ drule bind_not_error + \\ fs[result_map_def, AllCaseEqs(), MEM_MAP] + \\ fs[MEM_EL] + \\ metis_tac[] + ) (*rest of proof works*) (*\\ qpat_x_assum ‘∀x y. exp_rel _ _ ⇒ _’ kall_tac*) \\ IF_CASES_TAC \\ gs [] >- ( @@ -719,9 +725,9 @@ Proof rw []) \\ gs [] \\ first_x_assum $ dxrule_then assume_tac \\ gvs [])) - >~ [‘Delay x’] >- ( - rw [Once exp_rel_cases] \\ gs [] - \\ simp [eval_to_def, v_rel_def]) + >~ [‘Delay x’] >- ( + rw [Once exp_rel_cases] \\ gs [] + \\ simp [eval_to_def, v_rel_def]) >~ [‘Force x’] >- ( rw [exp_rel_def] \\ gs [] @@ -756,8 +762,7 @@ Proof \\ once_rewrite_tac [eval_to_def] \\ IF_CASES_TAC \\ gs [] \\ last_x_assum $ drule - \\ impl_tac - >- (CCONTR_TAC \\ fs[Once $ eval_to_def]) + \\ impl_tac >- (CCONTR_TAC \\ fs[Once $ eval_to_def]) \\ strip_tac \\ Cases_on ‘eval_to k y’ \\ Cases_on ‘eval_to k x’ \\ gvs [] \\ rename1 ‘v_rel v w’ @@ -802,8 +807,7 @@ Proof \\ ‘EL n (MAP FST xs) = EL n (MAP FST ys)’ by gs [] \\ gvs [EL_MAP]) \\ last_x_assum $ drule_then irule))) - - >~[`Thunk _ _`] >-( + >~[`Thunk _`] >-( simp[subst_funs_def] \\ last_x_assum $ qspec_then `k-1` assume_tac \\ `eval_to (k-1) x ≠ INL Type_error` by ( @@ -813,34 +817,35 @@ Proof \\ `eval_to k x = INL Type_error` by ( qspecl_then [`k-1`, `x`, `k`] assume_tac eval_to_mono \\ fs[]) \\ fs[Once $ eval_to_def]) - \\ `k-1 < k` by fs[] - \\ Cases_on `eval_to (k-1) e` \\ Cases_on `eval_to (k-1) y'` \\ gs[bind_not_error] - >- (cheat) + \\ `eval_to (k-1) e ≠ INL Type_error ⇒ + ($= +++ v_rel) (eval_to (k − 1) e) (eval_to (k − 1) y')` by ( + `k-1 < k` by fs[] + \\ res_tac) + \\ Cases_on `eval_to (k-1) y'` \\ Cases_on `eval_to (k-1) e` \\ fs[] >- ( - qsuff_tac `is_anyThunk y''` - >- (strip_tac \\ fs[]) - >- ( - Cases_on `y''` \\ simp[is_anyThunk_def, dest_anyThunk_def, dest_Thunk_def, v_rel_anyThunk] - \\ cheat - ) - ) + first_x_assum irule + \\ Cases_on `x''` \\ fs[] + \\ qpat_x_assum `eval_to k (Force x) ≠ _` mp_tac \\ simp[Once eval_to_def] + \\ fs[dest_anyThunk_def, subst_funs_def]) >- ( - Cases_on `is_anyThunk y''` \\ Cases_on `is_anyThunk y'''` \\ gs[] + Cases_on `is_anyThunk y''` \\ fs[] + \\ qpat_x_assum `eval_to k (Force x) ≠ _` mp_tac \\ simp[Once eval_to_def] + \\ fs[dest_anyThunk_def, subst_funs_def]) + >- ( + Cases_on `is_anyThunk y''` \\ Cases_on `is_anyThunk y'''`\\ gs[] + \\ `eval_to (k-1) e ≠ INL Type_error` by fs[] \\ res_tac >- ( qpat_x_assum `¬ is_anyThunk y'''` mp_tac \\ fs[] \\ mp_tac v_rel_anyThunk \\ strip_tac - \\ `is_anyThunk y'' ⇔ is_anyThunk y'''` by ( + \\ `is_anyThunk y''' ⇔ is_anyThunk y''` by ( first_x_assum irule \\ fs[]) \\ fs[]) >- ( qpat_x_assum `¬ is_anyThunk y''` mp_tac \\ fs[] \\ mp_tac v_rel_anyThunk \\ strip_tac - `is_anyThunk y'' ⇔ is_anyThunk y'''` by ( + \\ `is_anyThunk y''' ⇔ is_anyThunk y''` by ( first_x_assum irule \\ fs[]) - \\ fs[]))) - ) - ) - + \\ fs[])))) >~[`dest_Tick w = SOME _`] >-( Cases_on ‘v’ \\ gs [v_rel_def, dest_Tick_def] \\ `k-1 < k` by simp [] @@ -853,53 +858,14 @@ Proof \\ `eval_to (k-1) x = eval_to k x` by simp[eval_to_mono] \\ fs[]) >- ( strip_tac - \\ last_assum $ irule - \\ conj_tac \\ fs[exp_rel_def] - \\ simp[Once $ eval_to_def] \\ IF_CASES_TAC \\ fs[] - \\ simp[Once $ eval_to_def] - \\ CASE_TAC \\ gs[bind_not_error] - \\ Cases_on `v'` \\ gs[dest_anyThunk_def] - cheat - (*stuck*))) - ) - - (*old proof -- Force case *) - (* - ‘dest_Tick v = NONE’ - by (Cases_on ‘v’ \\ Cases_on ‘w’ \\ gs [] - \\ gs [Once v_rel_def]) - \\ gs [] - \\ Cases_on ‘v’ \\ gvs [dest_anyThunk_def, v_rel_def] - >~[‘Recclosure _ _’] - >- (rename1 ‘LIST_REL _ (MAP SND xs) (MAP SND ys)’ - \\ ‘OPTREL exp_rel - (ALOOKUP (REVERSE xs) s) - (ALOOKUP (REVERSE ys) s)’ - by (irule LIST_REL_OPTREL - \\ gvs [LIST_REL_EL_EQN, ELIM_UNCURRY, EL_MAP, LIST_EQ_REWRITE]) - \\ gs [OPTREL_def] - \\ rename1 ‘exp_rel x0 y0’ - \\ ‘MEM (s, x0) xs’ by (rpt $ dxrule_then assume_tac ALOOKUP_MEM \\ gvs []) - \\ gvs [EVERY_MEM, MEM_MAP, PULL_EXISTS] - - \\ first_assum $ dxrule_then assume_tac - \\ Cases_on ‘x0’ \\ gvs [ok_bind_def, exp_rel_def] - >~[‘subst_funs ys e2’] - - >- ( - last_x_assum irule \\ simp [subst_funs_def] - \\ irule exp_rel_subst \\ simp [] - \\ gs [FORALL_PROD] - \\ gvs [MAP_MAP_o, combinTheory.o_DEF, LAMBDA_PROD, GSYM FST_THM, LIST_REL_EL_EQN, EL_MAP] - \\ rw [] \\ pairarg_tac \\ gs [] \\ pairarg_tac \\ gs [v_rel_def, LIST_REL_EL_EQN, EL_MAP] - \\ gs [EVERY_MEM, MEM_MAP, PULL_EXISTS, FORALL_PROD] - \\ rw [] - >- ( - rename [‘n < _’, ‘MAP FST xs = MAP FST ys’] - \\ ‘EL n (MAP FST xs) = EL n (MAP FST ys)’ by gs [] - \\ gvs [EL_MAP]) - \\ last_x_assum $ drule_then irule)) - \\ gs [subst_funs_def, subst_empty]) *) + \\ `exp_rel (Force (Value v')) (Force (Value x'))` by + metis_tac[SUM_REL_THM, exp_rel_def] + \\ `eval_to (k-1) (Force (Value v')) ≠ INL Type_error` by ( + CCONTR_TAC + \\ qpat_x_assum `eval_to k (Force x) ≠ _` mp_tac \\ fs[Once eval_to_def] + \\ Cases_on `k ≤ 1` \\ fs[] + \\ simp[Once eval_to_def]) + \\ metis_tac[])))) >~ [‘Value v’] >- ( rw [Once exp_rel_cases] @@ -934,7 +900,6 @@ Proof by (irule eval_to_mono \\ gs [arithmeticTheory.MAX_DEF]) \\ ‘eval_to (MAX k j) y = eval_to j y’ by (irule eval_to_mono \\ gs [arithmeticTheory.MAX_DEF]) - \\ gs [] QED Theorem exp_rel_apply_closure[local]: From a2ce907f957d8e3d8846bf47b23c72cf4984230a Mon Sep 17 00:00:00 2001 From: artisanbk Date: Fri, 9 Jan 2026 13:57:55 +0800 Subject: [PATCH 8/9] some progress --- .../passes/proofs/thunk_force_delayScript.sml | 72 ++++++++++++++++--- 1 file changed, 61 insertions(+), 11 deletions(-) diff --git a/compiler/backend/passes/proofs/thunk_force_delayScript.sml b/compiler/backend/passes/proofs/thunk_force_delayScript.sml index 67db0ada..96e5aa30 100644 --- a/compiler/backend/passes/proofs/thunk_force_delayScript.sml +++ b/compiler/backend/passes/proofs/thunk_force_delayScript.sml @@ -370,7 +370,6 @@ Proof metis_tac[] QED - Theorem exp_rel_eval_to[local]: ∀x y. exp_rel x y ∧ @@ -537,8 +536,7 @@ Proof \\ fs[result_map_def, AllCaseEqs(), MEM_MAP] \\ fs[MEM_EL] \\ metis_tac[] - ) (*rest of proof works*) - (*\\ qpat_x_assum ‘∀x y. exp_rel _ _ ⇒ _’ kall_tac*) + ) \\ IF_CASES_TAC \\ gs [] >- ( rename1 ‘m < LENGTH ys’ @@ -884,32 +882,83 @@ Proof \\ Cases_on ‘eval_to k y’ \\ Cases_on ‘eval_to k x’ \\ gs [v_rel_def]) QED -(* TODO: broken under here *) Theorem exp_rel_eval: - exp_rel x y ⇒ + exp_rel x y ∧ (eval x ≠ INL Type_error) ⇒ ($= +++ v_rel) (eval x) (eval y) Proof strip_tac + \\ `eval_to u x ≠ INL Type_error` by fs[eval_not_error] \\ simp [eval_def] \\ dxrule_then assume_tac exp_rel_eval_to \\ simp [] \\ DEEP_INTRO_TAC some_intro \\ DEEP_INTRO_TAC some_intro \\ rw [] \\ gs [] - \\ rename1 ‘_ (eval_to k x) (eval_to j y)’ - \\ first_x_assum (qspec_then ‘MAX k j’ assume_tac) - \\ ‘eval_to (MAX k j) x = eval_to k x’ - by (irule eval_to_mono \\ gs [arithmeticTheory.MAX_DEF]) - \\ ‘eval_to (MAX k j) y = eval_to j y’ - by (irule eval_to_mono \\ gs [arithmeticTheory.MAX_DEF]) + >- ( + rename1 ‘_ (eval_to k x) (eval_to j y)’ + \\ first_x_assum (qspec_then ‘MAX k j’ assume_tac) + \\ ‘eval_to (MAX k j) x = eval_to k x’ + by (irule eval_to_mono \\ gs [arithmeticTheory.MAX_DEF]) + \\ ‘eval_to (MAX k j) y = eval_to j y’ + by (irule eval_to_mono \\ gs [arithmeticTheory.MAX_DEF]) + \\ qsuff_tac `eval_to (MAX k j) x ≠ INL Type_error` \\ fs[] + \\ irule eval_not_error \\ fs[] + ) + >- ( + rename1 ‘_ (eval_to k x) _’ + \\ first_x_assum (qspec_then ‘MAX k j’ assume_tac) + \\ ‘eval_to (MAX k j) x = eval_to k x’ + by (irule eval_to_mono \\ gs [arithmeticTheory.MAX_DEF]) + \\ qsuff_tac `eval_to (MAX k j) x ≠ INL Type_error` \\ fs[] + \\ irule eval_not_error \\ fs[] + ) QED + Theorem exp_rel_apply_closure[local]: exp_rel x y ∧ v_rel v2 w2 ∧ + eval x ≠ INL Type_error ∧ (∀x y. ($= +++ v_rel) x y ⇒ next_rel v_rel exp_rel (f x) (g y)) ⇒ next_rel v_rel exp_rel (apply_closure x v2 f) (apply_closure y w2 g) Proof rw [apply_closure_def] >> simp[with_value_def] >> dxrule_then assume_tac exp_rel_eval >> + Cases_on `eval x` >> Cases_on `eval y` >> gs[exp_rel_eval_to] + >- (Cases_on `x''` >> fs[]) + >- ( + Cases_on `dest_anyClosure y'` >> Cases_on `dest_anyClosure y''` >> fs[next_rel_def] + >-( + CASE_TAC >> CASE_TAC >> + `x' = Type_error` by ( + Cases_on `y'` >> fs[dest_anyClosure_def] >> + Cases_on `ALOOKUP (REVERSE l) s` >> fs[] >> Cases_on `x''` >> fs[]) >> + CCONTR_TAC >> qpat_x_assum `v_rel y' y''` mp_tac >> fs[v_rel_def] >> + Cases_on `y'` >> Cases_on `y''` >> fs[v_rel_def,dest_anyClosure_def] >> rpt strip_tac >> + `ALOOKUP (REVERSE l) s = SOME _` by fs[] + Cases_on `ALOOKUP (REVERSE l) s` >> fs[] + >-( + Cases_on `ALOOKUP (REVERSE l') s` >> fs[] >> Cases_on `x''` >> fs[] + + ) + >-( + Cases_on `x''` >> fs[] >> + `EXISTS ($¬ o ok_bind) (MAP SND l)` by ( + `∃n. n < LENGTH l ∧ EL n l = (s, Var s'')` by simp[ALOOKUP_SOME_REVERSE_EL] >> + `MEM (Var s'') (MAP SND l)` by ( + qspecl_then [`n`, `l`] assume_tac EL_MEM >> res_tac >> + `MEM (s, Var s'') l` by metis_tac[] >> + `EL n (MAP SND l) = SND (EL n l)` by simp[EL_MAP] >> + ` Var s'' = SND (EL n l)` by fs[] >> pop_assum (fn x => pure_rewrite_tac[x]) >> + metis_tac[MEM_MAP])>> + simp[EXISTS_MEM] >> qexists `(Var s'')` >> simp[ok_bind_def] + ) >> + fs[]) + ) + ) + >-() + >-() + ) + + (* Old proof Cases_on `eval x` >> Cases_on `eval y` >> gvs[] >- (CASE_TAC >> gvs[]) >> rename1 `eval x = INR v1` >> rename1 `eval y = INR w1` @@ -935,6 +984,7 @@ Proof \\ simp [EVERY2_MAP, LAMBDA_PROD, v_rel_def, MAP_MAP_o, combinTheory.o_DEF, GSYM FST_THM] \\ gvs [LIST_REL_EL_EQN, ELIM_UNCURRY, EVERY_EL, EL_MAP, LIST_EQ_REWRITE]) + *) QED Theorem exp_rel_rel_ok[local]: From dc18fb2457dee4fc37a4eb1ef85566fb65da835f Mon Sep 17 00:00:00 2001 From: tanyongkiam Date: Fri, 9 Jan 2026 14:32:19 +0800 Subject: [PATCH 9/9] fix thunk_force_delay with @artisanbk --- .../passes/proofs/thunk_force_delayScript.sml | 92 +++++++------------ 1 file changed, 33 insertions(+), 59 deletions(-) diff --git a/compiler/backend/passes/proofs/thunk_force_delayScript.sml b/compiler/backend/passes/proofs/thunk_force_delayScript.sml index 96e5aa30..a0210a1d 100644 --- a/compiler/backend/passes/proofs/thunk_force_delayScript.sml +++ b/compiler/backend/passes/proofs/thunk_force_delayScript.sml @@ -912,62 +912,34 @@ Proof ) QED - Theorem exp_rel_apply_closure[local]: - exp_rel x y ∧ + exp_rel v1 w1 ∧ v_rel v2 w2 ∧ - eval x ≠ INL Type_error ∧ - (∀x y. ($= +++ v_rel) x y ⇒ next_rel v_rel exp_rel (f x) (g y)) ⇒ - next_rel v_rel exp_rel (apply_closure x v2 f) (apply_closure y w2 g) + apply_closure v1 v2 f ≠ Err ∧ + f (INL Type_error) = Err ∧ + (∀x y. ($= +++ v_rel) x y ∧ f x ≠ Err ⇒ + next_rel v_rel exp_rel (f x) (g y)) ⇒ + next_rel v_rel exp_rel (apply_closure v1 v2 f) (apply_closure w1 w2 g) Proof - rw [apply_closure_def] >> simp[with_value_def] >> - dxrule_then assume_tac exp_rel_eval >> - Cases_on `eval x` >> Cases_on `eval y` >> gs[exp_rel_eval_to] - >- (Cases_on `x''` >> fs[]) + rw [apply_closure_def] >> fs[with_value_def] >> + Cases_on`eval v1 = INL Type_error` >- fs[]>> + drule_all_then assume_tac exp_rel_eval >> + Cases_on `eval v1` >> Cases_on `eval w1` >> + gvs[exp_rel_eval_to] >- ( - Cases_on `dest_anyClosure y'` >> Cases_on `dest_anyClosure y''` >> fs[next_rel_def] - >-( - CASE_TAC >> CASE_TAC >> - `x' = Type_error` by ( - Cases_on `y'` >> fs[dest_anyClosure_def] >> - Cases_on `ALOOKUP (REVERSE l) s` >> fs[] >> Cases_on `x''` >> fs[]) >> - CCONTR_TAC >> qpat_x_assum `v_rel y' y''` mp_tac >> fs[v_rel_def] >> - Cases_on `y'` >> Cases_on `y''` >> fs[v_rel_def,dest_anyClosure_def] >> rpt strip_tac >> - `ALOOKUP (REVERSE l) s = SOME _` by fs[] - Cases_on `ALOOKUP (REVERSE l) s` >> fs[] - >-( - Cases_on `ALOOKUP (REVERSE l') s` >> fs[] >> Cases_on `x''` >> fs[] - - ) - >-( - Cases_on `x''` >> fs[] >> - `EXISTS ($¬ o ok_bind) (MAP SND l)` by ( - `∃n. n < LENGTH l ∧ EL n l = (s, Var s'')` by simp[ALOOKUP_SOME_REVERSE_EL] >> - `MEM (Var s'') (MAP SND l)` by ( - qspecl_then [`n`, `l`] assume_tac EL_MEM >> res_tac >> - `MEM (s, Var s'') l` by metis_tac[] >> - `EL n (MAP SND l) = SND (EL n l)` by simp[EL_MAP] >> - ` Var s'' = SND (EL n l)` by fs[] >> pop_assum (fn x => pure_rewrite_tac[x]) >> - metis_tac[MEM_MAP])>> - simp[EXISTS_MEM] >> qexists `(Var s'')` >> simp[ok_bind_def] - ) >> - fs[]) - ) - ) - >-() - >-() - ) - - (* Old proof - Cases_on `eval x` >> Cases_on `eval y` >> gvs[] - >- (CASE_TAC >> gvs[]) >> - rename1 `eval x = INR v1` >> rename1 `eval y = INR w1` - \\ Cases_on ‘v1’ \\ Cases_on ‘w1’ \\ gvs [v_rel_def, dest_anyClosure_def] + rename1`INL xx`>> + Cases_on `xx` >> fs[]) >- ( - first_x_assum irule - \\ irule exp_rel_eval - \\ irule exp_rel_subst \\ gs []) - >- (rename1 ‘LIST_REL _ (MAP SND xs) (MAP SND ys)’ + Cases_on`y` + \\ Cases_on`y'` + \\ gvs [v_rel_def, dest_anyClosure_def] + >- ( + first_x_assum irule \\ simp[] + \\ irule exp_rel_eval + \\ CONJ_TAC >- metis_tac[] + \\ irule exp_rel_subst \\ gs []) + >- ( + rename1 ‘LIST_REL _ (MAP SND xs) (MAP SND ys)’ \\ ‘OPTREL exp_rel (ALOOKUP (REVERSE xs) s) (ALOOKUP (REVERSE ys) s)’ by (irule LIST_REL_OPTREL \\ gvs [LIST_REL_EL_EQN, ELIM_UNCURRY, EL_MAP, LIST_EQ_REWRITE]) @@ -979,36 +951,38 @@ Proof \\ drule_then assume_tac ALOOKUP_SOME_REVERSE_EL \\ gs [] \\ gvs [EVERY_EL, EL_MAP] \\ first_x_assum irule + \\ simp[] \\ irule exp_rel_eval + \\ CONJ_TAC >- metis_tac[] \\ irule exp_rel_subst \\ simp [EVERY2_MAP, LAMBDA_PROD, v_rel_def, MAP_MAP_o, combinTheory.o_DEF, GSYM FST_THM] - \\ gvs [LIST_REL_EL_EQN, ELIM_UNCURRY, EVERY_EL, EL_MAP, LIST_EQ_REWRITE]) - *) + \\ gvs [LIST_REL_EL_EQN, ELIM_UNCURRY, EVERY_EL, EL_MAP, LIST_EQ_REWRITE])) QED Theorem exp_rel_rel_ok[local]: - rel_ok T v_rel exp_rel + rel_ok F v_rel exp_rel Proof rw [rel_ok_def, v_rel_def, exp_rel_def] \\ rw [exp_rel_apply_closure] QED Theorem exp_rel_sim_ok[local]: - sim_ok T v_rel exp_rel + sim_ok F v_rel exp_rel Proof rw [sim_ok_def, exp_rel_eval, exp_rel_subst] QED Theorem exp_rel_semantics[local]: exp_rel x y ∧ - closed x ⇒ + closed x ∧ + safe_itree (semantics x Done []) ⇒ semantics x Done [] = semantics y Done [] Proof strip_tac \\ irule sim_ok_semantics \\ gs [] \\ first_assum (irule_at Any) - \\ qexists_tac ‘T’ \\ gs [] + \\ qexists_tac ‘F’ \\ gs [] \\ irule_at Any exp_rel_rel_ok \\ irule_at Any exp_rel_sim_ok QED @@ -1066,7 +1040,8 @@ QED Theorem force_delay_semantics: force_delay_rel x y ∧ - closed x ⇒ + closed x ∧ + safe_itree (semantics x Done []) ⇒ semantics x Done [] = semantics y Done [] Proof strip_tac @@ -1077,4 +1052,3 @@ Proof \\ gs [closed_def] QED -