source: LTS/imp.ma @ 3553

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

inizio prima compilazione

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