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