1 | |
---|
2 | include "RTLabs/CostSpec.ma". |
---|
3 | |
---|
4 | (* TODO: move ----→ *) |
---|
5 | |
---|
6 | lemma 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 ] ] |
---|
10 | qed. |
---|
11 | |
---|
12 | let rec all (A:Type[0]) (P:A → bool) (l:list A) on l : bool ≝ |
---|
13 | match l with |
---|
14 | [ nil ⇒ true |
---|
15 | | cons h t ⇒ P h ∧ all A P t |
---|
16 | ]. |
---|
17 | |
---|
18 | lemma 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 | |
---|
29 | definition check_well_cost_fn : internal_function → bool ≝ |
---|
30 | λf. |
---|
31 | idmap_all … (f_graph f) (λl,s,PR. well_cost_labelled_statement f s (f_closed f l s PR)) ∧ |
---|
32 | is_cost_label (lookup_present … (f_graph f) (f_entry f) ?). |
---|
33 | cases (f_entry f) // |
---|
34 | qed. |
---|
35 | |
---|
36 | lemma 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 | |
---|
49 | axiom check_sound_cost_fn : internal_function → bool. |
---|
50 | axiom check_sound_cost_fn_ok : ∀fn. bool_to_Prop (check_sound_cost_fn fn) ↔ soundly_labelled_fn fn. |
---|
51 | |
---|
52 | definition check_cost_program : RTLabs_program → bool ≝ |
---|
53 | λp. all ? (λfn. match \snd fn with |
---|
54 | [ Internal fn ⇒ check_well_cost_fn fn ∧ check_sound_cost_fn fn |
---|
55 | | External _ ⇒ true |
---|
56 | ]) (prog_funct … p). |
---|
57 | |
---|
58 | theorem check_cost_program_ok : ∀p. bool_to_Prop (check_cost_program p) ↔ well_cost_labelled_program p. |
---|
59 | #p whd in ⊢ (?(?%)%); % |
---|
60 | [ #H lapply ((proj1 ?? (all_All ???)) H) @All_mp |
---|
61 | * #id * #fd |
---|
62 | [ #H cases (andb_Prop_true … H) #W #S % |
---|
63 | [ @(proj1 … (check_well_cost_fn_ok … )) // |
---|
64 | | @(proj1 … (check_sound_cost_fn_ok …)) // |
---|
65 | ] |
---|
66 | | // |
---|
67 | ] |
---|
68 | | #H @(proj2 … (all_All …)) @(All_mp … H) |
---|
69 | * #id * #fd |
---|
70 | [ * #W #S |
---|
71 | lapply ((proj2 … (check_well_cost_fn_ok …)) W) |
---|
72 | lapply ((proj2 … (check_sound_cost_fn_ok …)) S) /2/ |
---|
73 | | // |
---|
74 | ] |
---|
75 | ] qed. |
---|
76 | |
---|