source: LTS/imp.ma @ 3547

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