Changeset 3559 for LTS/imp.ma
 Timestamp:
 Apr 30, 2015, 5:48:58 PM (4 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/imp.ma
r3553 r3559 118 118 119 119 lemma expr_eq_refl:∀e:expr.expr_eq e e=true. 120 #e elim e [1,2: #v change with (v==v = true); @(\b ?) % 120 #e elim e [1,2: #v whd in match (expr_eq ? ?); /2 by / 121 (*change with (v==v = true); @(\b ?) %*) 121 122 3,4: #f1 #f2 normalize #H1 >H1 #H2 >H2 %]qed. 122 123 … … 125 126 lemma expr_eq_equality:∀e1,e2:expr.expr_eq e1 e2=true ↔ e1=e2. 126 127 #e1 #e2 % [2:* lapply e2 e2 elim e1 127 [1,2:#n #_ change with (n==n = true) @(\b ?) %128 3,4:#f1 #f2 #H1 #H2 #e2 @expr_eq_refl]128 [1,2:#n #_ (*change with (n==n = true) @(\b ?) %*) 129 3,4:#f1 #f2 #H1 #H2 #e2] @expr_eq_refl 129 130 lapply e2 e2 elim e1 130 [1,2: #v1 #e2 cases e2131 [1,2: #v1 * 131 132 [1,6: #v2 #H >(\P H) % 132 2,5: #v2 #H normalize in H;destruct133 3,4,7,8: #e #f normalize#ABS destruct]134 3,4: #e #e2 #H #K #f cases f133 2,5: #v2 whd in ⊢((??%?)→ ?); #ABS destruct 134 3,4,7,8: #e #f whd in ⊢((??%?)→ ?); #ABS destruct] 135 3,4: #e #e2 #H #K * 135 136 [1,2,5,6: #v2 normalize #ABS destruct 136 137 3,4,7,8:#f1 #f2 normalize inversion(expr_eq e f1) #INV1 >INV1 inversion(expr_eq e2 f2) … … 158 159 #s cases s try(#v) try(#e) try % 159 160 [ whd in ⊢ (??%?); >(\b (refl … v)) >expr_eq_refl % 160  change with (v==v = true); >(\b ?) %] qed. 161 whd in match(seq_i_eq ? ?); /2 by / 162 (*change with (v==v = true); >(\b ?) %*)] qed. 161 163 162 164 lemma seq_i_eq_equality:∀s1,s2.seq_i_eq s1 s2=true ↔ s1=s2. … … 184 186 185 187 lemma condition_eq_refl:∀c:condition.cond_i_eq c c=true. 186 #c elim c [#e #f whd in ⊢ (??%?); >expr_eq_refl >expr_eq_refl normalize%188 #c elim c [#e #f whd in ⊢ (??%?); >expr_eq_refl >expr_eq_refl % 187 189 #c' normalize * %] qed. 188 190 … … 193 195 inversion(expr_eq e1 f1) [2: #_ normalize #EQ destruct ] #H1 194 196 >(proj1 … (expr_eq_equality …) … H1) 195 inversion(expr_eq e2 f2) [2: #_ normalize #EQ destruct ] #H2 #_197 inversion(expr_eq e2 f2) [2: #_ normalize #EQ destruct ] #H2 * 196 198 >(proj1 … (expr_eq_equality …) … H2) % 197 199  normalize #c #H destruct … … 459 461 definition imp_store:DeqSet≝mk_DeqSet store_t store_eq store_eq_equality. 460 462 461 definition imp_state_params:state_params≝mk_state_params imp_instr_params imp_env_params imp_store (*DeqEnv*). 463 (* Abitare record label_params *) 464 465 (* Abitare record monoid *) 466 467 (*definition nat_monoid:monoid≝mk_monoid DeqNat times 1 …. /2 by commutative_times / qed.*) 468 469 (* definition imp_label_params:label_params≝mk_label_params deqnat_monoid ….*) 470 471 definition imp_state_params:state_params≝mk_state_params imp_instr_params imp_env_params flat_labels imp_store (*DeqEnv*). 472 473 462 474 463 475 definition current_env:store_type imp_state_params→ option environment≝λs.match s with [nil⇒ None ? … … 578 590 definition imp_signature≝signature imp_state_params imp_state_params. 579 591 580 check CallCostLabel 581 582 definition imp_envitem:(env_item imp_env_params imp_instr_params)≝ 592 definition fact_signature:imp_signature≝mk_signature ? …. 593 [% @0@0% @0]qed. 594 (* signature of a function whose name is 0, takes a formal parameter x0 and 595 returns on x0 *) 596 597 definition imp_envitem:(env_item imp_env_params imp_instr_params flat_labels)≝ 598 ?. 599 @mk_env_item [@fact_signature% @1@CALL 600 ]qed. 601 602 check imp_envitem 583 603 584 604 (*  mIfThenElse1:
Note: See TracChangeset
for help on using the changeset viewer.