Changeset 3575 for LTS/imp.ma


Ignore:
Timestamp:
Jun 19, 2015, 12:00:22 AM (4 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/imp.ma

    r3560 r3575  
    1313(**************************************************************************)
    1414
    15 include "basics/lists/list.ma".
    16 include "arithmetics/nat.ma".
    17 include "basics/bool.ma".
    1815include "Language.ma".
    19 include "basics/finset.ma".
     16
    2017
    2118(* Syntax *)
     
    3330 | Not: condition → condition.
    3431
    35 let rec expr_eq (e1:expr) (e2:expr):bool≝
    36 match e1 with [Var v1⇒ match e2 with [Var v2⇒ v1==v2|_⇒ false]
    37 |Const v1⇒ match e2 with [Const v2⇒ v1==v2|_⇒ false]
     32let rec expr_eq (e1:expr) (e2:expr) on e1 :bool≝
     33match e1 with [Var v1⇒ match e2 with [Var v2⇒ eqb v1 v2|_⇒ false]
     34|Const v1⇒ match e2 with [Const v2⇒ eqb v1 v2|_⇒ false]
    3835|Plus le1 re1 ⇒ match e2 with [Plus le2 re2 ⇒ andb (expr_eq le1 le2) (expr_eq re1 re2)|_⇒ false]
    3936|Minus le1 re1 ⇒ match e2 with [Minus le2 re2 ⇒ andb (expr_eq le1 le2) (expr_eq re1 re2)|_⇒ false]
    4037].
    4138
    42 lemma expr_eq_refl:∀e:expr.expr_eq e e=true.
    43 #e elim e [1,2: #v whd in match (expr_eq ? ?); /2 by /
    44 (*change with (v==v = true); @(\b ?) %*)
    45 |3,4: #f1 #f2 normalize #H1 >H1 #H2 >H2 %]qed.
    46 
    47   (* the predicate expr_eq corresponds to syntactical equality on the type expr *)
    48 
    49 lemma expr_eq_equality:∀e1,e2:expr.expr_eq e1 e2=true ↔ e1=e2.
    50 #e1 #e2 % [2:* lapply e2 -e2 elim e1
    51   [1,2:#n #_ (*change with (n==n = true) @(\b ?) %*)
    52   |3,4:#f1 #f2 #H1 #H2 #e2] @expr_eq_refl
    53 |lapply e2 -e2 elim e1
    54   [1,2: #v1 *
    55     [1,6: #v2 #H >(\P H) %
    56     |2,5: #v2 whd in ⊢((??%?)→ ?); #ABS destruct
    57     |3,4,7,8: #e #f whd in ⊢((??%?)→ ?); #ABS destruct]
    58   |3,4: #e #e2 #H #K *
    59     [1,2,5,6: #v2 normalize #ABS destruct
    60     |3,4,7,8:#f1 #f2 normalize inversion(expr_eq e f1) #INV1 >INV1 inversion(expr_eq e2 f2)
    61     #INV2 >INV2 normalize #T destruct >(H ? INV1) >(K ? INV2) % qed.
    62 
    63 
    64 
    65 
     39lemma expr_eq_elim : ∀P : bool → Prop.∀e1,e2.(e1 = e2 → P true) → (e1 ≠ e2 → P false) → P (expr_eq e1 e2).
     40#P #e1 lapply P -P elim e1 -e1
     41[1,2: #v #P * [1,5: #v' |2,6: #v' |*: #e1 #e2 ] #H1 #H2 normalize try(@H2 % #EQ destruct) @(eqb_elim v v')
     42  [1,3: #EQ destruct @H1 % |*: * #H @H2 % #EQ destruct @H %]
     43|*: #e1 #e2 #IH1 #IH2 #P * [1,5: #v' |2,6: #v' |*: #e1' #e2' ] #H1 #H2 try(@H2 % #EQ destruct) normalize
     44    @IH1
     45    [1,3: #EQ destruct normalize @IH2 [1,3: #EQ destruct @H1 % |*: * #H @H2 % #EQ destruct @H %]
     46    |*: * #H @H2 % #EQ destruct @H %
     47    ]
     48]
     49qed.
     50
     51definition DeqExpr ≝
     52mk_DeqSet expr expr_eq ?.
     53@hide_prf #e1 #e2 @expr_eq_elim
     54[ #EQ destruct % // | * #H % #EQ destruct cases H % ]
     55qed.
     56
     57unification hint  0 ≔ ;
     58    X ≟ DeqExpr
     59(* ---------------------------------------- *) ⊢
     60    expr ≡ carr X.
     61
     62(* ambigous input? why?
     63unification hint  0 ≔ p1,p2;
     64    X ≟ DeqExpr
     65(* ---------------------------------------- *) ⊢
     66    expr_eq p1 p2 ≡ eqb X p1 p2.
     67*)
    6668(* for the syntactical record in Language.ma *)
    6769
     
    6971  (* seq_i: type of sequential instructions *)
    7072
    71 inductive seq_i:Type[0]≝sNop: seq_i|sAss: variable → expr → seq_i.
    72 
    73 definition seq_i_eq:seq_i→ seq_i → bool≝λs1,s2:seq_i.match s1 with [
    74  sNop ⇒ match s2 with [sNop ⇒ true| _⇒ false]
    75 |sAss v e ⇒ match s2 with [sAss v' e' ⇒ (andb (v==v') (expr_eq e e'))| _⇒ false]
    76 ].
    77 
    78   (* technical lemma(s) for seq_i_eq *)
    79 
    80 lemma seq_i_eq_refl:∀s.seq_i_eq s s=true.
    81 #s cases s try(#v) try(#e) try %
    82 whd in ⊢ (??%?); >(\b (refl … v)) >expr_eq_refl %
    83 (*|whd in match(seq_i_eq ? ?); /2 by /*)
    84 (*change with (v==v = true); >(\b ?) %*) qed.
    85 
    86 lemma seq_i_eq_equality:∀s1,s2.seq_i_eq s1 s2=true ↔ s1=s2.
    87 #s1 #s2 % [2: * elim s1 [2:#v try(#e)] @seq_i_eq_refl
    88 |lapply s2 -s2 elim s1 [2:#v] [#e] #s2 cases s2 [2,4:#v' #e']
    89 [2,3,4,6,7,8: normalize #H destruct
    90 |1: whd in ⊢ (??%? → ?); inversion (v==v') [2: normalize #_ #H destruct]
    91  #EQ inversion (expr_eq e e') [2: normalize #_ #H destruct] #H #_
    92  >(proj1 … (expr_eq_equality …) H) >(\P EQ) %
    93 ] %
    94 qed.
    95 
    96   (* cond_i: type of (guards of) conditional instructions,
    97              i.e., possible conditions of IfThenElse *)
    98 
    99 definition cond_i:Type[0]≝condition.
    100 
    101 let rec cond_i_eq (c1:cond_i) (c2:cond_i):bool ≝
     73inductive seq_i:Type[0]≝ |sAss: variable → expr → seq_i.
     74
     75definition seq_i_eq:seq_i→ seq_i → bool≝λs1,s2:seq_i.
     76match s1 with [
     77sAss v e ⇒ match s2 with [sAss v' e' ⇒ (andb (v==v') (expr_eq e e')) ]
     78].
     79
     80
     81lemma seq_i_eq_elim : ∀P : bool → Prop.∀s1,s2.(s1 = s2 → P true) → (s1 ≠ s2→ P false) → P (seq_i_eq s1 s2).
     82#P * #v #e * #v' #e' #H1 #H2 normalize @(eqb_elim v v')
     83[ #EQ destruct @expr_eq_elim [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H %]
     84| * #H @H2 % #EQ destruct @H %
     85]
     86qed.
     87
     88definition DeqSeqI ≝ mk_DeqSet seq_i seq_i_eq ?.
     89@hide_prf #e1 #e2 @seq_i_eq_elim
     90[ #EQ destruct % // | * #H % #EQ destruct cases H % ]
     91qed.
     92
     93unification hint  0 ≔ ;
     94    X ≟ DeqSeqI
     95(* ---------------------------------------- *) ⊢
     96    seq_i ≡ carr X.
     97
     98(* ambigous input! why?
     99unification hint  0 ≔ p1,p2;
     100    X ≟ DeqSeqI
     101(* ---------------------------------------- *) ⊢
     102    seq_i_eq p1 p2 ≡ eqb X p1 p2.
     103*)
     104
     105
     106let rec cond_i_eq (c1:condition) (c2:condition):bool ≝
    102107match c1 with [Eq e1 e2⇒ match c2 with [Eq f1 f2 ⇒
    103108(andb (expr_eq e1 f1) (expr_eq e2 f2))|_⇒ false]
    104109|Not e⇒ match c2 with [Not f⇒ cond_i_eq e f|_⇒ false]].
    105110
    106   (* technical lemma(s) for cond_i *)
    107 
    108 lemma condition_eq_refl:∀c:condition.cond_i_eq c c=true.
    109 #c elim c [#e #f whd in ⊢ (??%?); >expr_eq_refl >expr_eq_refl %
    110 |#c' normalize * %] qed.
    111 
    112 lemma cond_i_eq_equality:∀c1,c2:condition.cond_i_eq c1 c2=true ↔ c1=c2.
    113 #c1 #c2 % [2: * // ]
    114 lapply c2 -c2 elim c1 [ #e1 #e2 *
    115 [ #f1 #f2 whd in ⊢ (??%? → ?);
    116   inversion(expr_eq e1 f1) [2: #_ normalize #EQ destruct ] #H1
    117   >(proj1 … (expr_eq_equality …) … H1)
    118   inversion(expr_eq e2 f2) [2: #_ normalize #EQ destruct ] #H2 *
    119   >(proj1 … (expr_eq_equality …) … H2) %
    120 | normalize #c #H destruct
    121 ]| #c2 #IH *
    122 [ normalize #e1 #e2 #H destruct
    123 | #c3 #H >(IH … H) % ]]
    124 qed.
    125 
    126   (* cond_i: type of (guards of) loop instructions,
    127              i.e., possible conditions of While *)
    128 
    129 definition loop_i:Type[0]≝condition.
    130 
    131 definition loop_i_eq:loop_i → loop_i → bool ≝cond_i_eq.
    132 
    133 lemma loop_i_eq_equality:∀l1,l2.loop_i_eq l1 l2=true ↔ l1=l2.@cond_i_eq_equality qed.
    134 
    135   (* io_i: type of I/O instructions (none in the language considered) *)
    136 
    137 definition io_i ≝ False.
    138 
    139 definition io_i_eq ≝ λi1,i2:False. true.
    140 
    141 lemma io_i_eq_equality: ∀i1,i2. io_i_eq i1 i2 = true ↔ i1=i2. * qed.
     111lemma cond_i_eq_elim : ∀P : bool → Prop.∀c1,c2.(c1 = c2 → P true) → (c1 ≠c2 → P false) → P (cond_i_eq c1 c2).
     112#P #c1 lapply P -P elim c1 -c1
     113[ #e1 #e2 #P * [ #e1' #e2' | #c' ] #H1 #H2 normalize try (@H2 % #EQ destruct) @expr_eq_elim
     114  [ #EQ destruct @expr_eq_elim [#EQ destruct @H1 % | * #H @H2 % #EQ destruct @H %]
     115  | * #H @H2 % #EQ destruct @H %
     116  ]
     117| #c #IH #P * [ #e1' #e2' | #c' ] #H1 #H2 normalize try (@H2 % #EQ destruct) @IH
     118  [#EQ destruct @H1 % | * #H @H2 % #EQ destruct @H %]
     119]
     120qed.
     121
     122definition DeqCondition ≝ mk_DeqSet condition cond_i_eq ?.
     123@hide_prf #e1 #e2 @cond_i_eq_elim
     124[ #EQ destruct % // | * #H % #EQ destruct cases H % ]
     125qed.
     126
     127unification hint  0 ≔ ;
     128    X ≟ DeqCondition
     129(* ---------------------------------------- *) ⊢
     130    condition ≡ carr X.
     131
     132(* ambigous input!!!
     133unification hint  0 ≔ p1,p2;
     134    X ≟ DeqCondition
     135(* ---------------------------------------- *) ⊢
     136    cond_i_eq p1 p2 ≡ eqb X p1 p2.
     137*)
    142138
    143139  (* syntactical record *)
    144140
    145 definition DeqExpr:DeqSet≝(mk_DeqSet expr expr_eq expr_eq_equality).
    146 
    147 definition imp_instr_params: instr_params ≝ mk_instr_params ? ? ? ? ? ?.
    148 [@(mk_DeqSet seq_i seq_i_eq seq_i_eq_equality)
    149 |@(mk_DeqSet io_i io_i_eq io_i_eq_equality)
    150 |@(mk_DeqSet cond_i cond_i_eq cond_i_eq_equality)
    151 |@(mk_DeqSet loop_i loop_i_eq loop_i_eq_equality)
    152 |@(DeqProd variable DeqExpr)
    153 |@DeqExpr].qed.
    154 
     141definition imp_instr_params: instr_params ≝ mk_instr_params DeqSeqI DeqFalse
     142DeqCondition DeqCondition (DeqProd variable DeqExpr) DeqExpr.
    155143
    156144definition environment ≝ DeqSet_List (DeqProd variable DeqNat).
    157  
    158 definition eq_environment: environment → environment → Prop ≝
    159  λenv1,env2.env1 = env2.
    160145
    161146
     
    246231
    247232
    248 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
    249 [sNop ⇒ Some ? s
    250 |sAss v e ⇒ match s with
     233definition imp_eval_seq:seq_i →store_t→ option store_t
     234≝λi,s.
     235match i with
     236[sAss v e ⇒ match s with
    251237  [nil⇒ None ?
    252238  |cons hd tl⇒ let 〈env,var〉 ≝ hd in
     
    257243
    258244
    259 definition imp_eval_io:(io_instr imp_state_params)→(store_type imp_state_params)→ option (store_type imp_state_params)≝?.
     245definition imp_eval_io: False → store_t→ option store_t≝?.
    260246// qed.
    261247
    262 definition imp_eval_cond_cond:(cond_instr imp_state_params)→ (store_type imp_state_params)→ option (bool × (store_type imp_state_params))≝λc,s.
     248definition imp_eval_cond_cond:condition → store_t→ option (bool × store_t)≝λc,s.
    263249!env ← current_env s;
    264250!b ← sem_condition env c;
     
    266252
    267253
    268 definition imp_eval_loop_cond:(loop_instr imp_state_params)→ (store_type imp_state_params)→ option (bool × (store_type imp_state_params))≝
     254definition imp_eval_loop_cond:condition→ store_t → option (bool × store_t)≝
    269255imp_eval_cond_cond.
    270256
    271 definition imp_init_store: (store_type imp_state_params)≝[〈(nil ?),O〉].
    272 
    273 definition imp_eval_call:(signature imp_state_params imp_state_params)→ act_params_type imp_state_params → store_t → (option store_t)≝
     257definition imp_init_store: store_t≝[〈(nil ?),O〉].
     258
     259definition imp_signature≝signature imp_state_params imp_state_params.
     260
     261definition imp_eval_call:imp_signature→ (variable × expr) → store_t → (option store_t)≝
    274262λsgn,e,st.
    275263  match sgn with
     
    284272  ].
    285273
    286 definition imp_return_call:(return_type imp_state_params)→ store_t→ (option store_t)≝
     274definition imp_return_call:expr→ store_t→ (option store_t)≝
    287275λr,s.match s with
    288276[nil⇒ None ?
     
    293281 
    294282
    295 
    296 
    297283definition imp_sem_state_params : sem_state_params imp_state_params ≝ mk_sem_state_params imp_state_params imp_eval_seq imp_eval_io
    298284imp_eval_cond_cond imp_eval_loop_cond imp_eval_call imp_return_call imp_init_store.
     
    302288definition imp_Instructions≝Instructions imp_state_params flat_labels.
    303289
    304 definition imp_signature≝signature imp_state_params imp_state_params.
    305 
    306 
    307290definition imp_envitem≝ (env_item imp_env_params imp_instr_params flat_labels).
    308 
Note: See TracChangeset for help on using the changeset viewer.