Changeset 3560
 Timestamp:
 Jun 16, 2015, 1:24:00 PM (6 years ago)
 Location:
 LTS
 Files:

 4 added
 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/imp.ma
r3559 r3560 19 19 include "basics/finset.ma". 20 20 21 22 23 (* Tools *)24 25 26 lemma ifthenelse_elim:∀b,T.∀t:T.if b then t else t=t.27 #b #T #t cases b % qed.28 29 (* use "whd in match (if ? then ? else ?);" instead of these two *)30 (* however, whd fails to rewrite in some cases *)31 (* to use it on hypothesis H write "whd in match(if ? then ? else ?) in H;" *)32 lemma ifthenelse_true:∀T:Type[0].∀t1,t2:T.if true then t1 else t2=t1.33 #T #t1 #t2 % qed.34 35 lemma ifthenelse_false:∀T:Type[0].∀t1,t2:T.if false then t1 else t2=t2.36 #T #t1 #t2 % qed.37 38 lemma ifthenelse_left:∀b,T.∀t1,t2:T.if b then t1 else t2=t1→ (b=true ∨ t1=t2).39 #b #T #t1 #t2 cases b #H normalize in H; destruct [%1%2] % qed.40 41 lemma ifthenelse_right:∀b,T.∀t1,t2:T.if b then t1 else t2=t2→ (b=false ∨ t1=t2).42 #b #T #t1 #t2 cases b #H normalize in H; destruct [%2%1] % qed.43 44 (* it does not seem to be useful at all (rewriting does not simplify) *)45 lemma ifthenelse_match:∀T:Type[0].∀t1,t2:T.∀b.if b then t1 else t2=match b with [true⇒ t1false⇒ t2].46 #T #t1 #t2 * [>ifthenelse_true>ifthenelse_false] % qed.47 48 (* are these two really needed now? *)49 lemma ifthenelse_mm:∀b,b':bool.if b then b' else false=true→ b'=true.50 #b #b' cases b normalize #H destruct % qed.51 52 lemma ifthenelse_mm2:∀b,b':bool.if b then b' else false=true→ b=true.53 #b #b' cases b normalize #H destruct % qed.54 55 (* is ex_falso in the standard libary? *)56 (*lemma ex_falso_quodlibet:∀P:Prop.False→ P.57 #P #F cases F qed.*)58 lemma ex_falso_quodlibet:False→ ∀P:Prop.P.59 #F cases F qed.60 61 (* what about this? *)62 (*lemma contradiction:∀A:Prop.∀P.P→¬P→ A.63 #A #P #H #Hn @(ex_falso_quodlibet ?) @(absurd P H Hn). qed.*)64 65 lemma contradiction:∀P.P→¬P→ (∀A:Prop.A).66 #P #H #Hn #A @(ex_falso_quodlibet (absurd P H Hn)) qed.67 68 (*69 lemma not_true:∀b.(b≠true)→ (b=false).#b cases b #H try(%)70 @(contradiction (true=true) (refl …) H) qed.71 72 lemma not_false:∀b.(b≠false)→ (b=true).#b cases b #H try(%)73 @(contradiction (false=false) (refl …) H) qed.74 *)75 76 lemma not_bool:∀b1,b2.(b1≠b2)→ b1=(notb b2).* * normalize #H try(%)77 @(contradiction (?=?) (refl …) H) qed.78 79 lemma neq_bool:∀b1,b2.b1=(notb b2)→(b1≠b2).* * normalize #H /2 by sym_not_eq/ qed.80 81 lemma eqb_refl:∀T:DeqSet.∀t:T.(t==t)=true.82 #T #t @(\b ?) % qed. (* inversion(t==t) #H try(%) lapply(\Pf H) #ABS @(contradiction …) [@(t=t)@refl@ABS] qed.*)83 84 lemma eqb_sym:∀T:DeqSet.∀t1,t2:T.(t1==t2)=(t2==t1).85 #T #t1 #t2 inversion(t1==t2) #INV [lapply(\P INV)lapply(\Pf INV)] #H [>H >eqb_refl %86 inversion(t2==t1) #INV2 [lapply(\P INV2) #ABS destruct @(contradiction ((t1==t1)=true) INV2 ?)87 /2 by /%] qed.88 89 lemma neq_refl_false:∀T.∀t:T.(t≠t)→ ∀P:Prop.P.90 #T #t #H @(contradiction (t=t) (refl …) H) qed.91 92 lemma neqb_refl_false:∀T:DeqSet.∀t:T.(t==t)=false→ ∀P:Prop.P.93 #T #t #ABS @(contradiction ((t==t)=true) (eqb_refl …) ?) @neq_bool whd in match(¬true);94 assumption qed.95 96 21 (* Syntax *) 97 22 … … 107 32 Eq: expr → expr → condition 108 33  Not: condition → condition. 109 110 (* technical lemmas for expr_eq*)111 34 112 35 let rec expr_eq (e1:expr) (e2:expr):bool≝ … … 146 69 (* seq_i: type of sequential instructions *) 147 70 148 inductive seq_i:Type[0]≝sNop: seq_isAss: variable → expr → seq_i sInc: variable → seq_i.71 inductive seq_i:Type[0]≝sNop: seq_isAss: variable → expr → seq_i. 149 72 150 73 definition seq_i_eq:seq_i→ seq_i → bool≝λs1,s2:seq_i.match s1 with [ 151 74 sNop ⇒ match s2 with [sNop ⇒ true _⇒ false] 152 75 sAss v e ⇒ match s2 with [sAss v' e' ⇒ (andb (v==v') (expr_eq e e')) _⇒ false] 153 sInc v ⇒ match s2 with [sInc v' ⇒ (v==v') _⇒ false]154 76 ]. 155 77 … … 158 80 lemma seq_i_eq_refl:∀s.seq_i_eq s s=true. 159 81 #s cases s try(#v) try(#e) try % 160 [whd in ⊢ (??%?); >(\b (refl … v)) >expr_eq_refl %161 whd in match(seq_i_eq ? ?); /2 by / 162 (*change with (v==v = true); >(\b ?) %*) ]qed.82 whd in ⊢ (??%?); >(\b (refl … v)) >expr_eq_refl % 83 (*whd in match(seq_i_eq ? ?); /2 by /*) 84 (*change with (v==v = true); >(\b ?) %*) qed. 163 85 164 86 lemma seq_i_eq_equality:∀s1,s2.seq_i_eq s1 s2=true ↔ s1=s2. 165 #s1 #s2 % [2: * elim s1 [2 ,3:#v try(#e)] @seq_i_eq_refl166 lapply s2 s2 elim s1 [2 ,3:#v] [#e] #s2 cases s2 [2,3,5,6,8,9:#v'] [1,3,5:#e']87 #s1 #s2 % [2: * elim s1 [2:#v try(#e)] @seq_i_eq_refl 88 lapply s2 s2 elim s1 [2:#v] [#e] #s2 cases s2 [2,4:#v' #e'] 167 89 [2,3,4,6,7,8: normalize #H destruct 168 90 1: whd in ⊢ (??%? → ?); inversion (v==v') [2: normalize #_ #H destruct] 169 91 #EQ inversion (expr_eq e e') [2: normalize #_ #H destruct] #H #_ 170 92 >(proj1 … (expr_eq_equality …) H) >(\P EQ) % 171 5: #H >(\P H) % 172  // ] 93 ] % 173 94 qed. 174 95 … … 229 150 @(mk_DeqSet cond_i cond_i_eq cond_i_eq_equality) 230 151 @(mk_DeqSet loop_i loop_i_eq loop_i_eq_equality) 231 @DeqExpr 232 @(mk_DeqSet expr expr_eq expr_eq_equality)].qed. 233 234 (*  IfThenElse: condition → command → command → command*) 235 (*  For: variable → expr → list command → command*) 236 inductive command: Type[0] ≝ 237 Nop: command 238  Ass: variable → expr → command 239  Inc: variable → command 240  IfThenElse: condition → list command → list command → command 241  While: condition → list command → command 242  Call: variable → expr → function → command 243  Return: expr → command 244 with function: Type[0] ≝ 245  Fun: variable → list command → function. 246 247 definition program ≝ list command. 248 249 250 251 (* Big step, operational semantics of expressions and conditions *) 252 253 254 definition environment ≝ list (variable × DeqNat). 255 256 (* definition environment ≝ variable → nat. *) 257 258 (* definition eq_environment: environment → environment → Prop ≝ 259 λenv1,env2. ∀v. env1 v = env2 v.*) 152 @(DeqProd variable DeqExpr) 153 @DeqExpr].qed. 154 155 156 definition environment ≝ DeqSet_List (DeqProd variable DeqNat). 260 157 261 158 definition eq_environment: environment → environment → Prop ≝ 262 159 λenv1,env2.env1 = env2. 263 160 264 (* definition default_env : environment ≝ λ_.0.*)265 161 266 162 definition default_env: environment ≝ nil ?. 267 268 (* 269 definition assign: environment → variable → nat → environment ≝ 270 λenv,v,val,x. 271 match eqb x v with 272 [ true ⇒ val 273  false ⇒ env x]. 274 *) 163 275 164 276 165 let rec assign (env:environment) (v:variable) (n:DeqNat):environment ≝match env with 277 166 [nil ⇒ [mk_Prod … v n] 278 cons hd tl ⇒ match hd with [(mk_Prod v' n') ⇒ match (v==v') with 279 [true ⇒ cons … (mk_Prod … v n) tl 280 false ⇒ cons … hd (assign tl v n) 281 ] 282 ]]. 283 284 (* 285 definition increment: environment →variable →environment ≝ 286 λenv,v,x. 287 match eqb x v with 288 [true ⇒ (env x)+1 289  false ⇒ env x]. 290 *) 291 292 let rec increment (env:environment) (v:variable):environment ≝match env with 293 [nil ⇒ nil … 294 cons hd tl ⇒ match hd with [(mk_Prod v' n) ⇒ match (v==v') with 295 [true ⇒ cons … (mk_Prod … v (S n)) tl 296 false ⇒ cons … hd (increment tl v) 297 ] 298 ]]. 167 cons hd tl ⇒ 168 let 〈v',n'〉≝ hd in if (v==v') 169 then 〈v,n〉::tl 170 else hd::(assign tl v n) 171 ]. 299 172 300 173 let rec read (env:environment) (v:variable):(option DeqNat)≝match env with 301 174 [nil ⇒ None … 302 cons hd tl ⇒ match hd with [(mk_Prod v' n) ⇒ match (v==v') with 303 [true ⇒ Some … n 304 false ⇒ read tl v 305 ] 306 ]]. 307 308 (* 309 lemma assign_hit: ∀env,v,val. assign env v val v = val. 310 #env #v #val normalize >(eqb_n_n v) normalize % 311 qed. 312 *) 175 cons hd tl ⇒ let 〈v',n〉≝ hd in 176 if (v==v') 177 then Some … n 178 else read tl v 179 ]. 180 313 181 314 182 lemma assign_hit: ∀env,v,val. read (assign env v val) v = Some … val. … … 320 188 #v #val whd in match (assign [ ] v val); normalize >(eqb_n_n v) %]qed. 321 189 322 (* 323 324 [in match t] in [H1:p ... Hn:p] [⊢ p] 325 326 p sono come termini dove ? significa qui no, % qui si' e tutti i nomi vanno usati _ 327 e non puoi usare costanti, costruttori, induttivi, etc. 328 329 la seconda parte del pattern individua un certo numero di posizioni chiamati RADICI; 330 se viene omessa la seconda parte c'e' una sola radice nella radice del termine 331 332 la prima parte del pattern cerca in ogni radice il sottotermine t e la tattica 333 lavora su quello 334 335 NOTA BENE: sia f una funzione ricorsiva sul primo argomento e nel goal c'e' 336 f (S m). Allora whd in match (f ?) identifica (f (S m)) che si riduce. 337 Mentre whd in match f identifica solo f che NON riduce. 338 339 *) 340 341 (* 342 lemma assign_miss: ∀env,v1,v2,val. v1 ≠ v2 → assign env v1 val v2 = env v2. 343 #env #v1 #v2 #val #E normalize >(not_eq_to_eqb_false v2 v1) /2 by refl, not_to_not/ 344 qed. 345 *) 190 346 191 347 192 lemma assign_miss: ∀env,v1,v2,val. v2 ≠ v1 → (read (assign env v1 val) v2)= (read env v2). 348 193 #env #v1 #v2 #val #E elim env [normalize >(not_eq_to_eqb_false v2 v1) /2 by refl, not_to_not/ 349 194 * #v #n #env' #IH inversion(v1==v) #INV [lapply(\P INV)lapply(\Pf INV)] #K [destruct 350 whd in match (assign ???); >INV >ifthenelse_truewhd in match (read (〈v,n〉::env') v2);351 inversion(v2==v) #INV2 >INV2 [>ifthenelse_true>ifthenelse_false]352 whd in match (read (〈v,val〉::env') v2); >INV2 [>ifthenelse_true>ifthenelse_false]195 whd in match (assign ???); >INV normalize nodelta whd in match (read (〈v,n〉::env') v2); 196 inversion(v2==v) #INV2 >INV2 normalize nodelta 197 whd in match (read (〈v,val〉::env') v2); >INV2 normalize nodelta 353 198 whd in match (read (〈v,n〉::env') v2); try % 354 lapply (\P INV2) #ABS @ex_falso_quodlibet @(absurd ? ABS E)199 lapply (\P INV2) #ABS cases(absurd ? ABS E) 355 200 (*elim E #ABS2 lapply (ABS2 ABS) #F cases F*) 356 whd in match (assign ???); >INV >ifthenelse_falsewhd in match (read ??);201 whd in match (assign ???); >INV normalize nodelta whd in match (read ??); 357 202 inversion(v2==v) #INV2 whd in match(if ? then ? else ?); 358 [whd in match (read ??); >INV2 >ifthenelse_true%359 >IH whd in match (read (〈v,n〉::env') v2); >INV2 >ifthenelse_false%203 [whd in match (read ??); >INV2 % 204 >IH whd in match (read (〈v,n〉::env') v2); >INV2 % 360 205 qed. 361 362 lemma assign_miss2: ∀env,v1,v2,val. v2 ≠ v1 → (read (assign env v1 val) v2)= (read env v2).363 #env #v1 #v2 #val #E elim env [whd in match (assign ???); whd in match(read ??);364 >(\bf E) >ifthenelse_false %* #v #n #env' inversion(v==v1) #INV [<(\P INV)365 #K whd in match (assign ???); >(\b refl …) whd in match(if ? then ? else ?);366 whd in match(read (〈v,n〉::env') v2); inversion(v2==v) #INV2367 whd in match(if ? then ? else ?); whd in match(if ? then ? else ?); whd in match(read ??);368 >INV2 try(%) inversion(E) #ABS #ABS2 destruct <(\P INV) in ABS; >(\P INV2) #ABS369 @(contradiction (v=v) (refl …) ?) % assumptionlapply (\Pf INV) #K whd in match (assign ???);370 whd in match (read (〈v,n〉::env') v2); inversion(v2==v) #INV2 [>ifthenelse_true>ifthenelse_false]371 >(\b INV2) #H whd in match (assign ???); inversion(v1==v) #INV'372 [1,3:>ifthenelse_true2,4:>ifthenelse_false] [2,4: <H whd in match(read ??); [373 >eqb_sym in INV; #INV @(contradiction ((v1==v)=true) ? ?) [@INV'/2 by /]374 >INV2 >ifthenelse_false %]@(contradiction ((v1==v)=true) ? ?)375 [assumption/2 by /]whd in match (read ??); >INV2 >ifthenelse_true % qed.376 206 377 207 let rec sem_expr (env:environment) (e: expr) on e : (option nat) ≝ … … 379 209 [ Var v ⇒ read env v 380 210  Const n ⇒ Some ? n 381  Plus e1 e2 ⇒ match sem_expr env e1 with [None ⇒ None ?Some n⇒ 382 match sem_expr env e2 with [None ⇒ None ?Some m⇒ Some ? (n+m)]] 383  Minus e1 e2 ⇒ match sem_expr env e1 with [None ⇒ None ?Some n⇒ 384 match sem_expr env e2 with [None ⇒ None ?Some m⇒ Some ? (nm)]]]. 385 386 (* 387 let rec sem_condition (env:environment) (c:condition) on c : bool ≝ 388 match c with 389 [ Eq e1 e2 ⇒ eqb (sem_expr env e1) (sem_expr env e2) 390  Not c ⇒ notb (sem_condition env c) ]. 391 *) 211  Plus e1 e2 ⇒ !n1 ← sem_expr env e1; 212 !n2 ← sem_expr env e2; 213 return (n1+n2) 214  Minus e1 e2 ⇒ !n1 ← sem_expr env e1; 215 !n2 ← sem_expr env e2; 216 return (n1n2) 217 ]. 392 218 393 219 let rec sem_condition (env:environment) (c:condition) on c : option bool ≝ 394 220 match c with 395 [ Eq e1 e2 ⇒ match (sem_expr env e1) with [None ⇒ None ?Some n⇒ 396 match (sem_expr env e2) with [None ⇒ None ?Some m⇒ Some ? (eqb n m)]] 397  Not c ⇒ match (sem_condition env c) with [None ⇒ None ?Some b⇒ Some ? (notb b)]]. 221 [ Eq e1 e2 ⇒ !n ← sem_expr env e1; 222 !m ← sem_expr env e2; 223 return (eqb n m) 224  Not c ⇒ !b ← sem_condition env c; 225 return (notb b) 226 ]. 398 227 399 228 … … 401 230 (*CERCO*) 402 231 403 404 232 definition imp_env_params:env_params≝mk_env_params variable. 405 233 406 let rec env_eq (env1:environment) (env2:environment):bool≝match env1 with 407 [nil ⇒ match env2 with [nil⇒ true_ ⇒ false] 408 cons hd1 tl1 ⇒ match env2 with 409 [nil⇒ false 410 cons hd2 tl2 ⇒ match hd1 with 411 [mk_Prod v1 n1⇒ match hd2 with 412 [mk_Prod v2 n2⇒ (andb (andb (v1==v2) (n1==n2)) (env_eq tl1 tl2))] 413 ] 414 ] 415 ]. 416 417 lemma env_eq_refl:∀e.env_eq e e=true. 418 #e elim e [%* #v #n #e' #IH normalize >(eqb_n_n v) >(eqb_n_n n) >ifthenelse_true @IH] qed. 419 420 lemma env_eq_to_true:∀e1,e2.env_eq e1 e2=true ↔ e1 =e2. 421 #e1 #e2 % [2:* @env_eq_refl 422 lapply e2 e2 elim e1 423 [#e2 cases e2 normalize #H try(#K #ABS) destruct % 424 * #v #n #e' #IH * normalize in match(env_eq ??); 425 #p destruct cases p p #v' #n' #e whd in match(env_eq ??); 426 inversion(v==v') #INVvv' [2: >ifthenelse_false #ABS destruct 427 inversion(n==n') #INVnn' [2: >ifthenelse_false #ABS destruct normalize 428 #EQee' >(IH e EQee') >(\P INVnn') >(\P INVvv') % qed. 429 430 definition DeqEnv:DeqSet≝mk_DeqSet environment env_eq env_eq_to_true. 431 432 definition store_t:Type[0]≝list (DeqEnv ×variable). 433 434 let rec store_eq (s1:store_t) (s2:store_t):bool≝ 435 match s1 with 436 [nil⇒ match s2 with [nil⇒ true_⇒ false] 437 cons hd1 tl1⇒ match s2 with [nil⇒ false cons hd2 tl2⇒ (andb (hd1==hd2) (store_eq tl1 tl2))]]. 438 439 lemma store_eq_refl:∀s.store_eq s s=true. 440 #s elim s [%* #e #v #tl #IH whd in match(store_eq ??); >IH 441 >(\b (refl …)) % 442 qed. 443 444 lemma store_eq_equality:∀s1,s2:store_t.store_eq s1 s2=true↔s1=s2. 445 #s1 #s2 % [2: * @store_eq_refl 446 lapply s2 s2 elim s1 447 [* 448 [#_ % 449 #p #s2 normalize #ABS destruct 450 ] 451 #p #s2 #IH * whd in match (store_eq ??); 452 [#ABS destruct 453 #p' #s whd in match (store_eq ??); inversion(p==p') #INV 454 [>ifthenelse_true #H >(IH s H) >(\P INV) % 455 >ifthenelse_false #ABS destruct 456 ] 457 ] 458 ] qed. 459 460 (* store is actually a stack of pairs 〈environment, returnvariable〉 *) 461 definition imp_store:DeqSet≝mk_DeqSet store_t store_eq store_eq_equality. 462 463 (* Abitare record label_params *) 464 465 (* Abitare record monoid *) 466 467 (*definition nat_monoid:monoid≝mk_monoid DeqNat times 1 …. /2 by commutative_times / qed.*) 468 469 (* definition imp_label_params:label_params≝mk_label_params deqnat_monoid ….*) 470 471 definition imp_state_params:state_params≝mk_state_params imp_instr_params imp_env_params flat_labels imp_store (*DeqEnv*). 472 473 474 475 definition current_env:store_type imp_state_params→ option environment≝λs.match s with [nil⇒ None ? 476 cons hd tl⇒ match hd with [(mk_Prod env var)⇒ Some ? env]]. 234 definition store_t≝ DeqSet_List (DeqProd environment variable). 235 236 definition imp_state_params:state_params≝ 237 mk_state_params imp_instr_params imp_env_params flat_labels store_t (*DeqEnv*). 238 239 definition current_env:store_type imp_state_params→ option environment≝λs.!hd ← option_hd … s; return \fst hd. 240 241 definition assign_var ≝ λenv:store_t.λv:variable.λn:DeqNat. 242 match env with 243 [ nil ⇒ None ? 244  cons hd tl ⇒ let 〈e,var〉 ≝ hd in return (〈assign e v n,var〉 :: tl) 245 ]. 246 477 247 478 248 definition imp_eval_seq:(seq_instr imp_state_params)→(store_type imp_state_params)→ option (store_type imp_state_params)≝λi,s.match i with … … 480 250 sAss v e ⇒ match s with 481 251 [nil⇒ None ? 482 cons hd tl⇒ match hd with 483 [(mk_Prod env var) ⇒ match (sem_expr env e) with 484 [None ⇒ None ? 485  Some n⇒ Some ? (cons ? (mk_Prod ? ? (assign env v n) var) tl) 486 ] 487 ] 252 cons hd tl⇒ let 〈env,var〉 ≝ hd in 253 ! n ← sem_expr env e; 254 assign_var s v n 488 255 ] 489 sInc v ⇒ match s with [nil⇒ None ?cons hd tl⇒ match hd with [(mk_Prod env var)⇒ 490 match (read env v) with [None ⇒ None ?Some n⇒ Some ? (cons ? (mk_Prod ? ? (assign env v (S n)) var) tl)]]] 491 ]. 256 ]. 257 492 258 493 259 definition imp_eval_io:(io_instr imp_state_params)→(store_type imp_state_params)→ option (store_type imp_state_params)≝?. 494 260 // qed. 495 261 496 definition imp_eval_cond_cond:(cond_instr imp_state_params)→ (store_type imp_state_params)→ option (bool × (store_type imp_state_params))≝λc,s.match c with 497 [Eq e1 e2⇒ match (current_env s) with 498 [None ⇒ None ? 499 Some env⇒ match (sem_expr env e1) with 500 [None⇒ None ? 501 Some n ⇒ match (sem_expr env e2) with 502 [None ⇒ None ? 503 Some m ⇒ Some ? (mk_Prod ?? (eqb n m) s)] 262 definition imp_eval_cond_cond:(cond_instr imp_state_params)→ (store_type imp_state_params)→ option (bool × (store_type imp_state_params))≝λc,s. 263 !env ← current_env s; 264 !b ← sem_condition env c; 265 return 〈b,s〉. 266 267 268 definition imp_eval_loop_cond:(loop_instr imp_state_params)→ (store_type imp_state_params)→ option (bool × (store_type imp_state_params))≝ 269 imp_eval_cond_cond. 270 271 definition imp_init_store: (store_type imp_state_params)≝[〈(nil ?),O〉]. 272 273 definition imp_eval_call:(signature imp_state_params imp_state_params)→ act_params_type imp_state_params → store_t → (option store_t)≝ 274 λsgn,e,st. 275 match sgn with 276 [ mk_signature fun fpt rt ⇒ 277 let 〈var,act_exp〉 ≝ e in 278 match st with 279 [nil ⇒ None ? 280 cons hd tl⇒ let 〈env,v〉≝ hd in 281 !n ← sem_expr env act_exp; 282 assign_var (〈(nil ?),var〉::st) fpt n 504 283 ] 505 ] 506 Not e ⇒ match (current_env s) with 507 [None ⇒ None ? 508 Some env⇒ match (sem_condition env e) with 509 [None ⇒ None ? 510 Some b ⇒ Some ? (mk_Prod ?? b s) 511 ] 512 ] 513 ]. 514 515 (* 516 let rec imp_eval_cond_cond (c: (cond_instr imp_state_params)) (s:(store_type imp_state_params)):option (bool × (store_type imp_state_params))≝ 517 match c with 518 [Eq e1 e2⇒ ? 519 Not c' ⇒ ? 520 ]. 521 *) 522 523 524 525 definition imp_eval_loop_cond:(loop_instr imp_state_params)→ (store_type imp_state_params)→ option (bool × (store_type imp_state_params))≝imp_eval_cond_cond. 526 (*λl,s.match l with 527 [lWhile g l⇒ match (sem_condition g) with [None ⇒ None ?Some b⇒ Some ? (mk_Prod b s)]].*) 528 529 definition imp_eval_call:(signature imp_state_params imp_state_params)→ expr→ imp_store→ (option imp_store)≝ 530 λsgn,e,st.match sgn with [mk_signature fun fpt rt ⇒ match st with 531 [nil ⇒ None ? 532 cons hd tl⇒ match hd with 533 [mk_Prod env v ⇒ match (sem_expr env e) with 534 [None ⇒ None ? 535 Some n⇒ Some ? (cons ? (mk_Prod … (assign default_env fpt n) v) st) 536 ] 537 ] 538 ] 539 ]. 540 541 definition imp_return_call:(return_type imp_state_params)→ imp_store→ (option imp_store)≝ 542 λr,s.match s with [nil⇒ None ? 543 cons hd tl⇒ match hd with 544 [mk_Prod env v ⇒ match (sem_expr env r) with 545 [None ⇒ None ? 546 Some n⇒ Some ? (cons ? (mk_Prod …(assign env v n) v) tl) 547 ] 548 ] 549 ]. 550 551 definition imp_init_store: (store_type imp_state_params)≝(mk_Prod DeqEnv variable (nil ?) O)::(nil ?). 284 ]. 285 286 definition imp_return_call:(return_type imp_state_params)→ store_t→ (option store_t)≝ 287 λr,s.match s with 288 [nil⇒ None ? 289 cons hd tl⇒ let 〈env,v〉≝ hd in 290 !n ← sem_expr env r; 291 assign_var tl v n 292 ]. 293 294 552 295 553 296 … … 555 298 imp_eval_cond_cond imp_eval_loop_cond imp_eval_call imp_return_call imp_init_store. 556 299 557 558 559 560 (* Big step, declarative semantics of programs *)561 562 definition status≝variable × (program × environment). (* indirizzo di ritorno, continuazione, ambiente *)563 564 definition stack≝list status.565 566 definition default_stack:stack≝nil ?.567 568 definition push: list status → status → list status ≝569 λl,s.cons ? s l.570 571 definition empty: list status → bool≝572 λl.match l with [nil ⇒ true  _ ⇒ false].573 574 definition peek: list status → status ≝575 λl.(hd ? l (mk_Prod ? ? 0 (mk_Prod ? ? [ ] default_env))).576 577 definition pop: list status → list status ≝578 λl.tail ? l.579 580 definition Geq:expr → expr → condition≝λe1,e2.Eq (Minus e1 e2) (Const 0).581 582 definition Lt:expr → expr → condition≝λe1,e2.Not (Geq e2 e1).583 584 (* Abitare tipo Program *)585 586 300 (* Abitare tipo Instructions *) 587 301 588 definition imp_Instructions≝Instructions imp_state_params .302 definition imp_Instructions≝Instructions imp_state_params flat_labels. 589 303 590 304 definition imp_signature≝signature imp_state_params imp_state_params. 591 305 592 definition fact_signature:imp_signature≝mk_signature ? …. 593 [% @0@0% @0]qed. 594 (* signature of a function whose name is 0, takes a formal parameter x0 and 595 returns on x0 *) 596 597 definition imp_envitem:(env_item imp_env_params imp_instr_params flat_labels)≝ 598 ?. 599 @mk_env_item [@fact_signature% @1@CALL 600 ]qed. 601 602 check imp_envitem 603 604 (*  mIfThenElse1: 605 ∀env,st,cond,c1,c2,cont. 606 sem_condition env cond = true → 607 moves ((IfThenElse cond c1 c2)::cont) env st (c1::cont) env st 608  mIfThenElse2: 609 ∀env,st,cond,c1,c2,cont. 610 sem_condition env cond = false → 611 moves ((IfThenElse cond c1 c2)::cont) env st (c2::cont) env st 612 *) 613 (*  mFor1: 614 ∀env,st,v,e,l,cont. 615 (sem_condition env (Lt (Var v) e))=true 616 → moves ((For v e l)::cont) env st (l@((Inc v)::(For v e l)::cont)) env st 617  mFor2: 618 ∀env,st,v,e,l,cont. 619 (sem_condition env (Lt (Var v) e ))=false 620 → moves ((For v e l)::cont) env st cont env st 621 *) 622 623 inductive moves: list command → environment → stack → list command → environment → stack → Prop ≝ 624 mNop: ∀env,st,cont. moves (Nop::cont) env st cont env st 625  mAss: ∀env,st,v,e,cont.moves ((Ass v e)::cont) env st cont (assign env v (sem_expr env e)) st 626  mInc: ∀env,st,v,cont.moves ((Inc v)::cont) env st cont (increment env v) st 627  mIfThenElse1: 628 ∀env,st,cond,l1,l2,cont. 629 sem_condition env cond = true → 630 moves ((IfThenElse cond l1 l2)::cont) env st (l1@cont) env st 631  mIfThenElse2: 632 ∀env,st,cond,l1,l2,cont. 633 sem_condition env cond = false → 634 moves ((IfThenElse cond l1 l2)::cont) env st (l2@cont) env st 635  mWhile1: 636 ∀env,st,cond,l,cont. 637 sem_condition env cond = true → 638 moves ((While cond l)::cont) env st (l@(While cond l)::cont) env st 639  mWhile2: 640 ∀env,st,cond,l,cont. 641 sem_condition env cond = false → 642 moves ((While cond l)::cont) env st cont env st 643  mCall: 644 ∀env,st,v,e,cont.∀v',l. 645 moves ((Call v e (Fun v' l))::cont) env st l (assign default_env v' (sem_expr env e)) (push st (mk_Prod ? ? v (mk_Prod ? ? cont env))) 646  mReturn: 647 ∀env,env',st,v,e,cont,cont'. 648 moves ((Return e)::cont) env ((mk_Prod ? ? v (mk_Prod ? ? cont' env'))::st) ((Ass v e)::cont') env' st. 649 650 (* bacato: diverge silentemente nel caso lista vuota *) 651 inductive moves_star: list command → environment → stack → list command → environment → stack → Prop ≝ 652 ms_done: ∀l,env,stack. moves_star l env stack l env stack 653  ms_step: ∀l1,env1,stack1,l2,env2,stack2,l3,env3,stack3. 654 moves l1 env1 stack1 l2 env2 stack2 → moves_star l2 env2 stack2 l3 env3 stack3 → 655 moves_star l1 env1 stack1 l3 env3 stack3. 656 657 (* corretto anche con lista vuota di sopra *) 658 inductive converges: list command → environment → stack → environment → stack → Prop ≝ 659 conv_done: ∀l,env,stack,env',stack'.moves l env stack [ ] env' stack' → converges l env stack env' stack' 660  conv_step: ∀l,hd,tl,env,stack,env',stack',env'',stack''.moves l env stack (hd::tl) env' stack' → converges (hd::tl) env' stack' env'' stack'' → 661 converges l env stack env'' stack''. 662 663 (*inductive converges: list command → environment → stack → environment → stack → Prop ≝ 664 conv_done: converges [] env stack env stack 665  conv_step: moves l env stack l' env' stack' → converges l' env' stack ' env'' stack'' → 666 converes l env stack env'' stack''.*) 667 668 669 (* Examples *) 670 671 example example1: 672 ∃env. 673 moves_star 674 [Ass 0 (Const 2) 675 ;While (Not (Eq (Var 0) (Const 0))) 676 [Ass 0 (Minus (Var 0) (Const 1)) 677 ;Ass 1 (Plus (Var 1) (Const 1))]] 678 default_env 679 default_stack 680 (nil ?) 681 env 682 default_stack 683 ∧ eq_environment env (assign default_env 1 2). 684 % [2: % [(*@(assign default_env 1 2)%[2:normalize #v cases v [%#v' %]*) 685 @(ms_step … (mAss …)) @(ms_step …(mWhile1 …)) [normalize % @(ms_step …(mAss …)) @(ms_step …(mAss …)) 686 @(ms_step … (mWhile1 …)) [normalize % @(ms_step …(mAss …)) @(ms_step …(mAss …)) 687 @(ms_step … (mWhile2 …)) [normalize % @(ms_done …) ]]] normalize #v cases v normalize [%#p cases p normalize [%#_ %]]]] skip qed. 688 689 (* Big step, declarative semantics of diverging programs *) 690 691 (* coinductive types are greatest fixpoints generated by the constructors; 692 they are built starting from the set of all terms and removing at every 693 step all terms that do not start with one of the constructors listed in the 694 coinductive type declaration. 695 696 Intuitively, they are inhabited by all the terms of the corresponding 697 inductive type and by new ``infinite'' terms obtained by chaining an infinite 698 number of constructors. Intuitively again, their abstract syntax tree is 699 infinite. In practice, however, we will only be able to inhabit coinductive 700 types with either finite terms or with circular terms obtained by corecursion. 701 702 Recursion over coinductive types is not allowed, since the recursive functions 703 could diverge on infinite (circular) term. Corecursion is allowed to create 704 circular terms *) 705 coinductive diverges: command → environment → Prop ≝ 706 cmIfThenElse1: 707 ∀env,cond,c1,c2. 708 sem_condition env cond = true → diverges c1 env → 709 diverges (IfThenElse cond c1 c2) env 710  cmIfThenElse2: 711 ∀env,cond,c1,c2. 712 sem_condition env cond = false → diverges c2 env → 713 diverges (IfThenElse cond c1 c2) env 714  cmIfThenElseList1: 715 ∀env,cond,l1,l2. 716 sem_condition env cond = true → diverges_l l1 env → 717 diverges (IfThenElseList cond l1 l2) env 718  cmIfThenElseList2: 719 ∀env,cond,l1,l2. 720 sem_condition env cond = false → diverges_l l2 env → 721 diverges (IfThenElseList cond l1 l2) env 722  cmWhile1: 723 ∀env,cond,l. 724 sem_condition env cond = true → diverges_l l env → diverges (While cond l) env → 725 diverges (While cond l) env 726  cmWhile2: 727 ∀env,env',cond,l. 728 sem_condition env cond = true → moves_l l env env' → diverges (While cond l) env' → 729 diverges (While cond l) env 730  cmFor: 731 ∀env,v,e,l. 732 ((sem_condition env (Eq (Minus e (Var v)) (Const 0))))=false → diverges_l l env → diverges (For v e l) env 733 with diverges_l: list command → environment → Prop ≝ 734 cmCons1: 735 ∀env,env',he,tl. 736 moves he env env' → diverges_l tl env' → 737 diverges_l (he::tl) env 738  cmCons2: 739 ∀env,he,tl. 740 diverges he env → diverges_l (he::tl) env. 741 742 (* Examples *) 743 744 (* Here we use corecursion to provide an infinite (circular) proof that 745 the following term diverges. The env will vary at every iteration, but 746 the value of the first variable will never be changed. 747 748 Note: a corecursive function (proof) must be _productive_, i.e. its weak 749 head normal form must start with a constructor. I.e. in a finite number of 750 steps the function must provide a first observation of the infinite term, 751 where observations are identified with constructors. This is the case in 752 the following definition. The exact conditions are omitted. *) 753 754 let corec example_div1' (x:unit) : 755 ∀env. env 0 = 2 → 756 diverges 757 (While (Not (Eq (Var 0) (Const 0))) 758 [Ass 1 (Minus (Var 0) (Const 1)) 759 ;Ass 1 (Plus (Var 1) (Const 1))]) 760 env ≝ ?. 761 #env #H 762 @cmWhile2 [2: normalize >H % 3: 763 @mCons [2: @mAss  skip  764 @mCons [3: @mNil  skip  @mAss]] skip  765 @example_div1' // @H 766 qed. 767 768 example example_div1: 769 diverges_l 770 [Ass 0 (Const 2) 771 ;While (Not (Eq (Var 0) (Const 0))) 772 [Ass 1 (Minus (Var 0) (Const 1)) 773 ;Ass 1 (Plus (Var 1) (Const 1))]] 774 default_env. 775 @cmCons1 [2: @mAss  skip] 776 @cmCons2 @example_div1' // 777 qed. 778 779 (* Small step, continuation style, computational semantics of programs *) 780 781 definition status ≝ program × environment. 782 783 definition final_environment_is: status → environment → Prop ≝ 784 λs,env. 785 match s with 786 [ (*was pair*) mk_Prod l env' ⇒ 787 match l with 788 [ nil ⇒ eq_environment env env' 789  cons _ _ ⇒ False]]. 790 791 definition step: status → option status ≝ 792 λs. 793 match s with 794 [ (*was pair*) mk_Prod p env ⇒ 795 match p with 796 [ nil ⇒ None ? 797  cons he tl ⇒ 798 Some … 799 match he with 800 [ Ass v val ⇒ 〈tl, assign env v (sem_expr env val)〉 801  Inc v ⇒ 〈tl, assign env v (sem_expr env (Plus (Var v) (Const 1)))〉 802  IfThenElse cond c1 c2 ⇒ 803 match sem_condition env cond with 804 [ true ⇒ 〈c1::tl, env〉 805  false ⇒ 〈c2::tl, env〉] 806  IfThenElseList cond l1 l2 ⇒ 807 match sem_condition env cond with 808 [ true ⇒ 〈l1@tl, env〉 809  false ⇒ 〈l2@tl, env〉] 810  While cond l ⇒ 811 match sem_condition env cond with 812 [ true ⇒ 〈l@(While cond l)::tl, env〉 813  false ⇒ 〈tl, env〉] 814  For v e l ⇒ 815 match sem_condition env (Eq (Minus (Var v) e) (Const 0)) with 816 [ true ⇒ 〈tl, env〉 817  false ⇒ 〈l@(Inc v::((For v e l)::tl)), env〉 818 ] 819 ]]]. 820 821 let rec steps (s:status) (n:nat) on n : status ≝ 822 match n with 823 [ O ⇒ s 824  S m ⇒ 825 match step s with 826 [ None ⇒ s 827  Some s' ⇒ steps s' m]]. 828 829 example example2: 830 final_environment_is 831 (steps 832 〈[Ass 0 (Const 2) 833 ;While (Not (Eq (Var 0) (Const 0))) 834 [Ass 0 (Minus (Var 0) (Const 1)) 835 ;Ass 1 (Plus (Var 1) (Const 1))]] 836 ,default_env〉 837 20) 838 (assign default_env 1 2). 839 normalize 840 #v cases v normalize // #p cases p // 841 qed. 842 843 (* Missing from the standard library *) 844 845 lemma bool_inv_ind: 846 ∀b:bool. ∀P: bool → Prop. (b=true → P true) → (b=false → P false) → P b. 847 #b #P cases b /2/ 848 qed. 849 850 lemma option_inv_ind: 851 ∀A.∀x:option A. ∀P: option A → Prop. 852 (x=None A → P (None A)) → (∀y. x = Some … y → P (Some … y)) → P x. 853 #A #x #P cases x /2/ 854 qed. 855 856 (* Equivalence of the two semantics on terminating programs *) 857 858 lemma moves_l_cons_invert: 859 ∀hd,tl,env,env'. 860 moves_l (hd::tl) env env' → 861 ∃env''. moves hd env env'' ∧ moves_l tl env'' env'. 862 #hd #tl #env #env' 863 lapply (refl … (hd::tl)) generalize in match (hd::tl) in ⊢ (??%? → %); #l 864 #H1 #H2 cases H2 in H1; 865 [ #env'' #abs destruct 866  #env1 #env2 #env'' #hd' #tl' #H1 #H2 #E destruct /3/ ] 867 qed. 868 869 lemma moves_l_append_invert: 870 ∀l1,l2,env,env'. 871 moves_l (l1@l2) env env' → 872 ∃env''. moves_l l1 env env'' ∧ moves_l l2 env'' env'. 873 #l1 elim l1 874 [ /3/ 875  #he #tl #IH #l2 #env #env' #H 876 cases (moves_l_cons_invert … H) 877 #env2 * #H1 #H2 cases (IH … H2) #env3 * /4/ ] 878 qed. 879 880 lemma commutative_plus: 881 ∀n,m.n+m=m+n. 882 #n #m elim m [normalize //#m' #IH //]qed. 883 884 lemma step_Some_to_moves_l: 885 ∀l,env,p',env',env''. 886 step 〈l,env〉 = Some … 〈p',env'〉 → moves_l p' env' env'' → moves_l l env env''. 887 #l #env #p' #env' #env'' whd in match step; normalize nodelta cases l normalize 888 [ #abs destruct 889  #he #tl normalize #E destruct E cases he in e0; normalize nodelta 890 [ #v #e #E destruct /2/ 891  #v #E destruct /2/ 892  #cond #c1 #c2 inversion (sem_condition env cond) normalize 893 #H1 #H2 destruct 894 [ #H2 cases (moves_l_cons_invert … H2) #env2 * /3/ 895  #H2 cases (moves_l_cons_invert … H2) #env2 * /3/ ] 896  #cond #l1 #l2 inversion (sem_condition env cond) normalize 897 #H1 #H2 destruct 898 [ #H2 cases (moves_l_append_invert … H2) #env2 * /3/ 899  #H2 cases (moves_l_append_invert … H2) #env2 * /3/ ] 900  #cond #l inversion (sem_condition env cond) normalize 901 #H1 #H2 destruct 902 [ (* entra nel while *) #H2 cases (moves_l_append_invert … H2) #env2 * #H3 903 #H4 cases (moves_l_cons_invert … H4) #env3 * /3/ 904  (* termina il while *) /3/ ] 905  (* caso For*) #v #e inversion(eqb(env vsem_expr env e) 0) normalize 906 #INV #l' 907 [ (* sottocaso non entro nel for *) 908 #HD destruct #H2 %2 [@env'%10 normalize @INV@H2] 909 (* sottocaso entro nel for *) 910 #HD destruct #H2 cases (moves_l_append_invert … H2) 911 #env2 * #H3 #H4 cases (moves_l_cons_invert … H4) 912 #env3 * 913 914 #H5 #H6 destruct cases (moves_l_cons_invert … H6) 915 #env4 * #H7 #H8 destruct %2 [@env4%9[3:normalize @INV@env24:@H3@env3 916 @H5@H7]@H8] 917 qed. 918 919 theorem steps_to_moves_l: 920 ∀n,l,env,env'. steps 〈l,env〉 n = 〈[],env'〉 → moves_l l env env'. 921 #n elim n 922 [ #l #env #env' #H normalize in H; destruct // 923  #m #IH #l #env #env' whd in ⊢ (??%? → ?); cases l 924 [ normalize #H destruct // 925  #he #tl inversion (step 〈he::tl,env〉) 926 [ #abs normalize in abs; destruct 927  * #l' #env2 #H #K normalize in K; lapply (IH ??? K) /3/ ]]] 928 qed. 929 930 let rec moves_l_to_steps (l:?) (env:?) (env':?) (H: moves_l l env env') on H : 931 ∃n1.∀n2,tl. steps 〈l@tl,env〉 (n1+n2) = steps 〈tl,env'〉 n2 ≝ ? 932 and moves_to_steps (c:?) (env:?) (env':?) (H: moves c env env') on H : 933 ∃n1.∀n2,tl. steps 〈c::tl,env〉 (n1+n2) = steps 〈tl,env'〉 n2 ≝ ?. 934 cases H 935 [ moves_l_to_steps moves_to_steps #env %{0} #n2 #tl % 936  #env1 #env2 #env3 #he #tl #H1 #H2 937 lapply (moves_to_steps … H1) moves_to_steps * #n1 #K1 938 lapply (moves_l_to_steps … H2) moves_l_to_steps * #n2 #K2 939 %{(n1+n2)} #n3 #tl >associative_plus >K1 @K2 940 941  #env1 #v #e %{1} #n #tl % 942 (* Inc *) #env1 #v %{1} #v' #tl' % 943  #env1 #env2 #cond #c1 #c2 #E 944 #H lapply (moves_to_steps … H) moves_to_steps moves_l_to_steps * #n1 #K 945 %{(S n1)} #n2 #tl normalize >E @K 946  #env1 #env2 #cond #c1 #c2 #E 947 #H lapply (moves_to_steps … H) moves_to_steps moves_l_to_steps * #n1 #K 948 %{(S n1)} #n2 #tl normalize >E @K 949  (* IfThenElseList *) #env1 #env2 #cond #l1 #l2 #E #H1 950 lapply (moves_l_to_steps … H1) moves_l_to_steps * #n1 #K1 951 %{(S n1)} #n3 #tl normalize >E normalize >associative_plus >K1 % 952 #env1 #env2 #cond #l1 #l2 #E #H1 953 lapply (moves_l_to_steps … H1) moves_l_to_steps * #n1 #K1 954 %{(S n1)} #n3 #tl normalize >E normalize >associative_plus >K1 % 955  #env1 #env2 #env3 #cond #l #E #H1 #H2 956 lapply (moves_l_to_steps … H1) moves_l_to_steps * #n1 #K1 957 lapply (moves_to_steps … H2) moves_to_steps * #n2 #K2 958 %{(S (n1+n2))} #n3 #tl normalize >E normalize >associative_plus >K1 @K2 959  #env #cond #l #E %{1} #n #tl normalize >E % 960 (* For *) #env1 #env2 #env3 #env4 #v #e #l #E normalize in E; #HL #HMI #HMF 961 lapply (moves_l_to_steps … HL) moves_l_to_steps * #n1 #K1 962 963 lapply (moves_to_steps … HMI) * #n2 #K2 964 lapply (moves_to_steps … HMF) moves_to_steps * #n3 #K3 965 %{(S(n1+n2+n3))} #n #tl normalize >E normalize >associative_plus >associative_plus 966 >K1 >K2 >K3 % 967 #env #v #e #l #E normalize in E; %{1} #n #tl normalize >E normalize % 968 ] 969 qed. 306 307 definition imp_envitem≝ (env_item imp_env_params imp_instr_params flat_labels). 308
Note: See TracChangeset
for help on using the changeset viewer.