source: LTS/imp.ma @ 3534

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

abitato record di tipo instr_params

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