source: src/RTLabs/CostCheck.ma @ 2307

Last change on this file since 2307 was 2307, checked in by campbell, 7 years ago

Half the proofs for sound cost labelling check.
File size: 22.6 KB
Line 
1
2include "RTLabs/CostSpec.ma".
3
4(* TODO: move ----→ *)
5
6lemma Exists_to_All : ∀T,P,l.
7  (∀x. Exists ? (λy. y = x) l → P x) →
8  All T P l.
9#T #P #l elim l [ // | #h #t #IH #H % [ @H %1 % | @IH #t #E @H %2 @E ] ]
10qed.
11
12let rec all (A:Type[0]) (P:A → bool) (l:list A) on l : bool ≝
13match l with
14[ nil ⇒ true
15| cons h t ⇒ P h ∧ all A P t
16].
17
18lemma all_All : ∀A,P,l. bool_to_Prop (all A P l) ↔ All A (λa.bool_to_Prop (P a)) l.
19#A #P #l elim l
20[ % //
21| #h #t * #IH #IH' %
22  [ whd in ⊢ (?% → %); cases (P h) [ #p % /2/ | * ]
23  | * #p #H whd in ⊢ (?%); >p /2/
24  ]
25] qed.
26
27(* ←---- move *)
28
29definition check_well_cost_fn : internal_function → bool ≝
30λf.
31  idmap_all … (f_graph f) (λl,s,PR. well_cost_labelled_statement (f_graph f) s (f_closed f l s PR)) ∧
32  is_cost_label (lookup_present … (f_graph f) (f_entry f) ?).
33cases (f_entry f) //
34qed.
35
36lemma check_well_cost_fn_ok : ∀fn. bool_to_Prop (check_well_cost_fn fn) ↔ well_cost_labelled_fn fn.
37#fn %
38[ #H cases (andb_Prop_true … H) #ST #EN
39  % [ lapply (proj1 … (idmap_all_ok …) ST) // | @EN ]
40| * #ST #EN @andb_Prop
41  [ @(proj2 … (idmap_all_ok …)) #l #st #L
42    cut (present ?? (f_graph fn) l) [ whd >L % #E destruct ] #PR
43    lapply (ST l PR) generalize in ⊢ (?(???%) → ?);
44    >(lookup_present_eq ????? L PR) //
45  | @eq_true_to_b @EN
46  ]
47] qed.
48
49include "basics/lists/listb.ma".
50include alias "utilities/deqsets.ma".
51
52lemma successors_present : ∀g,st.
53  labels_present g st →
54  ∀l. l ∈ successors st →
55  present ?? g l.
56#g *
57[ #l1 #PR #l2 #IN >(memb_single … IN) @PR
58| #cs #l1 #PR #l2 #IN >(memb_single … IN) @PR
59| #ty #r #c #l1 #PR #l2 #IN >(memb_single … IN) @PR
60| #ty1 #ty2 #op #r1 #r2  #l1 #PR #l2 #IN >(memb_single … IN) @PR
61| #ty1 #ty2 #ty3 #op #r1 #r2 #r3 #l1 #PR #l2 #IN >(memb_single … IN) @PR
62| #ty #r1 #r2 #l1 #PR #l2 #IN >(memb_single … IN) @PR
63| #ty #r1 #r2 #l1 #PR #l2 #IN >(memb_single … IN) @PR
64| #id #args #dst #l1 #PR #l2 #IN >(memb_single … IN) @PR
65| #r #args #dst #l1 #PR #l2 #IN >(memb_single … IN) @PR
66| #r #l1 #l2 * #PR1 #PR2 #l3 whd in ⊢ (?% → ?); @eqb_elim [ // | #_ #IN >(memb_single … IN) // ]
67| #_ #l *
68] qed.
69
70include alias "common/Identifiers.ma".
71
72(* Check that from [checking] we reach a cost label without going through
73   [checking_tail], which would form a loop in the CFG.  We also have a set of
74   labels that we have still [to_check], and return an updated set of labels
75   to check if the check for the current label is successful. *)
76let rec check_label_bounded
77  (g : graph statement)
78  (CL : graph_closed g)
79  (checking : label)
80  (PR : present ?? g checking)
81  (checking_tail : list label)
82  (to_check : identifier_set LabelTag)
83  (term_check : nat)
84on term_check : gt term_check (id_map_size … to_check) → option (identifier_set LabelTag) ≝
85let stop_now ≝ Some ? to_check in
86match term_check return λx. ge x ? → ? with
87[ O ⇒ λH.⊥
88| S term_check' ⇒ λH.
89  let st ≝ lookup_present … g checking PR in
90  let succs ≝ successors st in
91  match succs return λsc. (∀l.l∈sc → ?) → ? with
92  [ nil ⇒ λ_. stop_now
93  | cons h t ⇒
94    match t with
95    [ nil ⇒ λSC. (* single successor *)
96      match try_remove … to_check h return λx. (∀a,m'. x = ? → ?) → ? with
97      [ Some to_check' ⇒ λH'.
98        let PR' ≝ ? in
99        let st' ≝ lookup_present … g h PR' in
100        if is_cost_label st' then stop_now else
101          if h ∈ checking_tail then None ? else
102            check_label_bounded g CL h PR' (checking::checking_tail) (\snd to_check') term_check' ?
103      | None ⇒ λ_.
104          if h == checking ∨ h ∈ checking_tail then None ? else
105            stop_now (* already checked successor *)
106      ] (try_remove_some_card … to_check h)
107    | cons _ _ ⇒ λ_. stop_now (* all branches are followed by a cost label *)
108    ]
109  ] (successors_present g st (CL … checking … (lookup_lookup_present …)))
110].
111[ /2 by absurd/
112| lapply (H' (\fst to_check') (\snd to_check') ?) [ cases to_check' // ]
113  #E -PR' >E in H; #H' /2/
114| @SC >memb_hd //
115] qed.
116
117(* An inductive specification of the above function that's easier to work with. *)
118
119inductive check_label_bounded_spec (g:graph statement) : label → list label → identifier_set LabelTag → identifier_set LabelTag → Prop ≝
120| clbs_ret : ∀l,PR,tl,toch.
121    successors (lookup_present … g l PR) = [ ] →
122    check_label_bounded_spec g l tl toch toch
123| clbs_checked : ∀l,PR,l',tl,toch.
124    successors (lookup_present … g l PR) = [l'] →
125    ¬ l' ∈ toch →
126    l' ≠ l →
127    ¬ l' ∈ tl →
128    check_label_bounded_spec g l tl toch toch
129| clbs_cost : ∀l,PR,l',PR',tl,toch.
130    successors (lookup_present … g l PR) = [l'] →
131    l' ∈ toch →
132    is_cost_label (lookup_present … g l' PR') →
133    check_label_bounded_spec g l tl toch toch
134| clbs_step : ∀l,PR,l',PR',tl,toch,toch',toch''.
135    successors (lookup_present … g l PR) = [l'] →
136(*    l' ∈ toch → implied *)
137    ¬ l' ∈ tl →
138    ¬ is_cost_label (lookup_present … g l' PR') →
139    try_remove … toch l' = Some ? 〈it,toch'〉 →
140    check_label_bounded_spec g l' (l::tl) toch' toch'' →
141    check_label_bounded_spec g l tl toch toch''
142| clbs_branch : ∀l,PR,x,y,zs,tl,toch.  (* the other check will show that these are cost labels *)
143    successors (lookup_present … g l PR) = x::y::zs →
144    check_label_bounded_spec g l tl toch toch.
145
146(* TODO: move (or is it somewhere already?) *)
147lemma if_elim : ∀T:Type[0]. ∀b:bool. ∀e1,e2:T. ∀P:T → Type[0].
148  (b → P e1) →
149  (¬b → P e2) →
150  P (if b then e1 else e2).
151#T * /2/
152qed.
153
154lemma not_orb : ∀b,c:bool.
155  ¬ (b∨c) →
156  (bool_to_Prop (¬b))∧(bool_to_Prop (¬c)).
157* * normalize /2/
158qed.
159
160lemma check_label_bounded_s : ∀term_check,g,CL,checking,PR,checking_tail,to_check,TERM,to_check'.
161  check_label_bounded g CL checking PR checking_tail to_check term_check TERM = Some ? to_check' →
162  check_label_bounded_spec g checking checking_tail to_check to_check'.
163#n elim n
164[ #a #b #c #d #d #e #g @⊥ /3 by n_plus_1_n_to_False, div_plus_times/ (* ! *)
165| #term_check #IH #g #CL #checking #PR #checking_tail #to_check #TERM #to_check'
166  whd in ⊢ (??%? → ?);
167  generalize in ⊢ (??(?%)? → ?);
168  lapply (refl ? (successors (lookup_present … PR)))
169  cases (successors (lookup_present … PR)) in ⊢ (???% → %);
170  [ #SUCC whd in ⊢ (? → ??%? → ?); #_ #E destruct %1 //
171  | #h * [ #SUCC whd in ⊢ (? → ??%? → ?); #PR' generalize in ⊢ (??(?%)? → ?);
172           lapply (refl ? (try_remove … to_check h))
173           cases (try_remove ????) in ⊢ (???% → %);
174           [ #RM whd in ⊢ (? → ??%? → ?); #H @if_elim
175             [ #H' #E destruct
176             | #H' cases (not_orb ?? H') #H1 #H2 #E destruct @(clbs_checked … SUCC)
177               [ whd in ⊢ (?(?%)); >(proj1 … (try_remove_empty …) RM) //
178               | % #E >E in H1; >(proj2 … (eqb_true …) (refl ??)) *
179               | assumption
180               ]
181             ]
182           | * * #to_check'' #RM #H whd in ⊢ (??%? → ?);
183             @if_elim
184             [ #CS #E destruct @(clbs_cost … SUCC … CS)
185               cases (try_remove_some ?????? RM) * #L #_ #_ whd in ⊢ (?%); >L //
186             | #CS
187               @if_elim
188               [ #IN whd in ⊢ (??%? → ?); #E destruct
189               | #OUT whd in ⊢ (??%? → ?); #H
190                 @(clbs_step … SUCC OUT CS RM) @(IH … H)
191               ]
192             ]
193           ]
194         | #h2 #t #SUCCS whd in ⊢ (? → ??%? → ?); #PR' #E destruct
195           @(clbs_branch … SUCCS)
196         ]
197  ]
198] qed.
199
200lemma check_label_bounded_c : ∀g,CL,checking,checking_tail,to_check,to_check'.
201  check_label_bounded_spec g checking checking_tail to_check to_check' →
202  ∀term_check,TERM,PR.
203  check_label_bounded g CL checking PR checking_tail to_check term_check TERM = Some ? to_check'.
204#g #CL #X1 #X2 #X3 #X4 #X elim X
205[ #l #PR #tl #toch #SUCC
206  * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR
207  whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1
208  whd in ⊢ (??%?); %
209| #l #PR #l' #tl #toch #SUCC #NIN_toch #NEQ #NIN_tl
210  * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR
211  whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1
212  whd in ⊢ (??%?); generalize in ⊢ (??(?%)?);
213  cut (lookup … toch l' = None ?) [ whd in NIN_toch:(?(?%)); cases (lookup ????) in NIN_toch ⊢ %; [ // | * * ] ]
214  #L >(proj2 … (try_remove_empty …) L) #H2
215  whd in ⊢ (??%?); >(proj2 … (eqb_false …) NEQ) >(Prop_notb … NIN_tl)
216  %
217| #l #PR #l' #PR' #tl #toch #SUCC #IN #CS
218  * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR
219  whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1
220  whd in ⊢ (??%?); generalize in ⊢ (??(?%)?);
221  cut (lookup … toch l' = Some ? it) [ whd in IN:(?%); cases (lookup ????) in IN ⊢ %; [ * | * // ] ]
222  #L cases (try_remove_this ????? L) #to_check' #RM >RM #H2
223  whd in ⊢ (??%?); >CS whd in ⊢ (??%?); %
224| #l #PR #l' #PR' #tl #toch #toch' #toch'' #SUCC #NIN #NCS #RM #H #IH
225  * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR
226  whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1
227  whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >RM #H2
228  whd in ⊢ (??%?); >(not_b_to_eq_false ? (Prop_notb ? NCS))
229  whd in ⊢ (??%?); >(not_b_to_eq_false ? (Prop_notb ? NIN))
230  whd in ⊢ (??%?); >(IH term_check' ??) %
231| #l #PR #x #y #zs #tl #toch #SUCC
232  * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR
233  whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1
234  whd in ⊢ (??%?); %
235] qed.
236
237lemma check_label_bounded_subset : ∀g,checking,checking_tail,to_check,to_check'.
238  check_label_bounded_spec g checking checking_tail to_check to_check' →
239  set_subset … to_check' to_check.
240#g #lX #lX' #tX #tX' #S elim S //
241#l #PR #l' #PR' #tl #toch #toch' #toch'' #SC #NI #CS #RM #H #IH
242cases (try_remove_some … toch' RM) * #L1 #L2 #L3
243#id #IN cases (L3 id)
244[ #E destruct whd in ⊢ (?%); >L1 //
245| #L4 whd in ⊢ (?%); >L4 @IH @IN
246] qed.
247
248lemma bound_on_instrs_to_cost_prime : ∀g,l,n.
249  bound_on_instrs_to_cost g l n →
250  bound_on_instrs_to_cost' g l n.
251#g #l #n #H inversion H
252#l' #n' #PR #H' #E1 #E2 #_ destruct
253lapply (refl ? (is_cost_label (lookup_present … g l' PR)))
254cases (is_cost_label ?) in ⊢ (???% → ?); #CS
255[ @boitc_here [ @PR | @eq_true_to_b @CS ]
256| @boitc_later [ @PR | @eq_false_to_notb @CS | @H ]
257] qed.
258
259lemma present_member : ∀tag,A,m,id.
260  present tag A m id → member tag A m id.
261#tag #A #m #id whd in ⊢ (% → ?%); cases (lookup ????) // * #H cases (H (refl ??))
262qed.
263
264(* TODO: move and eliminate dup in Traces.ma *)
265lemma Exists_memb : ∀S:DeqSet. ∀x:S. ∀l:list S.
266  Exists S (λy. y = x) l →
267  x ∈ l.
268#S #x #l elim l
269[ //
270| #h #t #IH
271  normalize lapply (eqb_true … x h)
272  cases (x==h) *
273  [ #E #_ >(E (refl ??)) //
274  | #_ #E * [ #E' destruct lapply (E (refl ??)) #E'' destruct
275            | #H @IH @H
276            ]
277  ]
278] qed.
279
280lemma successors_inv : ∀st,x,y,zs.
281  successors st = x::y::zs →
282  ∃r,l1,l2. st = St_cond r l1 l2.
283* normalize
284#a #b #c #d try #e try #f try #g try #h try #i try #j try #k try #l destruct
285/4/
286qed.
287
288include alias "utilities/deqsets.ma".
289
290lemma after_branch_are_cost_labels : ∀g. ∀CL:graph_closed g.
291  (∀l,PR. well_cost_labelled_statement g (lookup_present … g l PR) (CL l ? (lookup_lookup_present … PR))) →
292  ∀l,PR,x,y,zs. successors (lookup_present … g l PR) = x::y::zs →
293  ∀l'. ∀IN : l' ∈ successors (lookup_present … g l PR).
294  is_cost_label (lookup_present … g l' ?).
295[2: @(successors_present … IN) @(CL l) @lookup_lookup_present ]
296#g #CL #WCL #l #PR #x #y #zs #SUCCS
297cases (successors_inv … SUCCS)
298#r * #l1 * #l2 #E
299#l' #IN generalize in ⊢ (?(?(?????%))); #OR' >E in IN;
300lapply (WCL l PR) generalize in ⊢ (?(???%) → ?); >E in ⊢ (% → % → ?); #LP #WCst
301cases (andb_Prop_true ?? WCst)
302#H1 #H2
303whd in ⊢ (?% → ?); @eqb_elim
304[ 2: #_ #IN lapply (memb_single … IN) ]
305#E destruct //
306qed.
307
308
309lemma check_label_bounded_ok : ∀g,checking,checking_tail,to_check,to_check'.
310  ∀CL:graph_closed g.
311  (∀l,PR. well_cost_labelled_statement g (lookup_present … g l PR) (CL l ? (lookup_lookup_present … PR))) →
312  check_label_bounded_spec g checking checking_tail to_check to_check' →
313  (∀l. l∈g → ¬l ∈ to_check → l≠checking → ¬l∈checking_tail → ∃n. bound_on_instrs_to_cost g l n) →
314  ∀l. l = checking ∨ bool_to_Prop (l∈to_check) →
315  bool_to_Prop (l∈to_check') ∨ ∃n. bound_on_instrs_to_cost g l n.
316#g #X1 #X2 #X3 #X4 #CL #WCL #X elim X
317[ #l #PR #tl #toch #SUCC #INV #l' *
318  [ #E destruct %2 %{1} % [ @PR | >SUCC #l' * ]
319  | #IN %1 @IN
320  ]
321| #l #PR #l' #tl #toch #SUCC #NIN_toch #NEQ #NIN_tl #INV #l'' *
322  [ #E destruct %2
323    cases (INV l' ????)
324    [ #n #B
325      %{(S n)} % [ @PR | >SUCC #l'' * [2: *] #E destruct /2/ ]
326    | @present_member @(successors_present … (CL l ? (lookup_lookup_present … PR)))
327      >SUCC @eq_true_to_b @memb_hd
328    | assumption
329    | assumption
330    | assumption
331    ]
332  | #IN %1 assumption
333  ]
334| #l #PR #l' #PR' #tl #toch #SUCC #IN #CS #INV #l'' *
335  [ #E destruct %2 %{1} % [ // | #l'' >SUCC * [2: *] #E destruct @boitc_here // ]
336  | /2/
337  ]
338| #l #PR #l' #PR' #tl #toch #toch' #toch'' #SUCC #NIN_tl #NCS #RM #H #IH #INV #l'' *
339  [ #E destruct %2 cases (IH ? l' ?)
340    [ #IN @⊥ lapply (check_label_bounded_subset … H l' IN) #IN'
341      cases (try_remove_some ?????? RM) * #_ #L #_ whd in IN':(?%);
342      cases (lookup ????) in IN' L; [ * | * #_ #E destruct ]
343    | * #n #B %{(S n)} % [ // | #l'' >SUCC * [2: *] #E destruct /2/ ]
344    | #l'' #INg #INch' #NEQ #NIN_ltl @(INV l'' INg ???)
345      [ @notb_Prop % #INch @(absurd ?? (Prop_notb … INch'))
346        cases (try_remove_some ?????? RM) * #_ #_ #L
347        cases (L l'') [ #E destruct cases NEQ #X cases (X (refl ??)) ]
348        #L' whd in ⊢ (?%); <L' @INch
349      | % #E destruct cases (Prop_notb … NIN_ltl) #X @X @eq_true_to_b @memb_hd
350      | @notb_Prop @(not_to_not … (Prop_notb … NIN_ltl)) #IN @eq_true_to_b @memb_cons @IN
351      ]
352    | %1 %
353    ]
354  | #IN @(IH ? l'' ?)
355    [ #l''' #INg #NINch' #NEQ #NINtl @INV
356      [ assumption
357      | @notb_Prop @(not_to_not … (Prop_notb … NINch'))
358        cases (try_remove_some ?????? RM) * #L1 #L2 #L3
359        cases (L3 l''')
360        [ #E destruct @⊥ cases NEQ /2/
361        | #L whd in ⊢ (?% → ?%); >L //
362        ]
363      | % #E destruct cases (Prop_notb … NINtl) #X @X @eq_true_to_b @memb_hd
364      | @notb_Prop @(not_to_not … (Prop_notb … NINtl)) #IN @eq_true_to_b @memb_cons @IN
365      ]
366    | cases (try_remove_some ?????? RM) * #L1 #L2 #L3
367      cases (L3 l'') [ #E destruct %1 % | #L %2 whd in ⊢ (?%); <L @IN ]
368    ]
369  ]
370| #l #PR #x #y #zs #tl #toch #SUCCS #INV #l' *
371  [ #E destruct %2 %{1} % [ // ]
372    #l' #EX @boitc_here
373    [ @(successors_present … (CL l ? (lookup_lookup_present … PR)))
374      @Exists_memb @EX
375    | @(after_branch_are_cost_labels … WCL … SUCCS)
376    ]
377  | /2/
378  ]
379] qed.
380
381let rec check_graph_bounded
382  (g : graph statement)
383  (CL : graph_closed g)
384  (to_check : identifier_set LabelTag)
385  (SUB : set_subset … to_check g)
386  (start : label)
387  (PR : present ?? g start)
388  (SMALLER : gt (id_map_size … g) (id_map_size … to_check))
389  (term_check : nat)
390on term_check : gt term_check (id_map_size … to_check) → bool ≝
391match term_check return λx. ge x ? → bool with
392[ O ⇒ λH.⊥
393| S term_check' ⇒ λH.
394  let TERM' ≝ ? in
395  match check_label_bounded g CL start PR [ ] to_check (id_map_size … g) TERM' return λx. check_label_bounded ???????? = x → ? with
396  [ None ⇒ λ_. false
397  | Some to_check' ⇒ λH'.
398    match choose … to_check' return λx. (∀id,a,m'. x = ? → ?) → (∀id,a,m'. x = ? → ?) → (∀id,a,m'. x = ? → ?) → ? with
399    [ None ⇒ λ_.λ_.λ_. true
400    | Some l_to_check'' ⇒ λL,SUB',C.
401        check_graph_bounded g CL (\snd l_to_check'') ? (\fst (\fst l_to_check'')) ?? term_check' ?
402    ] (choose_some … to_check') (choose_some_subset … to_check') (choose_some_card … to_check')
403  ] (refl ??)
404].
405[ 2,3,4,5: cases l_to_check'' in C L SUB' ⊢ %; * #l * #to_check'' #C #L #SUB'
406  lapply (check_label_bounded_subset … (check_label_bounded_s … H')) #SUB''
407]
408[ #id #IN @SUB @SUB'' @(SUB' ??? (refl ??)) @IN
409| @member_present @SUB @SUB'' cases (L ??? (refl ??)) * #L #_ #_ whd in ⊢ (?%); >L //
410| whd <(C ??? (refl ??)) lapply (subset_card … SUB'') #Z @(transitive_le … Z) /2/
411| whd <(C ??? (refl ??)) lapply (subset_card … SUB'') #Z @(transitive_le … Z) /2/
412| /2/
413| @SMALLER
414] qed.
415
416lemma check_graph_bounded_ok : ∀g.∀CL:graph_closed g. ∀term_check,to_check,SUB,start,PR,SMALLER,TERM.
417  (∀l,PR. well_cost_labelled_statement g (lookup_present … g l PR) (CL l ? (lookup_lookup_present … PR))) →
418  check_graph_bounded g CL to_check SUB start PR SMALLER term_check TERM = true →
419  (∀l. l∈g → ¬l∈to_check → l≠start → ∃n. bound_on_instrs_to_cost g l n) →
420  ∀l. l∈g → ∃n. bound_on_instrs_to_cost g l n.
421#g #CL #term_check elim term_check
422[ #to_check #SUB #start #PR #SMALLER #TERM @⊥ inversion TERM #A try #B try #C try #D destruct
423| #term_check' #IH #to_check #SUB #start #PR #SMALLER #TERM #WCL
424  whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
425  cases (check_label_bounded ????????) in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)? → ?);
426  [2:#to_check'] #CHECK_LABEL whd in ⊢ (??%? → ?); [2: #E destruct ]
427  generalize in ⊢ (??(?%??)? → ?); generalize in ⊢ (? → ??(??%?)? → ?); generalize in ⊢ (? → ? → ??(???%)? → ?);
428  lapply (choose_empty … to_check')
429  cases (choose LabelTag unit to_check')
430  [ * #H1 #H1' #H2 #H3 #H4 whd in ⊢ (??%? → ?); #_ #H #l #IN
431    cases (true_or_false_Prop (l∈to_check ∨ l == start))
432    [ #CHECKED cases (check_label_bounded_ok … (check_label_bounded_s … CHECK_LABEL) ? l ?)
433      [ #IN' @⊥ lapply (H1 (refl ??) l) #E whd in IN':(?%); >E in IN'; *
434      | //
435      | //
436      | @WCL
437      | #l' #IN_g #NIN_to_check #NEQ #_ @H //
438      | cases (orb_Prop_true … CHECKED) /2/ #E %1 @(proj1 … (eqb_true …)) @E
439      ]
440    | #NOT @H // [ @notb_Prop @(not_to_not … NOT) /2/ | % #E @(absurd ?? NOT) @orb_Prop_r >(proj2 … (eqb_true …)) // ]
441    ]
442 | * * #next * #to_check'' * #H1 #H1' #H2 #H3 #H4 whd in ⊢ (??%? → ?);
443   #CHECK #H @(IH … CHECK)
444   [ @WCL
445   | #l #INg #NIN'' #NEQ
446     cut (¬l∈to_check') [ @notb_Prop @(not_to_not … (Prop_notb … NIN''))
447                          cases (H4 … (refl ??)) * #L1 #L2 #L3
448                          cases (L3 l) [ #EQ @⊥ @(absurd ?? NEQ) >EQ % | #E whd in ⊢ (?% → ?%); >E // ] ]
449     #NIN'
450      cases (true_or_false_Prop (l∈to_check ∨ l == start))
451      [ #CHECKED cases (check_label_bounded_ok … (check_label_bounded_s … CHECK_LABEL) ? l ?)
452        [ #IN' @⊥ @(absurd … IN' (Prop_notb … NIN'))
453        | //
454        | //
455        | @WCL
456        | #l' #IN_g #NIN_to_check #NEQ #_ @H //
457        | cases (orb_Prop_true … CHECKED) /2/ #E %1 @(proj1 … (eqb_true …)) @E
458        ]
459      | #NOT @H // [ @notb_Prop @(not_to_not … NOT) /2/ | % #E @(absurd ?? NOT) @orb_Prop_r >(proj2 … (eqb_true …)) // ]
460      ]
461   ]
462 ]
463] qed.
464
465(* TODO: move *)
466definition id_set_of_map : ∀tag,A. identifier_map tag A → identifier_set tag ≝
467λtag,A,m. an_id_map tag unit (map … (λ_. it) (match m with [ an_id_map m' ⇒ m'])).
468
469lemma id_set_of_map_subset : ∀tag,A,m.
470  id_set_of_map tag A m ⊆ m.
471#tag #A * #m * #id normalize
472>lookup_opt_map normalize cases (lookup_opt ???) //
473qed.
474
475lemma id_set_of_map_present : ∀tag,A,m,id.
476  present tag A m id ↔ present tag unit (id_set_of_map … m) id.
477#tag #A * #m * #id %
478normalize @not_to_not
479>lookup_opt_map cases (lookup_opt ???) normalize //
480#a #E destruct
481qed.
482
483lemma id_set_of_map_card : ∀tag,A,m.
484  |m| = |id_set_of_map tag A m|.
485#tag #A * #m whd in ⊢ (??%%); >map_size //
486qed.
487
488definition check_sound_cost_fn : internal_function → bool ≝
489λfn.
490  match try_remove … (id_set_of_map … (f_graph fn)) (f_entry fn) return λx. (x = ? → ?) → (∀a,m'. x = ? → ?) → (∀a,m'. x = ? → ?) → ? with
491  [ None ⇒ λEMP. ⊥
492  | Some to_check ⇒ λ_.λCARD,L.
493              check_graph_bounded (f_graph fn) (f_closed fn) (\snd to_check) ? (f_entry fn) ?? (|f_graph fn|) ?
494  ] (proj1 ?? (try_remove_empty LabelTag unit (id_set_of_map … (f_graph fn)) (f_entry fn)))
495    (try_remove_some_card ????)
496    (try_remove_some ????).
497[ cases (f_entry fn) in EMP; #l #PR cases (proj1 … (id_set_of_map_present …) PR) #PR' #H
498  @PR' @H %
499| cases to_check in L ⊢ %; * #m' #L cases (L … (refl ??)) * #L1 #L2 #L3 #id #IN
500  cases (L3 id)
501  [ #E destruct whd in ⊢ (?%); cases (f_entry fn) #l * cases (lookup ????) /2/
502  | #E whd in ⊢ (?%); lapply (id_set_of_map_present … (f_graph fn) id) *
503    whd in match (present ????); whd in match (present ? unit ??);
504    lapply (member_present … IN) whd in match (present ? unit ??); <E
505    cases (lookup … (f_graph fn) id) // #X #_ #Y @⊥ cases (Y X) /2/
506  ]
507| cases (f_entry fn) //
508| 4,5: <id_set_of_map_card in CARD; cases to_check * #m' #CARD >(CARD ?? (refl ??)) //
509] qed.
510
511axiom check_sound_cost_fn_ok : ∀fn.
512  well_cost_labelled_fn fn →
513  bool_to_Prop (check_sound_cost_fn fn) ↔ soundly_labelled_fn fn.
514(*
515#fn #WCL %
516[ whd in ⊢ (?% → %);
517  generalize in ⊢ (?(?%??) → ?); generalize in ⊢ (? → ?(??%?) → ?); generalize in ⊢ (? → ? → ?(???%) → ?);
518  cases (try_remove ????)
519  [ #H1 #H2 #H3 @⊥ cases (f_entry fn) in H3; #l #PR #E
520    lapply (proj1 … (id_set_of_map_present …) PR) whd in ⊢ (% → ?);
521    >(E (refl ??)) * /3/
522  | * * #to_check #H1 #H2 #H3
523    whd in ⊢ (?% → ?); #CHECK
524    #l #PR @(check_graph_bounded_ok … CHECK)
525    [ #l' #PR' cases WCL //
526    | #l' #IN #NIN #NEQ @⊥
527      cases (H1 … (refl ??)) * #L1 #L2 #L3
528      @(absurd ?? (Prop_notb … NIN))
529      cases (L3 l')
530      [ #E >E in NEQ; * #H cases (H (refl ??))
531      | #L whd in ⊢ (?%); <L @present_member @(proj1 … (id_set_of_map_present …))
532        @member_present @IN
533      ]
534    | /2/
535    ]
536  ]
537| TODO
538*)
539
540definition check_cost_program : RTLabs_program → bool ≝
541λp. all ? (λfn. match \snd fn with
542                 [ Internal fn ⇒ check_well_cost_fn fn ∧ check_sound_cost_fn fn
543                 | External _ ⇒ true
544                 ]) (prog_funct … p).
545
546theorem check_cost_program_ok : ∀p. bool_to_Prop (check_cost_program p) ↔ well_cost_labelled_program p.
547#p whd in ⊢ (?(?%)%); %
548[ #H lapply ((proj1 ?? (all_All ???)) H) @All_mp
549  * #id * #fd
550  [ #H cases (andb_Prop_true … H) #W #S
551    lapply (proj1 … (check_well_cost_fn_ok …) W) #W'
552    %
553    [ //
554    | @(proj1 … (check_sound_cost_fn_ok …)) //
555    ]
556  | //
557  ]
558| #H @(proj2 … (all_All …)) @(All_mp … H)
559  * #id * #fd
560  [ * #W #S
561    lapply ((proj2 … (check_well_cost_fn_ok …)) W)
562    lapply ((proj2 … (check_sound_cost_fn_ok …)) S) /2/
563  | //
564  ]
565] qed.
566
Note: See TracBrowser for help on using the repository browser.