source: LTS/imp.ma @ 3545

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

risolto un problema di mismatch di tipo legato al fatto che lo store precedentemente era un ambiente e non uno stack di coppie ambiente variabile di ritorno

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