source: LTS/imp.ma @ 3538

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