source: LTS/imp.ma @ 3528

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

eliminati dal linguaggio i comandi For e IfThenElse?, ridondanti rispetto a While e IfThenElse? generalizzato o IfThenElseList? (rinominato semplicemente IfThenElse?)

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