source: LTS/imp.ma @ 3559

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