source: src/RTLabs/CostCheck.ma @ 2303

Last change on this file since 2303 was 2303, checked in by campbell, 8 years ago

Some preliminary checking of cost labelling properties in RTLabs.

File size: 2.3 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 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
49axiom check_sound_cost_fn : internal_function → bool.
50axiom check_sound_cost_fn_ok : ∀fn. bool_to_Prop (check_sound_cost_fn fn) ↔ soundly_labelled_fn fn.
51
52definition 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
58theorem 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
Note: See TracBrowser for help on using the repository browser.