source: LTS/imp.ma @ 3548

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