Changeset 3543


Ignore:
Timestamp:
Mar 18, 2015, 6:32:10 PM (5 years ago)
Author:
pellitta
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/imp.ma

    r3541 r3543  
    1919include "basics/finset.ma".
    2020
     21
     22
    2123(* Tools *)
     24
    2225
    2326lemma ifthenelse_elim:∀b,T.∀t:T.if b then t else t=t.
     
    4245#b #b' cases b normalize #H destruct % qed.
    4346
     47
     48
    4449(* Syntax *)
     50
    4551
    4652definition variable ≝ DeqNat.
     
    8591    #INV2 >INV2 normalize #T destruct >(H ? INV1) >(K ? INV2) % qed.
    8692
     93
     94
     95
    8796(* for the syntactical record in Language.ma *)
     97
    8898
    8999  (* seq_i: type of sequential instructions *)
     
    172182|@(mk_DeqSet expr expr_eq expr_eq_equality)].qed.
    173183
    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*)
    176186inductive command: Type[0] ≝
    177187   Nop: command
     
    187197definition program ≝ list command.
    188198
     199
     200
    189201(* Big step, operational semantics of expressions and conditions *)
    190202
     203
    191204definition environment ≝ list (variable × DeqNat).
    192205
    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 ≝
    196209 λenv1,env2. ∀v. env1 v = env2 v.*)
    197210 
     
    199212 λenv1,env2.env1 = env2.
    200213
    201 (* definition default_env : environment ≝ λ_.0.*)
     214          (* definition default_env : environment ≝ λ_.0.*)
    202215
    203216definition default_env: environment ≝ nil ?.
    204217
    205 (*
    206 definition assign: environment → variable → nat → environment ≝
    207  λenv,v,val,x.
    208   match eqb x v with
    209    [ true ⇒ val
    210    | 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          *)
    212225
    213226let rec assign (env:environment) (v:variable) (n:DeqNat):environment ≝match env with
     
    318331   | Not c ⇒ match (sem_condition env c) with [None ⇒ None ?|Some b⇒ Some ? (notb b)]].
    319332
     333
     334
    320335(*CERCO*)
    321336
    322337
    323 
    324338definition imp_env_params:env_params≝mk_env_params environment.
    325339
    326 axiom env_eq:environment→ environment → bool.
    327 axiom env_eq_to_true:∀e1,e2.env_eq e1 e2=true ↔ e1 =e2.
     340let 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
     351lemma 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
     354lemma 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
    328364definition DeqEnv:DeqSet≝mk_DeqSet environment env_eq env_eq_to_true.
     365
     366definition store_t:Type[0]≝list (DeqEnv ×variable).
     367
     368let rec store_eq (s1:store_t) (s2:store_t):bool≝
     369match 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
     373lemma 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 …)) %
     376qed.
     377
     378lemma 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, return-variable〉 *)
     396definition imp_store:Type[0]≝mk_DeqSet store_t store_eq store_eq_equality.
    329397
    330398definition imp_state_params:state_params≝mk_state_params imp_instr_params imp_env_params DeqEnv.
     
    361429[lWhile g l⇒ match (sem_condition g) with [None ⇒ None ?|Some b⇒ Some ? (mk_Prod b s)]].*)
    362430
    363 definition imp_sem_state_params≝mk_sem_state_params imp_instr_.
     431definition imp_sem_state_params : sem_state_params imp_state_params ≝ mk_sem_state_params … imp_eval_seq imp_eval_io
     432imp_eval_cond_cond imp_eval_loop_cond ….
    364433
    365434
Note: See TracChangeset for help on using the changeset viewer.