source: LTS/imp.ma @ 3546

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

abitato record semantico

File size: 31.7 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_return_call:(return_type imp_state_params)→ imp_store→ (option imp_store)≝
468λr,s.match s with [nil⇒ None ?
469|cons hd tl⇒ match hd with
470  [mk_Prod env v ⇒ match (sem_expr env r) with
471    [None ⇒ None ?
472    |Some n⇒ Some ? (cons ? (mk_Prod …(assign env v n) v) tl)
473    ]
474  ]
475].
476
477definition imp_init_store: (store_type imp_state_params)≝(mk_Prod DeqEnv variable (nil ?) O)::(nil ?).
478
479
480definition imp_sem_state_params : sem_state_params imp_state_params ≝ mk_sem_state_params imp_state_params imp_eval_seq imp_eval_io
481imp_eval_cond_cond imp_eval_loop_cond imp_eval_call imp_return_call imp_init_store.
482
483
484
485
486(* Big step, declarative semantics of programs *)
487
488definition status≝variable × (program × environment). (* indirizzo di ritorno, continuazione, ambiente *)
489
490definition stack≝list status.
491
492definition default_stack:stack≝nil ?.
493
494definition push: list status → status → list status ≝
495  λl,s.cons ? s l.
496 
497definition empty: list status → bool≝
498 λl.match l with [nil ⇒ true | _ ⇒ false].
499
500definition peek: list status → status ≝
501 λl.(hd ? l (mk_Prod ? ? 0 (mk_Prod ? ? [ ] default_env))).
502 
503definition pop: list status → list status ≝
504 λl.tail ? l.
505
506definition Geq:expr → expr → condition≝λe1,e2.Eq (Minus e1 e2) (Const 0).
507
508definition Lt:expr → expr → condition≝λe1,e2.Not (Geq e2 e1).
509
510(* | mIfThenElse1:
511   ∀env,st,cond,c1,c2,cont.
512    sem_condition env cond = true →
513    moves ((IfThenElse cond c1 c2)::cont) env st (c1::cont) env st
514 | mIfThenElse2:
515   ∀env,st,cond,c1,c2,cont.
516    sem_condition env cond = false →
517    moves ((IfThenElse cond c1 c2)::cont) env st (c2::cont) env st
518*)
519(* | mFor1:
520    ∀env,st,v,e,l,cont.
521    (sem_condition env (Lt (Var v) e))=true
522       → moves ((For v e l)::cont) env st (l@((Inc v)::(For v e l)::cont)) env st
523 | mFor2:
524    ∀env,st,v,e,l,cont.
525    (sem_condition env (Lt (Var v) e ))=false
526     → moves ((For v e l)::cont) env st cont env st
527*)
528
529inductive moves: list command → environment → stack → list command → environment → stack → Prop ≝
530   mNop: ∀env,st,cont. moves (Nop::cont) env st cont env st
531 | mAss: ∀env,st,v,e,cont.moves ((Ass v e)::cont) env st cont (assign env v (sem_expr env e)) st
532 | mInc: ∀env,st,v,cont.moves ((Inc v)::cont) env st cont (increment env v) st
533 | mIfThenElse1:
534   ∀env,st,cond,l1,l2,cont.
535    sem_condition env cond = true  →
536    moves ((IfThenElse cond l1 l2)::cont) env st (l1@cont) env st
537 | mIfThenElse2:
538   ∀env,st,cond,l1,l2,cont.
539    sem_condition env cond = false →
540    moves ((IfThenElse cond l1 l2)::cont) env st (l2@cont) env st
541 | mWhile1:
542   ∀env,st,cond,l,cont.
543     sem_condition env cond = true →
544     moves ((While cond l)::cont) env st (l@(While cond l)::cont) env st
545 | mWhile2:
546   ∀env,st,cond,l,cont.
547    sem_condition env cond = false →
548    moves ((While cond l)::cont) env st cont env st
549 | mCall:
550    ∀env,st,v,e,cont.∀v',l.
551    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)))
552 | mReturn:
553    ∀env,env',st,v,e,cont,cont'.
554    moves ((Return e)::cont) env ((mk_Prod ? ? v (mk_Prod ? ? cont' env'))::st) ((Ass v e)::cont') env' st.
555
556(* bacato: diverge silentemente nel caso lista vuota *)
557inductive moves_star: list command → environment → stack → list command → environment → stack → Prop ≝
558   ms_done: ∀l,env,stack. moves_star l env stack l env stack
559 | ms_step: ∀l1,env1,stack1,l2,env2,stack2,l3,env3,stack3.
560    moves l1 env1 stack1 l2 env2 stack2 → moves_star l2 env2 stack2 l3 env3 stack3 →
561     moves_star l1 env1 stack1 l3 env3 stack3.
562
563(* corretto anche con lista vuota di sopra *)
564inductive converges: list command → environment → stack → environment → stack → Prop ≝
565   conv_done: ∀l,env,stack,env',stack'.moves l env stack [ ] env' stack' → converges l env stack env' stack'
566 | 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'' →
567    converges l env stack env'' stack''.
568
569(*inductive converges: list command → environment → stack → environment → stack → Prop ≝
570   conv_done: converges [] env stack env stack
571 | conv_step: moves l env stack l' env' stack' → converges l' env' stack ' env'' stack'' →
572    converes l env stack env'' stack''.*)
573
574
575(* Examples *)
576
577example example1:
578 ∃env.
579  moves_star
580   [Ass 0 (Const 2)
581   ;While (Not (Eq (Var 0) (Const 0)))
582       [Ass 0 (Minus (Var 0) (Const 1))
583       ;Ass 1 (Plus (Var 1) (Const 1))]]
584   default_env
585   default_stack
586   (nil ?)
587   env
588   default_stack
589   ∧ eq_environment env (assign default_env 1 2).
590% [2: % [(*@(assign default_env 1 2)|%[2:normalize #v cases v [%|#v' %]|*)
591@(ms_step … (mAss …)) @(ms_step …(mWhile1 …)) [normalize %| @(ms_step …(mAss …)) @(ms_step …(mAss …))
592@(ms_step … (mWhile1 …)) [normalize %| @(ms_step …(mAss …)) @(ms_step …(mAss …))
593@(ms_step … (mWhile2 …)) [normalize % |@(ms_done …) ]]]| normalize #v cases v normalize [%|#p cases p normalize [%|#_ %]]]] skip qed.
594
595(* Big step, declarative semantics of diverging programs *)
596
597(* coinductive types are greatest fixpoints generated by the constructors;
598   they are built starting from the set of all terms and removing at every
599   step all terms that do not start with one of the constructors listed in the
600   coinductive type declaration.
601   
602   Intuitively, they are inhabited by all the terms of the corresponding
603   inductive type and by new ``infinite'' terms obtained by chaining an infinite
604   number of constructors. Intuitively again, their abstract syntax tree is
605   infinite. In practice, however, we will only be able to inhabit coinductive
606   types with either finite terms or with circular terms obtained by co-recursion.
607   
608   Recursion over coinductive types is not allowed, since the recursive functions
609   could diverge on infinite (circular) term. Co-recursion is allowed to create
610   circular terms *)
611coinductive diverges: command → environment → Prop ≝
612   cmIfThenElse1:
613   ∀env,cond,c1,c2.
614    sem_condition env cond = true → diverges c1 env →
615    diverges (IfThenElse cond c1 c2) env
616 | cmIfThenElse2:
617   ∀env,cond,c1,c2.
618    sem_condition env cond = false → diverges c2 env →
619    diverges (IfThenElse cond c1 c2) env
620 | cmIfThenElseList1:
621   ∀env,cond,l1,l2.
622   sem_condition env cond = true → diverges_l l1 env →
623   diverges (IfThenElseList cond l1 l2) env
624 | cmIfThenElseList2:
625   ∀env,cond,l1,l2.
626   sem_condition env cond = false → diverges_l l2 env →
627   diverges (IfThenElseList cond l1 l2) env
628 | cmWhile1:
629   ∀env,cond,l.
630    sem_condition env cond = true → diverges_l l env → diverges (While cond l) env →
631    diverges (While cond l) env
632 | cmWhile2:
633   ∀env,env',cond,l.
634    sem_condition env cond = true → moves_l l env env' → diverges (While cond l) env' →
635    diverges (While cond l) env
636 | cmFor:
637   ∀env,v,e,l.
638    ((sem_condition env (Eq (Minus e (Var v)) (Const 0))))=false → diverges_l l env → diverges (For v e l) env
639with diverges_l: list command → environment → Prop ≝
640   cmCons1:
641    ∀env,env',he,tl.
642     moves he env env' → diverges_l tl env' →
643     diverges_l (he::tl) env
644 | cmCons2:
645    ∀env,he,tl.
646     diverges he env → diverges_l (he::tl) env.
647
648(* Examples *)
649
650(* Here we use co-recursion to provide an infinite (circular) proof that
651   the following term diverges. The env will vary at every iteration, but
652   the value of the first variable will never be changed.
653   
654   Note: a co-recursive function (proof) must be _productive_, i.e. its weak
655   head normal form must start with a constructor. I.e. in a finite number of
656   steps the function must provide a first observation of the infinite term,
657   where observations are identified with constructors. This is the case in
658   the following definition. The exact conditions are omitted. *)
659   
660let corec example_div1' (x:unit) :
661 ∀env. env 0 = 2 →
662 diverges
663    (While (Not (Eq (Var 0) (Const 0)))
664       [Ass 1 (Minus (Var 0) (Const 1))
665       ;Ass 1 (Plus (Var 1) (Const 1))])
666  env ≝ ?.
667#env #H
668                          @cmWhile2 [2: normalize >H % |3:
669@mCons [2:                @mAss | skip |
670@mCons [3: @mNil | skip | @mAss]]| skip |
671@example_div1' // @H
672qed.
673
674example example_div1:
675  diverges_l
676   [Ass 0 (Const 2)
677   ;While (Not (Eq (Var 0) (Const 0)))
678       [Ass 1 (Minus (Var 0) (Const 1))
679       ;Ass 1 (Plus (Var 1) (Const 1))]]
680   default_env.
681@cmCons1 [2:                @mAss | skip]
682@cmCons2                    @example_div1' //
683qed.
684
685(* Small step, continuation style, computational semantics of programs *)
686
687definition status ≝ program × environment.
688
689definition final_environment_is: status → environment → Prop ≝
690 λs,env.
691  match s with
692  [ (*was pair*) mk_Prod l env' ⇒
693    match l with
694    [ nil ⇒ eq_environment env env'
695    | cons _ _ ⇒ False]].
696
697definition step: status → option status ≝
698 λs.
699  match s with
700  [ (*was pair*) mk_Prod p env ⇒
701     match p with
702     [ nil ⇒ None ?
703     | cons he tl ⇒
704        Some …
705         match he with
706         [ Ass v val ⇒ 〈tl, assign env v (sem_expr env val)〉
707         | Inc v ⇒ 〈tl, assign env v (sem_expr env (Plus (Var v) (Const 1)))〉
708         | IfThenElse cond c1 c2 ⇒
709            match sem_condition env cond with
710            [ true ⇒ 〈c1::tl, env〉
711            | false ⇒ 〈c2::tl, env〉]
712         | IfThenElseList cond l1 l2 ⇒
713            match sem_condition env cond with
714            [ true ⇒ 〈l1@tl, env〉
715            | false ⇒ 〈l2@tl, env〉]
716         | While cond l ⇒
717            match sem_condition env cond with
718            [ true ⇒ 〈l@(While cond l)::tl, env〉
719            | false ⇒ 〈tl, env〉]
720         | For v e l ⇒
721            match sem_condition env (Eq (Minus (Var v) e) (Const 0)) with
722            [ true ⇒  〈tl, env〉
723            | false ⇒ 〈l@(Inc v::((For v e l)::tl)), env〉
724            ]           
725            ]]].
726
727let rec steps (s:status) (n:nat) on n : status ≝
728 match n with
729  [ O ⇒ s
730  | S m ⇒
731    match step s with
732    [ None ⇒ s
733    | Some s' ⇒ steps s' m]].
734
735example example2:
736 final_environment_is
737  (steps
738   〈[Ass 0 (Const 2)
739    ;While (Not (Eq (Var 0) (Const 0)))
740        [Ass 0 (Minus (Var 0) (Const 1))
741        ;Ass 1 (Plus (Var 1) (Const 1))]]
742   ,default_env〉
743   20)
744  (assign default_env 1 2).
745 normalize
746 #v cases v normalize // #p cases p //
747qed.
748
749(* Missing from the standard library *)
750
751lemma bool_inv_ind:
752 ∀b:bool. ∀P: bool → Prop. (b=true → P true) → (b=false → P false) → P b.
753 #b #P cases b /2/
754qed.
755
756lemma option_inv_ind:
757 ∀A.∀x:option A. ∀P: option A → Prop.
758  (x=None A → P (None A)) → (∀y. x = Some … y → P (Some … y)) → P x.
759 #A #x #P cases x /2/
760qed.
761
762(* Equivalence of the two semantics on terminating programs *)
763
764lemma moves_l_cons_invert:
765 ∀hd,tl,env,env'.
766  moves_l (hd::tl) env env' →
767   ∃env''. moves hd env env'' ∧ moves_l tl env'' env'.
768 #hd #tl #env #env'
769 lapply (refl … (hd::tl)) generalize in match (hd::tl) in  ⊢ (??%? → %); #l
770 #H1 #H2 cases H2 in H1;
771 [ #env'' #abs destruct
772 | #env1 #env2 #env'' #hd' #tl' #H1 #H2 #E destruct /3/ ]
773qed.
774
775lemma moves_l_append_invert:
776 ∀l1,l2,env,env'.
777  moves_l (l1@l2) env env' →
778   ∃env''. moves_l l1 env env'' ∧ moves_l l2 env'' env'.
779 #l1 elim l1
780 [ /3/
781 | #he #tl #IH #l2 #env #env' #H
782   cases (moves_l_cons_invert … H)
783   #env2 * #H1 #H2 cases (IH … H2) #env3 * /4/ ]
784qed.
785
786lemma commutative_plus:
787∀n,m.n+m=m+n.
788#n #m elim m [normalize //|#m' #IH //]qed.
789
790lemma step_Some_to_moves_l:
791 ∀l,env,p',env',env''.
792  step 〈l,env〉 = Some … 〈p',env'〉 → moves_l p' env' env'' → moves_l l env env''.
793 #l #env #p' #env' #env'' whd in match step; normalize nodelta cases l normalize
794 [ #abs destruct
795 | #he #tl normalize #E destruct -E cases he in e0; normalize nodelta
796   [ #v #e #E destruct /2/
797   | #v #E destruct /2/
798   | #cond #c1 #c2 inversion (sem_condition env cond) normalize
799     #H1 #H2 destruct
800     [ #H2 cases (moves_l_cons_invert … H2) #env2 * /3/
801     | #H2 cases (moves_l_cons_invert … H2) #env2 * /3/ ]
802   | #cond #l1 #l2 inversion (sem_condition env cond) normalize
803     #H1 #H2 destruct
804     [ #H2 cases (moves_l_append_invert … H2) #env2 * /3/
805     | #H2 cases (moves_l_append_invert … H2) #env2 * /3/ ]
806   | #cond #l inversion (sem_condition env cond) normalize
807     #H1 #H2 destruct
808     [ (* entra nel while *) #H2 cases (moves_l_append_invert … H2) #env2 * #H3
809       #H4 cases (moves_l_cons_invert … H4) #env3 * /3/
810     | (* termina il while *) /3/ ]
811     | (* caso For*) #v #e inversion(eqb(env v-sem_expr env e) 0) normalize
812     #INV #l'
813     [ (* sottocaso non entro nel for *)
814      #HD destruct #H2 %2 [@env'|%10 normalize @INV|@H2]
815      |(* sottocaso entro nel for *)
816      #HD destruct #H2 cases (moves_l_append_invert … H2)
817      #env2 * #H3 #H4 cases (moves_l_cons_invert … H4)
818      #env3 *
819     
820      #H5 #H6 destruct cases (moves_l_cons_invert … H6)
821      #env4 * #H7 #H8 destruct %2 [@env4|%9[3:normalize @INV|@env2|4:@H3|@env3
822      |@H5|@H7]|@H8]
823qed.
824     
825theorem steps_to_moves_l:
826 ∀n,l,env,env'. steps 〈l,env〉 n = 〈[],env'〉 → moves_l l env env'.
827 #n elim n
828 [ #l #env #env' #H normalize in H; destruct //
829 | #m #IH #l #env #env' whd in ⊢ (??%? → ?); cases l
830   [ normalize #H destruct //
831   | #he #tl inversion (step 〈he::tl,env〉)
832     [ #abs normalize in abs; destruct
833     | * #l' #env2 #H #K normalize in K; lapply (IH ??? K) /3/ ]]]
834qed.
835
836let rec moves_l_to_steps (l:?) (env:?) (env':?) (H: moves_l l env env') on H :
837 ∃n1.∀n2,tl. steps 〈l@tl,env〉 (n1+n2) = steps 〈tl,env'〉 n2 ≝ ?
838and moves_to_steps (c:?) (env:?) (env':?) (H: moves c env env') on H :
839 ∃n1.∀n2,tl. steps 〈c::tl,env〉 (n1+n2) = steps 〈tl,env'〉 n2 ≝ ?.
840 cases H
841 [ -moves_l_to_steps -moves_to_steps #env %{0} #n2 #tl %
842 | #env1 #env2 #env3 #he #tl #H1 #H2
843   lapply (moves_to_steps … H1) -moves_to_steps * #n1 #K1
844   lapply (moves_l_to_steps … H2) -moves_l_to_steps * #n2 #K2
845   %{(n1+n2)} #n3 #tl >associative_plus >K1 @K2
846
847 | #env1 #v #e %{1} #n #tl %
848 |(* Inc *) #env1 #v %{1} #v' #tl' %
849 | #env1 #env2 #cond #c1 #c2 #E
850   #H lapply (moves_to_steps … H) -moves_to_steps -moves_l_to_steps * #n1 #K
851   %{(S n1)} #n2 #tl normalize >E @K
852 | #env1 #env2 #cond #c1 #c2 #E
853   #H lapply (moves_to_steps … H) -moves_to_steps -moves_l_to_steps * #n1 #K
854   %{(S n1)} #n2 #tl normalize >E @K
855 | (* IfThenElseList *) #env1 #env2 #cond #l1 #l2 #E #H1
856 lapply (moves_l_to_steps … H1) -moves_l_to_steps * #n1 #K1
857 %{(S n1)} #n3 #tl normalize >E normalize >associative_plus >K1 %
858 |#env1 #env2 #cond #l1 #l2 #E #H1
859 lapply (moves_l_to_steps … H1) -moves_l_to_steps * #n1 #K1
860 %{(S n1)} #n3 #tl normalize >E normalize >associative_plus >K1 %
861 | #env1 #env2 #env3 #cond #l #E #H1 #H2
862   lapply (moves_l_to_steps … H1) -moves_l_to_steps * #n1 #K1
863   lapply (moves_to_steps … H2) -moves_to_steps * #n2 #K2
864   %{(S (n1+n2))} #n3 #tl normalize >E normalize >associative_plus >K1 @K2
865 | #env #cond #l #E %{1} #n #tl normalize >E %
866 |(* For *) #env1 #env2 #env3 #env4 #v #e #l #E normalize in E; #HL #HMI #HMF
867 lapply (moves_l_to_steps … HL) -moves_l_to_steps * #n1 #K1
868 
869 lapply (moves_to_steps … HMI) * #n2 #K2
870 lapply (moves_to_steps … HMF) -moves_to_steps * #n3 #K3
871 %{(S(n1+n2+n3))} #n #tl normalize >E normalize >associative_plus >associative_plus
872>K1 >K2 >K3 %
873|#env #v #e #l #E normalize in E; %{1} #n #tl normalize >E normalize %
874 ]
875qed.
Note: See TracBrowser for help on using the repository browser.