source: LTS/imp.ma @ 3544

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

record semantico: abitato eval_call

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