source: LTS/imp.ma @ 3529

Last change on this file since 3529 was 3529, checked in by pellitta, 5 years ago

abitazione tipo instr_params in corso

File size: 20.6 KB
Line 
1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "basics/lists/list.ma".
16include "arithmetics/nat.ma".
17include "basics/bool.ma".
18include "Language.ma".
19
20(* Syntax *)
21
22definition variable ≝ nat.
23axiom label:Type[0].
24
25inductive expr: Type[0] ≝
26   Var: variable → expr
27 | Const: nat → expr
28 | Plus: expr → expr → expr
29 | Minus: expr → expr → expr.
30
31inductive condition: Type[0] ≝
32   Eq: expr → expr → condition
33 | Not: condition → condition.
34 
35inductive seq_i:Type[0]≝sNop: seq_i|sAss: seq_i|sInc: seq_i.
36definition seq_i_eq:seq_i→ seq_i → bool≝λs1,s2:seq_i.match s1 with [
37 sNop ⇒ match s2 with [sNop ⇒ true| _⇒ false]
38|sAss ⇒ match s2 with [sAss ⇒ true| _⇒ false]
39|sInc ⇒ match s2 with [sInc ⇒ true| _⇒ false]
40].
41lemma seq_i_eq_equality:∀s1,s2.seq_i_eq s1 s2=true ↔ s1=s2.#s1 #s2
42cases s1 cases s2 normalize % #H destruct % qed.
43
44inductive io_i:Type[0]≝.
45definition io_i_eq:io_i→ io_i→ bool≝λi1,i2:io_i.true.
46lemma io_i_eq_equality:∀i1,i2.io_i_eq i1 i2=true ↔ i1=i2.#i1 #i2
47cases i1 qed.
48
49let rec neqb n m ≝
50match 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  ].
54axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true ↔ n = m.
55
56definition cond_i:Type[0]≝condition.
57let rec expr_eq (e1:expr) (e2:expr):bool≝
58match e1 with [Var v1⇒ match e2 with [Var v2⇒ neqb v1 v2|_⇒ false]
59|Const v1⇒ match e2 with [Const v2⇒ neqb v1 v2|_⇒ false]
60|Plus le1 re1 ⇒ match e2 with [Plus le2 re2 ⇒ andb (expr_eq le1 le2) (expr_eq re1 re2)|_⇒ false]
61|Minus le1 re1 ⇒ match e2 with [Minus le2 re2 ⇒ andb (expr_eq le1 le2) (expr_eq re1 re2)|_⇒ false]
62].
63let rec cond_i_eq (c1:cond_i) (c2:cond_i):bool ≝
64match c1 with [Eq e1 e2⇒ match c2 with [Eq f1 f2 ⇒
65(andb (expr_eq e1 f1) (expr_eq e2 f2))|_⇒ false]
66|Not e⇒ match c2 with [Not f⇒ cond_i_eq e f|_⇒ false]].
67
68lemma expr_eq_equality:∀e1,e2:expr.expr_eq e1 e2=true ↔e1=e2.
69#e1 #e2 elim e1 elim e2 normalize [#v #v' % #H elim v elim v' normalize in H;
70[%|#v2 #H' destruct
71lemma condition_eq_equality:∀c1,c2:condition.cond_i_eq c1 c2=true ↔ c1=c2.
72#c1 #c2 elim c1 elim c2 [#H1 #H2 #H3 #H4 % #H normalize in H;
73(*
74inductive cond_i:Type[0]≝cIfThenElse: cond_i.
75definition cond_i_eq:cond_i → cond_i → bool ≝λc1,c2:cond_i.true.
76lemma cond_i_eq_equality:∀c1,c2.cond_i_eq c1 c2=true ↔ c1=c2.#c1 #c2
77cases c1 cases c2 % #_ % qed.
78*)
79
80(*
81inductive loop_i:Type[0]≝lWhile: loop_i.
82definition loop_i_eq:loop_i → loop_i → bool ≝λl1,l2:loop_i.true.
83lemma loop_i_eq_equality:∀l1,l2.loop_i_eq l1 l2=true ↔ l1=l2.#l1 #l2
84cases l1 cases l2 % #_ % qed.
85*)
86
87(*
88let rec neqb n m ≝
89match n with
90  [ O ⇒ match m with [ O ⇒ true | S q ⇒ false]
91  | S p ⇒ match m with [ O ⇒ false | S q ⇒ neqb p q]
92  ].
93axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true ↔ n = m.
94*)
95
96definition imp_instr_params: instr_params ≝ mk_instr_params ? ? ? ? ? ?.
97[@(mk_DeqSet seq_i seq_i_eq seq_i_eq_equality)
98|@(mk_DeqSet io_i io_i_eq io_i_eq_equality)
99|@(mk_DeqSet cond_i cond_i_eq cond_i_eq_equality)
100|@(mk_DeqSet loop_i loop_i_eq loop_i_eq_equality)
101|@(mk_DeqSet nat neqb neqb_true_to_eq)
102|@(mk_DeqSet nat neqb neqb_true_to_eq)].qed.
103
104(* | IfThenElse: condition → command → command → command*)
105(* | For: variable → expr → list command → command*)
106inductive command: Type[0] ≝
107   Nop: command
108 | Ass: variable → expr → command
109 | Inc: variable → command
110 | IfThenElse: condition → list command → list command → command
111 | While: condition → list command → command
112 | Call: variable → expr → function → command
113 | Return: expr → command
114with function: Type[0] ≝
115 | Fun: variable → list command → function.
116
117definition program ≝ list command.
118
119(* Big step, operational semantics of expressions and conditions *)
120
121definition environment ≝ variable → nat.
122
123definition eq_environment: environment → environment → Prop ≝
124 λenv1,env2. ∀v. env1 v = env2 v.
125
126definition default_env : environment ≝ λ_.0.
127
128definition assign: environment → variable → nat → environment ≝
129 λenv,v,val,x.
130  match eqb x v with
131   [ true ⇒ val
132   | false ⇒ env x].
133
134definition increment: environment →variable →environment ≝
135 λenv,v,x.
136  match eqb x v with
137   [true ⇒ (env x)+1
138   | false ⇒ env x].
139
140lemma assign_hit: ∀env,v,val. assign env v val v = val.
141 #env #v #val normalize >eqb_n_n normalize %
142qed.
143
144lemma assign_miss: ∀env,v1,v2,val. v1 ≠ v2 → assign env v1 val v2 = env v2.
145 #env #v1 #v2 #val #E normalize >not_eq_to_eqb_false /2/
146qed.
147
148let rec sem_expr (env:environment) (e: expr) on e : nat ≝
149 match e with
150  [ Var v ⇒ env v
151  | Const n ⇒ n
152  | Plus e1 e2 ⇒ sem_expr env e1 + sem_expr env e2
153  | Minus e1 e2 ⇒ sem_expr env e1 - sem_expr env e2 ].
154
155let rec sem_condition (env:environment) (c:condition) on c : bool ≝
156  match c with
157   [ Eq e1 e2 ⇒ eqb (sem_expr env e1) (sem_expr env e2)
158   | Not c ⇒ notb (sem_condition env c) ].
159
160(* Big step, declarative semantics of programs *)
161
162definition status≝variable × (program × environment). (* indirizzo di ritorno, continuazione, ambiente *)
163
164definition stack≝list status.
165
166definition default_stack:stack≝nil ?.
167
168definition push: list status → status → list status ≝
169  λl,s.cons ? s l.
170 
171definition empty: list status → bool≝
172 λl.match l with [nil ⇒ true | _ ⇒ false].
173
174definition peek: list status → status ≝
175 λl.(hd ? l (mk_Prod ? ? 0 (mk_Prod ? ? [ ] default_env))).
176 
177definition pop: list status → list status ≝
178 λl.tail ? l.
179
180definition Geq:expr → expr → condition≝λe1,e2.Eq (Minus e1 e2) (Const 0).
181
182definition Lt:expr → expr → condition≝λe1,e2.Not (Geq e2 e1).
183
184(* | mIfThenElse1:
185   ∀env,st,cond,c1,c2,cont.
186    sem_condition env cond = true →
187    moves ((IfThenElse cond c1 c2)::cont) env st (c1::cont) env st
188 | mIfThenElse2:
189   ∀env,st,cond,c1,c2,cont.
190    sem_condition env cond = false →
191    moves ((IfThenElse cond c1 c2)::cont) env st (c2::cont) env st
192*)
193(* | mFor1:
194    ∀env,st,v,e,l,cont.
195    (sem_condition env (Lt (Var v) e))=true
196       → moves ((For v e l)::cont) env st (l@((Inc v)::(For v e l)::cont)) env st
197 | mFor2:
198    ∀env,st,v,e,l,cont.
199    (sem_condition env (Lt (Var v) e ))=false
200     → moves ((For v e l)::cont) env st cont env st
201*)
202
203inductive moves: list command → environment → stack → list command → environment → stack → Prop ≝
204   mNop: ∀env,st,cont. moves (Nop::cont) env st cont env st
205 | mAss: ∀env,st,v,e,cont.moves ((Ass v e)::cont) env st cont (assign env v (sem_expr env e)) st
206 | mInc: ∀env,st,v,cont.moves ((Inc v)::cont) env st cont (increment env v) st
207 | mIfThenElse1:
208   ∀env,st,cond,l1,l2,cont.
209    sem_condition env cond = true  →
210    moves ((IfThenElse cond l1 l2)::cont) env st (l1@cont) env st
211 | mIfThenElse2:
212   ∀env,st,cond,l1,l2,cont.
213    sem_condition env cond = false →
214    moves ((IfThenElse cond l1 l2)::cont) env st (l2@cont) env st
215 | mWhile1:
216   ∀env,st,cond,l,cont.
217     sem_condition env cond = true →
218     moves ((While cond l)::cont) env st (l@(While cond l)::cont) env st
219 | mWhile2:
220   ∀env,st,cond,l,cont.
221    sem_condition env cond = false →
222    moves ((While cond l)::cont) env st cont env st
223 | mCall:
224    ∀env,st,v,e,cont.∀v',l.
225    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)))
226 | mReturn:
227    ∀env,env',st,v,e,cont,cont'.
228    moves ((Return e)::cont) env ((mk_Prod ? ? v (mk_Prod ? ? cont' env'))::st) ((Ass v e)::cont') env' st.
229
230(* bacato: diverge silentemente nel caso lista vuota *)
231inductive moves_star: list command → environment → stack → list command → environment → stack → Prop ≝
232   ms_done: ∀l,env,stack. moves_star l env stack l env stack
233 | ms_step: ∀l1,env1,stack1,l2,env2,stack2,l3,env3,stack3.
234    moves l1 env1 stack1 l2 env2 stack2 → moves_star l2 env2 stack2 l3 env3 stack3 →
235     moves_star l1 env1 stack1 l3 env3 stack3.
236
237(* corretto anche con lista vuota di sopra *)
238inductive converges: list command → environment → stack → environment → stack → Prop ≝
239   conv_done: ∀l,env,stack,env',stack'.moves l env stack [ ] env' stack' → converges l env stack env' stack'
240 | 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'' →
241    converges l env stack env'' stack''.
242
243(*inductive converges: list command → environment → stack → environment → stack → Prop ≝
244   conv_done: converges [] env stack env stack
245 | conv_step: moves l env stack l' env' stack' → converges l' env' stack ' env'' stack'' →
246    converes l env stack env'' stack''.*)
247
248
249(* Examples *)
250
251example example1:
252 ∃env.
253  moves_star
254   [Ass 0 (Const 2)
255   ;While (Not (Eq (Var 0) (Const 0)))
256       [Ass 0 (Minus (Var 0) (Const 1))
257       ;Ass 1 (Plus (Var 1) (Const 1))]]
258   default_env
259   default_stack
260   (nil ?)
261   env
262   default_stack
263   ∧ eq_environment env (assign default_env 1 2).
264% [2: % [(*@(assign default_env 1 2)|%[2:normalize #v cases v [%|#v' %]|*)
265@(ms_step … (mAss …)) @(ms_step …(mWhile1 …)) [normalize %| @(ms_step …(mAss …)) @(ms_step …(mAss …))
266@(ms_step … (mWhile1 …)) [normalize %| @(ms_step …(mAss …)) @(ms_step …(mAss …))
267@(ms_step … (mWhile2 …)) [normalize % |@(ms_done …) ]]]| normalize #v cases v normalize [%|#p cases p normalize [%|#_ %]]]] skip qed.
268
269(* Big step, declarative semantics of diverging programs *)
270
271(* coinductive types are greatest fixpoints generated by the constructors;
272   they are built starting from the set of all terms and removing at every
273   step all terms that do not start with one of the constructors listed in the
274   coinductive type declaration.
275   
276   Intuitively, they are inhabited by all the terms of the corresponding
277   inductive type and by new ``infinite'' terms obtained by chaining an infinite
278   number of constructors. Intuitively again, their abstract syntax tree is
279   infinite. In practice, however, we will only be able to inhabit coinductive
280   types with either finite terms or with circular terms obtained by co-recursion.
281   
282   Recursion over coinductive types is not allowed, since the recursive functions
283   could diverge on infinite (circular) term. Co-recursion is allowed to create
284   circular terms *)
285coinductive diverges: command → environment → Prop ≝
286   cmIfThenElse1:
287   ∀env,cond,c1,c2.
288    sem_condition env cond = true → diverges c1 env →
289    diverges (IfThenElse cond c1 c2) env
290 | cmIfThenElse2:
291   ∀env,cond,c1,c2.
292    sem_condition env cond = false → diverges c2 env →
293    diverges (IfThenElse cond c1 c2) env
294 | cmIfThenElseList1:
295   ∀env,cond,l1,l2.
296   sem_condition env cond = true → diverges_l l1 env →
297   diverges (IfThenElseList cond l1 l2) env
298 | cmIfThenElseList2:
299   ∀env,cond,l1,l2.
300   sem_condition env cond = false → diverges_l l2 env →
301   diverges (IfThenElseList cond l1 l2) env
302 | cmWhile1:
303   ∀env,cond,l.
304    sem_condition env cond = true → diverges_l l env → diverges (While cond l) env →
305    diverges (While cond l) env
306 | cmWhile2:
307   ∀env,env',cond,l.
308    sem_condition env cond = true → moves_l l env env' → diverges (While cond l) env' →
309    diverges (While cond l) env
310 | cmFor:
311   ∀env,v,e,l.
312    ((sem_condition env (Eq (Minus e (Var v)) (Const 0))))=false → diverges_l l env → diverges (For v e l) env
313with diverges_l: list command → environment → Prop ≝
314   cmCons1:
315    ∀env,env',he,tl.
316     moves he env env' → diverges_l tl env' →
317     diverges_l (he::tl) env
318 | cmCons2:
319    ∀env,he,tl.
320     diverges he env → diverges_l (he::tl) env.
321
322(* Examples *)
323
324(* Here we use co-recursion to provide an infinite (circular) proof that
325   the following term diverges. The env will vary at every iteration, but
326   the value of the first variable will never be changed.
327   
328   Note: a co-recursive function (proof) must be _productive_, i.e. its weak
329   head normal form must start with a constructor. I.e. in a finite number of
330   steps the function must provide a first observation of the infinite term,
331   where observations are identified with constructors. This is the case in
332   the following definition. The exact conditions are omitted. *)
333   
334let corec example_div1' (x:unit) :
335 ∀env. env 0 = 2 →
336 diverges
337    (While (Not (Eq (Var 0) (Const 0)))
338       [Ass 1 (Minus (Var 0) (Const 1))
339       ;Ass 1 (Plus (Var 1) (Const 1))])
340  env ≝ ?.
341#env #H
342                          @cmWhile2 [2: normalize >H % |3:
343@mCons [2:                @mAss | skip |
344@mCons [3: @mNil | skip | @mAss]]| skip |
345@example_div1' // @H
346qed.
347
348example example_div1:
349  diverges_l
350   [Ass 0 (Const 2)
351   ;While (Not (Eq (Var 0) (Const 0)))
352       [Ass 1 (Minus (Var 0) (Const 1))
353       ;Ass 1 (Plus (Var 1) (Const 1))]]
354   default_env.
355@cmCons1 [2:                @mAss | skip]
356@cmCons2                    @example_div1' //
357qed.
358
359(* Small step, continuation style, computational semantics of programs *)
360
361definition status ≝ program × environment.
362
363definition final_environment_is: status → environment → Prop ≝
364 λs,env.
365  match s with
366  [ (*was pair*) mk_Prod l env' ⇒
367    match l with
368    [ nil ⇒ eq_environment env env'
369    | cons _ _ ⇒ False]].
370
371definition step: status → option status ≝
372 λs.
373  match s with
374  [ (*was pair*) mk_Prod p env ⇒
375     match p with
376     [ nil ⇒ None ?
377     | cons he tl ⇒
378        Some …
379         match he with
380         [ Ass v val ⇒ 〈tl, assign env v (sem_expr env val)〉
381         | Inc v ⇒ 〈tl, assign env v (sem_expr env (Plus (Var v) (Const 1)))〉
382         | IfThenElse cond c1 c2 ⇒
383            match sem_condition env cond with
384            [ true ⇒ 〈c1::tl, env〉
385            | false ⇒ 〈c2::tl, env〉]
386         | IfThenElseList cond l1 l2 ⇒
387            match sem_condition env cond with
388            [ true ⇒ 〈l1@tl, env〉
389            | false ⇒ 〈l2@tl, env〉]
390         | While cond l ⇒
391            match sem_condition env cond with
392            [ true ⇒ 〈l@(While cond l)::tl, env〉
393            | false ⇒ 〈tl, env〉]
394         | For v e l ⇒
395            match sem_condition env (Eq (Minus (Var v) e) (Const 0)) with
396            [ true ⇒  〈tl, env〉
397            | false ⇒ 〈l@(Inc v::((For v e l)::tl)), env〉
398            ]           
399            ]]].
400
401let rec steps (s:status) (n:nat) on n : status ≝
402 match n with
403  [ O ⇒ s
404  | S m ⇒
405    match step s with
406    [ None ⇒ s
407    | Some s' ⇒ steps s' m]].
408
409example example2:
410 final_environment_is
411  (steps
412   〈[Ass 0 (Const 2)
413    ;While (Not (Eq (Var 0) (Const 0)))
414        [Ass 0 (Minus (Var 0) (Const 1))
415        ;Ass 1 (Plus (Var 1) (Const 1))]]
416   ,default_env〉
417   20)
418  (assign default_env 1 2).
419 normalize
420 #v cases v normalize // #p cases p //
421qed.
422
423(* Missing from the standard library *)
424
425lemma bool_inv_ind:
426 ∀b:bool. ∀P: bool → Prop. (b=true → P true) → (b=false → P false) → P b.
427 #b #P cases b /2/
428qed.
429
430lemma option_inv_ind:
431 ∀A.∀x:option A. ∀P: option A → Prop.
432  (x=None A → P (None A)) → (∀y. x = Some … y → P (Some … y)) → P x.
433 #A #x #P cases x /2/
434qed.
435
436(* Equivalence of the two semantics on terminating programs *)
437
438lemma moves_l_cons_invert:
439 ∀hd,tl,env,env'.
440  moves_l (hd::tl) env env' →
441   ∃env''. moves hd env env'' ∧ moves_l tl env'' env'.
442 #hd #tl #env #env'
443 lapply (refl … (hd::tl)) generalize in match (hd::tl) in  ⊢ (??%? → %); #l
444 #H1 #H2 cases H2 in H1;
445 [ #env'' #abs destruct
446 | #env1 #env2 #env'' #hd' #tl' #H1 #H2 #E destruct /3/ ]
447qed.
448
449lemma moves_l_append_invert:
450 ∀l1,l2,env,env'.
451  moves_l (l1@l2) env env' →
452   ∃env''. moves_l l1 env env'' ∧ moves_l l2 env'' env'.
453 #l1 elim l1
454 [ /3/
455 | #he #tl #IH #l2 #env #env' #H
456   cases (moves_l_cons_invert … H)
457   #env2 * #H1 #H2 cases (IH … H2) #env3 * /4/ ]
458qed.
459
460lemma commutative_plus:
461∀n,m.n+m=m+n.
462#n #m elim m [normalize //|#m' #IH //]qed.
463
464lemma step_Some_to_moves_l:
465 ∀l,env,p',env',env''.
466  step 〈l,env〉 = Some … 〈p',env'〉 → moves_l p' env' env'' → moves_l l env env''.
467 #l #env #p' #env' #env'' whd in match step; normalize nodelta cases l normalize
468 [ #abs destruct
469 | #he #tl normalize #E destruct -E cases he in e0; normalize nodelta
470   [ #v #e #E destruct /2/
471   | #v #E destruct /2/
472   | #cond #c1 #c2 inversion (sem_condition env cond) normalize
473     #H1 #H2 destruct
474     [ #H2 cases (moves_l_cons_invert … H2) #env2 * /3/
475     | #H2 cases (moves_l_cons_invert … H2) #env2 * /3/ ]
476   | #cond #l1 #l2 inversion (sem_condition env cond) normalize
477     #H1 #H2 destruct
478     [ #H2 cases (moves_l_append_invert … H2) #env2 * /3/
479     | #H2 cases (moves_l_append_invert … H2) #env2 * /3/ ]
480   | #cond #l inversion (sem_condition env cond) normalize
481     #H1 #H2 destruct
482     [ (* entra nel while *) #H2 cases (moves_l_append_invert … H2) #env2 * #H3
483       #H4 cases (moves_l_cons_invert … H4) #env3 * /3/
484     | (* termina il while *) /3/ ]
485     | (* caso For*) #v #e inversion(eqb(env v-sem_expr env e) 0) normalize
486     #INV #l'
487     [ (* sottocaso non entro nel for *)
488      #HD destruct #H2 %2 [@env'|%10 normalize @INV|@H2]
489      |(* sottocaso entro nel for *)
490      #HD destruct #H2 cases (moves_l_append_invert … H2)
491      #env2 * #H3 #H4 cases (moves_l_cons_invert … H4)
492      #env3 *
493     
494      #H5 #H6 destruct cases (moves_l_cons_invert … H6)
495      #env4 * #H7 #H8 destruct %2 [@env4|%9[3:normalize @INV|@env2|4:@H3|@env3
496      |@H5|@H7]|@H8]
497qed.
498     
499theorem steps_to_moves_l:
500 ∀n,l,env,env'. steps 〈l,env〉 n = 〈[],env'〉 → moves_l l env env'.
501 #n elim n
502 [ #l #env #env' #H normalize in H; destruct //
503 | #m #IH #l #env #env' whd in ⊢ (??%? → ?); cases l
504   [ normalize #H destruct //
505   | #he #tl inversion (step 〈he::tl,env〉)
506     [ #abs normalize in abs; destruct
507     | * #l' #env2 #H #K normalize in K; lapply (IH ??? K) /3/ ]]]
508qed.
509
510let rec moves_l_to_steps (l:?) (env:?) (env':?) (H: moves_l l env env') on H :
511 ∃n1.∀n2,tl. steps 〈l@tl,env〉 (n1+n2) = steps 〈tl,env'〉 n2 ≝ ?
512and moves_to_steps (c:?) (env:?) (env':?) (H: moves c env env') on H :
513 ∃n1.∀n2,tl. steps 〈c::tl,env〉 (n1+n2) = steps 〈tl,env'〉 n2 ≝ ?.
514 cases H
515 [ -moves_l_to_steps -moves_to_steps #env %{0} #n2 #tl %
516 | #env1 #env2 #env3 #he #tl #H1 #H2
517   lapply (moves_to_steps … H1) -moves_to_steps * #n1 #K1
518   lapply (moves_l_to_steps … H2) -moves_l_to_steps * #n2 #K2
519   %{(n1+n2)} #n3 #tl >associative_plus >K1 @K2
520
521 | #env1 #v #e %{1} #n #tl %
522 |(* Inc *) #env1 #v %{1} #v' #tl' %
523 | #env1 #env2 #cond #c1 #c2 #E
524   #H lapply (moves_to_steps … H) -moves_to_steps -moves_l_to_steps * #n1 #K
525   %{(S n1)} #n2 #tl normalize >E @K
526 | #env1 #env2 #cond #c1 #c2 #E
527   #H lapply (moves_to_steps … H) -moves_to_steps -moves_l_to_steps * #n1 #K
528   %{(S n1)} #n2 #tl normalize >E @K
529 | (* IfThenElseList *) #env1 #env2 #cond #l1 #l2 #E #H1
530 lapply (moves_l_to_steps … H1) -moves_l_to_steps * #n1 #K1
531 %{(S n1)} #n3 #tl normalize >E normalize >associative_plus >K1 %
532 |#env1 #env2 #cond #l1 #l2 #E #H1
533 lapply (moves_l_to_steps … H1) -moves_l_to_steps * #n1 #K1
534 %{(S n1)} #n3 #tl normalize >E normalize >associative_plus >K1 %
535 | #env1 #env2 #env3 #cond #l #E #H1 #H2
536   lapply (moves_l_to_steps … H1) -moves_l_to_steps * #n1 #K1
537   lapply (moves_to_steps … H2) -moves_to_steps * #n2 #K2
538   %{(S (n1+n2))} #n3 #tl normalize >E normalize >associative_plus >K1 @K2
539 | #env #cond #l #E %{1} #n #tl normalize >E %
540 |(* For *) #env1 #env2 #env3 #env4 #v #e #l #E normalize in E; #HL #HMI #HMF
541 lapply (moves_l_to_steps … HL) -moves_l_to_steps * #n1 #K1
542 
543 lapply (moves_to_steps … HMI) * #n2 #K2
544 lapply (moves_to_steps … HMF) -moves_to_steps * #n3 #K3
545 %{(S(n1+n2+n3))} #n #tl normalize >E normalize >associative_plus >associative_plus
546>K1 >K2 >K3 %
547|#env #v #e #l #E normalize in E; %{1} #n #tl normalize >E normalize %
548 ]
549qed.
Note: See TracBrowser for help on using the repository browser.