Changeset 3539 for LTS/imp.ma


Ignore:
Timestamp:
Mar 17, 2015, 3:53:13 PM (5 years ago)
Author:
pellitta
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/imp.ma

    r3538 r3539  
    2424#b #T #t cases b % qed.
    2525
     26lemma ifthenelse_true:∀T:Type[0].∀t1,t2:T.if true then t1 else t2=t1.
     27#T #t1 #t2 % qed.
     28
     29lemma ifthenelse_false:∀T:Type[0].∀t1,t2:T.if false then t1 else t2=t2.
     30#T #t1 #t2 % qed.
     31
    2632lemma ifthenelse_left:∀b,T.∀t1,t2:T.if b then t1 else t2=t1→ (b=true ∨ t1=t2).
    2733#b #T #t1 #t2 cases b #H normalize in H; destruct [%1|%2] % qed.
     
    133139qed.
    134140
    135 inductive loop_i:Type[0]≝lWhile: loop_i.
    136 definition loop_i_eq:loop_i → loop_i → bool ≝λl1,l2:loop_i.true.
    137 lemma loop_i_eq_equality:∀l1,l2.loop_i_eq l1 l2=true ↔ l1=l2.#l1 #l2
    138 cases l1 cases l2 % #_ % qed.
    139 
    140 definition io_i ≝ False.
    141 
    142 definition io_i_eq ≝ λi1,i2:False. true.
    143 
    144 lemma io_i_eq_equality: ∀i1,i2. io_i_eq i1 i2 = true ↔ i1=i2. * qed.
    145 
    146 (*
    147 let rec neqb n m ≝
    148 match n with
    149   [ O ⇒ match m with [ O ⇒ true | S q ⇒ false]
    150   | S p ⇒ match m with [ O ⇒ false | S q ⇒ neqb p q]
    151   ].
    152 axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true ↔ n = m.
    153 *)
    154 
    155 definition imp_instr_params: instr_params ≝ mk_instr_params ? ? ? ? ? ?.
    156 [@(mk_DeqSet seq_i seq_i_eq seq_i_eq_equality)
    157 |@(mk_DeqSet io_i io_i_eq io_i_eq_equality)
    158 |@(mk_DeqSet cond_i cond_i_eq cond_i_eq_equality)
    159 |@(mk_DeqSet loop_i loop_i_eq loop_i_eq_equality)
    160 |@(mk_DeqSet expr expr_eq expr_eq_equality)
    161 |@(mk_DeqSet expr expr_eq expr_eq_equality)].qed.
    162 
    163 
    164141(* | IfThenElse: condition → command → command → command*)
    165142(* | For: variable → expr → list command → command*)
     
    177154definition program ≝ list command.
    178155
     156(* NO, modificare: serve solo la guardia del while (senza la roba qui sopra),
     157di fatto come per l'IfThenElse ho considerato solo Eq e Not *)
     158inductive loop_i:Type[0]≝lWhile: condition → program → loop_i.
     159definition loop_i_eq:loop_i → loop_i → bool ≝λl1,l2:loop_i.match l1 with
     160[lWhile c1 p1 ⇒ match l2 with [lWhile c2 p2 ⇒ (andb (c1==c2) (p1==p2))]].
     161
     162lemma loop_i_eq_equality:∀l1,l2.loop_i_eq l1 l2=true ↔ l1=l2.#l1 #l2
     163cases l1 cases l2 % #_ % qed.
     164
     165definition io_i ≝ False.
     166
     167definition io_i_eq ≝ λi1,i2:False. true.
     168
     169lemma io_i_eq_equality: ∀i1,i2. io_i_eq i1 i2 = true ↔ i1=i2. * qed.
     170
     171(*
     172let rec neqb n m ≝
     173match n with
     174  [ O ⇒ match m with [ O ⇒ true | S q ⇒ false]
     175  | S p ⇒ match m with [ O ⇒ false | S q ⇒ neqb p q]
     176  ].
     177axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true ↔ n = m.
     178*)
     179
     180definition imp_instr_params: instr_params ≝ mk_instr_params ? ? ? ? ? ?.
     181[@(mk_DeqSet seq_i seq_i_eq seq_i_eq_equality)
     182|@(mk_DeqSet io_i io_i_eq io_i_eq_equality)
     183|@(mk_DeqSet cond_i cond_i_eq cond_i_eq_equality)
     184|@(mk_DeqSet loop_i loop_i_eq loop_i_eq_equality)
     185|@(mk_DeqSet expr expr_eq expr_eq_equality)
     186|@(mk_DeqSet expr expr_eq expr_eq_equality)].qed.
     187
     188
     189
    179190(* Big step, operational semantics of expressions and conditions *)
    180191
    181 definition environment ≝ variable → nat.
    182 
     192definition environment ≝ list (variable × DeqNat).
     193
     194(* definition environment ≝ variable → nat. *)
     195
     196(* definition eq_environment: environment → environment → Prop ≝
     197 λenv1,env2. ∀v. env1 v = env2 v.*)
     198 
    183199definition eq_environment: environment → environment → Prop ≝
    184  λenv1,env2. ∀v. env1 v = env2 v.
    185 
    186 definition default_env : environment ≝ λ_.0.
    187 
     200 λenv1,env2.env1 = env2.
     201
     202(* definition default_env : environment ≝ λ_.0.*)
     203
     204definition default_env: environment ≝ nil ?.
     205
     206(*
    188207definition assign: environment → variable → nat → environment ≝
    189208 λenv,v,val,x.
     
    191210   [ true ⇒ val
    192211   | false ⇒ env x].
    193 
     212*)
     213
     214let rec assign (env:environment) (v:variable) (n:DeqNat):environment ≝match env with
     215[nil ⇒ [mk_Prod … v n]
     216|cons hd tl ⇒ match hd with [(mk_Prod v' n') ⇒ match (v==v') with
     217  [true ⇒ cons … (mk_Prod … v n) tl
     218  |false ⇒ cons … hd (assign tl v n)
     219  ]
     220]].
     221
     222(*
    194223definition increment: environment →variable →environment ≝
    195224 λenv,v,x.
     
    197226   [true ⇒ (env x)+1
    198227   | false ⇒ env x].
    199 
     228*)
     229
     230let rec increment (env:environment) (v:variable):environment ≝match env with
     231[nil ⇒ nil …
     232|cons hd tl ⇒ match hd with [(mk_Prod v' n) ⇒ match (v==v') with
     233  [true ⇒ cons … (mk_Prod … v (S n)) tl
     234  |false ⇒ cons … hd (increment tl v)
     235  ]
     236]].
     237
     238let rec read (env:environment) (v:variable):(option DeqNat)≝match env with
     239[nil ⇒ None …
     240|cons hd tl ⇒ match hd with [(mk_Prod v' n) ⇒ match (v==v') with
     241  [true ⇒ Some … n
     242  |false ⇒ read tl v
     243  ]
     244]].
     245
     246(*
    200247lemma assign_hit: ∀env,v,val. assign env v val v = val.
    201248 #env #v #val normalize >(eqb_n_n v) normalize %
    202249qed.
    203 
     250*)
     251
     252lemma assign_hit: ∀env,v,val. read (assign env v val) v = Some … val.
     253#env elim env
     254[2: * #v' #val' #env' #IH #v #val whd in match (assign ???);
     255inversion (v==v')
     256 [#INV whd in ⊢ (??%?); >(\b (refl …)) %
     257 |#INV whd in ⊢ (??%?); >INV whd in ⊢ (??%?); @IH ]
     258|#v #val whd in match (assign [ ] v val); normalize >(eqb_n_n v) %]qed.
     259
     260(*
     261
     262[in match t] in [H1:p ... Hn:p] [⊢ p]
     263
     264p sono come termini dove ? significa qui no, % qui si' e tutti i nomi vanno usati _
     265e non puoi usare costanti, costruttori, induttivi, etc.
     266
     267la seconda parte del pattern individua un certo numero di posizioni chiamati RADICI;
     268se viene omessa la seconda parte c'e' una sola radice nella radice del termine
     269
     270la prima parte del pattern cerca in ogni radice il sottotermine t e la tattica
     271lavora su quello
     272
     273NOTA BENE: sia f una funzione ricorsiva sul primo argomento e nel goal c'e'
     274f (S m). Allora whd in match (f ?) identifica (f (S m)) che si riduce.
     275Mentre whd in match f identifica solo f che NON riduce.
     276
     277 *)
     278
     279(*
    204280lemma assign_miss: ∀env,v1,v2,val. v1 ≠ v2 → assign env v1 val v2 = env v2.
    205281 #env #v1 #v2 #val #E normalize >(not_eq_to_eqb_false v2 v1) /2 by refl, not_to_not/
    206282qed.
    207 
    208 let rec sem_expr (env:environment) (e: expr) on e : nat ≝
     283*)
     284
     285lemma assign_miss: ∀env,v1,v2,val. v2 ≠ v1 → (read (assign env v1 val) v2)= (read env v2).
     286 #env #v1 #v2 #val #E elim env [normalize >(not_eq_to_eqb_false v2 v1) /2 by refl, not_to_not/
     287|* #v #n #env' #IH inversion(v1==v) #INV [lapply(\P INV)|lapply(\Pf INV)] #K [destruct
     288whd in match (assign ???); >INV >ifthenelse_true whd in match (read (〈v,n〉::env') v2);
     289inversion(v2==v) #INV2 >INV2 [>ifthenelse_true|>ifthenelse_false]
     290whd in match (read (〈v,val〉::env') v2); >INV2 [>ifthenelse_true|>ifthenelse_false]
     291whd in match (read (〈v,n〉::env') v2); try %
     292lapply (\P INV2) #ABS elim E #ABS2 lapply (ABS2 ABS) #F cases F
     293|whd in match (assign ???); >INV >ifthenelse_false whd in match (read ??);
     294inversion(v2==v) #INV2 [>ifthenelse_true|>ifthenelse_false]
     295[whd in match (read ??); >INV2 >ifthenelse_true %
     296|>IH whd in match (read (〈v,n〉::env') v2);  >INV2 >ifthenelse_false %
     297qed.
     298
     299let rec sem_expr (env:environment) (e: expr) on e : (option nat) ≝
    209300 match e with
    210   [ Var v ⇒ env v
    211   | Const n ⇒ n
    212   | Plus e1 e2 ⇒ sem_expr env e1 + sem_expr env e2
    213   | Minus e1 e2 ⇒ sem_expr env e1 - sem_expr env e2 ].
    214 
     301  [ Var v ⇒ read env v
     302  | Const n ⇒ Some ? n
     303  | Plus e1 e2 ⇒ match sem_expr env e1 with [None ⇒ None ?|Some n⇒
     304                 match sem_expr env e2 with [None ⇒ None ?|Some m⇒ Some ? (n+m)]]
     305  | Minus e1 e2 ⇒ match sem_expr env e1 with [None ⇒ None ?|Some n⇒
     306                 match sem_expr env e2 with [None ⇒ None ?|Some m⇒ Some ? (n-m)]]].
     307
     308(*
    215309let rec sem_condition (env:environment) (c:condition) on c : bool ≝
    216310  match c with
    217311   [ Eq e1 e2 ⇒ eqb (sem_expr env e1) (sem_expr env e2)
    218312   | Not c ⇒ notb (sem_condition env c) ].
     313*)
     314
     315let rec sem_condition (env:environment) (c:condition) on c : option bool ≝
     316  match c with
     317   [ Eq e1 e2 ⇒ match (sem_expr env e1) with [None ⇒ None ?|Some n⇒
     318                match (sem_expr env e2) with [None ⇒ None ?|Some m⇒ Some ? (eqb n m)]]
     319   | Not c ⇒ match (sem_condition env c) with [None ⇒ None ?|Some b⇒ Some ? (notb b)]].
    219320
    220321(*CERCO*)
     
    230331definition imp_state_params:state_params≝mk_state_params imp_instr_params imp_env_params DeqEnv.
    231332
    232 definition imp_eval_seq:(seq_instr imp_state_params)→(store_type imp_state_params)→ option (store_type imp_state_params)≝?.
    233 normalize * [| 2: #v #e |3: #v ] #env [@(Some ? env)|@(Some ? n)|@(Some ? (S n))]qed.
     333definition imp_eval_seq:(seq_instr imp_state_params)→(store_type imp_state_params)→ option (store_type imp_state_params)≝λi,s.match i with
     334[sNop ⇒ Some ? s
     335|sAss v e ⇒ match (sem_expr s e) with [None ⇒ None ?| Some n⇒ Some ? (assign s v n)]
     336|sInc v ⇒ match (read s v) with [None ⇒ None ?|Some n⇒ Some ? (assign s v (S n))]
     337].
    234338
    235339definition imp_eval_io:(io_instr imp_state_params)→(store_type imp_state_params)→ option (store_type imp_state_params)≝?.
    236340// qed.
    237341
    238 definition imp_eval_cond_cond:(cond_instr imp_state_params)→ (store_type imp_state_params)→ option (bool × (store_type imp_state_params))≝?.
    239 normalize #c cases c [(*case Eq e1 e2*) #e1 #e2 #n |(*case Not g*) #g]
     342definition 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
     343[Eq e1 e2⇒ match (sem_expr s e1) with
     344  [None⇒ None ?
     345  |Some n ⇒ match (sem_expr s e2) with
     346    [None ⇒ None ?
     347    |Some m ⇒ Some ? (mk_Prod ?? (eqb n m) s)]
     348  ]
     349|Not e ⇒ match (sem_condition s e) with [None ⇒ None ?|Some b ⇒ Some ? (mk_Prod ?? b s)]
     350].
    240351
    241352(*
     
    246357].
    247358*)
     359
     360definition imp_eval_loop_cond:(loop_instr imp_state_params)→ (store_type imp_state_params)→ option (bool × (store_type imp_state_params))≝λl,s.match l with
     361[lWhile g l⇒ match (sem_condition g) with [None ⇒ None ?|Some b⇒ Some ? (mk_Prod b s)]].
    248362
    249363definition imp_sem_state_params≝mk_sem_state_params imp_instr_.
Note: See TracChangeset for help on using the changeset viewer.