source: LTS/imp.ma @ 3533

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

prova predicato uguaglianza tipo condition completata

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