source: LTS/imp.ma @ 3541

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