Changeset 3543
 Timestamp:
 Mar 18, 2015, 6:32:10 PM (5 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/imp.ma
r3541 r3543 19 19 include "basics/finset.ma". 20 20 21 22 21 23 (* Tools *) 24 22 25 23 26 lemma ifthenelse_elim:∀b,T.∀t:T.if b then t else t=t. … … 42 45 #b #b' cases b normalize #H destruct % qed. 43 46 47 48 44 49 (* Syntax *) 50 45 51 46 52 definition variable ≝ DeqNat. … … 85 91 #INV2 >INV2 normalize #T destruct >(H ? INV1) >(K ? INV2) % qed. 86 92 93 94 95 87 96 (* for the syntactical record in Language.ma *) 97 88 98 89 99 (* seq_i: type of sequential instructions *) … … 172 182 @(mk_DeqSet expr expr_eq expr_eq_equality)].qed. 173 183 174 (*  IfThenElse: condition → command → command → command*)175 (*  For: variable → expr → list command → command*)184 (*  IfThenElse: condition → command → command → command*) 185 (*  For: variable → expr → list command → command*) 176 186 inductive command: Type[0] ≝ 177 187 Nop: command … … 187 197 definition program ≝ list command. 188 198 199 200 189 201 (* Big step, operational semantics of expressions and conditions *) 190 202 203 191 204 definition environment ≝ list (variable × DeqNat). 192 205 193 (* definition environment ≝ variable → nat. *)194 195 (* definition eq_environment: environment → environment → Prop ≝206 (* definition environment ≝ variable → nat. *) 207 208 (* definition eq_environment: environment → environment → Prop ≝ 196 209 λenv1,env2. ∀v. env1 v = env2 v.*) 197 210 … … 199 212 λenv1,env2.env1 = env2. 200 213 201 (* definition default_env : environment ≝ λ_.0.*)214 (* definition default_env : environment ≝ λ_.0.*) 202 215 203 216 definition default_env: environment ≝ nil ?. 204 217 205 (*206 definition assign: environment → variable → nat → environment ≝207 λenv,v,val,x.208 match eqb x v with209 [ true ⇒ val210  false ⇒ env x].211 *)218 (* 219 definition assign: environment → variable → nat → environment ≝ 220 λenv,v,val,x. 221 match eqb x v with 222 [ true ⇒ val 223  false ⇒ env x]. 224 *) 212 225 213 226 let rec assign (env:environment) (v:variable) (n:DeqNat):environment ≝match env with … … 318 331  Not c ⇒ match (sem_condition env c) with [None ⇒ None ?Some b⇒ Some ? (notb b)]]. 319 332 333 334 320 335 (*CERCO*) 321 336 322 337 323 324 338 definition imp_env_params:env_params≝mk_env_params environment. 325 339 326 axiom env_eq:environment→ environment → bool. 327 axiom env_eq_to_true:∀e1,e2.env_eq e1 e2=true ↔ e1 =e2. 340 let rec env_eq (env1:environment) (env2:environment):bool≝match env1 with 341 [nil ⇒ match env2 with [nil⇒ true_ ⇒ false] 342 cons hd1 tl1 ⇒ match env2 with 343 [nil⇒ false 344 cons hd2 tl2 ⇒ match hd1 with 345 [mk_Prod v1 n1⇒ match hd2 with 346 [mk_Prod v2 n2⇒ (andb (andb (v1==v2) (n1==n2)) (env_eq tl1 tl2))] 347 ] 348 ] 349 ]. 350 351 lemma env_eq_refl:∀e.env_eq e e=true. 352 #e elim e [%* #v #n #e' #IH normalize >(eqb_n_n v) >(eqb_n_n n) >ifthenelse_true @IH] qed. 353 354 lemma env_eq_to_true:∀e1,e2.env_eq e1 e2=true ↔ e1 =e2. 355 #e1 #e2 % [2:* @env_eq_refl 356 lapply e2 e2 elim e1 357 [#e2 cases e2 normalize #H try(#K #ABS) destruct % 358 * #v #n #e' #IH * normalize in match(env_eq ??); 359 #p destruct cases p p #v' #n' #e whd in match(env_eq ??); 360 inversion(v==v') #INVvv' [2: >ifthenelse_false #ABS destruct 361 inversion(n==n') #INVnn' [2: >ifthenelse_false #ABS destruct normalize 362 #EQee' >(IH e EQee') >(\P INVnn') >(\P INVvv') % qed. 363 328 364 definition DeqEnv:DeqSet≝mk_DeqSet environment env_eq env_eq_to_true. 365 366 definition store_t:Type[0]≝list (DeqEnv ×variable). 367 368 let rec store_eq (s1:store_t) (s2:store_t):bool≝ 369 match s1 with 370 [nil⇒ match s2 with [nil⇒ true_⇒ false] 371 cons hd1 tl1⇒ match s2 with [nil⇒ false cons hd2 tl2⇒ (andb (hd1==hd2) (store_eq tl1 tl2))]]. 372 373 lemma store_eq_refl:∀s.store_eq s s=true. 374 #s elim s [%* #e #v #tl #IH whd in match(store_eq ??); >IH 375 >(\b (refl …)) % 376 qed. 377 378 lemma store_eq_equality:∀s1,s2:store_t.store_eq s1 s2=true↔s1=s2. 379 #s1 #s2 % [2: * @store_eq_refl 380 lapply s2 s2 elim s1 381 [* 382 [#_ % 383 #p #s2 normalize #ABS destruct 384 ] 385 #p #s2 #IH * whd in match (store_eq ??); 386 [#ABS destruct 387 #p' #s whd in match (store_eq ??); inversion(p==p') #INV 388 [>ifthenelse_true #H >(IH s H) >(\P INV) % 389 >ifthenelse_false #ABS destruct 390 ] 391 ] 392 ] qed. 393 394 395 (* store is actually a stack of pairs 〈environment, returnvariable〉 *) 396 definition imp_store:Type[0]≝mk_DeqSet store_t store_eq store_eq_equality. 329 397 330 398 definition imp_state_params:state_params≝mk_state_params imp_instr_params imp_env_params DeqEnv. … … 361 429 [lWhile g l⇒ match (sem_condition g) with [None ⇒ None ?Some b⇒ Some ? (mk_Prod b s)]].*) 362 430 363 definition imp_sem_state_params≝mk_sem_state_params imp_instr_. 431 definition imp_sem_state_params : sem_state_params imp_state_params ≝ mk_sem_state_params … imp_eval_seq imp_eval_io 432 imp_eval_cond_cond imp_eval_loop_cond …. 364 433 365 434
Note: See TracChangeset
for help on using the changeset viewer.