source: LTS/imp.ma @ 3526

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