source: LTS/imp.ma @ 3536

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

roll-back per avere tipo seq_i con parametri e store_type come environment decidibile (rifatta prova predicato uguaglianza su expr)

File size: 29.4 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".
19
20(* Tools *)
21
22lemma ifthenelse_elim:∀b,T.∀t:T.if b then t else t=t.
23#b #T #t cases b % qed.
24
25lemma ifthenelse_left:∀b,T.∀t1,t2:T.if b then t1 else t2=t1→ (b=true ∨ t1=t2).
26#b #T #t1 #t2 cases b #H normalize in H; destruct [%1|%2] % qed.
27
28lemma ifthenelse_right:∀b,T.∀t1,t2:T.if b then t1 else t2=t2→ (b=false ∨ t1=t2).
29#b #T #t1 #t2 cases b #H normalize in H; destruct [%2|%1] % qed.
30
31lemma ifthenelse_mm:∀b,b':bool.if b then b' else false=true→ b'=true.
32#b #b' cases b normalize #H destruct % qed.
33
34lemma ifthenelse_mm2:∀b,b':bool.if b then b' else false=true→ b=true.
35#b #b' cases b normalize #H destruct % qed.
36
37let rec neqb n m ≝
38match n with
39  [ O ⇒ match m with [ O ⇒ true | S q ⇒ false]
40  | S p ⇒ match m with [ O ⇒ false | S q ⇒ neqb p q]
41  ].
42 
43axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true ↔ n = m.
44
45definition DeqNat:DeqSet≝mk_DeqSet nat neqb neqb_true_to_eq.
46
47lemma neqb_refl:∀n.neqb n n=true.
48#n elim n [%|#n' normalize * %]qed.
49
50lemma neqb_sym:∀n1,n2.neqb n1 n2=neqb n2 n1.
51#n1 elim n1 [#n2 cases n2 [%|#n' normalize %]|#n2' #IH #n2 cases n2 normalize [2: #m >IH]
52% qed.
53
54(* Syntax *)
55
56definition variable ≝ DeqNat.
57
58inductive expr: Type[0] ≝
59   Var: variable → expr
60 | Const: DeqNat → expr
61 | Plus: expr → expr → expr
62 | Minus: expr → expr → expr.
63
64inductive condition: Type[0] ≝
65   Eq: expr → expr → condition
66 | Not: condition → condition.
67
68let rec expr_eq (e1:expr) (e2:expr):bool≝
69match e1 with [Var v1⇒ match e2 with [Var v2⇒ neqb v1 v2|_⇒ false]
70|Const v1⇒ match e2 with [Const v2⇒ neqb v1 v2|_⇒ false]
71|Plus le1 re1 ⇒ match e2 with [Plus le2 re2 ⇒ andb (expr_eq le1 le2) (expr_eq re1 re2)|_⇒ false]
72|Minus le1 re1 ⇒ match e2 with [Minus le2 re2 ⇒ andb (expr_eq le1 le2) (expr_eq re1 re2)|_⇒ false]
73].
74
75lemma expr_eq_refl:∀e:expr.expr_eq e e=true.
76#e elim e [1,2: #v normalize lapply(neqb_true_to_eq v v) * #_ * %
77|3,4: #f1 #f2 normalize #H1 >H1 #H2 >H2 %]qed.
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 #_ normalize >neqb_refl %
82  |3,4:#f1 #f2 #H1 #H2 #e2 @expr_eq_refl]
83|lapply e2 -e2 elim e1
84  [1,2: #v1 #e2 cases e2 normalize
85    [1,2,5,6: #v2 #H lapply(neqb_true_to_eq v1 v2) * #A destruct >(A H) #_ %
86    |3,4,7,8: #e #f #ABS destruct]
87  |3,4: #e #e2 #H #K #f cases f
88    [1,2,5,6: #v2 normalize #ABS destruct
89    |3,4,7,8:#f1 #f2 normalize inversion(expr_eq e f1) #INV1 >INV1 inversion(expr_eq e2 f2)
90    #INV2 >INV2 normalize #T destruct >(H ? INV1) >(K ? INV2) % qed.
91
92inductive seq_i:Type[0]≝sNop: seq_i|sAss: variable → expr → seq_i|sInc: variable → seq_i.
93definition seq_i_eq:seq_i→ seq_i → bool≝λs1,s2:seq_i.match s1 with [
94 sNop ⇒ match s2 with [sNop ⇒ true| _⇒ false]
95|sAss ⇒ match s2 with [sAss ⇒ true| _⇒ false]
96|sInc ⇒ match s2 with [sInc ⇒ true| _⇒ false]
97].
98lemma seq_i_eq_equality:∀s1,s2.seq_i_eq s1 s2=true ↔ s1=s2.#s1 #s2
99cases s1 cases s2 normalize % #H destruct % qed.
100
101inductive io_i:Type[0]≝.
102definition io_i_eq:io_i→ io_i→ bool≝λi1,i2:io_i.true.
103lemma io_i_eq_equality:∀i1,i2.io_i_eq i1 i2=true ↔ i1=i2.#i1 #i2
104cases i1 qed.
105
106(*axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true → n = m.
107axiom neqb_true_to_eq2: ∀n,m:nat. neqb n m = true ↔ n = m.*)
108lemma neqb_refl:∀n.neqb n n=true.
109#n elim n [%|#n' normalize * %]qed.
110lemma neqb_sym:∀n1,n2.neqb n1 n2=neqb n2 n1.
111#n1 elim n1 [#n2 cases n2 [%|#n' normalize %]|#n2' #IH #n2 cases n2 normalize [2: #m >IH]
112% qed.
113
114definition cond_i:Type[0]≝condition.
115let rec expr_eq (e1:expr) (e2:expr):bool≝
116match e1 with [Var v1⇒ match e2 with [Var v2⇒ neqb v1 v2|_⇒ false]
117|Const v1⇒ match e2 with [Const v2⇒ neqb v1 v2|_⇒ false]
118|Plus le1 re1 ⇒ match e2 with [Plus le2 re2 ⇒ andb (expr_eq le1 le2) (expr_eq re1 re2)|_⇒ false]
119|Minus le1 re1 ⇒ match e2 with [Minus le2 re2 ⇒ andb (expr_eq le1 le2) (expr_eq re1 re2)|_⇒ false]
120].
121let rec cond_i_eq (c1:cond_i) (c2:cond_i):bool ≝
122match c1 with [Eq e1 e2⇒ match c2 with [Eq f1 f2 ⇒
123(andb (expr_eq e1 f1) (expr_eq e2 f2))|_⇒ false]
124|Not e⇒ match c2 with [Not f⇒ cond_i_eq e f|_⇒ false]].
125
126lemma expr_eq_aux:∀e:expr.expr_eq e e=true.
127#e elim e [1,2: #v normalize lapply(neqb_true_to_eq v v) * @neqb_refl
128|3,4: #f1 #f2 normalize #H1 >H1 #H2 >H2 %]qed.
129
130
131lemma expr_eq_plus:∀e1,e2,f1,f2:expr.expr_eq (Plus e1 e2) (Plus f1 f2)=true→ ((expr_eq e1 f1)=true∧(expr_eq e2 f2)=true).
132#e1 #e2 #f1 #f2 #H normalize in H; % [inversion(expr_eq e1 f1)
133|inversion(expr_eq e2 f2)] [1,3:#_ %|2,4:#K >K in H; normalize * [2:>ifthenelse_aux] % qed.
134
135lemma expr_eq_minus:∀e1,e2,f1,f2:expr.expr_eq (Minus e1 e2) (Minus f1 f2)=true→ ((expr_eq e1 f1)=true∧(expr_eq e2 f2)=true).
136#e1 #e2 #f1 #f2 #H normalize in H; % [inversion(expr_eq e1 f1)
137|inversion(expr_eq e2 f2)] [1,3:#_ %|2,4:#K >K in H; normalize * [2:>ifthenelse_aux] % qed.
138
139
140lemma expr_eq_equality_one:∀e1,e2:expr.expr_eq e1 e2=true → e1=e2.
141#e1 elim e1
142[1,2: #v1 * normalize
143  [1,2,5,6: #v2 #H lapply(neqb_true_to_eq v1 v2) #A destruct >(A H) %
144  |3,4,7,8: #e #f #ABS destruct]
145|3,4: #e *
146  [1,2,5: #v2 #H #K * [1,2,5,6,9,10:#n #ABS normalize in ABS; destruct
147  |3,4,7,8,11,12:#f1 #f2 #T [2,4,5: normalize in T; destruct|1,3,6: >(H f1) >(K f2)
148  [1,5,9:% 
149  |2,4,10,12: inversion(f2) [2,6,10,14:#n #Hf2 >Hf2 in T;
150  inversion(expr_eq e f1) #Heqef1 normalize >Heqef1 normalize #ABS destruct(ABS)
151  |3,4,7,8,11,12,15,16:#f1 #f2 #_ #H1 #H2
152  >H2 in T; normalize >ifthenelse_aux * %
153  |1,5,9,13:#v #H2 >H2 in T; normalize #Hite >(ifthenelse_mm (expr_eq e f1) (neqb v2 v))
154[1,3,5,7:%|2,4,6,8:assumption]]
155|3:lapply(expr_eq_plus e (Var v2) f1 f2)|6,7,8:lapply(expr_eq_plus e (Const v2) f1 f2)
156|11:lapply(expr_eq_minus e (Var v2) f1 f2)]* try(#H1 #H2) assumption]]
157|6:#n #H #K #f cases f [1,2:#k|3,4:#f1 #f2] #T normalize in T; destruct(T)
158>(K f2) [>(H f1) [%|inversion (expr_eq e f1) #II try(%) >II in T; #ABS normalize in ABS; destruct]
159|inversion(f2) [#v #IHf >IHf in T; normalize >ifthenelse_aux * %
160|#v #IHf >IHf in T; normalize inversion(neqb n v) #IHnenv #T try (%) >ifthenelse_aux in T; * %
161|3,4: #g1 #g2 #Hg1 #Hg2 #Hf2 >Hf2 in T; normalize >ifthenelse_aux * %]]
162|3,4,7,8:#f1 #f2 #H #K * [1,2,5,6,9,10:#n #T normalize in T; destruct
163|3,4,7,8,9,11,12,15,16: #g1 #g2|13,14:#n] #T normalize in T; destruct
164>(H g1) [1,3,5: >(K g2) [1,3,5:%|2,4,6: /2 by sym_eq, ifthenelse_mm/]
165|2,4,6,8: /2 by ifthenelse_mm2/|7:>(K g2) [%|/2 by ifthenelse_mm/ qed.
166
167lemma expr_eq_equality_two:∀e1,e2.e1=e2→ expr_eq e1 e2=true.
168#e1 #e2 * elim e1 [1,2:#n normalize >neqb_refl %|3,4:#f1 #f2 normalize
169#H1 >H1 #H2 >H2 normalize %]qed.
170
171lemma expr_eq_equality:∀e1,e2.expr_eq e1 e2=true ↔ e1=e2.
172#e1 #e2 % [@expr_eq_equality_one|@expr_eq_equality_two] qed.
173
174(*
175lemma expr_eq_equality_two':∀e1,e2.e1≠e2→ expr_eq e1 e2=false.
176#e1 #e2 * lapply e2 -e2 #e2 elim e1 [1,2:#n normalize /3 by _/|3,4:#f1 #f2 normalize
177#H1 >H1 #H2 >H2 normalize %]qed.
178*)
179lemma expr_eq_refl:∀e.expr_eq e e=true.
180#e >expr_eq_equality_two % qed.
181
182lemma expr_eq_sym:∀e1,e2.expr_eq e1 e2=expr_eq e2 e1.
183#e1 elim e1 [1,2:#n #e2 cases e2 [1,2:#n' normalize >neqb_sym %
184|#f1 #f2 normalize %|4,5,7,8:#f1 try(#f2) normalize %
185|#n normalize //]
186|3,4:#f1 #f2 #H1 #H2 #e2 cases e2 normalize [1,2,5,6:#_ %|3,8:#g1 #g2 >(H1 g1) >(H2 g2) %
187|4,7:#_ #_ %] qed.
188
189(*
190
191lemma expr_eq_equality:∀e1,e2:expr.expr_eq e1 e2=true ↔e1=e2.
192#e1 elim e1
193[ #v1 *
194  [ #v2 normalize % #H cases (neqb_true_to_eq v1 v2) #H1 #H2
195    >H1 // destruct /2/
196  | #c normalize % #H destruct
197  |*: cases daemon ]
198|
199| #e1 #e2 #IH1 #IH2 *
200  [3: #f1 #f2 normalize %
201      [ inversion (expr_eq e1 f1) normalize #H1 #H2 [2: destruct ]
202        cases (IH1 f1) cases (IH2 f2) /4 by eq_f2, sym_eq/
203      | #H destruct cases (IH1 f1) cases (IH2 f2) #H1 #H2 #H3 #H4
204        >H4/2 by /
205*)     
206
207lemma condition_eq_sym:∀c:condition.cond_i_eq c c=true.
208#c elim c [#e #f normalize >expr_eq_aux >expr_eq_aux normalize %
209|#c' normalize * %] qed.
210
211lemma cond_i_eq_equality:∀c1,c2:condition.cond_i_eq c1 c2=true ↔ c1=c2.
212#c1 #c2 % [2: * @condition_eq_sym
213| lapply c2 -c2 elim c1 normalize
214  [ #e1 #e2 * normalize
215    [ #f1 #f2 inversion(expr_eq f1 e1) normalize cases f1 cases e1 [1,2,5,6,17,18,21,22:#n1 #n2 normalize
216#H destruct [1,2:>(neqb_true_to_eq n2 n1 H) cases f2 cases e2
217[1,2,5,6,17,18,21,22:#k1 #k2 >neqb_refl normalize #K destruct >(neqb_true_to_eq k1 k2 K) %
218|3,4,7,8,11,12,15,16,19,20,23,24,27,28,31,32:#g1 #g2 [1,2,3,4,9,10,11,12:#n normalize
219#ABS destruct|5,6,7,8,13,14,15,16:#h1 #h2 normalize [2,3:#ABS destruct
220|1,4,5,6,7,8: inversion(expr_eq h1 g1) #INV1 >INV1 normalize #INV2 destruct
221-c1 try(-c2) -e1 -e2 -f1 -f2 -H >INV1 in INV2; >neqb_refl >INV1 normalize
222#INV2 >expr_eq_sym in INV1; #INV1 >INV1 in INV2; normalize #INV2 >expr_eq_sym in INV1;
223#INV1 destruct >(expr_eq_equality_one g2 h2 INV2) >expr_eq_sym in INV1; #INV1
224>(expr_eq_equality_one g1 h1 INV1) %] >neqb_refl in ABS; normalize #ABS destruct]
225>neqb_refl in ABS; normalize #ABS destruct
226|9,10,13,14,25,26,29,30:#n #h1 #h2 normalize #ABS >neqb_refl in ABS; normalize #ABS destruct]
227|3,4,5,6:#ABS destruct >neqb_sym in H; #H >H in ABS; normalize #ABS destruct]
228|9,10,13,14,25,26,29,30:#n #h1 #h2 normalize #ABS1 #ABS2 destruct
229|11,12,15,16,27,28,31,32:#g1 #g2 #h1 #h2 normalize inversion(expr_eq h1 g1)
230#INV1 >INV1 normalize #INV2 #E destruct >INV1 in E; normalize #E >expr_eq_sym in INV1; #INV1; >INV1 in E;
231normalize #E destruct >expr_eq_sym in INV1; #INV1 >(expr_eq_equality_one h1 g1 INV1)
232>expr_eq_sym in INV2; #INV2 >INV2 in E; normalize #E destruct >expr_eq_sym in INV2; #INV2
233>(expr_eq_equality_one h2 g2 INV2) >expr_eq_sym in E; #E >(expr_eq_equality_one f2 e2 E) %
234]#f1 #f2 #n normalize #ABS1 #ABS2 destruct
235|#c2 #ABS destruct]|#c2 #H #c' cases c' [#e1 #e2 normalize #ABS destruct|#c3 normalize #K
236>(H c3 K) % qed.
237
238
239(*
240inductive cond_i:Type[0]≝cIfThenElse: cond_i.
241definition cond_i_eq:cond_i → cond_i → bool ≝λc1,c2:cond_i.true.
242lemma cond_i_eq_equality:∀c1,c2.cond_i_eq c1 c2=true ↔ c1=c2.#c1 #c2
243cases c1 cases c2 % #_ % qed.
244*)
245
246inductive loop_i:Type[0]≝lWhile: loop_i.
247definition loop_i_eq:loop_i → loop_i → bool ≝λl1,l2:loop_i.true.
248lemma loop_i_eq_equality:∀l1,l2.loop_i_eq l1 l2=true ↔ l1=l2.#l1 #l2
249cases l1 cases l2 % #_ % qed.
250
251(*
252let rec neqb n m ≝
253match n with
254  [ O ⇒ match m with [ O ⇒ true | S q ⇒ false]
255  | S p ⇒ match m with [ O ⇒ false | S q ⇒ neqb p q]
256  ].
257axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true ↔ n = m.
258*)
259
260definition imp_instr_params: instr_params ≝ mk_instr_params ? ? ? ? ? ?.
261[@(mk_DeqSet seq_i seq_i_eq seq_i_eq_equality)
262|@(mk_DeqSet io_i io_i_eq io_i_eq_equality)
263|@(mk_DeqSet cond_i cond_i_eq cond_i_eq_equality)
264|@(mk_DeqSet loop_i loop_i_eq loop_i_eq_equality)
265|@(mk_DeqSet expr expr_eq expr_eq_equality)
266|@(mk_DeqSet expr expr_eq expr_eq_equality)].qed.
267
268
269(* | IfThenElse: condition → command → command → command*)
270(* | For: variable → expr → list command → command*)
271inductive command: Type[0] ≝
272   Nop: command
273 | Ass: variable → expr → command
274 | Inc: variable → command
275 | IfThenElse: condition → list command → list command → command
276 | While: condition → list command → command
277 | Call: variable → expr → function → command
278 | Return: expr → command
279with function: Type[0] ≝
280 | Fun: variable → list command → function.
281
282definition program ≝ list command.
283
284(* Big step, operational semantics of expressions and conditions *)
285
286definition environment ≝ variable → nat.
287
288definition eq_environment: environment → environment → Prop ≝
289 λenv1,env2. ∀v. env1 v = env2 v.
290
291definition default_env : environment ≝ λ_.0.
292
293definition assign: environment → variable → nat → environment ≝
294 λenv,v,val,x.
295  match eqb x v with
296   [ true ⇒ val
297   | false ⇒ env x].
298
299definition increment: environment →variable →environment ≝
300 λenv,v,x.
301  match eqb x v with
302   [true ⇒ (env x)+1
303   | false ⇒ env x].
304
305lemma assign_hit: ∀env,v,val. assign env v val v = val.
306 #env #v #val normalize >(eqb_n_n v) normalize %
307qed.
308
309lemma assign_miss: ∀env,v1,v2,val. v1 ≠ v2 → assign env v1 val v2 = env v2.
310 #env #v1 #v2 #val #E normalize >(not_eq_to_eqb_false v2 v1) /2 by refl, not_to_not/
311qed.
312
313let rec sem_expr (env:environment) (e: expr) on e : nat ≝
314 match e with
315  [ Var v ⇒ env v
316  | Const n ⇒ n
317  | Plus e1 e2 ⇒ sem_expr env e1 + sem_expr env e2
318  | Minus e1 e2 ⇒ sem_expr env e1 - sem_expr env e2 ].
319
320let rec sem_condition (env:environment) (c:condition) on c : bool ≝
321  match c with
322   [ Eq e1 e2 ⇒ eqb (sem_expr env e1) (sem_expr env e2)
323   | Not c ⇒ notb (sem_condition env c) ].
324
325(*CERCO*)
326
327
328
329definition imp_env_params:env_params≝mk_env_params environment.
330
331axiom env_eq:environment→ environment → bool.
332axiom env_eq_to_true:∀e1,e2.env_eq e1 e2=true ↔ e1 =e2.
333definition DeqEnv:DeqSet≝mk_DeqSet environment env_eq env_eq_to_true.
334
335definition imp_state_params:state_params≝mk_state_params imp_instr_params imp_env_params DeqEnv.
336
337definition imp_eval_seq:(seq_instr imp_state_params)→(store_type imp_state_params)→ option (store_type imp_state_params)≝?.
338normalize #s inversion(s) #INV #env [@(Some ? n)|@(Some ? n)|@(Some ? (S n))]qed.
339
340definition imp_eval_io:(io_instr imp_state_params)→(store_type imp_state_params)→ option (store_type imp_state_params)≝?.
341// qed.
342
343definition imp_eval_cond_cond:(cond_instr imp_state_params)→ (store_type imp_state_params)→ option (bool × (store_type imp_state_params))≝?.
344normalize #c cases c [(*case Eq e1 e2*) #e1 #e2 #n |(*case Not g*) #g]
345
346(*
347let rec imp_eval_cond_cond (c: (cond_instr imp_state_params)) (s:(store_type imp_state_params)):option (bool × (store_type imp_state_params))≝
348match c with
349[Eq e1 e2⇒ ?
350|Not c' ⇒ ?
351].
352*)
353
354definition imp_sem_state_params≝mk_sem_state_params imp_instr_.
355
356
357
358
359(* Big step, declarative semantics of programs *)
360
361definition status≝variable × (program × environment). (* indirizzo di ritorno, continuazione, ambiente *)
362
363definition stack≝list status.
364
365definition default_stack:stack≝nil ?.
366
367definition push: list status → status → list status ≝
368  λl,s.cons ? s l.
369 
370definition empty: list status → bool≝
371 λl.match l with [nil ⇒ true | _ ⇒ false].
372
373definition peek: list status → status ≝
374 λl.(hd ? l (mk_Prod ? ? 0 (mk_Prod ? ? [ ] default_env))).
375 
376definition pop: list status → list status ≝
377 λl.tail ? l.
378
379definition Geq:expr → expr → condition≝λe1,e2.Eq (Minus e1 e2) (Const 0).
380
381definition Lt:expr → expr → condition≝λe1,e2.Not (Geq e2 e1).
382
383(* | mIfThenElse1:
384   ∀env,st,cond,c1,c2,cont.
385    sem_condition env cond = true →
386    moves ((IfThenElse cond c1 c2)::cont) env st (c1::cont) env st
387 | mIfThenElse2:
388   ∀env,st,cond,c1,c2,cont.
389    sem_condition env cond = false →
390    moves ((IfThenElse cond c1 c2)::cont) env st (c2::cont) env st
391*)
392(* | mFor1:
393    ∀env,st,v,e,l,cont.
394    (sem_condition env (Lt (Var v) e))=true
395       → moves ((For v e l)::cont) env st (l@((Inc v)::(For v e l)::cont)) env st
396 | mFor2:
397    ∀env,st,v,e,l,cont.
398    (sem_condition env (Lt (Var v) e ))=false
399     → moves ((For v e l)::cont) env st cont env st
400*)
401
402inductive moves: list command → environment → stack → list command → environment → stack → Prop ≝
403   mNop: ∀env,st,cont. moves (Nop::cont) env st cont env st
404 | mAss: ∀env,st,v,e,cont.moves ((Ass v e)::cont) env st cont (assign env v (sem_expr env e)) st
405 | mInc: ∀env,st,v,cont.moves ((Inc v)::cont) env st cont (increment env v) st
406 | mIfThenElse1:
407   ∀env,st,cond,l1,l2,cont.
408    sem_condition env cond = true  →
409    moves ((IfThenElse cond l1 l2)::cont) env st (l1@cont) env st
410 | mIfThenElse2:
411   ∀env,st,cond,l1,l2,cont.
412    sem_condition env cond = false →
413    moves ((IfThenElse cond l1 l2)::cont) env st (l2@cont) env st
414 | mWhile1:
415   ∀env,st,cond,l,cont.
416     sem_condition env cond = true →
417     moves ((While cond l)::cont) env st (l@(While cond l)::cont) env st
418 | mWhile2:
419   ∀env,st,cond,l,cont.
420    sem_condition env cond = false →
421    moves ((While cond l)::cont) env st cont env st
422 | mCall:
423    ∀env,st,v,e,cont.∀v',l.
424    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)))
425 | mReturn:
426    ∀env,env',st,v,e,cont,cont'.
427    moves ((Return e)::cont) env ((mk_Prod ? ? v (mk_Prod ? ? cont' env'))::st) ((Ass v e)::cont') env' st.
428
429(* bacato: diverge silentemente nel caso lista vuota *)
430inductive moves_star: list command → environment → stack → list command → environment → stack → Prop ≝
431   ms_done: ∀l,env,stack. moves_star l env stack l env stack
432 | ms_step: ∀l1,env1,stack1,l2,env2,stack2,l3,env3,stack3.
433    moves l1 env1 stack1 l2 env2 stack2 → moves_star l2 env2 stack2 l3 env3 stack3 →
434     moves_star l1 env1 stack1 l3 env3 stack3.
435
436(* corretto anche con lista vuota di sopra *)
437inductive converges: list command → environment → stack → environment → stack → Prop ≝
438   conv_done: ∀l,env,stack,env',stack'.moves l env stack [ ] env' stack' → converges l env stack env' stack'
439 | 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'' →
440    converges l env stack env'' stack''.
441
442(*inductive converges: list command → environment → stack → environment → stack → Prop ≝
443   conv_done: converges [] env stack env stack
444 | conv_step: moves l env stack l' env' stack' → converges l' env' stack ' env'' stack'' →
445    converes l env stack env'' stack''.*)
446
447
448(* Examples *)
449
450example example1:
451 ∃env.
452  moves_star
453   [Ass 0 (Const 2)
454   ;While (Not (Eq (Var 0) (Const 0)))
455       [Ass 0 (Minus (Var 0) (Const 1))
456       ;Ass 1 (Plus (Var 1) (Const 1))]]
457   default_env
458   default_stack
459   (nil ?)
460   env
461   default_stack
462   ∧ eq_environment env (assign default_env 1 2).
463% [2: % [(*@(assign default_env 1 2)|%[2:normalize #v cases v [%|#v' %]|*)
464@(ms_step … (mAss …)) @(ms_step …(mWhile1 …)) [normalize %| @(ms_step …(mAss …)) @(ms_step …(mAss …))
465@(ms_step … (mWhile1 …)) [normalize %| @(ms_step …(mAss …)) @(ms_step …(mAss …))
466@(ms_step … (mWhile2 …)) [normalize % |@(ms_done …) ]]]| normalize #v cases v normalize [%|#p cases p normalize [%|#_ %]]]] skip qed.
467
468(* Big step, declarative semantics of diverging programs *)
469
470(* coinductive types are greatest fixpoints generated by the constructors;
471   they are built starting from the set of all terms and removing at every
472   step all terms that do not start with one of the constructors listed in the
473   coinductive type declaration.
474   
475   Intuitively, they are inhabited by all the terms of the corresponding
476   inductive type and by new ``infinite'' terms obtained by chaining an infinite
477   number of constructors. Intuitively again, their abstract syntax tree is
478   infinite. In practice, however, we will only be able to inhabit coinductive
479   types with either finite terms or with circular terms obtained by co-recursion.
480   
481   Recursion over coinductive types is not allowed, since the recursive functions
482   could diverge on infinite (circular) term. Co-recursion is allowed to create
483   circular terms *)
484coinductive diverges: command → environment → Prop ≝
485   cmIfThenElse1:
486   ∀env,cond,c1,c2.
487    sem_condition env cond = true → diverges c1 env →
488    diverges (IfThenElse cond c1 c2) env
489 | cmIfThenElse2:
490   ∀env,cond,c1,c2.
491    sem_condition env cond = false → diverges c2 env →
492    diverges (IfThenElse cond c1 c2) env
493 | cmIfThenElseList1:
494   ∀env,cond,l1,l2.
495   sem_condition env cond = true → diverges_l l1 env →
496   diverges (IfThenElseList cond l1 l2) env
497 | cmIfThenElseList2:
498   ∀env,cond,l1,l2.
499   sem_condition env cond = false → diverges_l l2 env →
500   diverges (IfThenElseList cond l1 l2) env
501 | cmWhile1:
502   ∀env,cond,l.
503    sem_condition env cond = true → diverges_l l env → diverges (While cond l) env →
504    diverges (While cond l) env
505 | cmWhile2:
506   ∀env,env',cond,l.
507    sem_condition env cond = true → moves_l l env env' → diverges (While cond l) env' →
508    diverges (While cond l) env
509 | cmFor:
510   ∀env,v,e,l.
511    ((sem_condition env (Eq (Minus e (Var v)) (Const 0))))=false → diverges_l l env → diverges (For v e l) env
512with diverges_l: list command → environment → Prop ≝
513   cmCons1:
514    ∀env,env',he,tl.
515     moves he env env' → diverges_l tl env' →
516     diverges_l (he::tl) env
517 | cmCons2:
518    ∀env,he,tl.
519     diverges he env → diverges_l (he::tl) env.
520
521(* Examples *)
522
523(* Here we use co-recursion to provide an infinite (circular) proof that
524   the following term diverges. The env will vary at every iteration, but
525   the value of the first variable will never be changed.
526   
527   Note: a co-recursive function (proof) must be _productive_, i.e. its weak
528   head normal form must start with a constructor. I.e. in a finite number of
529   steps the function must provide a first observation of the infinite term,
530   where observations are identified with constructors. This is the case in
531   the following definition. The exact conditions are omitted. *)
532   
533let corec example_div1' (x:unit) :
534 ∀env. env 0 = 2 →
535 diverges
536    (While (Not (Eq (Var 0) (Const 0)))
537       [Ass 1 (Minus (Var 0) (Const 1))
538       ;Ass 1 (Plus (Var 1) (Const 1))])
539  env ≝ ?.
540#env #H
541                          @cmWhile2 [2: normalize >H % |3:
542@mCons [2:                @mAss | skip |
543@mCons [3: @mNil | skip | @mAss]]| skip |
544@example_div1' // @H
545qed.
546
547example example_div1:
548  diverges_l
549   [Ass 0 (Const 2)
550   ;While (Not (Eq (Var 0) (Const 0)))
551       [Ass 1 (Minus (Var 0) (Const 1))
552       ;Ass 1 (Plus (Var 1) (Const 1))]]
553   default_env.
554@cmCons1 [2:                @mAss | skip]
555@cmCons2                    @example_div1' //
556qed.
557
558(* Small step, continuation style, computational semantics of programs *)
559
560definition status ≝ program × environment.
561
562definition final_environment_is: status → environment → Prop ≝
563 λs,env.
564  match s with
565  [ (*was pair*) mk_Prod l env' ⇒
566    match l with
567    [ nil ⇒ eq_environment env env'
568    | cons _ _ ⇒ False]].
569
570definition step: status → option status ≝
571 λs.
572  match s with
573  [ (*was pair*) mk_Prod p env ⇒
574     match p with
575     [ nil ⇒ None ?
576     | cons he tl ⇒
577        Some …
578         match he with
579         [ Ass v val ⇒ 〈tl, assign env v (sem_expr env val)〉
580         | Inc v ⇒ 〈tl, assign env v (sem_expr env (Plus (Var v) (Const 1)))〉
581         | IfThenElse cond c1 c2 ⇒
582            match sem_condition env cond with
583            [ true ⇒ 〈c1::tl, env〉
584            | false ⇒ 〈c2::tl, env〉]
585         | IfThenElseList cond l1 l2 ⇒
586            match sem_condition env cond with
587            [ true ⇒ 〈l1@tl, env〉
588            | false ⇒ 〈l2@tl, env〉]
589         | While cond l ⇒
590            match sem_condition env cond with
591            [ true ⇒ 〈l@(While cond l)::tl, env〉
592            | false ⇒ 〈tl, env〉]
593         | For v e l ⇒
594            match sem_condition env (Eq (Minus (Var v) e) (Const 0)) with
595            [ true ⇒  〈tl, env〉
596            | false ⇒ 〈l@(Inc v::((For v e l)::tl)), env〉
597            ]           
598            ]]].
599
600let rec steps (s:status) (n:nat) on n : status ≝
601 match n with
602  [ O ⇒ s
603  | S m ⇒
604    match step s with
605    [ None ⇒ s
606    | Some s' ⇒ steps s' m]].
607
608example example2:
609 final_environment_is
610  (steps
611   〈[Ass 0 (Const 2)
612    ;While (Not (Eq (Var 0) (Const 0)))
613        [Ass 0 (Minus (Var 0) (Const 1))
614        ;Ass 1 (Plus (Var 1) (Const 1))]]
615   ,default_env〉
616   20)
617  (assign default_env 1 2).
618 normalize
619 #v cases v normalize // #p cases p //
620qed.
621
622(* Missing from the standard library *)
623
624lemma bool_inv_ind:
625 ∀b:bool. ∀P: bool → Prop. (b=true → P true) → (b=false → P false) → P b.
626 #b #P cases b /2/
627qed.
628
629lemma option_inv_ind:
630 ∀A.∀x:option A. ∀P: option A → Prop.
631  (x=None A → P (None A)) → (∀y. x = Some … y → P (Some … y)) → P x.
632 #A #x #P cases x /2/
633qed.
634
635(* Equivalence of the two semantics on terminating programs *)
636
637lemma moves_l_cons_invert:
638 ∀hd,tl,env,env'.
639  moves_l (hd::tl) env env' →
640   ∃env''. moves hd env env'' ∧ moves_l tl env'' env'.
641 #hd #tl #env #env'
642 lapply (refl … (hd::tl)) generalize in match (hd::tl) in  ⊢ (??%? → %); #l
643 #H1 #H2 cases H2 in H1;
644 [ #env'' #abs destruct
645 | #env1 #env2 #env'' #hd' #tl' #H1 #H2 #E destruct /3/ ]
646qed.
647
648lemma moves_l_append_invert:
649 ∀l1,l2,env,env'.
650  moves_l (l1@l2) env env' →
651   ∃env''. moves_l l1 env env'' ∧ moves_l l2 env'' env'.
652 #l1 elim l1
653 [ /3/
654 | #he #tl #IH #l2 #env #env' #H
655   cases (moves_l_cons_invert … H)
656   #env2 * #H1 #H2 cases (IH … H2) #env3 * /4/ ]
657qed.
658
659lemma commutative_plus:
660∀n,m.n+m=m+n.
661#n #m elim m [normalize //|#m' #IH //]qed.
662
663lemma step_Some_to_moves_l:
664 ∀l,env,p',env',env''.
665  step 〈l,env〉 = Some … 〈p',env'〉 → moves_l p' env' env'' → moves_l l env env''.
666 #l #env #p' #env' #env'' whd in match step; normalize nodelta cases l normalize
667 [ #abs destruct
668 | #he #tl normalize #E destruct -E cases he in e0; normalize nodelta
669   [ #v #e #E destruct /2/
670   | #v #E destruct /2/
671   | #cond #c1 #c2 inversion (sem_condition env cond) normalize
672     #H1 #H2 destruct
673     [ #H2 cases (moves_l_cons_invert … H2) #env2 * /3/
674     | #H2 cases (moves_l_cons_invert … H2) #env2 * /3/ ]
675   | #cond #l1 #l2 inversion (sem_condition env cond) normalize
676     #H1 #H2 destruct
677     [ #H2 cases (moves_l_append_invert … H2) #env2 * /3/
678     | #H2 cases (moves_l_append_invert … H2) #env2 * /3/ ]
679   | #cond #l inversion (sem_condition env cond) normalize
680     #H1 #H2 destruct
681     [ (* entra nel while *) #H2 cases (moves_l_append_invert … H2) #env2 * #H3
682       #H4 cases (moves_l_cons_invert … H4) #env3 * /3/
683     | (* termina il while *) /3/ ]
684     | (* caso For*) #v #e inversion(eqb(env v-sem_expr env e) 0) normalize
685     #INV #l'
686     [ (* sottocaso non entro nel for *)
687      #HD destruct #H2 %2 [@env'|%10 normalize @INV|@H2]
688      |(* sottocaso entro nel for *)
689      #HD destruct #H2 cases (moves_l_append_invert … H2)
690      #env2 * #H3 #H4 cases (moves_l_cons_invert … H4)
691      #env3 *
692     
693      #H5 #H6 destruct cases (moves_l_cons_invert … H6)
694      #env4 * #H7 #H8 destruct %2 [@env4|%9[3:normalize @INV|@env2|4:@H3|@env3
695      |@H5|@H7]|@H8]
696qed.
697     
698theorem steps_to_moves_l:
699 ∀n,l,env,env'. steps 〈l,env〉 n = 〈[],env'〉 → moves_l l env env'.
700 #n elim n
701 [ #l #env #env' #H normalize in H; destruct //
702 | #m #IH #l #env #env' whd in ⊢ (??%? → ?); cases l
703   [ normalize #H destruct //
704   | #he #tl inversion (step 〈he::tl,env〉)
705     [ #abs normalize in abs; destruct
706     | * #l' #env2 #H #K normalize in K; lapply (IH ??? K) /3/ ]]]
707qed.
708
709let rec moves_l_to_steps (l:?) (env:?) (env':?) (H: moves_l l env env') on H :
710 ∃n1.∀n2,tl. steps 〈l@tl,env〉 (n1+n2) = steps 〈tl,env'〉 n2 ≝ ?
711and moves_to_steps (c:?) (env:?) (env':?) (H: moves c env env') on H :
712 ∃n1.∀n2,tl. steps 〈c::tl,env〉 (n1+n2) = steps 〈tl,env'〉 n2 ≝ ?.
713 cases H
714 [ -moves_l_to_steps -moves_to_steps #env %{0} #n2 #tl %
715 | #env1 #env2 #env3 #he #tl #H1 #H2
716   lapply (moves_to_steps … H1) -moves_to_steps * #n1 #K1
717   lapply (moves_l_to_steps … H2) -moves_l_to_steps * #n2 #K2
718   %{(n1+n2)} #n3 #tl >associative_plus >K1 @K2
719
720 | #env1 #v #e %{1} #n #tl %
721 |(* Inc *) #env1 #v %{1} #v' #tl' %
722 | #env1 #env2 #cond #c1 #c2 #E
723   #H lapply (moves_to_steps … H) -moves_to_steps -moves_l_to_steps * #n1 #K
724   %{(S n1)} #n2 #tl normalize >E @K
725 | #env1 #env2 #cond #c1 #c2 #E
726   #H lapply (moves_to_steps … H) -moves_to_steps -moves_l_to_steps * #n1 #K
727   %{(S n1)} #n2 #tl normalize >E @K
728 | (* IfThenElseList *) #env1 #env2 #cond #l1 #l2 #E #H1
729 lapply (moves_l_to_steps … H1) -moves_l_to_steps * #n1 #K1
730 %{(S n1)} #n3 #tl normalize >E normalize >associative_plus >K1 %
731 |#env1 #env2 #cond #l1 #l2 #E #H1
732 lapply (moves_l_to_steps … H1) -moves_l_to_steps * #n1 #K1
733 %{(S n1)} #n3 #tl normalize >E normalize >associative_plus >K1 %
734 | #env1 #env2 #env3 #cond #l #E #H1 #H2
735   lapply (moves_l_to_steps … H1) -moves_l_to_steps * #n1 #K1
736   lapply (moves_to_steps … H2) -moves_to_steps * #n2 #K2
737   %{(S (n1+n2))} #n3 #tl normalize >E normalize >associative_plus >K1 @K2
738 | #env #cond #l #E %{1} #n #tl normalize >E %
739 |(* For *) #env1 #env2 #env3 #env4 #v #e #l #E normalize in E; #HL #HMI #HMF
740 lapply (moves_l_to_steps … HL) -moves_l_to_steps * #n1 #K1
741 
742 lapply (moves_to_steps … HMI) * #n2 #K2
743 lapply (moves_to_steps … HMF) -moves_to_steps * #n3 #K3
744 %{(S(n1+n2+n3))} #n #tl normalize >E normalize >associative_plus >associative_plus
745>K1 >K2 >K3 %
746|#env #v #e #l #E normalize in E; %{1} #n #tl normalize >E normalize %
747 ]
748qed.
Note: See TracBrowser for help on using the repository browser.