Changeset 3559 for LTS


Ignore:
Timestamp:
Apr 30, 2015, 5:48:58 PM (4 years ago)
Author:
pellitta
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/imp.ma

    r3553 r3559  
    118118
    119119lemma 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 ?) %*)
    121122|3,4: #f1 #f2 normalize #H1 >H1 #H2 >H2 %]qed.
    122123
     
    125126lemma expr_eq_equality:∀e1,e2:expr.expr_eq e1 e2=true ↔ e1=e2.
    126127#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
    129130|lapply e2 -e2 elim e1
    130   [1,2: #v1 #e2 cases e2
     131  [1,2: #v1 *
    131132    [1,6: #v2 #H >(\P H) %
    132     |2,5: #v2 #H normalize in H; destruct
    133     |3,4,7,8: #e #f normalize #ABS destruct]
    134   |3,4: #e #e2 #H #K #f cases f
     133    |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 *
    135136    [1,2,5,6: #v2 normalize #ABS destruct
    136137    |3,4,7,8:#f1 #f2 normalize inversion(expr_eq e f1) #INV1 >INV1 inversion(expr_eq e2 f2)
     
    158159#s cases s try(#v) try(#e) try %
    159160[ 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.
    161163
    162164lemma seq_i_eq_equality:∀s1,s2.seq_i_eq s1 s2=true ↔ s1=s2.
     
    184186
    185187lemma 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 %
    187189|#c' normalize * %] qed.
    188190
     
    193195  inversion(expr_eq e1 f1) [2: #_ normalize #EQ destruct ] #H1
    194196  >(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 *
    196198  >(proj1 … (expr_eq_equality …) … H2) %
    197199| normalize #c #H destruct
     
    459461definition imp_store:DeqSet≝mk_DeqSet store_t store_eq store_eq_equality.
    460462
    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
     471definition imp_state_params:state_params≝mk_state_params imp_instr_params imp_env_params flat_labels imp_store (*DeqEnv*).
     472
     473
    462474
    463475definition current_env:store_type imp_state_params→ option environment≝λs.match s with [nil⇒ None ?
     
    578590definition imp_signature≝signature imp_state_params imp_state_params.
    579591
    580 check CallCostLabel
    581 
    582 definition imp_envitem:(env_item imp_env_params imp_instr_params)≝
     592definition 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
     595returns on x0 *)
     596
     597definition imp_envitem:(env_item imp_env_params imp_instr_params flat_labels)≝
     598?.
     599@mk_env_item [@fact_signature|% @1|@CALL
     600]qed.
     601
     602check imp_envitem
    583603
    584604(* | mIfThenElse1:
Note: See TracChangeset for help on using the changeset viewer.