source: src/joint/blocks.ma @ 2217

Last change on this file since 2217 was 2214, checked in by tranquil, 8 years ago
  • changed order of parameters of joint_internal_function and genv in semantics
  • in semantics, unified more_sem_unserialized_params and more_sem_genv_params
  • renamed all <language>_params to <LANGUAGE>
File size: 22.4 KB
Line 
1include "joint/Joint_paolo.ma".
2include "utilities/bindLists.ma".
3
4(* inductive block_step (p : stmt_params) (globals : list ident) : Type[0] ≝
5  | block_seq : joint_seq p globals → block_step p globals
6  | block_skip : label → block_step p globals.
7
8definition if_seq : ∀p,globals.∀A:Type[2].block_step p globals → A → A → A ≝
9λp,g,A,s.match s with
10[ block_seq _ ⇒ λx,y.x
11| _ ⇒ λx,y.y
12].
13
14definition stmt_of_block_step : ∀p : stmt_params.∀globals.
15  ∀s : block_step p globals.if_seq … s (succ p) unit → joint_statement p globals ≝
16  λp,g,s.match s return λx.if_seq ??? x ?? → joint_statement ?? with
17  [ block_seq s' ⇒ λnxt.sequential … s' nxt
18  | block_skip l ⇒ λ_.GOTO … l
19  ].
20
21definition seq_to_block_step_list : ∀p : stmt_params.∀globals.
22  list (joint_seq p globals) →
23  list (block_step p globals) ≝ λp,globals.map ?? (block_seq ??).
24
25coercion block_step_from_seq_list : ∀p : stmt_params.∀globals.
26  ∀l:list (joint_seq p globals).
27  list (block_step p globals) ≝
28  seq_to_block_step_list
29  on _l:list (joint_seq ??)
30  to list (block_step ??).
31
32definition is_inr : ∀A,B.A + B → bool ≝ λA,B,x.match x with
33  [ inl _ ⇒ true
34  | inr _ ⇒ false
35  ].
36definition is_inl : ∀A,B.A + B → bool ≝ λA,B,x.match x with
37  [ inl _ ⇒ true
38  | inr _ ⇒ false
39  ].
40
41definition skip_block ≝ λp,globals,A.
42  (list (block_step p globals)) × A.*)
43
44definition seq_block ≝ λp : stmt_params.λglobals,A.
45  (list (joint_seq p globals)) × A.
46
47(*definition seq_to_skip_block :
48  ∀p,g,A.seq_block p g A → skip_block p g A
49 ≝ λp,g,A,b.〈\fst b, \snd b〉.
50
51coercion skip_from_seq_block :
52  ∀p,g,A.∀b : seq_block p g A.skip_block p g A ≝
53  seq_to_skip_block on _b : seq_block ??? to skip_block ???.*)
54
55definition bind_seq_block ≝ λp : stmt_params.λglobals,A.
56  bind_new (localsT p) (seq_block p globals A).
57unification hint 0 ≔ p : stmt_params, g, X;
58R ≟ localsT p,
59P ≟ seq_block p g X
60(*---------------------------------------*)⊢
61bind_seq_block p g X ≡ bind_new R P.
62
63definition bind_seq_list ≝ λp : stmt_params.λglobals.
64  bind_new (localsT p) (list (joint_seq p globals)).
65unification hint 0 ≔ p : stmt_params, g;
66R ≟ localsT p,
67S ≟ joint_seq p g,
68L ≟ list S
69(*---------------------------------------*)⊢
70bind_seq_list p g ≡ bind_new R L.
71
72(*definition bind_skip_block ≝ λp : stmt_params.λglobals,A.
73  bind_new (localsT p) (skip_block p globals A).
74unification hint 0 ≔ p : stmt_params, g, A;
75B ≟ skip_block p g A, R ≟ localsT p
76(*---------------------------------------*)⊢
77bind_skip_block p g A ≡ bind_new R B.
78
79definition bind_seq_to_skip_block :
80  ∀p,g,A.bind_seq_block p g A → bind_skip_block p g A ≝
81  λp,g,A.m_map ? (seq_block p g A) (skip_block p g A)
82    (λx.x).
83
84coercion bind_skip_from_seq_block :
85  ∀p,g,A.∀b:bind_seq_block p g A.bind_skip_block p g A ≝
86  bind_seq_to_skip_block on _b : bind_seq_block ??? to bind_skip_block ???.*)
87(*
88definition block_classifier ≝
89  λp,g.λb : other_block p g.
90  seq_or_fin_step_classifier ?? (\snd b).
91*)
92
93let rec split_on_last A (dflt : A) (l : list A) on l : (list A) × A ≝
94match l with
95[ nil ⇒ 〈[ ], dflt〉
96| cons hd tl ⇒
97  match tl with
98  [ nil ⇒ 〈[ ], hd〉
99  | _ ⇒
100    let 〈pref, post〉 ≝ split_on_last A dflt tl in
101    〈hd :: pref, post〉
102  ]
103].
104
105lemma split_on_last_ok :
106  ∀A,dflt,l.
107  match l with
108  [ nil ⇒ True
109  | _ ⇒ l = (let 〈pre, post〉 ≝ split_on_last A dflt l in pre @ [post])
110  ].
111#A #dflt #l elim l normalize nodelta
112[ %
113| #hd * [ #_ %]
114  #hd' #tl #IH whd in match (split_on_last ???); >IH in ⊢ (??%?);
115  elim (split_on_last ???) #a #b %
116]
117qed.
118
119definition seq_block_from_seq_list :
120∀p : stmt_params.∀g.list (joint_seq p g) → seq_block p g (joint_step p g) ≝
121λp,g,l.let 〈pre,post〉 ≝ split_on_last … (NOOP ??) l in 〈pre, (post : joint_step ??)〉.
122
123definition bind_seq_block_from_bind_seq_list :
124  ∀p : stmt_params.∀g.bind_new (localsT p) (list (joint_seq p g)) →
125    bind_seq_block p g (joint_step p g) ≝ λp.λg.m_map … (seq_block_from_seq_list …).
126
127definition bind_seq_block_step :
128  ∀p,g.bind_seq_block p g (joint_step p g) →
129    bind_seq_block p g (joint_step p g) + bind_seq_block p g (joint_fin_step p) ≝
130  λp,g.inl ….
131coercion bind_seq_block_from_step :
132  ∀p,g.∀b:bind_seq_block p g (joint_step p g).
133    bind_seq_block p g (joint_step p g) + bind_seq_block p g (joint_fin_step p) ≝
134  bind_seq_block_step on _b : bind_seq_block ?? (joint_step ??) to
135    bind_seq_block ?? (joint_step ??) + bind_seq_block ?? (joint_fin_step ?).
136
137definition bind_seq_block_fin_step :
138  ∀p,g.bind_seq_block p g (joint_fin_step p) →
139    bind_seq_block p g (joint_step p g) + bind_seq_block p g (joint_fin_step p) ≝
140  λp,g.inr ….
141coercion bind_seq_block_from_fin_step :
142  ∀p,g.∀b:bind_seq_block p g (joint_fin_step p).
143    bind_seq_block p g (joint_step p g) + bind_seq_block p g (joint_fin_step p) ≝
144  bind_seq_block_fin_step on _b : bind_seq_block ?? (joint_fin_step ?) to
145    bind_seq_block ?? (joint_step ??) + bind_seq_block ?? (joint_fin_step ?).
146
147definition seq_block_bind_seq_block :
148  ∀p : stmt_params.∀g,A.seq_block p g A → bind_seq_block p g A ≝ λp,g,A.bret ….
149coercion seq_block_to_bind_seq_block :
150  ∀p : stmt_params.∀g,A.∀b:seq_block p g A.bind_seq_block p g A ≝
151  seq_block_bind_seq_block
152  on _b : seq_block ??? to bind_seq_block ???.
153
154definition joint_step_seq_block : ∀p : stmt_params.∀g.joint_step p g → seq_block p g (joint_step p g) ≝
155  λp,g,x.〈[ ], x〉.
156coercion joint_step_to_seq_block : ∀p : stmt_params.∀g.∀b : joint_step p g.seq_block p g (joint_step p g) ≝
157  joint_step_seq_block on _b : joint_step ?? to seq_block ?? (joint_step ??).
158
159definition joint_fin_step_seq_block : ∀p : stmt_params.∀g.joint_fin_step p → seq_block p g (joint_fin_step p) ≝
160  λp,g,x.〈[ ], x〉.
161coercion joint_fin_step_to_seq_block : ∀p : stmt_params.∀g.∀b : joint_fin_step p.seq_block p g (joint_fin_step p) ≝
162  joint_fin_step_seq_block on _b : joint_fin_step ? to seq_block ?? (joint_fin_step ?).
163
164definition seq_list_seq_block :
165  ∀p:stmt_params.∀g.list (joint_seq p g) → seq_block p g (joint_step p g) ≝
166  λp,g,l.let pr ≝ split_on_last … (NOOP ??) l in 〈\fst pr, \snd pr〉.
167coercion seq_list_to_seq_block :
168  ∀p:stmt_params.∀g.∀l:list (joint_seq p g).seq_block p g (joint_step p g) ≝
169  seq_list_seq_block on _l : list (joint_seq ??) to seq_block ?? (joint_step ??).
170
171definition bind_seq_list_bind_seq_block :
172  ∀p:stmt_params.∀g.bind_new (localsT p) (list (joint_seq p g)) → bind_seq_block p g (joint_step p g) ≝
173  λp,g.m_map ??? (λx : list (joint_seq ??).(x : seq_block ???)).
174
175coercion bind_seq_list_to_bind_seq_block :
176  ∀p:stmt_params.∀g.∀l:bind_new (localsT p) (list (joint_seq p g)).bind_seq_block p g (joint_step p g) ≝
177  bind_seq_list_bind_seq_block on _l : bind_new ? (list (joint_seq ??)) to bind_seq_block ?? (joint_step ??).
178
179notation > "x ~❨ B , l ❩~> y 'in' c" with precedence 56 for
180  @{'block_in_code $c $x $B $l $y}.
181 
182notation < "hvbox(x ~❨ B , l ❩~> y \nbsp 'in' \nbsp break c)" with precedence 56 for
183  @{'block_in_code $c $x $B $l $y}.
184
185definition step_in_code ≝
186  λp,globals.λc : codeT p globals.λsrc : code_point p.λs : joint_step p globals.
187  λdst : code_point p.
188  ∃nxt.stmt_at … c src = Some ? (sequential … s nxt) ∧
189       point_of_succ … src nxt = dst.
190
191definition fin_step_in_code ≝
192  λp,globals.λc : codeT p globals.λsrc : code_point p.λs : joint_fin_step p.
193  stmt_at … c src = Some ? (final … s).
194
195let rec seq_list_in_code p globals (c : codeT p globals)
196  (src : code_point p) (B : list (joint_seq p globals))
197  (l : list (code_point p)) (dst : code_point p) on B : Prop ≝
198  match B with
199  [ nil ⇒
200    match l with
201    [ nil ⇒ src = dst
202    | _ ⇒ False
203    ]
204  | cons hd tl ⇒
205    match l with
206    [ nil ⇒ False
207    | cons mid rest ⇒
208      step_in_code …  c src hd mid ∧ seq_list_in_code … c mid tl rest dst
209    ]
210  ].
211
212interpretation "seq list in code" 'block_in_code c x B l y = (seq_list_in_code ?? c x B l y).
213
214lemma seq_list_in_code_append :
215  ∀p,globals.∀c : codeT p globals.∀src,B1,l1,mid,B2,l2,dst.
216  src ~❨B1,l1❩~> mid in c → mid ~❨B2,l2❩~> dst in c →
217  src ~❨B1@B2,l1@l2❩~> dst in c.
218#p #globals #c #src #B1 lapply src -src elim B1
219[ #src * [2: #mid' #rest] #mid #B2 #l2 #dst [*] #EQ normalize in EQ; destruct(EQ)
220  #H @H
221| #hd #tl #IH #src * [2: #mid' #rest] #mid #B2 #l2 #dst * #H1 #H2
222  #H3 %{H1 (IH … H2 H3)}
223]
224qed.
225
226lemma seq_list_in_code_append_inv :
227  ∀p,globals.∀c : codeT p globals.∀src,B1,B2,l,dst.
228  src ~❨B1@B2,l❩~> dst in c →
229  ∃l1,mid,l2.l = l1 @ l2 ∧ src ~❨B1,l1❩~> mid in c ∧ mid ~❨B2,l2❩~> dst in c.
230#p #globals #c #src #B1 lapply src -src elim B1
231[ #src #B2 #l #dst #H %{[ ]} %{src} %{l} %{H} % %
232| #hd #tl #IH #src #B2 * [2: #mid #rest] #dst * #H1 #H2
233  elim (IH … H2) #l1 * #mid' * #l2 ** #G1 #G2 #G3
234  %{(mid::l1)} %{mid'} %{l2} %{G3} >G1 %{(refl …)}
235  %{H1 G2}
236]
237qed.
238
239definition seq_block_step_in_code ≝
240  λp,g.λc:codeT p g.λsrc.λB : seq_block p g (joint_step p g).λl,dst.
241  src ~❨\fst B, \fst l❩~> \snd l in c ∧ step_in_code … c (\snd l) (\snd B) dst.
242
243definition seq_block_fin_step_in_code ≝
244  λp,g.λc:codeT p g.λsrc.λB : seq_block p g (joint_fin_step p).λl.λdst : unit.
245  src ~❨\fst B, \fst l❩~> \snd l in c ∧ fin_step_in_code … c (\snd l) (\snd B).
246
247(* generates ambiguity even if it shouldn't
248interpretation "seq block step in code" 'block_in_code c x B l y = (seq_block_step_in_code ?? c x B l y).
249interpretation "seq block fin step in code" 'block_in_code c x B l y = (seq_block_fin_step_in_code ?? c x B l y).
250*)
251
252(*
253
254definition seq_block_append :
255  ∀p,g.
256  ∀b1 : Σb.is_safe_block p g b.
257  ∀b2 : seq_block p g.
258  seq_block p g ≝ λp,g,b1,b2.
259  〈match b1 with
260  [ mk_Sig instr prf ⇒
261    match \snd instr return λx.bool_to_Prop (is_inl … x) ∧ seq_or_fin_step_classifier … x = ? → ? with
262    [ inl i ⇒ λprf.\fst b1 @ i :: \fst b2
263    | inr _ ⇒ λprf.⊥
264    ] prf
265  ],\snd b2〉.
266  cases prf #H1 #H2 assumption
267  qed.
268
269definition other_block_append :
270  ∀p,g.
271  (Σb.block_classifier ?? b = cl_other) →
272  other_block p g →
273  other_block p g ≝ λp,g,b1,b2.
274  〈\fst b1 @ «\snd b1, pi2 … b1» :: \fst b2, \snd b2〉.
275
276definition seq_block_cons : ∀p : stmt_params.∀g.(Σs.step_classifier p g s = cl_other) →
277  seq_block p g → seq_block p g ≝
278  λp,g,x,b.〈x :: \fst b,\snd b〉.
279definition other_block_cons : ∀p,g.
280  (Σs.seq_or_fin_step_classifier p g s = cl_other) → other_block p g →
281  other_block p g ≝
282  λp,g,x,b.〈x :: \fst b,\snd b〉.
283
284interpretation "seq block cons" 'cons x b = (seq_block_cons ?? x b).
285interpretation "other block cons" 'vcons x b = (other_block_cons ?? x b).
286interpretation "seq block append" 'append b1 b2 = (seq_block_append ?? b1 b2).
287interpretation "other block append" 'vappend b1 b2 = (other_block_append ?? b1 b2).
288
289definition step_to_block : ∀p,g.
290  seq_or_fin_step p g → seq_block p g ≝ λp,g,s.〈[ ], s〉.
291
292coercion block_from_step : ∀p,g.∀s : seq_or_fin_step p g.
293  seq_block p g ≝ step_to_block on _s : seq_or_fin_step ?? to seq_block ??.
294
295definition bind_seq_block_cons :
296  ∀p : stmt_params.∀g,is_seq.
297  (Σs.step_classifier p g s = cl_other) → bind_seq_block p g is_seq →
298  bind_seq_block p g is_seq ≝
299  λp,g,is_seq,x.m_map ??? (λb.〈x::\fst b,\snd b〉).
300
301definition bind_other_block_cons :
302  ∀p,g.(Σs.seq_or_fin_step_classifier p g s = cl_other) → bind_other_block p g → bind_other_block p g ≝
303  λp,g,x.m_map … (other_block_cons … x).
304
305let rec bind_pred_aux B X (P : X → Prop) (c : bind_new B X) on c : Prop ≝
306  match c with
307  [ bret x ⇒ P x
308  | bnew f ⇒ ∀b.bind_pred_aux B X P (f b)
309  ].
310
311let rec bind_pred_inj_aux B X (P : X → Prop) (c : bind_new B X) on c :
312  bind_pred_aux B X P c → bind_new B (Σx.P x) ≝
313  match c return λx.bind_pred_aux B X P x → bind_new B (Σx.P x) with
314  [ bret x ⇒ λprf.return «x, prf»
315  | bnew f ⇒ λprf.bnew … (λx.bind_pred_inj_aux B X P (f x) (prf x))
316  ].
317
318definition bind_pred ≝ λB.
319  mk_InjMonadPred (BindNew B)
320    (mk_MonadPred ?
321      (bind_pred_aux B)
322      ???)
323    (λX,P,c_sig.bind_pred_inj_aux B X P c_sig (pi2 … c_sig))
324    ?.
325[ #X #P #Q #H #y elim y [ #x @H | #f #IH #G #b @IH @G]
326| #X #Y #Pin #Pout #m elim m [#x | #f #IH] #H #g #G [ @G @H | #b @(IH … G) @H]
327| #X #P #x #Px @Px
328| #X #P * #m elim m [#x | #f #IH] #H [ % | @bnew_proper #b @IH]
329]
330qed.
331
332definition bind_seq_block_append :
333  ∀p,g,is_seq.(Σb : bind_seq_block p g true.bind_pred ? (λb.step_classifier p g (\snd b) = cl_other) b) →
334  bind_seq_block p g is_seq → bind_seq_block p g is_seq ≝
335  λp,g,is_seq,b1,b2.
336    !«p, prf» ← mp_inject … b1;
337    !〈post, last〉 ← b2;
338    return 〈\fst p @ «\snd p, prf» :: post, last〉.
339
340definition bind_other_block_append :
341  ∀p,g.(Σb : bind_other_block p g.bind_pred ?
342    (λx.block_classifier ?? x = cl_other) b) →
343  bind_other_block p g → bind_other_block p g ≝
344  λp,g,b1.m_bin_op … (other_block_append ??) (mp_inject … b1).
345
346interpretation "bind seq block cons" 'cons x b = (bind_seq_block_cons ??? x b).
347interpretation "bind other block cons" 'vcons x b = (bind_other_block_cons ?? x b).
348interpretation "bind seq block append" 'append b1 b2 = (bind_seq_block_append ??? b1 b2).
349interpretation "bind other block append" 'vappend b1 b2 = (bind_other_block_append ?? b1 b2).
350
351let rec instantiates_to B X
352  (b : bind_new B X) (l : list B) (x : X) on b : Prop ≝
353  match b with
354  [ bret B ⇒
355    match l with
356    [ nil ⇒ x = B
357    | _ ⇒ False
358    ]
359  | bnew f ⇒
360    match l with
361    [ nil ⇒ False
362    | cons r l' ⇒
363      instantiates_to B X (f r) l' x
364    ]
365  ].
366
367lemma instantiates_to_bind_pred :
368  ∀B,X,P,b,l,x.instantiates_to B X b l x → bind_pred B P b → P x.
369#B #X #P #b elim b
370[ #x * [ #y #EQ >EQ normalize // | #hd #tl #y *]
371| #f #IH * [ #y * | #hd #tl normalize #b #H #G @(IH … H) @G ]
372]
373qed.
374
375lemma seq_block_append_proof_irr :
376  ∀p,g,b1,b1',b2.pi1 ?? b1 = pi1 ?? b1' →
377    seq_block_append p g b1 b2 = seq_block_append p g b1' b2.
378#p #g * #b1 #b1prf * #b1' #b1prf' #b2 #EQ destruct(EQ) %
379qed.
380
381lemma other_block_append_proof_irr :
382  ∀p,g,b1,b1',b2.pi1 ?? b1 = pi1 ?? b1' →
383  other_block_append p g b1 b2 = other_block_append p g b1' b2.
384#p #g * #b1 #b1prf * #b1' #b1prf' #b2 #EQ destruct(EQ) %
385qed.
386
387(*
388lemma is_seq_block_instance_append : ∀p,g,is_seq.
389  ∀B1.
390  ∀B2 : bind_seq_block p g is_seq.
391  ∀l1,l2.
392  ∀b1 : Σb.is_safe_block p g b.
393  ∀b2 : seq_block p g.
394  instantiates_to ? (seq_block p g) B1 l1 (pi1 … b1) →
395  instantiates_to ? (seq_block p g) B2 l2 b2 →
396  instantiates_to ? (seq_block p g) (B1 @ B2) (l1 @ l2) (b1 @ b2).
397#p #g * #B1 elim B1 -B1
398[ #B1 | #f1 #IH1 ]
399#B1prf whd in B1prf;
400#B2 * [2,4: #r1 #l1' ] #l2 #b1 #b2 [1,4: *]
401whd in ⊢ (%→?);
402[ @IH1
403| #EQ destruct(EQ) lapply b2 -b2 lapply l2 -l2 elim B2 -B2
404  [ #B2 | #f2 #IH2] * [2,4: #r2 #l2'] #b2 [1,4: *]
405  whd in ⊢ (%→?);
406  [ @IH2
407  | #EQ' whd destruct @seq_block_append_proof_irr %
408  ]
409]
410qed.
411
412lemma is_other_block_instance_append : ∀p,g.
413  ∀B1 : Σb.bind_pred ? (λx.block_classifier p g x = cl_other) b.
414  ∀B2 : bind_other_block p g.
415  ∀l1,l2.
416  ∀b1 : Σb.block_classifier p g b = cl_other.
417  ∀b2 : other_block p g.
418  instantiates_to ? (other_block p g) B1 l1 (pi1 … b1) →
419  instantiates_to ? (other_block p g) B2 l2 b2 →
420  instantiates_to ? (other_block p g) (B1 @@ B2) (l1 @ l2) (b1 @@ b2).
421#p #g * #B1 elim B1 -B1
422[ #B1 | #f1 #IH1 ]
423#B1prf whd in B1prf;
424#B2 * [2,4: #r1 #l1' ] #l2 #b1 #b2 [1,4: *]
425whd in ⊢ (%→?);
426[ @IH1
427| #EQ destruct(EQ) lapply b2 -b2 lapply l2 -l2 elim B2 -B2
428  [ #B2 | #f2 #IH2] * [2,4: #r2 #l2'] #b2 [1,4: *]
429  whd in ⊢ (%→?);
430  [ @IH2
431  | #EQ' whd destruct @other_block_append_proof_irr %
432  ]
433]
434qed.
435
436lemma other_fin_step_has_one_label :
437  ∀p,g.∀s:(Σs.fin_step_classifier p g s = cl_other).
438  match fin_step_labels ?? s with
439  [ nil ⇒ False
440  | cons _ tl ⇒
441    match tl with
442    [ nil ⇒ True
443    | _ ⇒ False
444    ]
445  ].
446#p #g ** [#lbl || #ext]
447normalize
448[3: cases (ext_fin_step_flows p ext)
449  [* [2: #lbl' * [2: #lbl'' #tl']]] normalize nodelta ]
450#EQ destruct %
451qed.
452
453definition label_of_other_fin_step : ∀p,g.
454  (Σs.fin_step_classifier p g s = cl_other) → label ≝
455λp,g,s.
456match fin_step_labels p ? s return λx.match x with [ nil ⇒ ? | cons _ tl ⇒ ?] → ? with
457[ nil ⇒ Ⓧ
458| cons lbl tl ⇒ λ_.lbl
459] (other_fin_step_has_one_label p g s).
460
461(*
462definition point_seq_transition : ∀p,g.codeT p g →
463  code_point p → code_point p → Prop ≝
464  λp,g,c,src,dst.
465  match stmt_at … c src with
466  [ Some stmt ⇒ match stmt with
467    [ sequential sq nxt ⇒
468      point_of_succ … src nxt = dst
469    | final fn ⇒
470      match fin_step_labels … fn with
471      [ nil ⇒ False
472      | cons lbl tl ⇒
473        match tl with
474        [ nil ⇒ point_of_label … c lbl = Some ? dst
475        | _ ⇒ False
476        ]
477      ]
478    ]
479  | None ⇒ False
480  ].
481
482lemma point_seq_transition_label_of_other_fin_step :
483  ∀p,c,src.∀s : (Σs.fin_step_classifier p s = cl_other).∀dst.
484  stmt_at ?? c src = Some ? s →
485  point_seq_transition p c src dst →
486  point_of_label … c (label_of_other_fin_step p s) = Some ? dst.
487#p #c #src ** [#lbl || #ext] #EQ1
488#dst #EQ2
489whd in match point_seq_transition; normalize nodelta
490>EQ2 normalize nodelta whd in ⊢ (?→??(????%)?);
491[#H @H | * ]
492lapply (other_fin_step_has_one_label ? «ext,?»)
493cases (fin_step_labels p ? ext) normalize nodelta [*]
494#hd * normalize nodelta [2: #_ #_ *] *
495#H @H
496qed.
497
498lemma point_seq_transition_succ :
499  ∀p,c,src.∀s,nxt.∀dst.
500  stmt_at ?? c src = Some ? (sequential ?? s nxt) →
501  point_seq_transition p c src dst →
502  point_of_succ … src nxt = dst.
503#p #c #src #s #nxt #dst #EQ
504whd in match point_seq_transition; normalize nodelta
505>EQ normalize nodelta #H @H
506qed.
507*)
508
509definition if_other : ∀p,g.∀A : Type[2].seq_or_fin_step p g → A → A → A ≝
510  λp,g,A,c.match seq_or_fin_step_classifier p g c with
511  [ cl_other ⇒ λx,y.x
512  | _ ⇒ λx,y.y
513  ].
514
515definition other_step_in_code ≝
516  λp,g.
517  λc : codeT p g.
518  λsrc : code_point p.
519  λs : seq_or_fin_step p g.
520  match s return λx.if_other p g ? x (code_point p) unit → Prop with
521  [ inl s'' ⇒ λdst.∃n.stmt_at … c src = Some ? (sequential … s'' n) ∧ ?
522  | inr s'' ⇒ λdst.stmt_at … c src = Some ? (final … s'') ∧ ?
523  ].
524  [ whd in dst; cases (seq_or_fin_step_classifier ???) in dst;
525    normalize nodelta [1,2,3: #_ @True |*: #dst
526      @(point_of_succ … src n = dst)]
527  | whd in dst;
528    lapply dst -dst
529    lapply (refl … (seq_or_fin_step_classifier ?? (inr … s'')))
530    cases (seq_or_fin_step_classifier ?? (inr … s'')) in ⊢ (???%→%);
531    normalize nodelta
532    [1,2,3: #_ #_ @True
533    |*: #EQ #dst
534      @(point_of_label … c (label_of_other_fin_step p g «s'', EQ») = Some ? dst)
535    ]
536  ]
537qed.
538
539definition if_other_sig :
540  ∀p,g.∀B,C : Type[0].∀s : Σs.seq_or_fin_step_classifier p g s = cl_other.
541  if_other p g ? s B C → B ≝
542  λp,g,B,C.?.
543  ** #s whd in match (if_other ??????);
544  cases (seq_or_fin_step_classifier ???) normalize nodelta #EQ destruct(EQ)
545  #x @x
546qed.
547
548definition if_other_block_sig :
549  ∀p,g.∀B,C : Type[0].∀b : Σb.block_classifier p g b = cl_other.
550  if_other p g ? (\snd b) B C → B ≝
551  λp,g,B,C.?.
552  ** #l #s
553  #prf #x @(if_other_sig ???? «s, prf» x)
554qed.
555
556coercion other_sig_to_if nocomposites:
557  ∀p,g.∀B,C : Type[0].∀s : Σs.seq_or_fin_step_classifier p g s = cl_other.
558  ∀x : if_other p g ? s B C.B ≝ if_other_sig
559  on _x : if_other ?? Type[0] ??? to ?.
560
561coercion other_block_sig_to_if nocomposites:
562  ∀p,g.∀B,C : Type[0].∀s : Σs.block_classifier p g s = cl_other.
563  ∀x : if_other p g ? (\snd s) B C.B ≝ if_other_block_sig
564  on _x : if_other ?? Type[0] (\snd ?) ?? to ?.
565
566let rec other_list_in_code p g (c : codeT p g)
567  src
568  (b : list (Σs.seq_or_fin_step_classifier p g s = cl_other))
569  dst on b : Prop ≝
570  match b with
571  [ nil ⇒ src = dst
572  | cons hd tl ⇒ ∃mid.
573    other_step_in_code p g c src hd mid ∧ other_list_in_code p g c mid tl dst
574  ].
575
576notation > "x ~❨ B ❩~> y 'in' c" with precedence 56 for
577  @{'block_in_code $c $x $B $y}.
578 
579notation < "hvbox(x ~❨ B ❩~> y \nbsp 'in' \nbsp break c)" with precedence 56 for
580  @{'block_in_code $c $x $B $y}.
581
582interpretation "list in code" 'block_in_code c x B y =
583  (other_list_in_code ?? c x B y).
584
585definition other_block_in_code : ∀p,g.codeT p g →
586  code_point p → ∀b : other_block p g.
587    if_other … (\snd b) (code_point p) unit → Prop ≝
588  λp,g,c,src,b,dst.
589  ∃mid.src ~❨\fst b❩~> mid in c ∧
590  other_step_in_code p g c mid (\snd b) dst.
591
592interpretation "block in code" 'block_in_code c x B y =
593  (other_block_in_code ?? c x B y).
594
595lemma other_list_in_code_append : ∀p,g.∀c : codeT p g.
596  ∀x.∀b1 : list ?.
597  ∀y.∀b2 : list ?.∀z.
598  x ~❨b1❩~> y in c→ y ~❨b2❩~> z in c → x ~❨b1@b2❩~> z in c.
599#p#g#c#x#b1 lapply x -x
600elim b1 [2: ** #hd #hd_prf #tl #IH] #x #y #b2 #z
601[3: #EQ normalize in EQ; destruct #H @H]
602* #mid * normalize nodelta [ *#n ] #H1 #H2 #H3
603whd normalize nodelta %{mid}
604%{(IH … H2 H3)}
605[ %{n} ] @H1
606qed.
607
608lemma other_block_in_code_append : ∀p,g.∀c : codeT p g.∀x.
609  ∀B1 : Σb.block_classifier p g b = cl_other.
610  ∀y.
611  ∀B2 : other_block p g.
612  ∀z.
613  x ~❨B1❩~> y in c → y ~❨B2❩~> z in c →
614  x ~❨B1@@B2❩~> z in c.
615#p#g#c #x ** #hd1 *#tl1 #tl1prf
616#y * #hd2 #tl2 #z
617* #mid1 * #H1 #H2
618* #mid2 * #G1 #G2
619%{mid2} %{G2}
620whd in match (\fst ?);
621@(other_list_in_code_append … H1)
622%{y} %{H2 G1}
623qed.
624
625(*
626definition instr_block_in_function :
627  ∀p : evaluation_params.∀fn : joint_internal_function (globals p) p.
628    code_point p →
629    ∀b : bind_other_block p.
630    ? → Prop ≝
631 λp,fn,src,B,dst.
632 ∃vars,B'.
633  All ? (In ? (joint_if_locals … fn)) vars ∧
634  instantiates_to … B vars B' ∧
635  src ~❨B'❩~> dst in joint_if_code … fn.
636
637interpretation "bind block in function" 'block_in_code fn x B y =
638  (instr_block_in_function ? fn x B y).
639
640lemma instr_block_in_function_trans :
641  ∀p,fn,src.
642  ∀B1 : ΣB.bind_pred ? (λb.block_classifier p b = cl_other) B.
643  ∀mid.
644  ∀B2 : bind_other_block p.
645  ∀dst.
646  src ~❨B1❩~> Some ? mid in fn →
647  mid ~❨B2❩~> dst in fn →
648  src ~❨B1@@B2❩~> dst in fn.
649#p#fn#src*#B1#B1prf#mid#B2#dst
650* #vars1 * #b1 ** #vars1_ok #b1B1 #b1_in
651* #vars2 * #b2 ** #vars2_ok #b2B2 #b2_in
652%{(vars1@vars2)} %{(«b1,instantiates_to_bind_pred … b1B1 B1prf» @@ b2)}
653/4 by All_append, conj, is_other_block_instance_append, other_block_in_code_append/
654qed.
655*)
656*)
657*)
Note: See TracBrowser for help on using the repository browser.