1(* By Scott Owens and Theo Laurent, 2016 2 * Prove that simply typed call-by-value lambda calculus programs always 3 * terminate. *) 4 5(* Standard things to open at the top of a script file *) 6open HolKernel boolLib bossLib Parse; 7 8(* Generally useful theories *) 9open integerTheory stringTheory alistTheory listTheory pred_setTheory; 10open pairTheory optionTheory finite_mapTheory arithmeticTheory rich_listTheory; 11 12(* The call-by-value LC that we're building on *) 13open cbvTheory; 14 15open RW; 16 17(* Name the theory types *) 18val _ = new_theory "types"; 19 20(* The datatype of types *) 21val _ = Datatype ` 22type = 23 Int 24| Arrow type type`; 25 26(* Get the size function generated by the call to Datatype *) 27val type_size_def = fetch "-" "type_size_def"; 28 29(* Our type environments will be type lists, because we are in a De Bruijn 30 * representation. *) 31val _ = type_abbrev ("type_env", ``:type list``); 32 33(* The standard inductive relation for typing STLC. 34 * Get a rules, induction and case split theorem back *) 35val (type_rules,type_ind,type_cases) = Hol_reln ` 36(!G i. 37 type G (Lit (Int i)) Int) ��� 38(���G n. 39 n < LENGTH G 40 ��� 41 type G (Var n) (EL n G)) ��� 42(!G e1 e2 t1 t2. 43 type G e1 (Arrow t1 t2) ��� 44 type G e2 t1 45 ��� 46 type G (App e1 e2) t2) ��� 47(!G e t1 t2. 48 type (t1::G) e t2 49 ��� 50 type G (Fun e) (Arrow t1 t2)) ��� 51(!G e t. 52 type G e t 53 ��� 54 type G (Tick e) t)`; 55 56(* Define a helper function for the termination argument below. *) 57val sn_v_term_fun_def = Define ` 58(sn_v_term_fun (INL (t, v)) = (type_size t, 0:num)) ��� 59(sn_v_term_fun (INR (INL (t, s, env, e))) = (type_size t, 2)) ��� 60(sn_v_term_fun (INR (INR s)) = (0, 1))`; 61 62(* A unary logical relation for strong normalisation, for values, executing 63 * expressions and states. HOL can't get the termination on it's own, so we 64 * have to supply a well-founded relation with WF_REL_TAC and prove that it 65 * works. Things in the store must be related at Int type, since higher-order 66 * stores lose strong normalisation. *) 67val sn_v_def = tDefine "sn_v" ` 68(sn_v Int (Litv l) ��� T) ��� 69(sn_v (Arrow t1 t2) (Clos env exp) ��� 70 !v s. sn_state s ��� sn_v t1 v ��� sn_exec t2 s (v::env) exp) ��� 71(sn_v _ _ ��� F) ��� 72(sn_exec t s env exp ��� 73 ?ck v s'. 74 sem env (s with clock := ck) exp = (Rval v, s') ��� 75 sn_v t v ��� 76 sn_state s') ��� 77(sn_state s ��� EVERY (sn_v Int) s.store)` 78(WF_REL_TAC `inv_image ((<) LEX (<)) sn_v_term_fun` >> 79 rw [sn_v_term_fun_def, type_size_def]); 80 81(* Define the logical relation for arbitrary expressions at a given type 82 * and typing context *) 83val sn_e_def = Define ` 84sn_e G t e ��� 85 !s env. sn_state s ��� LIST_REL sn_v G env ��� sn_exec t s env e`; 86 87 88(* The main lemma, proceed by rule induction over the type relation. *) 89val sn_lemma = Q.prove ( 90`!G e t. type G e t ��� sn_e G t e`, 91ho_match_mp_tac type_ind >> rw [] 92>- fs [sn_e_def, sn_v_def, sem_def] 93>- (rw [sn_e_def, sn_v_def] 94 >> qexists_tac `1` 95 >> qexists_tac `EL n env` 96 >> qexists_tac `s with clock := 1` 97 >> (rw [sem_def] 98 >- metis_tac [LIST_REL_LENGTH] 99 >- metis_tac [LIST_REL_EL_EQN])) 100>- ( 101 rw [sn_e_def, sn_v_def] 102 >> qpat_assum `_ _ (Arrow t t') _` 103 (fn t => assume_tac (RW_RULE [sn_e_def, sn_v_def] t)) 104 >> first_x_assum (qspecl_then [`s`, `env`] assume_tac) >> rfs [] 105 >> rename1 `sem _ _ _ = (_, s')` 106 >> Cases_on `v` >> fs [sn_v_def] 107 >> qpat_assum `sn_e _ _ _` 108 (fn t => assume_tac (RW_RULE [sn_e_def, sn_v_def] t)) 109 >> first_x_assum (qspecl_then [`s'`, `env`] assume_tac) >> rfs [] 110 >> first_x_assum (qspecl_then [`v`, `s''`] assume_tac) >> rfs [] 111 >> qexists_tac `ck + ck' + ck'' + 1` 112 >> qexists_tac `v'` 113 >> qexists_tac `s''' with clock := s'.clock + (s''.clock + s'''.clock)` 114 >> qspecl_then [`env`, `s`, `e`, `Clos l e''`, `s'`, `ck`, `ck' + ck'' + 1`] assume_tac sem_clock_add 115 >> rfs [] 116 >> simp [sem_def] 117 >> qspecl_then [`env`, `s'`, `e'`, `v`, `s''`, `ck'`, `ck'' + s'.clock + 1`] assume_tac sem_clock_add 118 >> rfs [] 119 >> simp [sem_def, dec_clock_def] 120 >> qspecl_then [`v::l`, `s''`, `e''`, `v'`, `s'''`, `ck''`, `s'.clock + s''.clock`] assume_tac sem_clock_add 121 >> rfs []) 122 123>- fs [sn_e_def, sn_v_def, sem_def] 124>- (first_x_assum mp_tac >> rw [sn_e_def, sn_v_def] 125 >> res_tac 126 >> rename1 `sem _ (s with clock := ck) _ = (_, s')` 127 >> qexists_tac `ck + 1` 128 >> qexists_tac `v` 129 >> qexists_tac `s'` 130 >> rw [sem_def, dec_clock_def])); 131 132(* The main theorem *) 133val strong_norm_thm = Q.store_thm ("strong_norm_thm", 134`!e t. type [] e t ��� ?v. eval e (Rval v)`, 135 rpt strip_tac 136>> `sn_e [] t e` by (match_mp_tac sn_lemma >> simp []) 137>> fs [sn_v_def, sn_e_def, eval_def] 138>> first_x_assum (qspec_then `<|clock := c; store := []|>` assume_tac) >> fs [] 139>> metis_tac [] 140); 141 142val _ = export_theory (); 143