source: LTS/imp.ma @ 3532

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

prova predicato uguaglianza su tipo expr completata, prova predicato uguaglianza su tipo condition in corso

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