Changeset 3539
 Timestamp:
 Mar 17, 2015, 3:53:13 PM (5 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/imp.ma
r3538 r3539 24 24 #b #T #t cases b % qed. 25 25 26 lemma ifthenelse_true:∀T:Type[0].∀t1,t2:T.if true then t1 else t2=t1. 27 #T #t1 #t2 % qed. 28 29 lemma ifthenelse_false:∀T:Type[0].∀t1,t2:T.if false then t1 else t2=t2. 30 #T #t1 #t2 % qed. 31 26 32 lemma ifthenelse_left:∀b,T.∀t1,t2:T.if b then t1 else t2=t1→ (b=true ∨ t1=t2). 27 33 #b #T #t1 #t2 cases b #H normalize in H; destruct [%1%2] % qed. … … 133 139 qed. 134 140 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 #l2138 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 with149 [ 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 164 141 (*  IfThenElse: condition → command → command → command*) 165 142 (*  For: variable → expr → list command → command*) … … 177 154 definition program ≝ list command. 178 155 156 (* NO, modificare: serve solo la guardia del while (senza la roba qui sopra), 157 di fatto come per l'IfThenElse ho considerato solo Eq e Not *) 158 inductive loop_i:Type[0]≝lWhile: condition → program → loop_i. 159 definition 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 162 lemma loop_i_eq_equality:∀l1,l2.loop_i_eq l1 l2=true ↔ l1=l2.#l1 #l2 163 cases l1 cases l2 % #_ % qed. 164 165 definition io_i ≝ False. 166 167 definition io_i_eq ≝ λi1,i2:False. true. 168 169 lemma io_i_eq_equality: ∀i1,i2. io_i_eq i1 i2 = true ↔ i1=i2. * qed. 170 171 (* 172 let rec neqb n m ≝ 173 match 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 ]. 177 axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true ↔ n = m. 178 *) 179 180 definition 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 179 190 (* Big step, operational semantics of expressions and conditions *) 180 191 181 definition environment ≝ variable → nat. 182 192 definition 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 183 199 definition 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 204 definition default_env: environment ≝ nil ?. 205 206 (* 188 207 definition assign: environment → variable → nat → environment ≝ 189 208 λenv,v,val,x. … … 191 210 [ true ⇒ val 192 211  false ⇒ env x]. 193 212 *) 213 214 let 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 (* 194 223 definition increment: environment →variable →environment ≝ 195 224 λenv,v,x. … … 197 226 [true ⇒ (env x)+1 198 227  false ⇒ env x]. 199 228 *) 229 230 let 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 238 let 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 (* 200 247 lemma assign_hit: ∀env,v,val. assign env v val v = val. 201 248 #env #v #val normalize >(eqb_n_n v) normalize % 202 249 qed. 203 250 *) 251 252 lemma 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 ???); 255 inversion (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 264 p sono come termini dove ? significa qui no, % qui si' e tutti i nomi vanno usati _ 265 e non puoi usare costanti, costruttori, induttivi, etc. 266 267 la seconda parte del pattern individua un certo numero di posizioni chiamati RADICI; 268 se viene omessa la seconda parte c'e' una sola radice nella radice del termine 269 270 la prima parte del pattern cerca in ogni radice il sottotermine t e la tattica 271 lavora su quello 272 273 NOTA BENE: sia f una funzione ricorsiva sul primo argomento e nel goal c'e' 274 f (S m). Allora whd in match (f ?) identifica (f (S m)) che si riduce. 275 Mentre whd in match f identifica solo f che NON riduce. 276 277 *) 278 279 (* 204 280 lemma assign_miss: ∀env,v1,v2,val. v1 ≠ v2 → assign env v1 val v2 = env v2. 205 281 #env #v1 #v2 #val #E normalize >(not_eq_to_eqb_false v2 v1) /2 by refl, not_to_not/ 206 282 qed. 207 208 let rec sem_expr (env:environment) (e: expr) on e : nat ≝ 283 *) 284 285 lemma 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 288 whd in match (assign ???); >INV >ifthenelse_true whd in match (read (〈v,n〉::env') v2); 289 inversion(v2==v) #INV2 >INV2 [>ifthenelse_true>ifthenelse_false] 290 whd in match (read (〈v,val〉::env') v2); >INV2 [>ifthenelse_true>ifthenelse_false] 291 whd in match (read (〈v,n〉::env') v2); try % 292 lapply (\P INV2) #ABS elim E #ABS2 lapply (ABS2 ABS) #F cases F 293 whd in match (assign ???); >INV >ifthenelse_false whd in match (read ??); 294 inversion(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 % 297 qed. 298 299 let rec sem_expr (env:environment) (e: expr) on e : (option nat) ≝ 209 300 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 ? (nm)]]]. 307 308 (* 215 309 let rec sem_condition (env:environment) (c:condition) on c : bool ≝ 216 310 match c with 217 311 [ Eq e1 e2 ⇒ eqb (sem_expr env e1) (sem_expr env e2) 218 312  Not c ⇒ notb (sem_condition env c) ]. 313 *) 314 315 let 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)]]. 219 320 220 321 (*CERCO*) … … 230 331 definition imp_state_params:state_params≝mk_state_params imp_instr_params imp_env_params DeqEnv. 231 332 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. 333 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 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 ]. 234 338 235 339 definition imp_eval_io:(io_instr imp_state_params)→(store_type imp_state_params)→ option (store_type imp_state_params)≝?. 236 340 // qed. 237 341 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] 342 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 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 ]. 240 351 241 352 (* … … 246 357 ]. 247 358 *) 359 360 definition 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)]]. 248 362 249 363 definition imp_sem_state_params≝mk_sem_state_params imp_instr_.
Note: See TracChangeset
for help on using the changeset viewer.