Changeset 3560 for LTS


Ignore:
Timestamp:
Jun 16, 2015, 1:24:00 PM (4 years ago)
Author:
piccolo
Message:

language example

Location:
LTS
Files:
4 added
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/imp.ma

    r3559 r3560  
    1919include "basics/finset.ma".
    2020
    21 
    22 
    23 (* Tools *)
    24 
    25 
    26 lemma ifthenelse_elim:∀b,T.∀t:T.if b then t else t=t.
    27 #b #T #t cases b % qed.
    28 
    29 (* use "whd in match (if ? then ? else ?);" instead of these two *)
    30 (* however, whd fails to rewrite in some cases *)
    31 (* to use it on hypothesis H write "whd in match(if ? then ? else ?) in H;" *)
    32 lemma ifthenelse_true:∀T:Type[0].∀t1,t2:T.if true then t1 else t2=t1.
    33 #T #t1 #t2 % qed.
    34 
    35 lemma ifthenelse_false:∀T:Type[0].∀t1,t2:T.if false then t1 else t2=t2.
    36 #T #t1 #t2 % qed.
    37 
    38 lemma ifthenelse_left:∀b,T.∀t1,t2:T.if b then t1 else t2=t1→ (b=true ∨ t1=t2).
    39 #b #T #t1 #t2 cases b #H normalize in H; destruct [%1|%2] % qed.
    40 
    41 lemma ifthenelse_right:∀b,T.∀t1,t2:T.if b then t1 else t2=t2→ (b=false ∨ t1=t2).
    42 #b #T #t1 #t2 cases b #H normalize in H; destruct [%2|%1] % qed.
    43 
    44 (* it does not seem to be useful at all (rewriting does not simplify) *)
    45 lemma ifthenelse_match:∀T:Type[0].∀t1,t2:T.∀b.if b then t1 else t2=match b with [true⇒ t1|false⇒ t2].
    46 #T #t1 #t2 * [>ifthenelse_true|>ifthenelse_false] % qed.
    47 
    48 (* are these two really needed now? *)
    49 lemma ifthenelse_mm:∀b,b':bool.if b then b' else false=true→ b'=true.
    50 #b #b' cases b normalize #H destruct % qed.
    51 
    52 lemma ifthenelse_mm2:∀b,b':bool.if b then b' else false=true→ b=true.
    53 #b #b' cases b normalize #H destruct % qed.
    54 
    55 (* is ex_falso in the standard libary? *)
    56 (*lemma ex_falso_quodlibet:∀P:Prop.False→ P.
    57 #P #F cases F qed.*)
    58 lemma ex_falso_quodlibet:False→ ∀P:Prop.P.
    59 #F cases F qed.
    60 
    61 (* what about this? *)
    62 (*lemma contradiction:∀A:Prop.∀P.P→¬P→ A.
    63 #A #P #H #Hn @(ex_falso_quodlibet ?) @(absurd P H Hn). qed.*)
    64 
    65 lemma contradiction:∀P.P→¬P→ (∀A:Prop.A).
    66 #P #H #Hn #A @(ex_falso_quodlibet (absurd P H Hn)) qed.
    67 
    68 (*
    69 lemma not_true:∀b.(b≠true)→ (b=false).#b cases b #H try(%)
    70 @(contradiction (true=true) (refl …) H) qed.
    71 
    72 lemma not_false:∀b.(b≠false)→ (b=true).#b cases b #H try(%)
    73 @(contradiction (false=false) (refl …) H) qed.
    74 *)
    75 
    76 lemma not_bool:∀b1,b2.(b1≠b2)→ b1=(notb b2).* * normalize #H try(%)
    77 @(contradiction (?=?) (refl …) H) qed.
    78 
    79 lemma neq_bool:∀b1,b2.b1=(notb b2)→(b1≠b2).* * normalize #H /2 by sym_not_eq/ qed.
    80 
    81 lemma eqb_refl:∀T:DeqSet.∀t:T.(t==t)=true.
    82 #T #t @(\b ?) % qed. (* inversion(t==t) #H try(%) lapply(\Pf H) #ABS @(contradiction …) [@(t=t)|@refl|@ABS] qed.*)
    83 
    84 lemma eqb_sym:∀T:DeqSet.∀t1,t2:T.(t1==t2)=(t2==t1).
    85 #T #t1 #t2 inversion(t1==t2) #INV [lapply(\P INV)|lapply(\Pf INV)] #H [>H >eqb_refl %
    86 |inversion(t2==t1) #INV2 [lapply(\P INV2) #ABS destruct @(contradiction ((t1==t1)=true) INV2 ?)
    87 /2 by /|%] qed.
    88 
    89 lemma neq_refl_false:∀T.∀t:T.(t≠t)→ ∀P:Prop.P.
    90 #T #t #H @(contradiction (t=t) (refl …) H) qed.
    91 
    92 lemma neqb_refl_false:∀T:DeqSet.∀t:T.(t==t)=false→ ∀P:Prop.P.
    93 #T #t #ABS @(contradiction ((t==t)=true) (eqb_refl …) ?) @neq_bool whd in match(¬true);
    94 assumption qed.
    95 
    9621(* Syntax *)
    9722
     
    10732   Eq: expr → expr → condition
    10833 | Not: condition → condition.
    109  
    110   (* technical lemmas for expr_eq*)
    11134
    11235let rec expr_eq (e1:expr) (e2:expr):bool≝
     
    14669  (* seq_i: type of sequential instructions *)
    14770
    148 inductive seq_i:Type[0]≝sNop: seq_i|sAss: variable → expr → seq_i|sInc: variable → seq_i.
     71inductive seq_i:Type[0]≝sNop: seq_i|sAss: variable → expr → seq_i.
    14972
    15073definition seq_i_eq:seq_i→ seq_i → bool≝λs1,s2:seq_i.match s1 with [
    15174 sNop ⇒ match s2 with [sNop ⇒ true| _⇒ false]
    15275|sAss v e ⇒ match s2 with [sAss v' e' ⇒ (andb (v==v') (expr_eq e e'))| _⇒ false]
    153 |sInc v ⇒ match s2 with [sInc v' ⇒ (v==v')| _⇒ false]
    15476].
    15577
     
    15880lemma seq_i_eq_refl:∀s.seq_i_eq s s=true.
    15981#s cases s try(#v) try(#e) try %
    160 [ whd in ⊢ (??%?); >(\b (refl … v)) >expr_eq_refl %
    161 |whd in match(seq_i_eq ? ?); /2 by /
    162 (*change with (v==v = true); >(\b ?) %*)] qed.
     82whd in ⊢ (??%?); >(\b (refl … v)) >expr_eq_refl %
     83(*|whd in match(seq_i_eq ? ?); /2 by /*)
     84(*change with (v==v = true); >(\b ?) %*) qed.
    16385
    16486lemma seq_i_eq_equality:∀s1,s2.seq_i_eq s1 s2=true ↔ s1=s2.
    165 #s1 #s2 % [2: * elim s1 [2,3:#v try(#e)] @seq_i_eq_refl
    166 |lapply s2 -s2 elim s1 [2,3:#v] [#e] #s2 cases s2 [2,3,5,6,8,9:#v'] [1,3,5: #e']
     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']
    16789[2,3,4,6,7,8: normalize #H destruct
    16890|1: whd in ⊢ (??%? → ?); inversion (v==v') [2: normalize #_ #H destruct]
    16991 #EQ inversion (expr_eq e e') [2: normalize #_ #H destruct] #H #_
    17092 >(proj1 … (expr_eq_equality …) H) >(\P EQ) %
    171 |5: #H >(\P H) %
    172 | // ]
     93] %
    17394qed.
    17495
     
    229150|@(mk_DeqSet cond_i cond_i_eq cond_i_eq_equality)
    230151|@(mk_DeqSet loop_i loop_i_eq loop_i_eq_equality)
    231 |@DeqExpr
    232 |@(mk_DeqSet expr expr_eq expr_eq_equality)].qed.
    233 
    234           (* | IfThenElse: condition → command → command → command*)
    235           (* | For: variable → expr → list command → command*)
    236 inductive command: Type[0] ≝
    237    Nop: command
    238  | Ass: variable → expr → command
    239  | Inc: variable → command
    240  | IfThenElse: condition → list command → list command → command
    241  | While: condition → list command → command
    242  | Call: variable → expr → function → command
    243  | Return: expr → command
    244 with function: Type[0] ≝
    245  | Fun: variable → list command → function.
    246 
    247 definition program ≝ list command.
    248 
    249 
    250 
    251 (* Big step, operational semantics of expressions and conditions *)
    252 
    253 
    254 definition environment ≝ list (variable × DeqNat).
    255 
    256           (* definition environment ≝ variable → nat. *)
    257 
    258           (* definition eq_environment: environment → environment → Prop ≝
    259  λenv1,env2. ∀v. env1 v = env2 v.*)
     152|@(DeqProd variable DeqExpr)
     153|@DeqExpr].qed.
     154
     155
     156definition environment ≝ DeqSet_List (DeqProd variable DeqNat).
    260157 
    261158definition eq_environment: environment → environment → Prop ≝
    262159 λenv1,env2.env1 = env2.
    263160
    264           (* definition default_env : environment ≝ λ_.0.*)
    265161
    266162definition default_env: environment ≝ nil ?.
    267 
    268           (*
    269           definition assign: environment → variable → nat → environment ≝
    270           λenv,v,val,x.
    271             match eqb x v with
    272              [ true ⇒ val
    273              | false ⇒ env x].
    274           *)
     163 
    275164
    276165let rec assign (env:environment) (v:variable) (n:DeqNat):environment ≝match env with
    277166[nil ⇒ [mk_Prod … v n]
    278 |cons hd tl ⇒ match hd with [(mk_Prod v' n') ⇒ match (v==v') with
    279   [true ⇒ cons … (mk_Prod … v n) tl
    280   |false ⇒ cons … hd (assign tl v n)
    281   ]
    282 ]].
    283 
    284 (*
    285 definition increment: environment →variable →environment ≝
    286  λenv,v,x.
    287   match eqb x v with
    288    [true ⇒ (env x)+1
    289    | false ⇒ env x].
    290 *)
    291 
    292 let rec increment (env:environment) (v:variable):environment ≝match env with
    293 [nil ⇒ nil …
    294 |cons hd tl ⇒ match hd with [(mk_Prod v' n) ⇒ match (v==v') with
    295   [true ⇒ cons … (mk_Prod … v (S n)) tl
    296   |false ⇒ cons … hd (increment tl v)
    297   ]
    298 ]].
     167|cons hd tl ⇒
     168    let 〈v',n'〉≝ hd in if (v==v')
     169                       then 〈v,n〉::tl
     170                       else hd::(assign tl v n)
     171].
    299172
    300173let rec read (env:environment) (v:variable):(option DeqNat)≝match env with
    301174[nil ⇒ None …
    302 |cons hd tl ⇒ match hd with [(mk_Prod v' n) ⇒ match (v==v') with
    303   [true ⇒ Some … n
    304   |false ⇒ read tl v
    305   ]
    306 ]].
    307 
    308 (*
    309 lemma assign_hit: ∀env,v,val. assign env v val v = val.
    310  #env #v #val normalize >(eqb_n_n v) normalize %
    311 qed.
    312 *)
     175|cons hd tl ⇒ let 〈v',n〉≝ hd in
     176  if (v==v')
     177  then Some … n
     178  else read tl v
     179].
     180
    313181
    314182lemma assign_hit: ∀env,v,val. read (assign env v val) v = Some … val.
     
    320188|#v #val whd in match (assign [ ] v val); normalize >(eqb_n_n v) %]qed.
    321189
    322 (*
    323 
    324 [in match t] in [H1:p ... Hn:p] [⊢ p]
    325 
    326 p sono come termini dove ? significa qui no, % qui si' e tutti i nomi vanno usati _
    327 e non puoi usare costanti, costruttori, induttivi, etc.
    328 
    329 la seconda parte del pattern individua un certo numero di posizioni chiamati RADICI;
    330 se viene omessa la seconda parte c'e' una sola radice nella radice del termine
    331 
    332 la prima parte del pattern cerca in ogni radice il sottotermine t e la tattica
    333 lavora su quello
    334 
    335 NOTA BENE: sia f una funzione ricorsiva sul primo argomento e nel goal c'e'
    336 f (S m). Allora whd in match (f ?) identifica (f (S m)) che si riduce.
    337 Mentre whd in match f identifica solo f che NON riduce.
    338 
    339  *)
    340 
    341 (*
    342 lemma assign_miss: ∀env,v1,v2,val. v1 ≠ v2 → assign env v1 val v2 = env v2.
    343  #env #v1 #v2 #val #E normalize >(not_eq_to_eqb_false v2 v1) /2 by refl, not_to_not/
    344 qed.
    345 *)
     190
    346191
    347192lemma assign_miss: ∀env,v1,v2,val. v2 ≠ v1 → (read (assign env v1 val) v2)= (read env v2).
    348193 #env #v1 #v2 #val #E elim env [normalize >(not_eq_to_eqb_false v2 v1) /2 by refl, not_to_not/
    349194|* #v #n #env' #IH inversion(v1==v) #INV [lapply(\P INV)|lapply(\Pf INV)] #K [destruct
    350 whd in match (assign ???); >INV >ifthenelse_true whd in match (read (〈v,n〉::env') v2);
    351 inversion(v2==v) #INV2 >INV2 [>ifthenelse_true|>ifthenelse_false]
    352 whd in match (read (〈v,val〉::env') v2); >INV2 [>ifthenelse_true|>ifthenelse_false]
     195whd in match (assign ???); >INV normalize nodelta whd in match (read (〈v,n〉::env') v2);
     196inversion(v2==v) #INV2 >INV2 normalize nodelta
     197whd in match (read (〈v,val〉::env') v2); >INV2 normalize nodelta
    353198whd in match (read (〈v,n〉::env') v2); try %
    354 lapply (\P INV2) #ABS @ex_falso_quodlibet @(absurd ? ABS E)
     199lapply (\P INV2) #ABS cases(absurd ? ABS E)
    355200(*elim E #ABS2 lapply (ABS2 ABS) #F cases F*)
    356 |whd in match (assign ???); >INV >ifthenelse_false whd in match (read ??);
     201|whd in match (assign ???); >INV normalize nodelta whd in match (read ??);
    357202inversion(v2==v) #INV2 whd in match(if ? then ? else ?);
    358 [whd in match (read ??); >INV2 >ifthenelse_true %
    359 |>IH whd in match (read (〈v,n〉::env') v2);  >INV2 >ifthenelse_false %
     203[whd in match (read ??); >INV2 %
     204|>IH whd in match (read (〈v,n〉::env') v2);  >INV2 %
    360205qed.
    361 
    362 lemma assign_miss2: ∀env,v1,v2,val. v2 ≠ v1 → (read (assign env v1 val) v2)= (read env v2).
    363  #env #v1 #v2 #val #E elim env [whd in match (assign ???); whd in match(read ??);
    364  >(\bf E) >ifthenelse_false %|* #v #n #env' inversion(v==v1) #INV [<(\P INV)
    365  #K whd in match (assign ???); >(\b refl …) whd in match(if ? then ? else ?);
    366  whd in match(read (〈v,n〉::env') v2); inversion(v2==v) #INV2
    367  whd in match(if ? then ? else ?);  whd in match(if ? then ? else ?); whd in match(read ??);
    368 >INV2 try(%) inversion(E) #ABS #ABS2 destruct <(\P INV) in ABS; >(\P INV2) #ABS
    369 @(contradiction (v=v) (refl …) ?) % assumption|lapply (\Pf INV) #K whd in match (assign ???);
    370 whd in match (read (〈v,n〉::env') v2); inversion(v2==v) #INV2 [>ifthenelse_true|>ifthenelse_false]
    371 >(\b INV2) #H whd in match (assign ???); inversion(v1==v) #INV'
    372 [1,3:>ifthenelse_true|2,4:>ifthenelse_false] [2,4: <H whd in match(read ??); [
    373 >eqb_sym in INV; #INV @(contradiction ((v1==v)=true) ? ?) [@INV'|/2 by /]
    374 |>INV2 >ifthenelse_false %]|@(contradiction ((v1==v)=true) ? ?)
    375 [assumption|/2 by /]|whd in match (read ??); >INV2 >ifthenelse_true % qed.
    376206
    377207let rec sem_expr (env:environment) (e: expr) on e : (option nat) ≝
     
    379209  [ Var v ⇒ read env v
    380210  | Const n ⇒ Some ? n
    381   | Plus e1 e2 ⇒ match sem_expr env e1 with [None ⇒ None ?|Some n⇒
    382                  match sem_expr env e2 with [None ⇒ None ?|Some m⇒ Some ? (n+m)]]
    383   | Minus e1 e2 ⇒ match sem_expr env e1 with [None ⇒ None ?|Some n⇒
    384                  match sem_expr env e2 with [None ⇒ None ?|Some m⇒ Some ? (n-m)]]].
    385 
    386 (*
    387 let rec sem_condition (env:environment) (c:condition) on c : bool ≝
    388   match c with
    389    [ Eq e1 e2 ⇒ eqb (sem_expr env e1) (sem_expr env e2)
    390    | Not c ⇒ notb (sem_condition env c) ].
    391 *)
     211  | Plus e1 e2 ⇒ !n1 ← sem_expr env e1;
     212                 !n2 ← sem_expr env e2;
     213                 return (n1+n2)
     214  | Minus e1 e2 ⇒ !n1 ← sem_expr env e1;
     215                  !n2 ← sem_expr env e2;
     216                  return (n1-n2)
     217  ].
    392218
    393219let rec sem_condition (env:environment) (c:condition) on c : option bool ≝
    394220  match c with
    395    [ Eq e1 e2 ⇒ match (sem_expr env e1) with [None ⇒ None ?|Some n⇒
    396                 match (sem_expr env e2) with [None ⇒ None ?|Some m⇒ Some ? (eqb n m)]]
    397    | Not c ⇒ match (sem_condition env c) with [None ⇒ None ?|Some b⇒ Some ? (notb b)]].
     221   [ Eq e1 e2 ⇒ !n ← sem_expr env e1;
     222                !m ← sem_expr env e2;
     223                return (eqb n m)
     224   | Not c ⇒ !b ← sem_condition env c;
     225             return (notb b)
     226   ].
    398227
    399228
     
    401230(*CERCO*)
    402231
    403 
    404232definition imp_env_params:env_params≝mk_env_params variable.
    405233
    406 let rec env_eq (env1:environment) (env2:environment):bool≝match env1 with
    407 [nil ⇒ match env2 with [nil⇒ true|_ ⇒ false]
    408 |cons hd1 tl1 ⇒ match env2 with
    409   [nil⇒ false
    410   |cons hd2 tl2 ⇒ match hd1 with
    411     [mk_Prod v1 n1⇒ match hd2 with
    412        [mk_Prod v2 n2⇒ (andb (andb (v1==v2) (n1==n2)) (env_eq tl1 tl2))]
    413     ]
    414   ]
    415 ].
    416 
    417 lemma env_eq_refl:∀e.env_eq e e=true.
    418 #e elim e [%|* #v #n #e' #IH normalize >(eqb_n_n v) >(eqb_n_n n) >ifthenelse_true @IH] qed.
    419 
    420 lemma env_eq_to_true:∀e1,e2.env_eq e1 e2=true ↔ e1 =e2.
    421 #e1 #e2 % [2:* @env_eq_refl
    422 |lapply e2 -e2 elim e1
    423   [#e2 cases e2 normalize #H try(#K #ABS) destruct %
    424   |* #v #n #e' #IH * normalize in match(env_eq ??);
    425   #p destruct cases p -p #v' #n' #e whd in match(env_eq ??);
    426   inversion(v==v') #INVvv' [2: >ifthenelse_false #ABS destruct|
    427   inversion(n==n') #INVnn' [2: >ifthenelse_false #ABS destruct| normalize
    428   #EQee' >(IH e EQee') >(\P INVnn') >(\P INVvv') % qed. 
    429 
    430 definition DeqEnv:DeqSet≝mk_DeqSet environment env_eq env_eq_to_true.
    431 
    432 definition store_t:Type[0]≝list (DeqEnv ×variable).
    433 
    434 let rec store_eq (s1:store_t) (s2:store_t):bool≝
    435 match s1 with
    436 [nil⇒ match s2 with [nil⇒ true|_⇒ false]
    437 |cons hd1 tl1⇒ match s2 with [nil⇒ false| cons hd2 tl2⇒ (andb (hd1==hd2) (store_eq tl1 tl2))]].
    438 
    439 lemma store_eq_refl:∀s.store_eq s s=true.
    440 #s elim s [%|* #e #v #tl #IH whd in match(store_eq ??); >IH
    441 >(\b (refl …)) %
    442 qed.
    443 
    444 lemma store_eq_equality:∀s1,s2:store_t.store_eq s1 s2=true↔s1=s2.
    445 #s1 #s2 % [2: * @store_eq_refl
    446 |lapply s2 -s2 elim s1
    447 [*
    448   [#_ %
    449   |#p #s2 normalize #ABS destruct
    450   ]
    451 |#p #s2 #IH * whd in match (store_eq ??);
    452   [#ABS destruct
    453   |#p' #s whd in match (store_eq ??); inversion(p==p') #INV
    454     [>ifthenelse_true #H >(IH s H) >(\P INV) %
    455     |>ifthenelse_false #ABS destruct
    456     ]
    457   ]
    458 ] qed.
    459 
    460 (* store is actually a stack of pairs 〈environment, return-variable〉 *)
    461 definition imp_store:DeqSet≝mk_DeqSet store_t store_eq store_eq_equality.
    462 
    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 
    474 
    475 definition current_env:store_type imp_state_params→ option environment≝λs.match s with [nil⇒ None ?
    476 |cons hd tl⇒ match hd with [(mk_Prod env var)⇒ Some ? env]].
     234definition store_t≝ DeqSet_List (DeqProd environment variable).
     235
     236definition imp_state_params:state_params≝
     237mk_state_params imp_instr_params imp_env_params flat_labels store_t (*DeqEnv*).
     238
     239definition current_env:store_type imp_state_params→ option environment≝λs.!hd ← option_hd … s; return \fst hd.
     240
     241definition assign_var ≝ λenv:store_t.λv:variable.λn:DeqNat.
     242match env with
     243[ nil ⇒ None ?
     244| cons hd tl ⇒ let 〈e,var〉 ≝ hd in return (〈assign e v n,var〉 :: tl)
     245].
     246
    477247
    478248definition imp_eval_seq:(seq_instr imp_state_params)→(store_type imp_state_params)→ option (store_type imp_state_params)≝λi,s.match i with
     
    480250|sAss v e ⇒ match s with
    481251  [nil⇒ None ?
    482   |cons hd tl⇒ match hd with
    483     [(mk_Prod env var) ⇒ match (sem_expr env e) with
    484       [None ⇒ None ?
    485       | Some n⇒ Some ? (cons ? (mk_Prod ? ? (assign env v n) var) tl)
    486       ]
    487     ]
     252  |cons hd tl⇒ let 〈env,var〉 ≝ hd in
     253               ! n ← sem_expr env e;
     254               assign_var s v n
    488255  ]
    489 |sInc v ⇒ match s with [nil⇒ None ?|cons hd tl⇒ match hd with [(mk_Prod env var)⇒
    490 match (read env v) with [None ⇒ None ?|Some n⇒ Some ? (cons ? (mk_Prod ? ? (assign env v (S n)) var) tl)]]]
    491 ].
     256].
     257
    492258
    493259definition imp_eval_io:(io_instr imp_state_params)→(store_type imp_state_params)→ option (store_type imp_state_params)≝?.
    494260// qed.
    495261
    496 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
    497 [Eq e1 e2⇒ match (current_env s) with
    498   [None ⇒ None ?
    499   |Some env⇒ match (sem_expr env e1) with
    500     [None⇒ None ?
    501     |Some n ⇒ match (sem_expr env e2) with
    502       [None ⇒ None ?
    503       |Some m ⇒ Some ? (mk_Prod ?? (eqb n m) s)]
     262definition imp_eval_cond_cond:(cond_instr imp_state_params)→ (store_type imp_state_params)→ option (bool × (store_type imp_state_params))≝λc,s.
     263!env ← current_env s;
     264!b ← sem_condition env c;
     265return 〈b,s〉.
     266
     267
     268definition imp_eval_loop_cond:(loop_instr imp_state_params)→ (store_type imp_state_params)→ option (bool × (store_type imp_state_params))≝
     269imp_eval_cond_cond.
     270
     271definition imp_init_store: (store_type imp_state_params)≝[〈(nil ?),O〉].
     272
     273definition imp_eval_call:(signature imp_state_params imp_state_params)→ act_params_type imp_state_params → store_t → (option store_t)≝
     274λsgn,e,st.
     275  match sgn with
     276  [ mk_signature fun fpt rt ⇒
     277    let 〈var,act_exp〉 ≝ e in
     278    match st with
     279    [nil ⇒ None ?
     280    |cons hd tl⇒ let 〈env,v〉≝ hd in
     281                 !n ← sem_expr env act_exp;
     282                 assign_var (〈(nil ?),var〉::st) fpt n
    504283    ]
    505   ]
    506 |Not e ⇒ match (current_env s) with
    507   [None ⇒ None ?
    508   |Some env⇒ match (sem_condition env e) with
    509     [None ⇒ None ?
    510     |Some b ⇒ Some ? (mk_Prod ?? b s)
    511     ]
    512   ]
    513 ].
    514 
    515 (*
    516 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))≝
    517 match c with
    518 [Eq e1 e2⇒ ?
    519 |Not c' ⇒ ?
    520 ].
    521 *)
    522 
    523 
    524 
    525 definition imp_eval_loop_cond:(loop_instr imp_state_params)→ (store_type imp_state_params)→ option (bool × (store_type imp_state_params))≝imp_eval_cond_cond.
    526 (*λl,s.match l with
    527 [lWhile g l⇒ match (sem_condition g) with [None ⇒ None ?|Some b⇒ Some ? (mk_Prod b s)]].*)
    528 
    529 definition imp_eval_call:(signature imp_state_params imp_state_params)→ expr→ imp_store→ (option imp_store)≝
    530 λsgn,e,st.match sgn with [mk_signature fun fpt rt ⇒ match st with
    531   [nil ⇒ None ?
    532   |cons hd tl⇒ match hd with
    533     [mk_Prod env v ⇒ match (sem_expr env e) with
    534       [None ⇒ None ?
    535       |Some n⇒ Some ? (cons ? (mk_Prod … (assign default_env fpt n) v) st)
    536       ]
    537     ]
    538   ]
    539 ].
    540 
    541 definition imp_return_call:(return_type imp_state_params)→ imp_store→ (option imp_store)≝
    542 λr,s.match s with [nil⇒ None ?
    543 |cons hd tl⇒ match hd with
    544   [mk_Prod env v ⇒ match (sem_expr env r) with
    545     [None ⇒ None ?
    546     |Some n⇒ Some ? (cons ? (mk_Prod …(assign env v n) v) tl)
    547     ]
    548   ]
    549 ].
    550 
    551 definition imp_init_store: (store_type imp_state_params)≝(mk_Prod DeqEnv variable (nil ?) O)::(nil ?).
     284  ].
     285
     286definition imp_return_call:(return_type imp_state_params)→ store_t→ (option store_t)≝
     287λr,s.match s with
     288[nil⇒ None ?
     289|cons hd tl⇒ let 〈env,v〉≝ hd in
     290             !n ← sem_expr env r;
     291             assign_var tl v n
     292].
     293 
     294
    552295
    553296
     
    555298imp_eval_cond_cond imp_eval_loop_cond imp_eval_call imp_return_call imp_init_store.
    556299
    557 
    558 
    559 
    560 (* Big step, declarative semantics of programs *)
    561 
    562 definition status≝variable × (program × environment). (* indirizzo di ritorno, continuazione, ambiente *)
    563 
    564 definition stack≝list status.
    565 
    566 definition default_stack:stack≝nil ?.
    567 
    568 definition push: list status → status → list status ≝
    569   λl,s.cons ? s l.
    570  
    571 definition empty: list status → bool≝
    572  λl.match l with [nil ⇒ true | _ ⇒ false].
    573 
    574 definition peek: list status → status ≝
    575  λl.(hd ? l (mk_Prod ? ? 0 (mk_Prod ? ? [ ] default_env))).
    576  
    577 definition pop: list status → list status ≝
    578  λl.tail ? l.
    579 
    580 definition Geq:expr → expr → condition≝λe1,e2.Eq (Minus e1 e2) (Const 0).
    581 
    582 definition Lt:expr → expr → condition≝λe1,e2.Not (Geq e2 e1).
    583 
    584 (* Abitare tipo Program *)
    585 
    586300  (* Abitare tipo Instructions *)
    587301 
    588 definition imp_Instructions≝Instructions imp_state_params.
     302definition imp_Instructions≝Instructions imp_state_params flat_labels.
    589303
    590304definition imp_signature≝signature imp_state_params imp_state_params.
    591305
    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
    603 
    604 (* | mIfThenElse1:
    605    ∀env,st,cond,c1,c2,cont.
    606     sem_condition env cond = true →
    607     moves ((IfThenElse cond c1 c2)::cont) env st (c1::cont) env st
    608  | mIfThenElse2:
    609    ∀env,st,cond,c1,c2,cont.
    610     sem_condition env cond = false →
    611     moves ((IfThenElse cond c1 c2)::cont) env st (c2::cont) env st
    612 *)
    613 (* | mFor1:
    614     ∀env,st,v,e,l,cont.
    615     (sem_condition env (Lt (Var v) e))=true
    616        → moves ((For v e l)::cont) env st (l@((Inc v)::(For v e l)::cont)) env st
    617  | mFor2:
    618     ∀env,st,v,e,l,cont.
    619     (sem_condition env (Lt (Var v) e ))=false
    620      → moves ((For v e l)::cont) env st cont env st
    621 *)
    622 
    623 inductive moves: list command → environment → stack → list command → environment → stack → Prop ≝
    624    mNop: ∀env,st,cont. moves (Nop::cont) env st cont env st
    625  | mAss: ∀env,st,v,e,cont.moves ((Ass v e)::cont) env st cont (assign env v (sem_expr env e)) st
    626  | mInc: ∀env,st,v,cont.moves ((Inc v)::cont) env st cont (increment env v) st
    627  | mIfThenElse1:
    628    ∀env,st,cond,l1,l2,cont.
    629     sem_condition env cond = true  →
    630     moves ((IfThenElse cond l1 l2)::cont) env st (l1@cont) env st
    631  | mIfThenElse2:
    632    ∀env,st,cond,l1,l2,cont.
    633     sem_condition env cond = false →
    634     moves ((IfThenElse cond l1 l2)::cont) env st (l2@cont) env st
    635  | mWhile1:
    636    ∀env,st,cond,l,cont.
    637      sem_condition env cond = true →
    638      moves ((While cond l)::cont) env st (l@(While cond l)::cont) env st
    639  | mWhile2:
    640    ∀env,st,cond,l,cont.
    641     sem_condition env cond = false →
    642     moves ((While cond l)::cont) env st cont env st
    643  | mCall:
    644     ∀env,st,v,e,cont.∀v',l.
    645     moves ((Call v e (Fun v' l))::cont) env st l (assign default_env v' (sem_expr env e)) (push st (mk_Prod ? ? v (mk_Prod ? ? cont env)))
    646  | mReturn:
    647     ∀env,env',st,v,e,cont,cont'.
    648     moves ((Return e)::cont) env ((mk_Prod ? ? v (mk_Prod ? ? cont' env'))::st) ((Ass v e)::cont') env' st.
    649 
    650 (* bacato: diverge silentemente nel caso lista vuota *)
    651 inductive moves_star: list command → environment → stack → list command → environment → stack → Prop ≝
    652    ms_done: ∀l,env,stack. moves_star l env stack l env stack
    653  | ms_step: ∀l1,env1,stack1,l2,env2,stack2,l3,env3,stack3.
    654     moves l1 env1 stack1 l2 env2 stack2 → moves_star l2 env2 stack2 l3 env3 stack3 →
    655      moves_star l1 env1 stack1 l3 env3 stack3.
    656 
    657 (* corretto anche con lista vuota di sopra *)
    658 inductive converges: list command → environment → stack → environment → stack → Prop ≝
    659    conv_done: ∀l,env,stack,env',stack'.moves l env stack [ ] env' stack' → converges l env stack env' stack'
    660  | conv_step: ∀l,hd,tl,env,stack,env',stack',env'',stack''.moves l env stack (hd::tl) env' stack' → converges (hd::tl) env' stack' env'' stack'' →
    661     converges l env stack env'' stack''.
    662 
    663 (*inductive converges: list command → environment → stack → environment → stack → Prop ≝
    664    conv_done: converges [] env stack env stack
    665  | conv_step: moves l env stack l' env' stack' → converges l' env' stack ' env'' stack'' →
    666     converes l env stack env'' stack''.*)
    667 
    668 
    669 (* Examples *)
    670 
    671 example example1:
    672  ∃env.
    673   moves_star
    674    [Ass 0 (Const 2)
    675    ;While (Not (Eq (Var 0) (Const 0)))
    676        [Ass 0 (Minus (Var 0) (Const 1))
    677        ;Ass 1 (Plus (Var 1) (Const 1))]]
    678    default_env
    679    default_stack
    680    (nil ?)
    681    env
    682    default_stack
    683    ∧ eq_environment env (assign default_env 1 2).
    684 % [2: % [(*@(assign default_env 1 2)|%[2:normalize #v cases v [%|#v' %]|*)
    685 @(ms_step … (mAss …)) @(ms_step …(mWhile1 …)) [normalize %| @(ms_step …(mAss …)) @(ms_step …(mAss …))
    686 @(ms_step … (mWhile1 …)) [normalize %| @(ms_step …(mAss …)) @(ms_step …(mAss …))
    687 @(ms_step … (mWhile2 …)) [normalize % |@(ms_done …) ]]]| normalize #v cases v normalize [%|#p cases p normalize [%|#_ %]]]] skip qed.
    688 
    689 (* Big step, declarative semantics of diverging programs *)
    690 
    691 (* coinductive types are greatest fixpoints generated by the constructors;
    692    they are built starting from the set of all terms and removing at every
    693    step all terms that do not start with one of the constructors listed in the
    694    coinductive type declaration.
    695    
    696    Intuitively, they are inhabited by all the terms of the corresponding
    697    inductive type and by new ``infinite'' terms obtained by chaining an infinite
    698    number of constructors. Intuitively again, their abstract syntax tree is
    699    infinite. In practice, however, we will only be able to inhabit coinductive
    700    types with either finite terms or with circular terms obtained by co-recursion.
    701    
    702    Recursion over coinductive types is not allowed, since the recursive functions
    703    could diverge on infinite (circular) term. Co-recursion is allowed to create
    704    circular terms *)
    705 coinductive diverges: command → environment → Prop ≝
    706    cmIfThenElse1:
    707    ∀env,cond,c1,c2.
    708     sem_condition env cond = true → diverges c1 env →
    709     diverges (IfThenElse cond c1 c2) env
    710  | cmIfThenElse2:
    711    ∀env,cond,c1,c2.
    712     sem_condition env cond = false → diverges c2 env →
    713     diverges (IfThenElse cond c1 c2) env
    714  | cmIfThenElseList1:
    715    ∀env,cond,l1,l2.
    716    sem_condition env cond = true → diverges_l l1 env →
    717    diverges (IfThenElseList cond l1 l2) env
    718  | cmIfThenElseList2:
    719    ∀env,cond,l1,l2.
    720    sem_condition env cond = false → diverges_l l2 env →
    721    diverges (IfThenElseList cond l1 l2) env
    722  | cmWhile1:
    723    ∀env,cond,l.
    724     sem_condition env cond = true → diverges_l l env → diverges (While cond l) env →
    725     diverges (While cond l) env
    726  | cmWhile2:
    727    ∀env,env',cond,l.
    728     sem_condition env cond = true → moves_l l env env' → diverges (While cond l) env' →
    729     diverges (While cond l) env
    730  | cmFor:
    731    ∀env,v,e,l.
    732     ((sem_condition env (Eq (Minus e (Var v)) (Const 0))))=false → diverges_l l env → diverges (For v e l) env
    733 with diverges_l: list command → environment → Prop ≝
    734    cmCons1:
    735     ∀env,env',he,tl.
    736      moves he env env' → diverges_l tl env' →
    737      diverges_l (he::tl) env
    738  | cmCons2:
    739     ∀env,he,tl.
    740      diverges he env → diverges_l (he::tl) env.
    741 
    742 (* Examples *)
    743 
    744 (* Here we use co-recursion to provide an infinite (circular) proof that
    745    the following term diverges. The env will vary at every iteration, but
    746    the value of the first variable will never be changed.
    747    
    748    Note: a co-recursive function (proof) must be _productive_, i.e. its weak
    749    head normal form must start with a constructor. I.e. in a finite number of
    750    steps the function must provide a first observation of the infinite term,
    751    where observations are identified with constructors. This is the case in
    752    the following definition. The exact conditions are omitted. *)
    753    
    754 let corec example_div1' (x:unit) :
    755  ∀env. env 0 = 2 →
    756  diverges
    757     (While (Not (Eq (Var 0) (Const 0)))
    758        [Ass 1 (Minus (Var 0) (Const 1))
    759        ;Ass 1 (Plus (Var 1) (Const 1))])
    760   env ≝ ?.
    761 #env #H
    762                           @cmWhile2 [2: normalize >H % |3:
    763 @mCons [2:                @mAss | skip |
    764 @mCons [3: @mNil | skip | @mAss]]| skip |
    765 @example_div1' // @H
    766 qed.
    767 
    768 example example_div1:
    769   diverges_l
    770    [Ass 0 (Const 2)
    771    ;While (Not (Eq (Var 0) (Const 0)))
    772        [Ass 1 (Minus (Var 0) (Const 1))
    773        ;Ass 1 (Plus (Var 1) (Const 1))]]
    774    default_env.
    775 @cmCons1 [2:                @mAss | skip]
    776 @cmCons2                    @example_div1' //
    777 qed.
    778 
    779 (* Small step, continuation style, computational semantics of programs *)
    780 
    781 definition status ≝ program × environment.
    782 
    783 definition final_environment_is: status → environment → Prop ≝
    784  λs,env.
    785   match s with
    786   [ (*was pair*) mk_Prod l env' ⇒
    787     match l with
    788     [ nil ⇒ eq_environment env env'
    789     | cons _ _ ⇒ False]].
    790 
    791 definition step: status → option status ≝
    792  λs.
    793   match s with
    794   [ (*was pair*) mk_Prod p env ⇒
    795      match p with
    796      [ nil ⇒ None ?
    797      | cons he tl ⇒
    798         Some …
    799          match he with
    800          [ Ass v val ⇒ 〈tl, assign env v (sem_expr env val)〉
    801          | Inc v ⇒ 〈tl, assign env v (sem_expr env (Plus (Var v) (Const 1)))〉
    802          | IfThenElse cond c1 c2 ⇒
    803             match sem_condition env cond with
    804             [ true ⇒ 〈c1::tl, env〉
    805             | false ⇒ 〈c2::tl, env〉]
    806          | IfThenElseList cond l1 l2 ⇒
    807             match sem_condition env cond with
    808             [ true ⇒ 〈l1@tl, env〉
    809             | false ⇒ 〈l2@tl, env〉]
    810          | While cond l ⇒
    811             match sem_condition env cond with
    812             [ true ⇒ 〈l@(While cond l)::tl, env〉
    813             | false ⇒ 〈tl, env〉]
    814          | For v e l ⇒
    815             match sem_condition env (Eq (Minus (Var v) e) (Const 0)) with
    816             [ true ⇒  〈tl, env〉
    817             | false ⇒ 〈l@(Inc v::((For v e l)::tl)), env〉
    818             ]           
    819             ]]].
    820 
    821 let rec steps (s:status) (n:nat) on n : status ≝
    822  match n with
    823   [ O ⇒ s
    824   | S m ⇒
    825     match step s with
    826     [ None ⇒ s
    827     | Some s' ⇒ steps s' m]].
    828 
    829 example example2:
    830  final_environment_is
    831   (steps
    832    〈[Ass 0 (Const 2)
    833     ;While (Not (Eq (Var 0) (Const 0)))
    834         [Ass 0 (Minus (Var 0) (Const 1))
    835         ;Ass 1 (Plus (Var 1) (Const 1))]]
    836    ,default_env〉
    837    20)
    838   (assign default_env 1 2).
    839  normalize
    840  #v cases v normalize // #p cases p //
    841 qed.
    842 
    843 (* Missing from the standard library *)
    844 
    845 lemma bool_inv_ind:
    846  ∀b:bool. ∀P: bool → Prop. (b=true → P true) → (b=false → P false) → P b.
    847  #b #P cases b /2/
    848 qed.
    849 
    850 lemma option_inv_ind:
    851  ∀A.∀x:option A. ∀P: option A → Prop.
    852   (x=None A → P (None A)) → (∀y. x = Some … y → P (Some … y)) → P x.
    853  #A #x #P cases x /2/
    854 qed.
    855 
    856 (* Equivalence of the two semantics on terminating programs *)
    857 
    858 lemma moves_l_cons_invert:
    859  ∀hd,tl,env,env'.
    860   moves_l (hd::tl) env env' →
    861    ∃env''. moves hd env env'' ∧ moves_l tl env'' env'.
    862  #hd #tl #env #env'
    863  lapply (refl … (hd::tl)) generalize in match (hd::tl) in  ⊢ (??%? → %); #l
    864  #H1 #H2 cases H2 in H1;
    865  [ #env'' #abs destruct
    866  | #env1 #env2 #env'' #hd' #tl' #H1 #H2 #E destruct /3/ ]
    867 qed.
    868 
    869 lemma moves_l_append_invert:
    870  ∀l1,l2,env,env'.
    871   moves_l (l1@l2) env env' →
    872    ∃env''. moves_l l1 env env'' ∧ moves_l l2 env'' env'.
    873  #l1 elim l1
    874  [ /3/
    875  | #he #tl #IH #l2 #env #env' #H
    876    cases (moves_l_cons_invert … H)
    877    #env2 * #H1 #H2 cases (IH … H2) #env3 * /4/ ]
    878 qed.
    879 
    880 lemma commutative_plus:
    881 ∀n,m.n+m=m+n.
    882 #n #m elim m [normalize //|#m' #IH //]qed.
    883 
    884 lemma step_Some_to_moves_l:
    885  ∀l,env,p',env',env''.
    886   step 〈l,env〉 = Some … 〈p',env'〉 → moves_l p' env' env'' → moves_l l env env''.
    887  #l #env #p' #env' #env'' whd in match step; normalize nodelta cases l normalize
    888  [ #abs destruct
    889  | #he #tl normalize #E destruct -E cases he in e0; normalize nodelta
    890    [ #v #e #E destruct /2/
    891    | #v #E destruct /2/
    892    | #cond #c1 #c2 inversion (sem_condition env cond) normalize
    893      #H1 #H2 destruct
    894      [ #H2 cases (moves_l_cons_invert … H2) #env2 * /3/
    895      | #H2 cases (moves_l_cons_invert … H2) #env2 * /3/ ]
    896    | #cond #l1 #l2 inversion (sem_condition env cond) normalize
    897      #H1 #H2 destruct
    898      [ #H2 cases (moves_l_append_invert … H2) #env2 * /3/
    899      | #H2 cases (moves_l_append_invert … H2) #env2 * /3/ ]
    900    | #cond #l inversion (sem_condition env cond) normalize
    901      #H1 #H2 destruct
    902      [ (* entra nel while *) #H2 cases (moves_l_append_invert … H2) #env2 * #H3
    903        #H4 cases (moves_l_cons_invert … H4) #env3 * /3/
    904      | (* termina il while *) /3/ ]
    905      | (* caso For*) #v #e inversion(eqb(env v-sem_expr env e) 0) normalize
    906      #INV #l'
    907      [ (* sottocaso non entro nel for *)
    908       #HD destruct #H2 %2 [@env'|%10 normalize @INV|@H2]
    909       |(* sottocaso entro nel for *)
    910       #HD destruct #H2 cases (moves_l_append_invert … H2)
    911       #env2 * #H3 #H4 cases (moves_l_cons_invert … H4)
    912       #env3 *
    913      
    914       #H5 #H6 destruct cases (moves_l_cons_invert … H6)
    915       #env4 * #H7 #H8 destruct %2 [@env4|%9[3:normalize @INV|@env2|4:@H3|@env3
    916       |@H5|@H7]|@H8]
    917 qed.
    918      
    919 theorem steps_to_moves_l:
    920  ∀n,l,env,env'. steps 〈l,env〉 n = 〈[],env'〉 → moves_l l env env'.
    921  #n elim n
    922  [ #l #env #env' #H normalize in H; destruct //
    923  | #m #IH #l #env #env' whd in ⊢ (??%? → ?); cases l
    924    [ normalize #H destruct //
    925    | #he #tl inversion (step 〈he::tl,env〉)
    926      [ #abs normalize in abs; destruct
    927      | * #l' #env2 #H #K normalize in K; lapply (IH ??? K) /3/ ]]]
    928 qed.
    929 
    930 let rec moves_l_to_steps (l:?) (env:?) (env':?) (H: moves_l l env env') on H :
    931  ∃n1.∀n2,tl. steps 〈l@tl,env〉 (n1+n2) = steps 〈tl,env'〉 n2 ≝ ?
    932 and moves_to_steps (c:?) (env:?) (env':?) (H: moves c env env') on H :
    933  ∃n1.∀n2,tl. steps 〈c::tl,env〉 (n1+n2) = steps 〈tl,env'〉 n2 ≝ ?.
    934  cases H
    935  [ -moves_l_to_steps -moves_to_steps #env %{0} #n2 #tl %
    936  | #env1 #env2 #env3 #he #tl #H1 #H2
    937    lapply (moves_to_steps … H1) -moves_to_steps * #n1 #K1
    938    lapply (moves_l_to_steps … H2) -moves_l_to_steps * #n2 #K2
    939    %{(n1+n2)} #n3 #tl >associative_plus >K1 @K2
    940 
    941  | #env1 #v #e %{1} #n #tl %
    942  |(* Inc *) #env1 #v %{1} #v' #tl' %
    943  | #env1 #env2 #cond #c1 #c2 #E
    944    #H lapply (moves_to_steps … H) -moves_to_steps -moves_l_to_steps * #n1 #K
    945    %{(S n1)} #n2 #tl normalize >E @K
    946  | #env1 #env2 #cond #c1 #c2 #E
    947    #H lapply (moves_to_steps … H) -moves_to_steps -moves_l_to_steps * #n1 #K
    948    %{(S n1)} #n2 #tl normalize >E @K
    949  | (* IfThenElseList *) #env1 #env2 #cond #l1 #l2 #E #H1
    950  lapply (moves_l_to_steps … H1) -moves_l_to_steps * #n1 #K1
    951  %{(S n1)} #n3 #tl normalize >E normalize >associative_plus >K1 %
    952  |#env1 #env2 #cond #l1 #l2 #E #H1
    953  lapply (moves_l_to_steps … H1) -moves_l_to_steps * #n1 #K1
    954  %{(S n1)} #n3 #tl normalize >E normalize >associative_plus >K1 %
    955  | #env1 #env2 #env3 #cond #l #E #H1 #H2
    956    lapply (moves_l_to_steps … H1) -moves_l_to_steps * #n1 #K1
    957    lapply (moves_to_steps … H2) -moves_to_steps * #n2 #K2
    958    %{(S (n1+n2))} #n3 #tl normalize >E normalize >associative_plus >K1 @K2
    959  | #env #cond #l #E %{1} #n #tl normalize >E %
    960  |(* For *) #env1 #env2 #env3 #env4 #v #e #l #E normalize in E; #HL #HMI #HMF
    961  lapply (moves_l_to_steps … HL) -moves_l_to_steps * #n1 #K1
    962  
    963  lapply (moves_to_steps … HMI) * #n2 #K2
    964  lapply (moves_to_steps … HMF) -moves_to_steps * #n3 #K3
    965  %{(S(n1+n2+n3))} #n #tl normalize >E normalize >associative_plus >associative_plus
    966 >K1 >K2 >K3 %
    967 |#env #v #e #l #E normalize in E; %{1} #n #tl normalize >E normalize %
    968  ]
    969 qed.
     306
     307definition imp_envitem≝ (env_item imp_env_params imp_instr_params flat_labels).
     308
Note: See TracChangeset for help on using the changeset viewer.