source: src/RTLabs/CostInj.ma @ 2420

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

Tidy away generic results about folds on positive/identifier maps.

File size: 4.7 KB
RevLine 
[2418]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
50
51lemma reverse_label_map_ok : ∀g,r.
52  reverse_label_map g = r →
53  match r with
54  [ None ⇒ ¬graph_cost_injectivity g
55  | Some m ⇒ graph_cost_injectivity g
56  ].
57#g #r #F change with (foldi ??????) in F:(??%?);
58lapply (foldi_ind' ??????? (λm,ls.
59  match m with
60  [ None ⇒ ¬(graph_cost_injectivity g)
61  | Some m ⇒ ∀l,cl. (present ?? ls l ∧ ∃PR. cost_label_of (lookup_present ?? g l PR) = Some ? cl) ↔ lookup ?? m cl = Some ? l
62  ]) ?? F)
63[ #l #ls #s *
64  [ #FR #L #H whd in H ⊢ %; @H
65  | #m #FR #L #H whd in H ⊢ (match % with [_⇒?|_⇒?]);
66    lapply (refl ? (cost_label_of s)) cases (cost_label_of s) in ⊢ (???% → %);
67    [ #NCS whd #l' #cl cases (H l' cl) #H1 #H2 %
68      [ * #H3 * #PR' #H4 cases (present_add_cases ?????? H3)
69        [ #E destruct @⊥ >(lookup_present_eq ????? L ?) in H4; >NCS #E destruct
70        | * #_ #PR'' @H1 /3/
71        ]
72      | #Lcl cases (H2 Lcl) #PR'' * #PR''' #CS % /2/
73      ]
74    | #cl #CL whd in  ⊢ (match % with [_⇒?|_⇒?]);
75      lapply (refl ? (lookup ?? m cl)) cases (lookup ?? m cl) in ⊢ (???% → %);
76      [ #Lcl whd #l' #cl' cases (H l' cl') #H1 #H2 %
77        [ * #H3 * #PRg' #H4 cases (present_add_cases ?????? H3)
78          [ #E destruct >(lookup_present_eq ????? L ?) in H4; >CL #E destruct
79            @lookup_add_hit
80          | * #NE #PR'' lapply (H1 ?) [/3/] #Lcl' >lookup_add_miss [ // | % #E destruct >Lcl in Lcl'; #E destruct ]
81          ]
82        | #Lcl' cases (lookup_add_cases ??????? Lcl')
83          [ * #E1 #E2 destruct % [ @present_add_hit | %{(lookup_is_present … L)} >(lookup_present_eq ????? L ?) assumption ]
84          | #Lcl'' cases (H2 Lcl'') /3/
85          ]
86        ]
87      | #l' #L' whd % #GCI whd in GCI;
88        cases (H l' cl) #H1 #H2 cases (H2 L') #PR' * #PRg' #CS'
89        lapply (GCI l l' (lookup_is_present … L) PRg' cl ??)
90        [ assumption
91        | >(lookup_present_eq ????? L ?) assumption
92        | #E destruct /2/
93        ]
94      ]
95    ]
96  ]
97| whd #l #cl %
98  [ * * #H cases (H (refl ??))
99  | #E normalize in E; destruct
100  ]
101| cases r
102  [ //
103  | #m whd in ⊢ (% → %); #H
104    #l1 #l2 #PR1 #PR2 #cl #CL1 #CL2
105    cases (H l1 cl) #H1 #_ lapply (H1 ?) [ % [ @(proj1 … (domain_of_map_present … )) // | %{PR1} @CL1 ] ]
106    cases (H l2 cl) #H2 #_ lapply (H2 ?) [ % [ @(proj1 … (domain_of_map_present … )) // | %{PR2} @CL2 ] ]
107    #E >E #E' destruct %
108  ]
109] qed.
110
111lemma check_fun_inj_ok : ∀f. bool_to_Prop (check_fun_inj f) ↔ function_cost_injectivity f.
112#f %
113[ whd in ⊢ (?% → ?);
114  lapply (reverse_label_map_ok (f_graph f))
115  cases (reverse_label_map ?)
116  [ #_ *
117  | #m #H #_ @(H (Some ? m)) %
118  ]
119| lapply (reverse_label_map_ok (f_graph f))
120  whd in ⊢ (? → ? → ?%);
121  cases (reverse_label_map ?)
122  [ #H #INJ @(absurd … INJ (H (None ?) (refl ??)))
123  | //
124  ]
125] qed.
126
127definition check_program_cost_injectivity : RTLabs_program → bool ≝
128λp. all ? (λx. match \snd x with [ Internal f ⇒ check_fun_inj f | _ ⇒ true ]) (prog_funct … p).
129
130theorem check_project_cost_injectivity_ok : ∀p.
131  bool_to_Prop (check_program_cost_injectivity p) ↔ program_cost_injectivity p.
132#p %
133[ #H whd in H:(?%) ⊢ %;
134  @(All_mp ????? (proj1 … (all_All …) H))
135  * #_ * // #f @(proj1 … (check_fun_inj_ok f))
136| whd in ⊢ (% → ?%);
137  #H
138  @(proj2 … (all_All …))
139  @(All_mp … H)
140  * #_ * // #f
141  @(proj2 … (check_fun_inj_ok f))
142] qed.
143
144
145
Note: See TracBrowser for help on using the repository browser.