source: src/RTLabs/CostInj.ma @ 2418

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

Add a checking function for the uniqueness of cost labels in RTLabs
programs.

File size: 11.7 KB
Line 
1include "RTLabs/Traces.ma".
2
3(* Check that the RTLabs pc → cost label map is injective for a given RTLabs
4   program.
5   
6   First we check functions individually, then lift to the whole program. *)
7
8definition graph_cost_injectivity : graph statement → Prop ≝
9λg. ∀l1,l2,PR1,PR2,cl.
10  cost_label_of (lookup_present ?? g l1 PR1) = Some ? cl →
11  cost_label_of (lookup_present ?? g l2 PR2) = Some ? cl →
12  l1 = l2.
13
14definition function_cost_injectivity ≝
15λf. graph_cost_injectivity (f_graph f).
16
17definition program_cost_injectivity : RTLabs_program → Prop ≝
18λp. All ? (λx. match \snd x with [ Internal f ⇒ function_cost_injectivity f | _ ⇒ True]) (prog_funct … p).
19
20definition reverse_label_map : graph statement → (option (identifier_map CostTag (identifier LabelTag))) ≝
21λg.
22  foldi
23    statement
24    (option (identifier_map CostTag (identifier LabelTag)))
25    LabelTag
26    (λl,s,m.
27      match m with
28      [ None ⇒ None ?
29      | Some m ⇒
30        match cost_label_of s with
31        [ Some cl ⇒
32          match lookup ?? m cl with
33          [ None ⇒ Some ? (add … m cl l)
34          | Some _ ⇒ None ?
35          ]
36        | None ⇒ Some ? m
37        ]
38      ])
39    g
40    (Some ? (empty_map …)).
41
42
43definition check_fun_inj : internal_function → bool ≝
44λf.
45match reverse_label_map (f_graph f) with
46[ None ⇒ false
47| Some _ ⇒ true
48].
49
50definition domain_of_pm : ∀A. positive_map A → positive_map unit ≝
51λA,t. fold A (positive_map unit) (λp,a,b. insert unit p it b) t (pm_leaf unit).
52
53lemma pm_fold_ignore_adding_junk : ∀A. ∀m. ∀f,g:Pos → Pos. ∀s.
54  (∀p,q. f p ≠ g q) →
55  ∀p. lookup_opt unit (f p) (fold A ? (λx,a,b. insert unit (g x) it b) m s) = lookup_opt unit (f p) s.
56#A #m elim m
57[ normalize //
58| #oa #l #r #IHl #IHr
59  #f #g #s #not_g #p
60  normalize
61  >IHr
62  [ >IHl
63    [ cases oa
64      [ normalize %
65      | #a normalize >(lookup_opt_insert_miss ?? (f p)) [ % | @not_g ]
66      ]
67    | #x #y % #E cases (not_g x (p0 y)) #H @H @E
68    ]
69  | #x #y % #E cases (not_g x (p1 y)) #H @H @E
70  ]
71] qed.
72
73lemma pm_fold_ind_gen : ∀A,B,m,f,b.
74  ∀pre:Pos→Pos. (∀x,y.pre x = pre y → x = y) → ∀ps. (∀p. lookup_opt ? (pre p) ps = None ?) →
75  ∀P:B → positive_map unit → Prop.
76  P b ps →
77  (∀p,ps,a,b. lookup_opt unit (pre p) ps = None unit → lookup_opt A p m = Some A a → P b ps → P (f (pre p) a b) (insert unit (pre p) it ps)) →
78  P (fold A B (λx. f (pre x)) m b) (fold ?? (λp,a,b. insert unit (pre p) it b) m ps).
79#A #B #m elim m
80[ //
81| #oa #l #r #IHl #IHr
82  #f #b #pre #PRE #ps #PS #P #emp #step whd in ⊢ (?%%);
83  @IHr
84  [ #x #y #E lapply (PRE … E) #E' destruct //
85  | #p change with ((λx. pre (p1 x)) p) in match (pre (p1 p)); >pm_fold_ignore_adding_junk
86    [ cases oa [ @PS | #a >(lookup_opt_insert_miss ?? (pre (p1 p))) [ @PS | % #E lapply (PRE … E) #E' destruct ] ]
87    | #p #q % #E lapply (PRE … E) #E' destruct
88    ]
89  | @IHl
90    [ #x #y #E lapply (PRE … E) #E' destruct //
91    | #p cases oa [ @PS | #a >(lookup_opt_insert_miss ?? (pre (p0 p))) [ @PS | % #E lapply (PRE … E) #E' destruct ] ]
92    | cases oa in step ⊢ %; [ #_ @emp | #a #step normalize @step [ @PS | % | @emp ] ]
93    | #p #ps' #a #b' @step
94    ]
95  | #p #ps' #a #b' @step
96  ]
97] qed.
98
99lemma pm_fold_ext : ∀A,B,m,f,b.
100  fold A B f m b = fold A B (λx:Pos. f x) m b.
101#A #B #m elim m /4/
102qed.
103
104lemma pm_fold_ind : ∀A,B,f,m,b. ∀P:B → positive_map unit → Prop.
105  P b (pm_leaf unit) →
106  (∀p,ps,a,b. lookup_opt unit p ps = None unit → lookup_opt A p m = Some A a → P b ps → P (f p a b) (insert unit p it ps)) →
107  P (fold A B f m b) (domain_of_pm A m).
108#A #B #f #m #b #P #emp #step
109>pm_fold_ext
110whd in ⊢ (??%);
111@(pm_fold_ind_gen A B m f b (λx.x) ? (pm_leaf unit) ???)
112[ //
113| //
114| @emp
115| @step
116] qed.
117
118lemma pm_fold_eq : ∀A,B,b,f.
119  (∀p,k:Pos. ∀a,s1,s2. lookup_opt B p s1 = lookup_opt B p s2 → lookup_opt B p (f k a s1) = lookup_opt B p (f k a s2)) →
120  ∀p,s1,s2.
121  lookup_opt B p s1 = lookup_opt B p s2 →
122  lookup_opt B p (fold A (positive_map B) f b s1) = lookup_opt B p (fold A (positive_map B) f b s2).
123#A #B #b elim b
124[ #f #H #p #s1 #s2 #H @H
125| #oa #l #r #IHl #IHr #f #H #p #s1 #s2 #H'
126  whd in match (fold ???? s1);
127  whd in match (fold ???? s2);
128  @IHr [ #q #k #a #s1' #s2' #H'' @H @H'' ]
129  @IHl [ #q #k #a #s1' #s2' #H'' @H @H'' ]
130  cases oa [ @H' | #a @H @H' ]
131] qed.
132
133
134
135lemma pm_fold_ignore_prefix : ∀A. ∀m. ∀pre:Pos → Pos. (∀x,y. pre x = pre y → x = y) →
136  ∀p. ∀pre'.
137      lookup_opt unit (pre p) (fold A ? (λx,a,b. insert unit (pre (pre' x)) it b) m (pm_leaf ?)) =
138      lookup_opt unit p (fold A ? (λx,a,b. insert unit (pre' x) it b) m (pm_leaf ?)).
139#A #m #pre #PRE
140cut (∀p. lookup_opt unit (pre p) (pm_leaf unit) = lookup_opt unit p (pm_leaf unit)) [ // ]
141generalize in match (pm_leaf unit) in ⊢ ((? → ??%?) → ? → ? → ??%?);
142generalize in match (pm_leaf unit);
143elim m
144[ #s1 #s2 #S #p #pre' @S
145| #oa #l #r #IHl #IHr
146  #s1 #s2 #S #p #pre'
147  whd in ⊢ (??(???%)(???%));
148  @(IHr ???? (λx. pre' (p1 x)))
149  #p' @IHl
150  #p'' cases oa
151  [ @S
152  | #a cases (decidable_eq_pos p'' (pre' one))
153    [ #E destruct
154      >(lookup_opt_insert_hit ?? (pre (pre' one)))
155      >(lookup_opt_insert_hit ?? (pre' one))
156      %
157    | #NE >(lookup_opt_insert_miss ??? (pre (pre' one)))
158      [ >(lookup_opt_insert_miss ??? (pre' one)) //
159      | % #E @(absurd … (PRE … E) NE)
160      ]
161    ]
162  ]
163] qed.
164
165lemma domain_of_pm_present : ∀A,m,p.
166  lookup_opt A p m ≠ None ? ↔ lookup_opt unit p (domain_of_pm A m) ≠ None ?.
167
168#A #m whd in match (domain_of_pm ??);
169elim m
170[ #p normalize /3/
171| #oa #l #r #IHl #IHr
172  whd in match (fold ???? (pm_leaf unit));
173  *
174  [ change with ((λx:Pos. one) one) in ⊢ (??(?(??(??%?)?)));
175    >pm_fold_ignore_adding_junk [2: #p #q % #E destruct ]
176    change with ((λx:Pos. one) one) in ⊢ (??(?(??(??%?)?)));
177    >pm_fold_ignore_adding_junk [2: #p #q % #E destruct ]
178    cases oa
179    [ normalize /3/
180    | #a change with (insert unit one ??) in ⊢ (??(?(??(???%)?)));
181      >(lookup_opt_insert_hit ?? one) normalize
182      % #_ % #E destruct
183    ]
184  | #p >(pm_fold_eq ??????? (pm_leaf unit))
185    [ >pm_fold_ignore_prefix [2: #x #y #E destruct % ]
186      @IHr
187    | >pm_fold_ignore_adding_junk [2: #x #y % #E destruct ]
188      cases oa
189      [ %
190      | #a >(lookup_opt_insert_miss ?? (p1 p)) [2: % #E destruct ]
191        %
192      ]
193    | #x #y #a #s1 #s2 #S cases (decidable_eq_pos x (p1 y))
194      [ #E destruct
195        >(lookup_opt_insert_hit ?? (p1 y))
196        >(lookup_opt_insert_hit ?? (p1 y))
197        %
198      | #NE >(lookup_opt_insert_miss ?? x … NE)
199        >(lookup_opt_insert_miss ?? x … NE)
200        @S
201      ]
202    ] 
203  | #p
204    >pm_fold_ignore_adding_junk [2: #x #y % #E destruct ]
205    >(pm_fold_eq ??????? (pm_leaf unit))
206    [ >pm_fold_ignore_prefix [2: #x #y #E destruct % ]
207      @IHl
208    | cases oa
209      [ %
210      | #a >(lookup_opt_insert_miss ?? (p0 p)) [2: % #E destruct ]
211        %
212      ]
213    | #x #y #a #s1 #s2 #S cases (decidable_eq_pos x (p0 y))
214      [ #E destruct
215        >(lookup_opt_insert_hit ?? (p0 y))
216        >(lookup_opt_insert_hit ?? (p0 y))
217        %
218      | #NE >(lookup_opt_insert_miss ?? x … NE)
219        >(lookup_opt_insert_miss ?? x … NE)
220        @S
221      ]
222    ]
223  ]
224] qed.
225
226
227(* Returns the domain of a map as the canonical set (one made only from the
228   empty set and addition. *)
229definition domain_of_map : ∀tag,A. identifier_map tag A → identifier_set tag ≝
230λtag,A,m. an_id_map tag unit (domain_of_pm A (match m with [ an_id_map m ⇒ m ])).
231lemma domain_of_map_present : ∀tag,A,m,id.
232  present tag A m id ↔ present tag unit (domain_of_map … m) id.
233#tag #A * #m * #p @domain_of_pm_present
234qed.
235
236lemma foldi_ind : ∀A,B,tag,f,m,b. ∀P:B → identifier_set tag → Prop.
237  P b (empty_set …) →
238  (∀k,ks,a,b. ¬present ?? ks k → lookup ?? m k = Some ? a → P b ks → P (f k a b) (add_set tag ks k)) →
239  P (foldi A B tag f m b) (domain_of_map … m).
240#A #B #tag #f * #m #b #P #P0 #STEP
241whd in match (foldi ??????); change with (an_id_map ?? (domain_of_pm A m)) in match (domain_of_map ???);
242@pm_fold_ind
243[ @P0
244| #p #ps #a #b0 #FR #L #pre @(STEP (an_identifier tag p) (an_id_map tag unit ps))
245  [ normalize >FR /3/
246  | @L
247  | @pre
248  ]
249] qed.
250
251lemma foldi_ind' : ∀A,B,tag,f,m,b,b'. ∀P:B → identifier_set tag → Prop.
252  P b (empty_set …) →
253  (∀k,ks,a,b. ¬present ?? ks k → lookup ?? m k = Some ? a → P b ks → P (f k a b) (add_set tag ks k)) →
254  foldi A B tag f m b = b' →
255  P b' (domain_of_map … m).
256#H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11  destruct @foldi_ind /2/
257qed.
258
259lemma reverse_label_map_ok : ∀g,r.
260  reverse_label_map g = r →
261  match r with
262  [ None ⇒ ¬graph_cost_injectivity g
263  | Some m ⇒ graph_cost_injectivity g
264  ].
265#g #r #F change with (foldi ??????) in F:(??%?);
266lapply (foldi_ind' ??????? (λm,ls.
267  match m with
268  [ None ⇒ ¬(graph_cost_injectivity g)
269  | Some m ⇒ ∀l,cl. (present ?? ls l ∧ ∃PR. cost_label_of (lookup_present ?? g l PR) = Some ? cl) ↔ lookup ?? m cl = Some ? l
270  ]) ?? F)
271[ #l #ls #s *
272  [ #FR #L #H whd in H ⊢ %; @H
273  | #m #FR #L #H whd in H ⊢ (match % with [_⇒?|_⇒?]);
274    lapply (refl ? (cost_label_of s)) cases (cost_label_of s) in ⊢ (???% → %);
275    [ #NCS whd #l' #cl cases (H l' cl) #H1 #H2 %
276      [ * #H3 * #PR' #H4 cases (present_add_cases ?????? H3)
277        [ #E destruct @⊥ >(lookup_present_eq ????? L ?) in H4; >NCS #E destruct
278        | * #_ #PR'' @H1 /3/
279        ]
280      | #Lcl cases (H2 Lcl) #PR'' * #PR''' #CS % /2/
281      ]
282    | #cl #CL whd in  ⊢ (match % with [_⇒?|_⇒?]);
283      lapply (refl ? (lookup ?? m cl)) cases (lookup ?? m cl) in ⊢ (???% → %);
284      [ #Lcl whd #l' #cl' cases (H l' cl') #H1 #H2 %
285        [ * #H3 * #PRg' #H4 cases (present_add_cases ?????? H3)
286          [ #E destruct >(lookup_present_eq ????? L ?) in H4; >CL #E destruct
287            @lookup_add_hit
288          | * #NE #PR'' lapply (H1 ?) [/3/] #Lcl' >lookup_add_miss [ // | % #E destruct >Lcl in Lcl'; #E destruct ]
289          ]
290        | #Lcl' cases (lookup_add_cases ??????? Lcl')
291          [ * #E1 #E2 destruct % [ @present_add_hit | %{(lookup_is_present … L)} >(lookup_present_eq ????? L ?) assumption ]
292          | #Lcl'' cases (H2 Lcl'') /3/
293          ]
294        ]
295      | #l' #L' whd % #GCI whd in GCI;
296        cases (H l' cl) #H1 #H2 cases (H2 L') #PR' * #PRg' #CS'
297        lapply (GCI l l' (lookup_is_present … L) PRg' cl ??)
298        [ assumption
299        | >(lookup_present_eq ????? L ?) assumption
300        | #E destruct /2/
301        ]
302      ]
303    ]
304  ]
305| whd #l #cl %
306  [ * * #H cases (H (refl ??))
307  | #E normalize in E; destruct
308  ]
309| cases r
310  [ //
311  | #m whd in ⊢ (% → %); #H
312    #l1 #l2 #PR1 #PR2 #cl #CL1 #CL2
313    cases (H l1 cl) #H1 #_ lapply (H1 ?) [ % [ @(proj1 … (domain_of_map_present … )) // | %{PR1} @CL1 ] ]
314    cases (H l2 cl) #H2 #_ lapply (H2 ?) [ % [ @(proj1 … (domain_of_map_present … )) // | %{PR2} @CL2 ] ]
315    #E >E #E' destruct %
316  ]
317] qed.
318
319lemma check_fun_inj_ok : ∀f. bool_to_Prop (check_fun_inj f) ↔ function_cost_injectivity f.
320#f %
321[ whd in ⊢ (?% → ?);
322  lapply (reverse_label_map_ok (f_graph f))
323  cases (reverse_label_map ?)
324  [ #_ *
325  | #m #H #_ @(H (Some ? m)) %
326  ]
327| lapply (reverse_label_map_ok (f_graph f))
328  whd in ⊢ (? → ? → ?%);
329  cases (reverse_label_map ?)
330  [ #H #INJ @(absurd … INJ (H (None ?) (refl ??)))
331  | //
332  ]
333] qed.
334
335definition check_program_cost_injectivity : RTLabs_program → bool ≝
336λp. all ? (λx. match \snd x with [ Internal f ⇒ check_fun_inj f | _ ⇒ true ]) (prog_funct … p).
337
338theorem check_project_cost_injectivity_ok : ∀p.
339  bool_to_Prop (check_program_cost_injectivity p) ↔ program_cost_injectivity p.
340#p %
341[ #H whd in H:(?%) ⊢ %;
342  @(All_mp ????? (proj1 … (all_All …) H))
343  * #_ * // #f @(proj1 … (check_fun_inj_ok f))
344| whd in ⊢ (% → ?%);
345  #H
346  @(proj2 … (all_All …))
347  @(All_mp … H)
348  * #_ * // #f
349  @(proj2 … (check_fun_inj_ok f))
350] qed.
351
352
353
Note: See TracBrowser for help on using the repository browser.