Changeset 3536
- Timestamp:
- Mar 16, 2015, 5:02:57 PM (6 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
LTS/imp.ma
r3534 r3536 18 18 include "Language.ma". 19 19 20 (* Tools *) 21 22 lemma ifthenelse_elim:∀b,T.∀t:T.if b then t else t=t. 23 #b #T #t cases b % qed. 24 25 lemma ifthenelse_left:∀b,T.∀t1,t2:T.if b then t1 else t2=t1→ (b=true ∨ t1=t2). 26 #b #T #t1 #t2 cases b #H normalize in H; destruct [%1|%2] % qed. 27 28 lemma ifthenelse_right:∀b,T.∀t1,t2:T.if b then t1 else t2=t2→ (b=false ∨ t1=t2). 29 #b #T #t1 #t2 cases b #H normalize in H; destruct [%2|%1] % qed. 30 31 lemma ifthenelse_mm:∀b,b':bool.if b then b' else false=true→ b'=true. 32 #b #b' cases b normalize #H destruct % qed. 33 34 lemma ifthenelse_mm2:∀b,b':bool.if b then b' else false=true→ b=true. 35 #b #b' cases b normalize #H destruct % qed. 36 37 let rec neqb n m ≝ 38 match n with 39 [ O ⇒ match m with [ O ⇒ true | S q ⇒ false] 40 | S p ⇒ match m with [ O ⇒ false | S q ⇒ neqb p q] 41 ]. 42 43 axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true ↔ n = m. 44 45 definition DeqNat:DeqSet≝mk_DeqSet nat neqb neqb_true_to_eq. 46 47 lemma neqb_refl:∀n.neqb n n=true. 48 #n elim n [%|#n' normalize * %]qed. 49 50 lemma neqb_sym:∀n1,n2.neqb n1 n2=neqb n2 n1. 51 #n1 elim n1 [#n2 cases n2 [%|#n' normalize %]|#n2' #IH #n2 cases n2 normalize [2: #m >IH] 52 % qed. 53 20 54 (* Syntax *) 21 55 22 definition variable ≝ nat. 23 axiom label:Type[0]. 56 definition variable ≝ DeqNat. 24 57 25 58 inductive expr: Type[0] ≝ 26 59 Var: variable → expr 27 | Const: nat → expr60 | Const: DeqNat → expr 28 61 | Plus: expr → expr → expr 29 62 | Minus: expr → expr → expr. … … 32 65 Eq: expr → expr → condition 33 66 | Not: condition → condition. 34 35 inductive seq_i:Type[0]≝sNop: seq_i|sAss: seq_i|sInc: seq_i. 67 68 let rec expr_eq (e1:expr) (e2:expr):bool≝ 69 match e1 with [Var v1⇒ match e2 with [Var v2⇒ neqb v1 v2|_⇒ false] 70 |Const v1⇒ match e2 with [Const v2⇒ neqb v1 v2|_⇒ false] 71 |Plus le1 re1 ⇒ match e2 with [Plus le2 re2 ⇒ andb (expr_eq le1 le2) (expr_eq re1 re2)|_⇒ false] 72 |Minus le1 re1 ⇒ match e2 with [Minus le2 re2 ⇒ andb (expr_eq le1 le2) (expr_eq re1 re2)|_⇒ false] 73 ]. 74 75 lemma expr_eq_refl:∀e:expr.expr_eq e e=true. 76 #e elim e [1,2: #v normalize lapply(neqb_true_to_eq v v) * #_ * % 77 |3,4: #f1 #f2 normalize #H1 >H1 #H2 >H2 %]qed. 78 79 lemma expr_eq_equality:∀e1,e2:expr.expr_eq e1 e2=true ↔ e1=e2. 80 #e1 #e2 % [2:* lapply e2 -e2 elim e1 81 [1,2:#n #_ normalize >neqb_refl % 82 |3,4:#f1 #f2 #H1 #H2 #e2 @expr_eq_refl] 83 |lapply e2 -e2 elim e1 84 [1,2: #v1 #e2 cases e2 normalize 85 [1,2,5,6: #v2 #H lapply(neqb_true_to_eq v1 v2) * #A destruct >(A H) #_ % 86 |3,4,7,8: #e #f #ABS destruct] 87 |3,4: #e #e2 #H #K #f cases f 88 [1,2,5,6: #v2 normalize #ABS destruct 89 |3,4,7,8:#f1 #f2 normalize inversion(expr_eq e f1) #INV1 >INV1 inversion(expr_eq e2 f2) 90 #INV2 >INV2 normalize #T destruct >(H ? INV1) >(K ? INV2) % qed. 91 92 inductive seq_i:Type[0]≝sNop: seq_i|sAss: variable → expr → seq_i|sInc: variable → seq_i. 36 93 definition seq_i_eq:seq_i→ seq_i → bool≝λs1,s2:seq_i.match s1 with [ 37 94 sNop ⇒ match s2 with [sNop ⇒ true| _⇒ false] … … 47 104 cases i1 qed. 48 105 49 let rec neqb n m ≝ 50 match n with 51 [ O ⇒ match m with [ O ⇒ true | S q ⇒ false] 52 | S p ⇒ match m with [ O ⇒ false | S q ⇒ neqb p q] 53 ]. 54 axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true → n = m. 106 (*axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true → n = m. 107 axiom neqb_true_to_eq2: ∀n,m:nat. neqb n m = true ↔ n = m.*) 55 108 lemma neqb_refl:∀n.neqb n n=true. 56 109 #n elim n [%|#n' normalize * %]qed. … … 75 128 |3,4: #f1 #f2 normalize #H1 >H1 #H2 >H2 %]qed. 76 129 77 lemma ifthenelse_aux:∀b,T.∀t:T.if b then t else t=t.78 #b #T #t cases b % qed.79 80 lemma ifthenelse_left:∀b,T.∀t1,t2:T.if b then t1 else t2=t1→ (b=true ∨ t1=t2).81 #b #T #t1 #t2 cases b #H normalize in H; destruct [%1|%2] % qed.82 83 lemma ifthenelse_right:∀b,T.∀t1,t2:T.if b then t1 else t2=t2→ (b=false ∨ t1=t2).84 #b #T #t1 #t2 cases b #H normalize in H; destruct [%2|%1] % qed.85 86 lemma ifthenelse_mm:∀b,b':bool.if b then b' else false=true→ b'=true.87 #b #b' cases b normalize #H destruct % qed.88 89 lemma ifthenelse_mm2:∀b,b':bool.if b then b' else false=true→ b=true.90 #b #b' cases b normalize #H destruct % qed.91 130 92 131 lemma expr_eq_plus:∀e1,e2,f1,f2:expr.expr_eq (Plus e1 e2) (Plus f1 f2)=true→ ((expr_eq e1 f1)=true∧(expr_eq e2 f2)=true). … … 227 266 |@(mk_DeqSet expr expr_eq expr_eq_equality)].qed. 228 267 268 229 269 (* | IfThenElse: condition → command → command → command*) 230 270 (* | For: variable → expr → list command → command*) … … 264 304 265 305 lemma assign_hit: ∀env,v,val. assign env v val v = val. 266 #env #v #val normalize > eqb_n_nnormalize %306 #env #v #val normalize >(eqb_n_n v) normalize % 267 307 qed. 268 308 269 309 lemma assign_miss: ∀env,v1,v2,val. v1 ≠ v2 → assign env v1 val v2 = env v2. 270 #env #v1 #v2 #val #E normalize > not_eq_to_eqb_false /2/310 #env #v1 #v2 #val #E normalize >(not_eq_to_eqb_false v2 v1) /2 by refl, not_to_not/ 271 311 qed. 272 312 … … 282 322 [ Eq e1 e2 ⇒ eqb (sem_expr env e1) (sem_expr env e2) 283 323 | Not c ⇒ notb (sem_condition env c) ]. 324 325 (*CERCO*) 326 327 328 329 definition imp_env_params:env_params≝mk_env_params environment. 330 331 axiom env_eq:environment→ environment → bool. 332 axiom env_eq_to_true:∀e1,e2.env_eq e1 e2=true ↔ e1 =e2. 333 definition DeqEnv:DeqSet≝mk_DeqSet environment env_eq env_eq_to_true. 334 335 definition imp_state_params:state_params≝mk_state_params imp_instr_params imp_env_params DeqEnv. 336 337 definition imp_eval_seq:(seq_instr imp_state_params)→(store_type imp_state_params)→ option (store_type imp_state_params)≝?. 338 normalize #s inversion(s) #INV #env [@(Some ? n)|@(Some ? n)|@(Some ? (S n))]qed. 339 340 definition imp_eval_io:(io_instr imp_state_params)→(store_type imp_state_params)→ option (store_type imp_state_params)≝?. 341 // qed. 342 343 definition imp_eval_cond_cond:(cond_instr imp_state_params)→ (store_type imp_state_params)→ option (bool × (store_type imp_state_params))≝?. 344 normalize #c cases c [(*case Eq e1 e2*) #e1 #e2 #n |(*case Not g*) #g] 345 346 (* 347 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))≝ 348 match c with 349 [Eq e1 e2⇒ ? 350 |Not c' ⇒ ? 351 ]. 352 *) 353 354 definition imp_sem_state_params≝mk_sem_state_params imp_instr_. 355 356 357 284 358 285 359 (* Big step, declarative semantics of programs *)
Note: See TracChangeset
for help on using the changeset viewer.