source: LTS/imp.ma @ 3539

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