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 | |
---|
15 | include "basics/lists/list.ma". |
---|
16 | include "arithmetics/nat.ma". |
---|
17 | include "basics/bool.ma". |
---|
18 | include "Language.ma". |
---|
19 | include "basics/finset.ma". |
---|
20 | |
---|
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 | lemma ifthenelse_true:∀T:Type[0].∀t1,t2:T.if true then t1 else t2=t1. |
---|
30 | #T #t1 #t2 % qed. |
---|
31 | |
---|
32 | lemma ifthenelse_false:∀T:Type[0].∀t1,t2:T.if false then t1 else t2=t2. |
---|
33 | #T #t1 #t2 % qed. |
---|
34 | |
---|
35 | lemma ifthenelse_left:∀b,T.∀t1,t2:T.if b then t1 else t2=t1→ (b=true ∨ t1=t2). |
---|
36 | #b #T #t1 #t2 cases b #H normalize in H; destruct [%1|%2] % qed. |
---|
37 | |
---|
38 | lemma ifthenelse_right:∀b,T.∀t1,t2:T.if b then t1 else t2=t2→ (b=false ∨ t1=t2). |
---|
39 | #b #T #t1 #t2 cases b #H normalize in H; destruct [%2|%1] % qed. |
---|
40 | |
---|
41 | lemma ifthenelse_mm:∀b,b':bool.if b then b' else false=true→ b'=true. |
---|
42 | #b #b' cases b normalize #H destruct % qed. |
---|
43 | |
---|
44 | lemma ifthenelse_mm2:∀b,b':bool.if b then b' else false=true→ b=true. |
---|
45 | #b #b' cases b normalize #H destruct % qed. |
---|
46 | |
---|
47 | |
---|
48 | |
---|
49 | (* Syntax *) |
---|
50 | |
---|
51 | |
---|
52 | definition variable ≝ DeqNat. |
---|
53 | |
---|
54 | inductive expr: Type[0] ≝ |
---|
55 | Var: variable → expr |
---|
56 | | Const: DeqNat → expr |
---|
57 | | Plus: expr → expr → expr |
---|
58 | | Minus: expr → expr → expr. |
---|
59 | |
---|
60 | inductive condition: Type[0] ≝ |
---|
61 | Eq: expr → expr → condition |
---|
62 | | Not: condition → condition. |
---|
63 | |
---|
64 | (* technical lemmas for expr_eq*) |
---|
65 | |
---|
66 | let rec expr_eq (e1:expr) (e2:expr):bool≝ |
---|
67 | match e1 with [Var v1⇒ match e2 with [Var v2⇒ v1==v2|_⇒ false] |
---|
68 | |Const v1⇒ match e2 with [Const v2⇒ v1==v2|_⇒ false] |
---|
69 | |Plus le1 re1 ⇒ match e2 with [Plus le2 re2 ⇒ andb (expr_eq le1 le2) (expr_eq re1 re2)|_⇒ false] |
---|
70 | |Minus le1 re1 ⇒ match e2 with [Minus le2 re2 ⇒ andb (expr_eq le1 le2) (expr_eq re1 re2)|_⇒ false] |
---|
71 | ]. |
---|
72 | |
---|
73 | lemma expr_eq_refl:∀e:expr.expr_eq e e=true. |
---|
74 | #e elim e [1,2: #v change with (v==v = true); @(\b ?) % |
---|
75 | |3,4: #f1 #f2 normalize #H1 >H1 #H2 >H2 %]qed. |
---|
76 | |
---|
77 | (* the predicate expr_eq corresponds to syntactical equality on the type expr *) |
---|
78 | |
---|
79 | lemma expr_eq_equality:∀e1,e2:expr.expr_eq e1 e2=true ↔ e1=e2. |
---|
80 | #e1 #e2 % [2:* lapply e2 -e2 elim e1 |
---|
81 | [1,2:#n #_ change with (n==n = true) @(\b ?) % |
---|
82 | |3,4:#f1 #f2 #H1 #H2 #e2 @expr_eq_refl] |
---|
83 | |lapply e2 -e2 elim e1 |
---|
84 | [1,2: #v1 #e2 cases e2 |
---|
85 | [1,6: #v2 #H >(\P H) % |
---|
86 | |2,5: #v2 #H normalize in H; destruct |
---|
87 | |3,4,7,8: #e #f normalize #ABS destruct] |
---|
88 | |3,4: #e #e2 #H #K #f cases f |
---|
89 | [1,2,5,6: #v2 normalize #ABS destruct |
---|
90 | |3,4,7,8:#f1 #f2 normalize inversion(expr_eq e f1) #INV1 >INV1 inversion(expr_eq e2 f2) |
---|
91 | #INV2 >INV2 normalize #T destruct >(H ? INV1) >(K ? INV2) % qed. |
---|
92 | |
---|
93 | |
---|
94 | |
---|
95 | |
---|
96 | (* for the syntactical record in Language.ma *) |
---|
97 | |
---|
98 | |
---|
99 | (* seq_i: type of sequential instructions *) |
---|
100 | |
---|
101 | inductive seq_i:Type[0]≝sNop: seq_i|sAss: variable → expr → seq_i|sInc: variable → seq_i. |
---|
102 | |
---|
103 | definition seq_i_eq:seq_i→ seq_i → bool≝λs1,s2:seq_i.match s1 with [ |
---|
104 | sNop ⇒ match s2 with [sNop ⇒ true| _⇒ false] |
---|
105 | |sAss v e ⇒ match s2 with [sAss v' e' ⇒ (andb (v==v') (expr_eq e e'))| _⇒ false] |
---|
106 | |sInc v ⇒ match s2 with [sInc v' ⇒ (v==v')| _⇒ false] |
---|
107 | ]. |
---|
108 | |
---|
109 | (* technical lemma(s) for seq_i_eq *) |
---|
110 | |
---|
111 | lemma seq_i_eq_refl:∀s.seq_i_eq s s=true. |
---|
112 | #s cases s try(#v) try(#e) try % |
---|
113 | [ whd in ⊢ (??%?); >(\b (refl … v)) >expr_eq_refl % |
---|
114 | | change with (v==v = true); >(\b ?) %] qed. |
---|
115 | |
---|
116 | lemma seq_i_eq_equality:∀s1,s2.seq_i_eq s1 s2=true ↔ s1=s2. |
---|
117 | #s1 #s2 % [2: * elim s1 [2,3:#v try(#e)] @seq_i_eq_refl |
---|
118 | |lapply s2 -s2 elim s1 [2,3:#v] [#e] #s2 cases s2 [2,3,5,6,8,9:#v'] [1,3,5: #e'] |
---|
119 | [2,3,4,6,7,8: normalize #H destruct |
---|
120 | |1: whd in ⊢ (??%? → ?); inversion (v==v') [2: normalize #_ #H destruct] |
---|
121 | #EQ inversion (expr_eq e e') [2: normalize #_ #H destruct] #H #_ |
---|
122 | >(proj1 … (expr_eq_equality …) H) >(\P EQ) % |
---|
123 | |5: #H >(\P H) % |
---|
124 | | // ] |
---|
125 | qed. |
---|
126 | |
---|
127 | (* cond_i: type of (guards of) conditional instructions, |
---|
128 | i.e., possible conditions of IfThenElse *) |
---|
129 | |
---|
130 | definition cond_i:Type[0]≝condition. |
---|
131 | |
---|
132 | let rec cond_i_eq (c1:cond_i) (c2:cond_i):bool ≝ |
---|
133 | match c1 with [Eq e1 e2⇒ match c2 with [Eq f1 f2 ⇒ |
---|
134 | (andb (expr_eq e1 f1) (expr_eq e2 f2))|_⇒ false] |
---|
135 | |Not e⇒ match c2 with [Not f⇒ cond_i_eq e f|_⇒ false]]. |
---|
136 | |
---|
137 | (* technical lemma(s) for cond_i *) |
---|
138 | |
---|
139 | lemma condition_eq_refl:∀c:condition.cond_i_eq c c=true. |
---|
140 | #c elim c [#e #f whd in ⊢ (??%?); >expr_eq_refl >expr_eq_refl normalize % |
---|
141 | |#c' normalize * %] qed. |
---|
142 | |
---|
143 | lemma cond_i_eq_equality:∀c1,c2:condition.cond_i_eq c1 c2=true ↔ c1=c2. |
---|
144 | #c1 #c2 % [2: * // ] |
---|
145 | lapply c2 -c2 elim c1 [ #e1 #e2 * |
---|
146 | [ #f1 #f2 whd in ⊢ (??%? → ?); |
---|
147 | inversion(expr_eq e1 f1) [2: #_ normalize #EQ destruct ] #H1 |
---|
148 | >(proj1 … (expr_eq_equality …) … H1) |
---|
149 | inversion(expr_eq e2 f2) [2: #_ normalize #EQ destruct ] #H2 #_ |
---|
150 | >(proj1 … (expr_eq_equality …) … H2) % |
---|
151 | | normalize #c #H destruct |
---|
152 | ]| #c2 #IH * |
---|
153 | [ normalize #e1 #e2 #H destruct |
---|
154 | | #c3 #H >(IH … H) % ]] |
---|
155 | qed. |
---|
156 | |
---|
157 | (* cond_i: type of (guards of) loop instructions, |
---|
158 | i.e., possible conditions of While *) |
---|
159 | |
---|
160 | definition loop_i:Type[0]≝condition. |
---|
161 | |
---|
162 | definition loop_i_eq:loop_i → loop_i → bool ≝cond_i_eq. |
---|
163 | |
---|
164 | lemma loop_i_eq_equality:∀l1,l2.loop_i_eq l1 l2=true ↔ l1=l2.@cond_i_eq_equality qed. |
---|
165 | |
---|
166 | (* io_i: type of I/O instructions (none in the language considered) *) |
---|
167 | |
---|
168 | definition io_i ≝ False. |
---|
169 | |
---|
170 | definition io_i_eq ≝ λi1,i2:False. true. |
---|
171 | |
---|
172 | lemma io_i_eq_equality: ∀i1,i2. io_i_eq i1 i2 = true ↔ i1=i2. * qed. |
---|
173 | |
---|
174 | (* syntactical record *) |
---|
175 | |
---|
176 | definition imp_instr_params: instr_params ≝ mk_instr_params ? ? ? ? ? ?. |
---|
177 | [@(mk_DeqSet seq_i seq_i_eq seq_i_eq_equality) |
---|
178 | |@(mk_DeqSet io_i io_i_eq io_i_eq_equality) |
---|
179 | |@(mk_DeqSet cond_i cond_i_eq cond_i_eq_equality) |
---|
180 | |@(mk_DeqSet loop_i loop_i_eq loop_i_eq_equality) |
---|
181 | |@(mk_DeqSet expr expr_eq expr_eq_equality) |
---|
182 | |@(mk_DeqSet expr expr_eq expr_eq_equality)].qed. |
---|
183 | |
---|
184 | (* | IfThenElse: condition → command → command → command*) |
---|
185 | (* | For: variable → expr → list command → command*) |
---|
186 | inductive command: Type[0] ≝ |
---|
187 | Nop: command |
---|
188 | | Ass: variable → expr → command |
---|
189 | | Inc: variable → command |
---|
190 | | IfThenElse: condition → list command → list command → command |
---|
191 | | While: condition → list command → command |
---|
192 | | Call: variable → expr → function → command |
---|
193 | | Return: expr → command |
---|
194 | with function: Type[0] ≝ |
---|
195 | | Fun: variable → list command → function. |
---|
196 | |
---|
197 | definition program ≝ list command. |
---|
198 | |
---|
199 | |
---|
200 | |
---|
201 | (* Big step, operational semantics of expressions and conditions *) |
---|
202 | |
---|
203 | |
---|
204 | definition environment ≝ list (variable × DeqNat). |
---|
205 | |
---|
206 | (* definition environment ≝ variable → nat. *) |
---|
207 | |
---|
208 | (* definition eq_environment: environment → environment → Prop ≝ |
---|
209 | λenv1,env2. ∀v. env1 v = env2 v.*) |
---|
210 | |
---|
211 | definition eq_environment: environment → environment → Prop ≝ |
---|
212 | λenv1,env2.env1 = env2. |
---|
213 | |
---|
214 | (* definition default_env : environment ≝ λ_.0.*) |
---|
215 | |
---|
216 | definition default_env: environment ≝ nil ?. |
---|
217 | |
---|
218 | (* |
---|
219 | definition assign: environment → variable → nat → environment ≝ |
---|
220 | λenv,v,val,x. |
---|
221 | match eqb x v with |
---|
222 | [ true ⇒ val |
---|
223 | | false ⇒ env x]. |
---|
224 | *) |
---|
225 | |
---|
226 | let rec assign (env:environment) (v:variable) (n:DeqNat):environment ≝match env with |
---|
227 | [nil ⇒ [mk_Prod … v n] |
---|
228 | |cons hd tl ⇒ match hd with [(mk_Prod v' n') ⇒ match (v==v') with |
---|
229 | [true ⇒ cons … (mk_Prod … v n) tl |
---|
230 | |false ⇒ cons … hd (assign tl v n) |
---|
231 | ] |
---|
232 | ]]. |
---|
233 | |
---|
234 | (* |
---|
235 | definition increment: environment →variable →environment ≝ |
---|
236 | λenv,v,x. |
---|
237 | match eqb x v with |
---|
238 | [true ⇒ (env x)+1 |
---|
239 | | false ⇒ env x]. |
---|
240 | *) |
---|
241 | |
---|
242 | let rec increment (env:environment) (v:variable):environment ≝match env with |
---|
243 | [nil ⇒ nil … |
---|
244 | |cons hd tl ⇒ match hd with [(mk_Prod v' n) ⇒ match (v==v') with |
---|
245 | [true ⇒ cons … (mk_Prod … v (S n)) tl |
---|
246 | |false ⇒ cons … hd (increment tl v) |
---|
247 | ] |
---|
248 | ]]. |
---|
249 | |
---|
250 | let rec read (env:environment) (v:variable):(option DeqNat)≝match env with |
---|
251 | [nil ⇒ None … |
---|
252 | |cons hd tl ⇒ match hd with [(mk_Prod v' n) ⇒ match (v==v') with |
---|
253 | [true ⇒ Some … n |
---|
254 | |false ⇒ read tl v |
---|
255 | ] |
---|
256 | ]]. |
---|
257 | |
---|
258 | (* |
---|
259 | lemma assign_hit: ∀env,v,val. assign env v val v = val. |
---|
260 | #env #v #val normalize >(eqb_n_n v) normalize % |
---|
261 | qed. |
---|
262 | *) |
---|
263 | |
---|
264 | lemma assign_hit: ∀env,v,val. read (assign env v val) v = Some … val. |
---|
265 | #env elim env |
---|
266 | [2: * #v' #val' #env' #IH #v #val whd in match (assign ???); |
---|
267 | inversion (v==v') |
---|
268 | [#INV whd in ⊢ (??%?); >(\b (refl …)) % |
---|
269 | |#INV whd in ⊢ (??%?); >INV whd in ⊢ (??%?); @IH ] |
---|
270 | |#v #val whd in match (assign [ ] v val); normalize >(eqb_n_n v) %]qed. |
---|
271 | |
---|
272 | (* |
---|
273 | |
---|
274 | [in match t] in [H1:p ... Hn:p] [⊢ p] |
---|
275 | |
---|
276 | p sono come termini dove ? significa qui no, % qui si' e tutti i nomi vanno usati _ |
---|
277 | e non puoi usare costanti, costruttori, induttivi, etc. |
---|
278 | |
---|
279 | la seconda parte del pattern individua un certo numero di posizioni chiamati RADICI; |
---|
280 | se viene omessa la seconda parte c'e' una sola radice nella radice del termine |
---|
281 | |
---|
282 | la prima parte del pattern cerca in ogni radice il sottotermine t e la tattica |
---|
283 | lavora su quello |
---|
284 | |
---|
285 | NOTA BENE: sia f una funzione ricorsiva sul primo argomento e nel goal c'e' |
---|
286 | f (S m). Allora whd in match (f ?) identifica (f (S m)) che si riduce. |
---|
287 | Mentre whd in match f identifica solo f che NON riduce. |
---|
288 | |
---|
289 | *) |
---|
290 | |
---|
291 | (* |
---|
292 | lemma assign_miss: ∀env,v1,v2,val. v1 ≠ v2 → assign env v1 val v2 = env v2. |
---|
293 | #env #v1 #v2 #val #E normalize >(not_eq_to_eqb_false v2 v1) /2 by refl, not_to_not/ |
---|
294 | qed. |
---|
295 | *) |
---|
296 | |
---|
297 | lemma assign_miss: ∀env,v1,v2,val. v2 ≠ v1 → (read (assign env v1 val) v2)= (read env v2). |
---|
298 | #env #v1 #v2 #val #E elim env [normalize >(not_eq_to_eqb_false v2 v1) /2 by refl, not_to_not/ |
---|
299 | |* #v #n #env' #IH inversion(v1==v) #INV [lapply(\P INV)|lapply(\Pf INV)] #K [destruct |
---|
300 | whd in match (assign ???); >INV >ifthenelse_true whd in match (read (〈v,n〉::env') v2); |
---|
301 | inversion(v2==v) #INV2 >INV2 [>ifthenelse_true|>ifthenelse_false] |
---|
302 | whd in match (read (〈v,val〉::env') v2); >INV2 [>ifthenelse_true|>ifthenelse_false] |
---|
303 | whd in match (read (〈v,n〉::env') v2); try % |
---|
304 | lapply (\P INV2) #ABS elim E #ABS2 lapply (ABS2 ABS) #F cases F |
---|
305 | |whd in match (assign ???); >INV >ifthenelse_false whd in match (read ??); |
---|
306 | inversion(v2==v) #INV2 [>ifthenelse_true|>ifthenelse_false] |
---|
307 | [whd in match (read ??); >INV2 >ifthenelse_true % |
---|
308 | |>IH whd in match (read (〈v,n〉::env') v2); >INV2 >ifthenelse_false % |
---|
309 | qed. |
---|
310 | |
---|
311 | let rec sem_expr (env:environment) (e: expr) on e : (option nat) ≝ |
---|
312 | match e with |
---|
313 | [ Var v ⇒ read env v |
---|
314 | | Const n ⇒ Some ? n |
---|
315 | | Plus e1 e2 ⇒ match sem_expr env e1 with [None ⇒ None ?|Some n⇒ |
---|
316 | match sem_expr env e2 with [None ⇒ None ?|Some m⇒ Some ? (n+m)]] |
---|
317 | | Minus e1 e2 ⇒ match sem_expr env e1 with [None ⇒ None ?|Some n⇒ |
---|
318 | match sem_expr env e2 with [None ⇒ None ?|Some m⇒ Some ? (n-m)]]]. |
---|
319 | |
---|
320 | (* |
---|
321 | let rec sem_condition (env:environment) (c:condition) on c : bool ≝ |
---|
322 | match c with |
---|
323 | [ Eq e1 e2 ⇒ eqb (sem_expr env e1) (sem_expr env e2) |
---|
324 | | Not c ⇒ notb (sem_condition env c) ]. |
---|
325 | *) |
---|
326 | |
---|
327 | let rec sem_condition (env:environment) (c:condition) on c : option bool ≝ |
---|
328 | match c with |
---|
329 | [ Eq e1 e2 ⇒ match (sem_expr env e1) with [None ⇒ None ?|Some n⇒ |
---|
330 | match (sem_expr env e2) with [None ⇒ None ?|Some m⇒ Some ? (eqb n m)]] |
---|
331 | | Not c ⇒ match (sem_condition env c) with [None ⇒ None ?|Some b⇒ Some ? (notb b)]]. |
---|
332 | |
---|
333 | |
---|
334 | |
---|
335 | (*CERCO*) |
---|
336 | |
---|
337 | |
---|
338 | definition imp_env_params:env_params≝mk_env_params environment. |
---|
339 | |
---|
340 | let rec env_eq (env1:environment) (env2:environment):bool≝match env1 with |
---|
341 | [nil ⇒ match env2 with [nil⇒ true|_ ⇒ false] |
---|
342 | |cons hd1 tl1 ⇒ match env2 with |
---|
343 | [nil⇒ false |
---|
344 | |cons hd2 tl2 ⇒ match hd1 with |
---|
345 | [mk_Prod v1 n1⇒ match hd2 with |
---|
346 | [mk_Prod v2 n2⇒ (andb (andb (v1==v2) (n1==n2)) (env_eq tl1 tl2))] |
---|
347 | ] |
---|
348 | ] |
---|
349 | ]. |
---|
350 | |
---|
351 | lemma env_eq_refl:∀e.env_eq e e=true. |
---|
352 | #e elim e [%|* #v #n #e' #IH normalize >(eqb_n_n v) >(eqb_n_n n) >ifthenelse_true @IH] qed. |
---|
353 | |
---|
354 | lemma env_eq_to_true:∀e1,e2.env_eq e1 e2=true ↔ e1 =e2. |
---|
355 | #e1 #e2 % [2:* @env_eq_refl |
---|
356 | |lapply e2 -e2 elim e1 |
---|
357 | [#e2 cases e2 normalize #H try(#K #ABS) destruct % |
---|
358 | |* #v #n #e' #IH * normalize in match(env_eq ??); |
---|
359 | #p destruct cases p -p #v' #n' #e whd in match(env_eq ??); |
---|
360 | inversion(v==v') #INVvv' [2: >ifthenelse_false #ABS destruct| |
---|
361 | inversion(n==n') #INVnn' [2: >ifthenelse_false #ABS destruct| normalize |
---|
362 | #EQee' >(IH e EQee') >(\P INVnn') >(\P INVvv') % qed. |
---|
363 | |
---|
364 | definition DeqEnv:DeqSet≝mk_DeqSet environment env_eq env_eq_to_true. |
---|
365 | |
---|
366 | definition store_t:Type[0]≝list (DeqEnv ×variable). |
---|
367 | |
---|
368 | let rec store_eq (s1:store_t) (s2:store_t):bool≝ |
---|
369 | match s1 with |
---|
370 | [nil⇒ match s2 with [nil⇒ true|_⇒ false] |
---|
371 | |cons hd1 tl1⇒ match s2 with [nil⇒ false| cons hd2 tl2⇒ (andb (hd1==hd2) (store_eq tl1 tl2))]]. |
---|
372 | |
---|
373 | lemma store_eq_refl:∀s.store_eq s s=true. |
---|
374 | #s elim s [%|* #e #v #tl #IH whd in match(store_eq ??); >IH |
---|
375 | >(\b (refl …)) % |
---|
376 | qed. |
---|
377 | |
---|
378 | lemma store_eq_equality:∀s1,s2:store_t.store_eq s1 s2=true↔s1=s2. |
---|
379 | #s1 #s2 % [2: * @store_eq_refl |
---|
380 | |lapply s2 -s2 elim s1 |
---|
381 | [* |
---|
382 | [#_ % |
---|
383 | |#p #s2 normalize #ABS destruct |
---|
384 | ] |
---|
385 | |#p #s2 #IH * whd in match (store_eq ??); |
---|
386 | [#ABS destruct |
---|
387 | |#p' #s whd in match (store_eq ??); inversion(p==p') #INV |
---|
388 | [>ifthenelse_true #H >(IH s H) >(\P INV) % |
---|
389 | |>ifthenelse_false #ABS destruct |
---|
390 | ] |
---|
391 | ] |
---|
392 | ] qed. |
---|
393 | |
---|
394 | |
---|
395 | (* store is actually a stack of pairs 〈environment, return-variable〉 *) |
---|
396 | definition imp_store:Type[0]≝mk_DeqSet store_t store_eq store_eq_equality. |
---|
397 | |
---|
398 | definition imp_state_params:state_params≝mk_state_params imp_instr_params imp_env_params DeqEnv. |
---|
399 | |
---|
400 | 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 |
---|
401 | [sNop ⇒ Some ? s |
---|
402 | |sAss v e ⇒ match (sem_expr s e) with [None ⇒ None ?| Some n⇒ Some ? (assign s v n)] |
---|
403 | |sInc v ⇒ match (read s v) with [None ⇒ None ?|Some n⇒ Some ? (assign s v (S n))] |
---|
404 | ]. |
---|
405 | |
---|
406 | definition imp_eval_io:(io_instr imp_state_params)→(store_type imp_state_params)→ option (store_type imp_state_params)≝?. |
---|
407 | // qed. |
---|
408 | |
---|
409 | 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 |
---|
410 | [Eq e1 e2⇒ match (sem_expr s e1) with |
---|
411 | [None⇒ None ? |
---|
412 | |Some n ⇒ match (sem_expr s e2) with |
---|
413 | [None ⇒ None ? |
---|
414 | |Some m ⇒ Some ? (mk_Prod ?? (eqb n m) s)] |
---|
415 | ] |
---|
416 | |Not e ⇒ match (sem_condition s e) with [None ⇒ None ?|Some b ⇒ Some ? (mk_Prod ?? b s)] |
---|
417 | ]. |
---|
418 | |
---|
419 | (* |
---|
420 | 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))≝ |
---|
421 | match c with |
---|
422 | [Eq e1 e2⇒ ? |
---|
423 | |Not c' ⇒ ? |
---|
424 | ]. |
---|
425 | *) |
---|
426 | |
---|
427 | 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. |
---|
428 | (*λl,s.match l with |
---|
429 | [lWhile g l⇒ match (sem_condition g) with [None ⇒ None ?|Some b⇒ Some ? (mk_Prod b s)]].*) |
---|
430 | |
---|
431 | definition imp_sem_state_params : sem_state_params imp_state_params ≝ mk_sem_state_params … imp_eval_seq imp_eval_io |
---|
432 | imp_eval_cond_cond imp_eval_loop_cond …. |
---|
433 | |
---|
434 | |
---|
435 | |
---|
436 | |
---|
437 | (* Big step, declarative semantics of programs *) |
---|
438 | |
---|
439 | definition status≝variable × (program × environment). (* indirizzo di ritorno, continuazione, ambiente *) |
---|
440 | |
---|
441 | definition stack≝list status. |
---|
442 | |
---|
443 | definition default_stack:stack≝nil ?. |
---|
444 | |
---|
445 | definition push: list status → status → list status ≝ |
---|
446 | λl,s.cons ? s l. |
---|
447 | |
---|
448 | definition empty: list status → bool≝ |
---|
449 | λl.match l with [nil ⇒ true | _ ⇒ false]. |
---|
450 | |
---|
451 | definition peek: list status → status ≝ |
---|
452 | λl.(hd ? l (mk_Prod ? ? 0 (mk_Prod ? ? [ ] default_env))). |
---|
453 | |
---|
454 | definition pop: list status → list status ≝ |
---|
455 | λl.tail ? l. |
---|
456 | |
---|
457 | definition Geq:expr → expr → condition≝λe1,e2.Eq (Minus e1 e2) (Const 0). |
---|
458 | |
---|
459 | definition Lt:expr → expr → condition≝λe1,e2.Not (Geq e2 e1). |
---|
460 | |
---|
461 | (* | mIfThenElse1: |
---|
462 | ∀env,st,cond,c1,c2,cont. |
---|
463 | sem_condition env cond = true → |
---|
464 | moves ((IfThenElse cond c1 c2)::cont) env st (c1::cont) env st |
---|
465 | | mIfThenElse2: |
---|
466 | ∀env,st,cond,c1,c2,cont. |
---|
467 | sem_condition env cond = false → |
---|
468 | moves ((IfThenElse cond c1 c2)::cont) env st (c2::cont) env st |
---|
469 | *) |
---|
470 | (* | mFor1: |
---|
471 | ∀env,st,v,e,l,cont. |
---|
472 | (sem_condition env (Lt (Var v) e))=true |
---|
473 | → moves ((For v e l)::cont) env st (l@((Inc v)::(For v e l)::cont)) env st |
---|
474 | | mFor2: |
---|
475 | ∀env,st,v,e,l,cont. |
---|
476 | (sem_condition env (Lt (Var v) e ))=false |
---|
477 | → moves ((For v e l)::cont) env st cont env st |
---|
478 | *) |
---|
479 | |
---|
480 | inductive moves: list command → environment → stack → list command → environment → stack → Prop ≝ |
---|
481 | mNop: ∀env,st,cont. moves (Nop::cont) env st cont env st |
---|
482 | | mAss: ∀env,st,v,e,cont.moves ((Ass v e)::cont) env st cont (assign env v (sem_expr env e)) st |
---|
483 | | mInc: ∀env,st,v,cont.moves ((Inc v)::cont) env st cont (increment env v) st |
---|
484 | | mIfThenElse1: |
---|
485 | ∀env,st,cond,l1,l2,cont. |
---|
486 | sem_condition env cond = true → |
---|
487 | moves ((IfThenElse cond l1 l2)::cont) env st (l1@cont) env st |
---|
488 | | mIfThenElse2: |
---|
489 | ∀env,st,cond,l1,l2,cont. |
---|
490 | sem_condition env cond = false → |
---|
491 | moves ((IfThenElse cond l1 l2)::cont) env st (l2@cont) env st |
---|
492 | | mWhile1: |
---|
493 | ∀env,st,cond,l,cont. |
---|
494 | sem_condition env cond = true → |
---|
495 | moves ((While cond l)::cont) env st (l@(While cond l)::cont) env st |
---|
496 | | mWhile2: |
---|
497 | ∀env,st,cond,l,cont. |
---|
498 | sem_condition env cond = false → |
---|
499 | moves ((While cond l)::cont) env st cont env st |
---|
500 | | mCall: |
---|
501 | ∀env,st,v,e,cont.∀v',l. |
---|
502 | 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))) |
---|
503 | | mReturn: |
---|
504 | ∀env,env',st,v,e,cont,cont'. |
---|
505 | moves ((Return e)::cont) env ((mk_Prod ? ? v (mk_Prod ? ? cont' env'))::st) ((Ass v e)::cont') env' st. |
---|
506 | |
---|
507 | (* bacato: diverge silentemente nel caso lista vuota *) |
---|
508 | inductive moves_star: list command → environment → stack → list command → environment → stack → Prop ≝ |
---|
509 | ms_done: ∀l,env,stack. moves_star l env stack l env stack |
---|
510 | | ms_step: ∀l1,env1,stack1,l2,env2,stack2,l3,env3,stack3. |
---|
511 | moves l1 env1 stack1 l2 env2 stack2 → moves_star l2 env2 stack2 l3 env3 stack3 → |
---|
512 | moves_star l1 env1 stack1 l3 env3 stack3. |
---|
513 | |
---|
514 | (* corretto anche con lista vuota di sopra *) |
---|
515 | inductive converges: list command → environment → stack → environment → stack → Prop ≝ |
---|
516 | conv_done: ∀l,env,stack,env',stack'.moves l env stack [ ] env' stack' → converges l env stack env' stack' |
---|
517 | | 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'' → |
---|
518 | converges l env stack env'' stack''. |
---|
519 | |
---|
520 | (*inductive converges: list command → environment → stack → environment → stack → Prop ≝ |
---|
521 | conv_done: converges [] env stack env stack |
---|
522 | | conv_step: moves l env stack l' env' stack' → converges l' env' stack ' env'' stack'' → |
---|
523 | converes l env stack env'' stack''.*) |
---|
524 | |
---|
525 | |
---|
526 | (* Examples *) |
---|
527 | |
---|
528 | example example1: |
---|
529 | ∃env. |
---|
530 | moves_star |
---|
531 | [Ass 0 (Const 2) |
---|
532 | ;While (Not (Eq (Var 0) (Const 0))) |
---|
533 | [Ass 0 (Minus (Var 0) (Const 1)) |
---|
534 | ;Ass 1 (Plus (Var 1) (Const 1))]] |
---|
535 | default_env |
---|
536 | default_stack |
---|
537 | (nil ?) |
---|
538 | env |
---|
539 | default_stack |
---|
540 | ∧ eq_environment env (assign default_env 1 2). |
---|
541 | % [2: % [(*@(assign default_env 1 2)|%[2:normalize #v cases v [%|#v' %]|*) |
---|
542 | @(ms_step … (mAss …)) @(ms_step …(mWhile1 …)) [normalize %| @(ms_step …(mAss …)) @(ms_step …(mAss …)) |
---|
543 | @(ms_step … (mWhile1 …)) [normalize %| @(ms_step …(mAss …)) @(ms_step …(mAss …)) |
---|
544 | @(ms_step … (mWhile2 …)) [normalize % |@(ms_done …) ]]]| normalize #v cases v normalize [%|#p cases p normalize [%|#_ %]]]] skip qed. |
---|
545 | |
---|
546 | (* Big step, declarative semantics of diverging programs *) |
---|
547 | |
---|
548 | (* coinductive types are greatest fixpoints generated by the constructors; |
---|
549 | they are built starting from the set of all terms and removing at every |
---|
550 | step all terms that do not start with one of the constructors listed in the |
---|
551 | coinductive type declaration. |
---|
552 | |
---|
553 | Intuitively, they are inhabited by all the terms of the corresponding |
---|
554 | inductive type and by new ``infinite'' terms obtained by chaining an infinite |
---|
555 | number of constructors. Intuitively again, their abstract syntax tree is |
---|
556 | infinite. In practice, however, we will only be able to inhabit coinductive |
---|
557 | types with either finite terms or with circular terms obtained by co-recursion. |
---|
558 | |
---|
559 | Recursion over coinductive types is not allowed, since the recursive functions |
---|
560 | could diverge on infinite (circular) term. Co-recursion is allowed to create |
---|
561 | circular terms *) |
---|
562 | coinductive diverges: command → environment → Prop ≝ |
---|
563 | cmIfThenElse1: |
---|
564 | ∀env,cond,c1,c2. |
---|
565 | sem_condition env cond = true → diverges c1 env → |
---|
566 | diverges (IfThenElse cond c1 c2) env |
---|
567 | | cmIfThenElse2: |
---|
568 | ∀env,cond,c1,c2. |
---|
569 | sem_condition env cond = false → diverges c2 env → |
---|
570 | diverges (IfThenElse cond c1 c2) env |
---|
571 | | cmIfThenElseList1: |
---|
572 | ∀env,cond,l1,l2. |
---|
573 | sem_condition env cond = true → diverges_l l1 env → |
---|
574 | diverges (IfThenElseList cond l1 l2) env |
---|
575 | | cmIfThenElseList2: |
---|
576 | ∀env,cond,l1,l2. |
---|
577 | sem_condition env cond = false → diverges_l l2 env → |
---|
578 | diverges (IfThenElseList cond l1 l2) env |
---|
579 | | cmWhile1: |
---|
580 | ∀env,cond,l. |
---|
581 | sem_condition env cond = true → diverges_l l env → diverges (While cond l) env → |
---|
582 | diverges (While cond l) env |
---|
583 | | cmWhile2: |
---|
584 | ∀env,env',cond,l. |
---|
585 | sem_condition env cond = true → moves_l l env env' → diverges (While cond l) env' → |
---|
586 | diverges (While cond l) env |
---|
587 | | cmFor: |
---|
588 | ∀env,v,e,l. |
---|
589 | ((sem_condition env (Eq (Minus e (Var v)) (Const 0))))=false → diverges_l l env → diverges (For v e l) env |
---|
590 | with diverges_l: list command → environment → Prop ≝ |
---|
591 | cmCons1: |
---|
592 | ∀env,env',he,tl. |
---|
593 | moves he env env' → diverges_l tl env' → |
---|
594 | diverges_l (he::tl) env |
---|
595 | | cmCons2: |
---|
596 | ∀env,he,tl. |
---|
597 | diverges he env → diverges_l (he::tl) env. |
---|
598 | |
---|
599 | (* Examples *) |
---|
600 | |
---|
601 | (* Here we use co-recursion to provide an infinite (circular) proof that |
---|
602 | the following term diverges. The env will vary at every iteration, but |
---|
603 | the value of the first variable will never be changed. |
---|
604 | |
---|
605 | Note: a co-recursive function (proof) must be _productive_, i.e. its weak |
---|
606 | head normal form must start with a constructor. I.e. in a finite number of |
---|
607 | steps the function must provide a first observation of the infinite term, |
---|
608 | where observations are identified with constructors. This is the case in |
---|
609 | the following definition. The exact conditions are omitted. *) |
---|
610 | |
---|
611 | let corec example_div1' (x:unit) : |
---|
612 | ∀env. env 0 = 2 → |
---|
613 | diverges |
---|
614 | (While (Not (Eq (Var 0) (Const 0))) |
---|
615 | [Ass 1 (Minus (Var 0) (Const 1)) |
---|
616 | ;Ass 1 (Plus (Var 1) (Const 1))]) |
---|
617 | env ≝ ?. |
---|
618 | #env #H |
---|
619 | @cmWhile2 [2: normalize >H % |3: |
---|
620 | @mCons [2: @mAss | skip | |
---|
621 | @mCons [3: @mNil | skip | @mAss]]| skip | |
---|
622 | @example_div1' // @H |
---|
623 | qed. |
---|
624 | |
---|
625 | example example_div1: |
---|
626 | diverges_l |
---|
627 | [Ass 0 (Const 2) |
---|
628 | ;While (Not (Eq (Var 0) (Const 0))) |
---|
629 | [Ass 1 (Minus (Var 0) (Const 1)) |
---|
630 | ;Ass 1 (Plus (Var 1) (Const 1))]] |
---|
631 | default_env. |
---|
632 | @cmCons1 [2: @mAss | skip] |
---|
633 | @cmCons2 @example_div1' // |
---|
634 | qed. |
---|
635 | |
---|
636 | (* Small step, continuation style, computational semantics of programs *) |
---|
637 | |
---|
638 | definition status ≝ program × environment. |
---|
639 | |
---|
640 | definition final_environment_is: status → environment → Prop ≝ |
---|
641 | λs,env. |
---|
642 | match s with |
---|
643 | [ (*was pair*) mk_Prod l env' ⇒ |
---|
644 | match l with |
---|
645 | [ nil ⇒ eq_environment env env' |
---|
646 | | cons _ _ ⇒ False]]. |
---|
647 | |
---|
648 | definition step: status → option status ≝ |
---|
649 | λs. |
---|
650 | match s with |
---|
651 | [ (*was pair*) mk_Prod p env ⇒ |
---|
652 | match p with |
---|
653 | [ nil ⇒ None ? |
---|
654 | | cons he tl ⇒ |
---|
655 | Some … |
---|
656 | match he with |
---|
657 | [ Ass v val ⇒ 〈tl, assign env v (sem_expr env val)〉 |
---|
658 | | Inc v ⇒ 〈tl, assign env v (sem_expr env (Plus (Var v) (Const 1)))〉 |
---|
659 | | IfThenElse cond c1 c2 ⇒ |
---|
660 | match sem_condition env cond with |
---|
661 | [ true ⇒ 〈c1::tl, env〉 |
---|
662 | | false ⇒ 〈c2::tl, env〉] |
---|
663 | | IfThenElseList cond l1 l2 ⇒ |
---|
664 | match sem_condition env cond with |
---|
665 | [ true ⇒ 〈l1@tl, env〉 |
---|
666 | | false ⇒ 〈l2@tl, env〉] |
---|
667 | | While cond l ⇒ |
---|
668 | match sem_condition env cond with |
---|
669 | [ true ⇒ 〈l@(While cond l)::tl, env〉 |
---|
670 | | false ⇒ 〈tl, env〉] |
---|
671 | | For v e l ⇒ |
---|
672 | match sem_condition env (Eq (Minus (Var v) e) (Const 0)) with |
---|
673 | [ true ⇒ 〈tl, env〉 |
---|
674 | | false ⇒ 〈l@(Inc v::((For v e l)::tl)), env〉 |
---|
675 | ] |
---|
676 | ]]]. |
---|
677 | |
---|
678 | let rec steps (s:status) (n:nat) on n : status ≝ |
---|
679 | match n with |
---|
680 | [ O ⇒ s |
---|
681 | | S m ⇒ |
---|
682 | match step s with |
---|
683 | [ None ⇒ s |
---|
684 | | Some s' ⇒ steps s' m]]. |
---|
685 | |
---|
686 | example example2: |
---|
687 | final_environment_is |
---|
688 | (steps |
---|
689 | 〈[Ass 0 (Const 2) |
---|
690 | ;While (Not (Eq (Var 0) (Const 0))) |
---|
691 | [Ass 0 (Minus (Var 0) (Const 1)) |
---|
692 | ;Ass 1 (Plus (Var 1) (Const 1))]] |
---|
693 | ,default_env〉 |
---|
694 | 20) |
---|
695 | (assign default_env 1 2). |
---|
696 | normalize |
---|
697 | #v cases v normalize // #p cases p // |
---|
698 | qed. |
---|
699 | |
---|
700 | (* Missing from the standard library *) |
---|
701 | |
---|
702 | lemma bool_inv_ind: |
---|
703 | ∀b:bool. ∀P: bool → Prop. (b=true → P true) → (b=false → P false) → P b. |
---|
704 | #b #P cases b /2/ |
---|
705 | qed. |
---|
706 | |
---|
707 | lemma option_inv_ind: |
---|
708 | ∀A.∀x:option A. ∀P: option A → Prop. |
---|
709 | (x=None A → P (None A)) → (∀y. x = Some … y → P (Some … y)) → P x. |
---|
710 | #A #x #P cases x /2/ |
---|
711 | qed. |
---|
712 | |
---|
713 | (* Equivalence of the two semantics on terminating programs *) |
---|
714 | |
---|
715 | lemma moves_l_cons_invert: |
---|
716 | ∀hd,tl,env,env'. |
---|
717 | moves_l (hd::tl) env env' → |
---|
718 | ∃env''. moves hd env env'' ∧ moves_l tl env'' env'. |
---|
719 | #hd #tl #env #env' |
---|
720 | lapply (refl … (hd::tl)) generalize in match (hd::tl) in ⊢ (??%? → %); #l |
---|
721 | #H1 #H2 cases H2 in H1; |
---|
722 | [ #env'' #abs destruct |
---|
723 | | #env1 #env2 #env'' #hd' #tl' #H1 #H2 #E destruct /3/ ] |
---|
724 | qed. |
---|
725 | |
---|
726 | lemma moves_l_append_invert: |
---|
727 | ∀l1,l2,env,env'. |
---|
728 | moves_l (l1@l2) env env' → |
---|
729 | ∃env''. moves_l l1 env env'' ∧ moves_l l2 env'' env'. |
---|
730 | #l1 elim l1 |
---|
731 | [ /3/ |
---|
732 | | #he #tl #IH #l2 #env #env' #H |
---|
733 | cases (moves_l_cons_invert … H) |
---|
734 | #env2 * #H1 #H2 cases (IH … H2) #env3 * /4/ ] |
---|
735 | qed. |
---|
736 | |
---|
737 | lemma commutative_plus: |
---|
738 | ∀n,m.n+m=m+n. |
---|
739 | #n #m elim m [normalize //|#m' #IH //]qed. |
---|
740 | |
---|
741 | lemma step_Some_to_moves_l: |
---|
742 | ∀l,env,p',env',env''. |
---|
743 | step 〈l,env〉 = Some … 〈p',env'〉 → moves_l p' env' env'' → moves_l l env env''. |
---|
744 | #l #env #p' #env' #env'' whd in match step; normalize nodelta cases l normalize |
---|
745 | [ #abs destruct |
---|
746 | | #he #tl normalize #E destruct -E cases he in e0; normalize nodelta |
---|
747 | [ #v #e #E destruct /2/ |
---|
748 | | #v #E destruct /2/ |
---|
749 | | #cond #c1 #c2 inversion (sem_condition env cond) normalize |
---|
750 | #H1 #H2 destruct |
---|
751 | [ #H2 cases (moves_l_cons_invert … H2) #env2 * /3/ |
---|
752 | | #H2 cases (moves_l_cons_invert … H2) #env2 * /3/ ] |
---|
753 | | #cond #l1 #l2 inversion (sem_condition env cond) normalize |
---|
754 | #H1 #H2 destruct |
---|
755 | [ #H2 cases (moves_l_append_invert … H2) #env2 * /3/ |
---|
756 | | #H2 cases (moves_l_append_invert … H2) #env2 * /3/ ] |
---|
757 | | #cond #l inversion (sem_condition env cond) normalize |
---|
758 | #H1 #H2 destruct |
---|
759 | [ (* entra nel while *) #H2 cases (moves_l_append_invert … H2) #env2 * #H3 |
---|
760 | #H4 cases (moves_l_cons_invert … H4) #env3 * /3/ |
---|
761 | | (* termina il while *) /3/ ] |
---|
762 | | (* caso For*) #v #e inversion(eqb(env v-sem_expr env e) 0) normalize |
---|
763 | #INV #l' |
---|
764 | [ (* sottocaso non entro nel for *) |
---|
765 | #HD destruct #H2 %2 [@env'|%10 normalize @INV|@H2] |
---|
766 | |(* sottocaso entro nel for *) |
---|
767 | #HD destruct #H2 cases (moves_l_append_invert … H2) |
---|
768 | #env2 * #H3 #H4 cases (moves_l_cons_invert … H4) |
---|
769 | #env3 * |
---|
770 | |
---|
771 | #H5 #H6 destruct cases (moves_l_cons_invert … H6) |
---|
772 | #env4 * #H7 #H8 destruct %2 [@env4|%9[3:normalize @INV|@env2|4:@H3|@env3 |
---|
773 | |@H5|@H7]|@H8] |
---|
774 | qed. |
---|
775 | |
---|
776 | theorem steps_to_moves_l: |
---|
777 | ∀n,l,env,env'. steps 〈l,env〉 n = 〈[],env'〉 → moves_l l env env'. |
---|
778 | #n elim n |
---|
779 | [ #l #env #env' #H normalize in H; destruct // |
---|
780 | | #m #IH #l #env #env' whd in ⊢ (??%? → ?); cases l |
---|
781 | [ normalize #H destruct // |
---|
782 | | #he #tl inversion (step 〈he::tl,env〉) |
---|
783 | [ #abs normalize in abs; destruct |
---|
784 | | * #l' #env2 #H #K normalize in K; lapply (IH ??? K) /3/ ]]] |
---|
785 | qed. |
---|
786 | |
---|
787 | let rec moves_l_to_steps (l:?) (env:?) (env':?) (H: moves_l l env env') on H : |
---|
788 | ∃n1.∀n2,tl. steps 〈l@tl,env〉 (n1+n2) = steps 〈tl,env'〉 n2 ≝ ? |
---|
789 | and moves_to_steps (c:?) (env:?) (env':?) (H: moves c env env') on H : |
---|
790 | ∃n1.∀n2,tl. steps 〈c::tl,env〉 (n1+n2) = steps 〈tl,env'〉 n2 ≝ ?. |
---|
791 | cases H |
---|
792 | [ -moves_l_to_steps -moves_to_steps #env %{0} #n2 #tl % |
---|
793 | | #env1 #env2 #env3 #he #tl #H1 #H2 |
---|
794 | lapply (moves_to_steps … H1) -moves_to_steps * #n1 #K1 |
---|
795 | lapply (moves_l_to_steps … H2) -moves_l_to_steps * #n2 #K2 |
---|
796 | %{(n1+n2)} #n3 #tl >associative_plus >K1 @K2 |
---|
797 | |
---|
798 | | #env1 #v #e %{1} #n #tl % |
---|
799 | |(* Inc *) #env1 #v %{1} #v' #tl' % |
---|
800 | | #env1 #env2 #cond #c1 #c2 #E |
---|
801 | #H lapply (moves_to_steps … H) -moves_to_steps -moves_l_to_steps * #n1 #K |
---|
802 | %{(S n1)} #n2 #tl normalize >E @K |
---|
803 | | #env1 #env2 #cond #c1 #c2 #E |
---|
804 | #H lapply (moves_to_steps … H) -moves_to_steps -moves_l_to_steps * #n1 #K |
---|
805 | %{(S n1)} #n2 #tl normalize >E @K |
---|
806 | | (* IfThenElseList *) #env1 #env2 #cond #l1 #l2 #E #H1 |
---|
807 | lapply (moves_l_to_steps … H1) -moves_l_to_steps * #n1 #K1 |
---|
808 | %{(S n1)} #n3 #tl normalize >E normalize >associative_plus >K1 % |
---|
809 | |#env1 #env2 #cond #l1 #l2 #E #H1 |
---|
810 | lapply (moves_l_to_steps … H1) -moves_l_to_steps * #n1 #K1 |
---|
811 | %{(S n1)} #n3 #tl normalize >E normalize >associative_plus >K1 % |
---|
812 | | #env1 #env2 #env3 #cond #l #E #H1 #H2 |
---|
813 | lapply (moves_l_to_steps … H1) -moves_l_to_steps * #n1 #K1 |
---|
814 | lapply (moves_to_steps … H2) -moves_to_steps * #n2 #K2 |
---|
815 | %{(S (n1+n2))} #n3 #tl normalize >E normalize >associative_plus >K1 @K2 |
---|
816 | | #env #cond #l #E %{1} #n #tl normalize >E % |
---|
817 | |(* For *) #env1 #env2 #env3 #env4 #v #e #l #E normalize in E; #HL #HMI #HMF |
---|
818 | lapply (moves_l_to_steps … HL) -moves_l_to_steps * #n1 #K1 |
---|
819 | |
---|
820 | lapply (moves_to_steps … HMI) * #n2 #K2 |
---|
821 | lapply (moves_to_steps … HMF) -moves_to_steps * #n3 #K3 |
---|
822 | %{(S(n1+n2+n3))} #n #tl normalize >E normalize >associative_plus >associative_plus |
---|
823 | >K1 >K2 >K3 % |
---|
824 | |#env #v #e #l #E normalize in E; %{1} #n #tl normalize >E normalize % |
---|
825 | ] |
---|
826 | qed. |
---|