source: LTS/imp.ma @ 3543

Last change on this file since 3543 was 3543, checked in by pellitta, 5 years ago
File size: 30.2 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".
19include "basics/finset.ma".
20
21
22
23(* Tools *)
24
25
26lemma ifthenelse_elim:∀b,T.∀t:T.if b then t else t=t.
27#b #T #t cases b % qed.
28
29lemma ifthenelse_true:∀T:Type[0].∀t1,t2:T.if true then t1 else t2=t1.
30#T #t1 #t2 % qed.
31
32lemma ifthenelse_false:∀T:Type[0].∀t1,t2:T.if false then t1 else t2=t2.
33#T #t1 #t2 % qed.
34
35lemma 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
38lemma 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
41lemma ifthenelse_mm:∀b,b':bool.if b then b' else false=true→ b'=true.
42#b #b' cases b normalize #H destruct % qed.
43
44lemma 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
52definition variable ≝ DeqNat.
53
54inductive expr: Type[0] ≝
55   Var: variable → expr
56 | Const: DeqNat → expr
57 | Plus: expr → expr → expr
58 | Minus: expr → expr → expr.
59
60inductive condition: Type[0] ≝
61   Eq: expr → expr → condition
62 | Not: condition → condition.
63 
64  (* technical lemmas for expr_eq*)
65
66let rec expr_eq (e1:expr) (e2:expr):bool≝
67match 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
73lemma 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
79lemma 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
101inductive seq_i:Type[0]≝sNop: seq_i|sAss: variable → expr → seq_i|sInc: variable → seq_i.
102
103definition 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
111lemma 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
116lemma 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| // ]
125qed.
126
127  (* cond_i: type of (guards of) conditional instructions,
128             i.e., possible conditions of IfThenElse *)
129
130definition cond_i:Type[0]≝condition.
131
132let rec cond_i_eq (c1:cond_i) (c2:cond_i):bool ≝
133match 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
139lemma 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
143lemma cond_i_eq_equality:∀c1,c2:condition.cond_i_eq c1 c2=true ↔ c1=c2.
144#c1 #c2 % [2: * // ]
145lapply 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) % ]]
155qed.
156
157  (* cond_i: type of (guards of) loop instructions,
158             i.e., possible conditions of While *)
159
160definition loop_i:Type[0]≝condition.
161
162definition loop_i_eq:loop_i → loop_i → bool ≝cond_i_eq.
163
164lemma 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
168definition io_i ≝ False.
169
170definition io_i_eq ≝ λi1,i2:False. true.
171
172lemma io_i_eq_equality: ∀i1,i2. io_i_eq i1 i2 = true ↔ i1=i2. * qed.
173
174  (* syntactical record *)
175
176definition 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*)
186inductive 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
194with function: Type[0] ≝
195 | Fun: variable → list command → function.
196
197definition program ≝ list command.
198
199
200
201(* Big step, operational semantics of expressions and conditions *)
202
203
204definition 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 
211definition eq_environment: environment → environment → Prop ≝
212 λenv1,env2.env1 = env2.
213
214          (* definition default_env : environment ≝ λ_.0.*)
215
216definition 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
226let 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(*
235definition 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
242let 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
250let 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(*
259lemma assign_hit: ∀env,v,val. assign env v val v = val.
260 #env #v #val normalize >(eqb_n_n v) normalize %
261qed.
262*)
263
264lemma 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 ???);
267inversion (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
276p sono come termini dove ? significa qui no, % qui si' e tutti i nomi vanno usati _
277e non puoi usare costanti, costruttori, induttivi, etc.
278
279la seconda parte del pattern individua un certo numero di posizioni chiamati RADICI;
280se viene omessa la seconda parte c'e' una sola radice nella radice del termine
281
282la prima parte del pattern cerca in ogni radice il sottotermine t e la tattica
283lavora su quello
284
285NOTA BENE: sia f una funzione ricorsiva sul primo argomento e nel goal c'e'
286f (S m). Allora whd in match (f ?) identifica (f (S m)) che si riduce.
287Mentre whd in match f identifica solo f che NON riduce.
288
289 *)
290
291(*
292lemma 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/
294qed.
295*)
296
297lemma 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
300whd in match (assign ???); >INV >ifthenelse_true whd in match (read (〈v,n〉::env') v2);
301inversion(v2==v) #INV2 >INV2 [>ifthenelse_true|>ifthenelse_false]
302whd in match (read (〈v,val〉::env') v2); >INV2 [>ifthenelse_true|>ifthenelse_false]
303whd in match (read (〈v,n〉::env') v2); try %
304lapply (\P INV2) #ABS elim E #ABS2 lapply (ABS2 ABS) #F cases F
305|whd in match (assign ???); >INV >ifthenelse_false whd in match (read ??);
306inversion(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 %
309qed.
310
311let 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(*
321let 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
327let 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
338definition imp_env_params:env_params≝mk_env_params environment.
339
340let 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
351lemma 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
354lemma 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
364definition DeqEnv:DeqSet≝mk_DeqSet environment env_eq env_eq_to_true.
365
366definition store_t:Type[0]≝list (DeqEnv ×variable).
367
368let rec store_eq (s1:store_t) (s2:store_t):bool≝
369match 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
373lemma 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 …)) %
376qed.
377
378lemma 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〉 *)
396definition imp_store:Type[0]≝mk_DeqSet store_t store_eq store_eq_equality.
397
398definition imp_state_params:state_params≝mk_state_params imp_instr_params imp_env_params DeqEnv.
399
400definition 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
406definition imp_eval_io:(io_instr imp_state_params)→(store_type imp_state_params)→ option (store_type imp_state_params)≝?.
407// qed.
408
409definition 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(*
420let rec imp_eval_cond_cond (c: (cond_instr imp_state_params)) (s:(store_type imp_state_params)):option (bool × (store_type imp_state_params))≝
421match c with
422[Eq e1 e2⇒ ?
423|Not c' ⇒ ?
424].
425*)
426
427definition 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
431definition imp_sem_state_params : sem_state_params imp_state_params ≝ mk_sem_state_params … imp_eval_seq imp_eval_io
432imp_eval_cond_cond imp_eval_loop_cond ….
433
434
435
436
437(* Big step, declarative semantics of programs *)
438
439definition status≝variable × (program × environment). (* indirizzo di ritorno, continuazione, ambiente *)
440
441definition stack≝list status.
442
443definition default_stack:stack≝nil ?.
444
445definition push: list status → status → list status ≝
446  λl,s.cons ? s l.
447 
448definition empty: list status → bool≝
449 λl.match l with [nil ⇒ true | _ ⇒ false].
450
451definition peek: list status → status ≝
452 λl.(hd ? l (mk_Prod ? ? 0 (mk_Prod ? ? [ ] default_env))).
453 
454definition pop: list status → list status ≝
455 λl.tail ? l.
456
457definition Geq:expr → expr → condition≝λe1,e2.Eq (Minus e1 e2) (Const 0).
458
459definition 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
480inductive 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 *)
508inductive 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 *)
515inductive 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
528example 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 *)
562coinductive 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
590with 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   
611let 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
623qed.
624
625example 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' //
634qed.
635
636(* Small step, continuation style, computational semantics of programs *)
637
638definition status ≝ program × environment.
639
640definition 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
648definition 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
678let 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
686example 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 //
698qed.
699
700(* Missing from the standard library *)
701
702lemma 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/
705qed.
706
707lemma 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/
711qed.
712
713(* Equivalence of the two semantics on terminating programs *)
714
715lemma 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/ ]
724qed.
725
726lemma 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/ ]
735qed.
736
737lemma commutative_plus:
738∀n,m.n+m=m+n.
739#n #m elim m [normalize //|#m' #IH //]qed.
740
741lemma 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]
774qed.
775     
776theorem 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/ ]]]
785qed.
786
787let 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 ≝ ?
789and 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 ]
826qed.
Note: See TracBrowser for help on using the repository browser.