1(*--------------------------------------------------------------------------- 2 3 An example taken from 4 5 "Automating induction over mutually recursive functions", 6 Deepak Kapur and M. Subramaniam, Proceedings of AMAST'96, 7 Springer LNCS 1101. 8 9 The example displays the equivalence of call-by-name and 10 call-by-value evaluation strategies for a type of simple arithmetic 11 terms. The evaluation functions feature mutual and nested recursions. 12 13 ---------------------------------------------------------------------------*) 14 15load "bossLib"; open bossLib; 16 17 18Hol_datatype `arith = Con of num (* constant *) 19 | Var of 'a (* variable *) 20 | Add of arith => arith (* addition *) 21 | App of arith => 'a => arith (* func. application *)`; 22 23 24(*--------------------------------------------------------------------------- 25 Call-by-name evaluation 26 ---------------------------------------------------------------------------*) 27 28val CBN_defn = 29 Hol_defn 30 "CBN" 31 `(CBN (Con n, y, N) = Con n) 32 /\ (CBN (Var x, y, N) = if x=y then CBNh N else Var x) 33 /\ (CBN (Add a1 a2, y, N) = Add (CBN(a1,y,N)) (CBN(a2,y,N))) 34 /\ (CBN (App B v M, y, N) = CBN (CBN(B,v,M), y, N)) 35 36 /\ (CBNh (Con n) = Con n) 37 /\ (CBNh (Var x) = Var x) 38 /\ (CBNh (Add a1 a2) = Add (CBNh a1) (CBNh a2)) 39 /\ (CBNh (App B v M) = CBN (B,v,M))`; 40 41 42val CBN_eqns = Defn.eqns_of CBN_defn; 43val SOME CBN_ind = Defn.ind_of CBN_defn; 44 45 46(*--------------------------------------------------------------------------- 47 Environment lookup 48 ---------------------------------------------------------------------------*) 49 50val lookup_def = 51 Define 52 `(lookup x [] = 0) 53 /\ (lookup x ((y,N)::rst) = if x=y then N else lookup x rst)`; 54 55 56(*--------------------------------------------------------------------------- 57 Call-by-value evaluation 58 ---------------------------------------------------------------------------*) 59 60val CBV_defn = Hol_defn "CBV" 61 `(CBV (Con n, env) = n) 62 /\ (CBV (Var x, env) = lookup x env) 63 /\ (CBV (Add a1 a2, env) = CBV(a1,env) + CBV(a2,env)) 64 /\ (CBV (App B v M, env) = CBV(B, (v,CBV(M,env))::env))`; 65 66 67val CBV_eqns = Defn.eqns_of CBV_defn; 68val SOME CBV_ind = Defn.ind_of CBV_defn; 69 70 71(*--------------------------------------------------------------------------- 72 Some munging to get tidier defns and induction thms. 73 ---------------------------------------------------------------------------*) 74 75val SOME R = Defn.reln_of CBN_defn; 76val SOME R1 = Defn.reln_of CBV_defn; 77 78val CBNTerminates_def = 79 Define 80 `CBNTerminates ^R = ^(list_mk_conj (Defn.tcs_of CBN_defn))`; 81 82val CBVTerminates_def = 83 Define 84 `CBVTerminates ^R1 = ^(list_mk_conj (Defn.tcs_of CBV_defn))`; 85 86val TC0thms = 87 CONJUNCTS 88 (EQ_MP (SPEC_ALL CBNTerminates_def) 89 (ASSUME (lhs(concl(SPEC_ALL CBNTerminates_def))))); 90 91val TC1thms = 92 CONJUNCTS 93 (EQ_MP (SPEC_ALL CBVTerminates_def) 94 (ASSUME (lhs(concl(SPEC_ALL CBVTerminates_def))))); 95 96val CBN_eqns' = itlist PROVE_HYP TC0thms (LIST_CONJ CBN_eqns); 97val CBN_ind' = itlist PROVE_HYP TC0thms CBN_ind; 98val CBV_eqns' = itlist PROVE_HYP TC1thms (LIST_CONJ CBV_eqns); 99 100 101(*--------------------------------------------------------------------------- 102 Partial correctness is phrased as the following: 103 104 CBNTerminates R /\ CBVTerminates R1 105 ==> 106 !x y N env. 107 CBV (CBN(x,y,N),env) 108 = 109 CBV (x, (y,CBV(N,env))::env) 110 111 We build an induction theorem first, by instantiating the 112 induction theorem for CBN to the predicates suggested by the 113 method of Richard Boulton. 114 ---------------------------------------------------------------------------*) 115 116val tm = Term 117 `\(x,y,N). 118 !env. CBV (CBN (x,y,N), env) 119 = 120 CBV(x, (y, CBV(N,env))::env)`; 121 122val tm1 = Term `\N. !env. CBV (CBNh N, env) = CBV(N,env)`; 123 124val [P0,P1] = fst(strip_forall(concl CBN_ind')); 125val ind0 = SPEC_ALL CBN_ind'; 126val ind1 = CONV_RULE (DEPTH_CONV pairLib.GEN_BETA_CONV) 127 (INST [P0 |-> tm, P1 |-> tm1] ind0); 128val [ind2a, _] = CONJUNCTS (UNDISCH ind1); 129val ind3 = REWRITE_RULE pairTheory.pair_rws 130 (SPEC (Term`(x,y,N):'a arith#'a#'a arith`) ind2a); 131val ind4 = DISCH (fst(dest_imp(concl ind1))) 132 (SPEC_ALL ind3); 133 134 135(*--------------------------------------------------------------------------- 136 We distinguish the names "R" and "R1" of the termination 137 relations; otherwise, the termination relations for both 138 CBN and CBV would have the same name, which is confusing. 139 ---------------------------------------------------------------------------*) 140 141val R1' = mk_var("R1", type_of R1);; 142 143val CBV_eqns'' = UNDISCH (INST [R1 |-> R1'] (DISCH_ALL CBV_eqns')); 144 145 146(*--------------------------------------------------------------------------- 147 Given ind4, the correctness proof is easy! 148 ---------------------------------------------------------------------------*) 149 150val KapurSubra = store_thm("KapurSubra", 151 Term`!R R1. 152 CBNTerminates ^R /\ CBVTerminates ^R1' 153 ==> 154 !x (y:'a) N env. 155 CBV (CBN(x,y,N),env) 156 = 157 CBV (x, (y, CBV(N,env))::env)`, 158REPEAT GEN_TAC THEN STRIP_TAC 159 THEN MATCH_MP_TAC ind4 160 THEN RW_TAC std_ss [CBN_eqns',CBV_eqns'',lookup_def]); 161 162 163(*--------------------------------------------------------------------------- 164 Remaining task: supply R and R1 such that 165 166 CBNTerminates R /\ CBVTerminates R1 167 168 This will require reasoning about the auxiliary functions 169 used in defining CBN and CBV. Since CBN is mutual recursive 170 with CBNh and also a nested recursion, this makes things 171 not completely obvious. We tackle CBV first, since it's 172 easier. 173 ---------------------------------------------------------------------------*) 174 175local val [guess1,_] = TotalDefn.guessR CBV_defn 176in 177val CBVTerminates = Q.prove 178(`CBVTerminates ^guess1`, 179 TotalDefn.TC_SIMP_TAC [] [prim_recTheory.WF_measure,CBVTerminates_def]) 180end; 181 182 183(*--------------------------------------------------------------------------- 184 Termination of CBN is much harder! First there's the problem of 185 seeing why it terminates, then there's the task of expressing 186 termination formally, and finally, the proof of termination is 187 also a little bit challenging. 188 189 1. Why it terminates. CBN eliminates all "App" nodes in an 190 expression. Thus, we can simply count the Apply nodes. 191 However, the case where there are no App nodes in the 192 expression must also be dealt with; in this case, the 193 recursion is always on smaller arguments. 194 195 2. Formal expression. The specification of CBN leads to several 196 background definitions: a "union" function is constructed to 197 handle the mutual recursion, and an "auxiliary" function is 198 built to handle the nested recursion. The termination constraints 199 that we have to eliminate are those of the union function, and 200 these contain occurrences of the auxiliary function. 201 202 The way the analysis of (1) is formalized starts by defining 203 a count of the App nodes in an expression. This measure will 204 be put together in a lexicographic combination with the normal 205 size functions. We just have to fiddle to make sure that 206 different size functions are applied in the different injections 207 into the sum. 208 209 ---------------------------------------------------------------------------*) 210 211val AppCount_def = 212 Define 213 `(AppCount (App B _ M) = 1 + AppCount B + AppCount M) 214 /\ (AppCount (Add M N) = AppCount M + AppCount N) 215 /\ (AppCount _____ = 0)`; 216 217val JointAppCount_def = 218 Define 219 `(JointAppCount (INL(P,_,Q)) = AppCount P + AppCount Q) 220 /\ (JointAppCount (INR P) = AppCount P)`; 221 222val JointStdSize_def = 223 Define 224 `(JointStdSize (INL(P,_,Q)) = arith_size (\v.0) P + arith_size (\v.0) Q) 225 /\ (JointStdSize (INR P) = arith_size (\v.0) P)`; 226 227 228val R = Term 229`inv_image ($< LEX $<) 230 (\x:'a arith#'a#'a arith + 'a arith. (JointAppCount x, JointStdSize x))`; 231 232(*--------------------------------------------------------------------------- 233 Set the termination relation of CBN_defn 234 ---------------------------------------------------------------------------*) 235 236val defnR = Defn.set_reln CBN_defn R; 237val tcs as [tc1,tc2,nested,tc3,tc4,tc5,tc6,tc7,tc8] = Defn.tcs_of defnR; 238 239(*--------------------------------------------------------------------------- 240 Prove the easy termination conditions 241 ---------------------------------------------------------------------------*) 242 243val easy_tcs = prove(list_mk_conj [tc1,tc2,tc3,tc4,tc5,tc6,tc7,tc8], 244 TotalDefn.TC_SIMP_TAC [] 245 [JointAppCount_def,JointStdSize_def, 246 AppCount_def,fetch "-" "arith_size_def"]); 247 248(*--------------------------------------------------------------------------- 249 And eliminate them from the definition 250 ---------------------------------------------------------------------------*) 251 252val defnR_1 = Defn.elim_tcs defnR (CONJUNCTS easy_tcs); 253 254(*--------------------------------------------------------------------------- 255 Fetch the equations for the auxiliary definition 256 ---------------------------------------------------------------------------*) 257 258val SOME Un = Defn.union_defn defnR_1; 259val SOME Aux_defn = Defn.aux_defn Un; 260 261(*--------------------------------------------------------------------------- 262 Remove the easy termination constraints from the equations and 263 the provisional induction theorem. 264 ---------------------------------------------------------------------------*) 265 266val eqns = map (REWRITE_RULE [easy_tcs]) (Defn.eqns_of Aux_defn); 267val ind = REWRITE_RULE [easy_tcs] (valOf (Defn.ind_of Aux_defn)); 268 269(*--------------------------------------------------------------------------- 270 An abbreviation to make the goal more readable. 271 ---------------------------------------------------------------------------*) 272 273val Fn_def = Define `Fn = CBN_UNION_aux ^R`; 274 275(*--------------------------------------------------------------------------- 276 Apply the abbreviation to the equations and provisional ind. thm. 277 ---------------------------------------------------------------------------*) 278 279val [e1,e2,e3,e4,e5,e6,e7,e8] = map (REWRITE_RULE [GSYM Fn_def]) eqns; 280val Fn_ind = REWRITE_RULE [GSYM Fn_def] ind; 281 282(*--------------------------------------------------------------------------- 283 e4 is the nested equation and has a remaining tc on its assumptions 284 ---------------------------------------------------------------------------*) 285 286val eqn4 = REWRITE_RULE [GSYM Fn_def] (DISCH_ALL e4); 287 288(*--------------------------------------------------------------------------- 289 CBN_UNION_aux, and therefore CBN, removes all App nodes from a term 290 ---------------------------------------------------------------------------*) 291 292val AppCountLem = Q.prove 293(`!e. AppCount (Fn e) = 0`, 294 recInduct Fn_ind 295 THEN RW_TAC arith_ss (AppCount_def::[e1,e2,e3,e5,e6,e7,e8]) THEN 296 Q.SUBGOAL_THEN 297 `inv_image ($< LEX $<) (\x. (JointAppCount x,JointStdSize x)) 298 (INL (Fn (INL (B,v,M)),y,N)) (INL (App B v M,y,N))` ASSUME_TAC THENL 299 [WEAKEN_TAC is_imp THEN 300 TotalDefn.TC_SIMP_TAC [] [JointAppCount_def,JointStdSize_def,AppCount_def], 301 PROVE_TAC [eqn4]]); 302 303(*--------------------------------------------------------------------------- 304 Termination of CBN 305 ---------------------------------------------------------------------------*) 306 307val (CBN_eqns, CBN_ind) = 308Defn.tprove(CBN_defn, 309 EXISTS_TAC R THEN REWRITE_TAC [SYM Fn_def, easy_tcs] 310 THEN TotalDefn.TC_SIMP_TAC [] 311 [JointAppCount_def,JointStdSize_def, AppCount_def,AppCountLem]); 312