source: LTS/imp.ma @ 3530

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

prova in corso lemma che il predicato sul tipo expr corrisponde all'uguaglianza

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