source: src/common/LabelledObjects.ma @ 2783

Last change on this file since 2783 was 2767, checked in by mckinna, 7 years ago

WARNING: BIG commit, which pushes code_size_opt check into LIN/LINToASM.ma
following CSC's comment on my previous partial commit
plus rolls all the miscellaneous code motion into the rest of the repo.

suggest REBUILD compiler.ma/correctness.ma from scratch.

File size: 10.3 KB
Line 
1include "utilities/lists.ma".
2include "common/Identifiers.ma".
3
4include alias "arithmetics/nat.ma".
5
6definition labelled_obj ≝ λtag,A.(option (identifier tag)) × A.
7
8definition instruction_matches_identifier ≝
9  λtag,A.
10  λy: identifier tag.
11  λx: labelled_obj tag A.
12    match \fst x with
13    [ None ⇒ false
14    | Some x ⇒ eq_identifier ? x y
15    ].
16
17let rec does_not_occur tag A (id : identifier tag) (l : list (labelled_obj tag A))
18  on l : bool ≝ match l with
19  [ nil ⇒ true
20  | cons x l ⇒ ¬instruction_matches_identifier … id x ∧ does_not_occur tag A id l
21  ].
22
23lemma does_not_occur_append : ∀tag,A,id,l1,l2.
24  does_not_occur tag A id (l1@l2) =
25    (does_not_occur tag A id l1 ∧ does_not_occur tag A id l2).
26#tag #A #id #l1 elim l1
27[ // ]
28#hd #tl #IH #l2 whd in match (does_not_occur ????) in ⊢ (??%%);
29>IH elim (¬instruction_matches_identifier ?? id hd) %
30qed.
31
32lemma does_not_occur_None:
33 ∀tag,A,id,i,list_instr.
34  does_not_occur tag A id (list_instr@[〈None …,i〉]) =
35  does_not_occur tag A id list_instr.
36 #tag #A #id #i #list_instr
37 >does_not_occur_append @commutative_andb
38qed.
39
40lemma does_not_occur_Some:
41 ∀tag,A,id,id',i,list_instr.
42  eq_identifier ? id' id = false →
43   does_not_occur tag A id (list_instr@[〈Some ? id',i〉]) =
44    does_not_occur … id list_instr.
45 #tag #A #id #id' #i #list_instr #eq_id_false
46 >does_not_occur_append >commutative_andb
47 whd in match (does_not_occur ??? [?]);
48 change with (eq_identifier ???) in match (instruction_matches_identifier ????);
49 >eq_id_false
50 %
51qed.
52
53lemma does_not_occur_absurd:
54 ∀tag,A,id,i,list_instr.
55  does_not_occur tag A id (list_instr@[〈Some ? id,i〉]) = false.
56 #tag #A #id #i #list_instr
57 >does_not_occur_append >commutative_andb
58 whd in match (does_not_occur ??? [?]);
59 change with (eq_identifier ???) in match (instruction_matches_identifier ????);
60 >eq_identifier_refl %
61qed.
62
63let rec occurs_exactly_once tag A (id : identifier tag) (l : list (labelled_obj tag A))
64  on l : bool ≝ match l with
65  [ nil ⇒ false
66  | cons x l ⇒
67    if instruction_matches_identifier … id x then
68      does_not_occur … id l
69    else
70      occurs_exactly_once … id l
71  ].
72 
73lemma occurs_exactly_once_append : ∀tag,A,id,l1,l2.
74  occurs_exactly_once tag A id (l1@l2) =
75    ((occurs_exactly_once … id l1 ∧ does_not_occur … id l2) ∨
76     (does_not_occur … id l1 ∧ occurs_exactly_once … id l2)).
77#tag #A #id #l1 elim l1
78[ // ]
79#hd #tl #IH #l2
80whd in match (occurs_exactly_once ????) in ⊢ (??%(?%%));
81whd in match (does_not_occur ????) in ⊢ (???(?%%));
82>does_not_occur_append
83>IH
84elim (instruction_matches_identifier … id hd) normalize nodelta
85>commutative_orb %
86qed.
87
88lemma occurs_exactly_once_None:
89 ∀tag,A,id,i,list_instr.
90  occurs_exactly_once tag A id (list_instr@[〈None …,i〉]) =
91  occurs_exactly_once … id list_instr.
92 #tag #A #id #i #list_instr
93 >occurs_exactly_once_append normalize
94 elim (occurs_exactly_once ?? id list_instr) [%]
95 elim (does_not_occur ?? id list_instr) %
96qed.
97
98lemma occurs_exactly_once_Some:
99 ∀tag,A,id,id',i,prefix.
100  occurs_exactly_once tag A id (prefix@[〈Some ? id',i〉]) → eq_identifier ? id' id ∨ occurs_exactly_once … id prefix.
101 #tag #A #id #id' #i #prefix
102 >occurs_exactly_once_append #H elim(orb_Prop_true ?? H) -H
103 #H elim (andb_Prop_true ?? H) -H
104 [ whd in match (does_not_occur ????); | whd in match (occurs_exactly_once ????);]
105  change with (eq_identifier ???) in match (instruction_matches_identifier ????);
106  elim (eq_identifier ???) normalize #H * //
107qed.
108
109lemma occurs_exactly_once_Some_stronger:
110  ∀tag,A,id,id',i,prefix.
111    occurs_exactly_once tag A id (prefix@[〈Some ? id',i〉]) →
112    (eq_identifier ? id' id ∧ does_not_occur … id prefix) ∨
113    (¬eq_identifier ? id' id ∧ occurs_exactly_once … id prefix).
114 #tag #A #id #id' #i #prefix
115 >occurs_exactly_once_append
116 #H elim(orb_Prop_true ?? H) -H
117 #H elim (andb_Prop_true ?? H) -H
118 [ whd in match (does_not_occur ????); | whd in match (occurs_exactly_once ????);]
119  change with (eq_identifier ???) in match (instruction_matches_identifier ????);
120  elim (eq_identifier ???) #H * >H //
121qed.
122
123lemma occurs_exactly_once_Some_eq :
124  ∀tag,A,id,id',i,prefix.
125    occurs_exactly_once tag A id (prefix@[〈Some ? id',i〉]) =
126      if eq_identifier ? id' id then
127        does_not_occur … id prefix
128      else
129        occurs_exactly_once … id prefix.
130 #tag #A #id #id' #i #prefix
131 >occurs_exactly_once_append
132 normalize in match (does_not_occur ????) in ⊢ (??(?%?)?);
133 normalize in match (occurs_exactly_once ????) in ⊢ (??(??%)?);
134 change with (eq_identifier ???) in match (match ? with [an_identifier _ ⇒ ?]) in ⊢ (??(?%%)?);
135 elim (eq_identifier ???)
136 elim (does_not_occur … id prefix)
137 elim (occurs_exactly_once … id prefix) %
138qed.
139
140lemma does_not_occur_occurs_absurd: ∀tag,A,id,list_instr.
141  does_not_occur tag A id list_instr = true →
142  occurs_exactly_once tag A id list_instr = true →
143  False.
144 #tag #A #id #list_instr elim list_instr
145 [ #_ whd in match (occurs_exactly_once ????); #ABS destruct (ABS)
146 | #h #t #Hind whd in match (does_not_occur ????);
147   whd in match (occurs_exactly_once ????);
148   cases (instruction_matches_identifier ?? id h) normalize nodelta
149   [ #ABS destruct (ABS)
150   | @Hind
151   ]
152 ]
153qed.
154
155
156let rec index_of_internal A (test : A → bool) (l : list A) acc on l : ℕ ≝
157  match l with
158  [ nil ⇒ ?
159  | cons x tl ⇒ if test x then acc else index_of_internal A test tl (S acc)
160  ].
161cases not_implemented
162qed.
163
164definition index_of ≝ λA,test,l.index_of_internal A test l 0.
165
166lemma index_of_internal_None: ∀tag,A,i,id,instr_list,n.
167 occurs_exactly_once ?? id (instr_list@[〈None …,i〉]) →
168   index_of_internal ? (instruction_matches_identifier tag A id) instr_list n =
169   index_of_internal ? (instruction_matches_identifier tag A id) (instr_list@[〈None …,i〉]) n.
170 #tag #A #i #id #instr_list >occurs_exactly_once_None
171  elim instr_list
172  [ #n *
173  | #hd #tl #IH #n whd in ⊢ (% → ??%%); whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ?);
174    cases (instruction_matches_identifier ????) normalize nodelta [ #_ % ]
175    #H @(IH ? H)
176  ]
177qed.
178
179lemma index_of_internal_Some_miss: ∀tag,A,i,id,id'.
180 eq_identifier ? id' id = false →
181 ∀instr_list,n.
182 occurs_exactly_once ?? id (instr_list@[〈Some ? id',i〉]) →
183  index_of_internal ? (instruction_matches_identifier tag A id) instr_list n =
184   index_of_internal ? (instruction_matches_identifier ?? id) (instr_list@[〈Some ? id',i〉]) n.
185 #tag #A #i #id #id' #EQ #instr_list #n
186 >occurs_exactly_once_Some_eq >EQ normalize nodelta
187 generalize in match n; -n elim instr_list
188  [ #n *
189  | #hd #tl #IH #n whd in ⊢ (?% → ??%%);
190    cases (instruction_matches_identifier ?? id hd)
191    normalize nodelta
192    [ // | #K @IH //]]
193qed.
194
195lemma index_of_internal_Some_hit: ∀tag,A,i,id.
196 ∀instr_list,n.
197  occurs_exactly_once tag A id (instr_list@[〈Some ? id,i〉]) →
198   index_of_internal ? (instruction_matches_identifier tag A id) (instr_list@[〈Some ? id,i〉]) n
199  = |instr_list| + n.
200 #tag #A #i #id #instr_list #n
201  >occurs_exactly_once_Some_eq >eq_identifier_refl normalize nodelta lapply n -n
202  elim instr_list
203  [ #n #_ whd in ⊢ (??%%); change with (if eq_identifier … id id then ? else ? = ?) >eq_identifier_refl %
204  | #hd #tl #IH #n whd in ⊢ (?% → ??%%);
205    cases (instruction_matches_identifier ?? id hd)
206    normalize nodelta
207    [ * | #H >plus_n_Sm <(IH (S n)) //]]
208qed.
209
210definition index_of_label : ∀tag,A.identifier tag →
211  list (labelled_obj tag A) → ℕ ≝
212  λtag,A,l.index_of ? (instruction_matches_identifier ?? l).
213 
214lemma index_of_label_from_internal : ∀tag,A,id,instrs,n.
215  occurs_exactly_once tag A id instrs →
216    index_of_internal ? (instruction_matches_identifier ?? id) instrs n =
217      n + index_of_label ?? id instrs.
218#tag #A #id #instrs elim instrs
219[ #n *
220| **[2: #lbl] #s #tl #IH #n
221  whd in match (occurs_exactly_once ????);
222  whd in match (index_of_label ????);
223  whd in match (index_of_internal ????);
224  [ change with (eq_identifier ???) in match (instruction_matches_identifier ????);
225    @eq_identifier_elim #Heq normalize nodelta
226    [ #_ @plus_n_O ] ]
227  #Htl >(IH ? Htl) >(IH ? Htl)
228  [ generalize in match (index_of_label ?? id tl);
229  | generalize in match (index_of_label ?? id tl);
230  ] /2 by plus_minus_m_m/
231]
232qed.
233 
234lemma index_of_label_nth_opt : ∀tag,A,id,instrs.
235  occurs_exactly_once tag A id instrs →
236    ∃s.nth_opt ? (index_of_label tag A id instrs) instrs = Some ? 〈Some ? id, s〉.
237#tag #A #id #instrs elim instrs
238[ *
239| * * [2: #lbl] #s #tl #IH
240  whd in match (occurs_exactly_once ????);
241  whd in match (index_of_label ????);
242  [ change with (eq_identifier ???) in match (instruction_matches_identifier ????);
243    @eq_identifier_elim #Heq normalize nodelta
244    [ #_ %{s} >Heq % ] ]
245  #occ_once_tl
246  >(index_of_label_from_internal … occ_once_tl)
247  whd in match (nth_opt ???);
248  @IH assumption
249]
250qed.
251
252lemma does_not_occur_All : ∀tag,A,id,instrs.does_not_occur tag A id instrs →
253  All ? (λls.¬(bool_to_Prop (instruction_matches_identifier tag A id ls))) instrs.
254#tag #A #id #instrs elim instrs
255[ * %
256| * * [2: #lbl] #s #tl #IH
257  whd in match (does_not_occur ????);
258  #H %
259  [1: lapply H -H
260    change with (eq_identifier ???) in match (instruction_matches_identifier ????);
261    @eq_identifier_elim #Heq normalize nodelta [1,3:* |*: #_ % *]
262  |3: % *
263  |*: @IH
264    [elim (¬(instruction_matches_identifier ????)) in H; normalize nodelta [ #H | *]]
265    assumption
266  ]
267]
268qed.
269
270lemma nth_opt_index_of_label : ∀tag,A,id,instrs,n,s.
271  occurs_exactly_once tag A id instrs →
272    nth_opt ? n instrs = Some ? 〈Some ? id, s〉 → index_of_label ?? id instrs = n.
273#tag #A #id #instrs elim instrs
274[ #n #s *
275| * * [2: #lbl] #s #tl #IH #n #s'
276  whd in match (occurs_exactly_once ????);
277  whd in match (index_of_label ????);
278  [ change with (eq_identifier ???) in match (instruction_matches_identifier ????);
279    @eq_identifier_elim #Heq normalize nodelta
280    [ #no_id_in_tl cases n [#_ %] -n #n whd in match (nth_opt ???); #nth_opt_n
281    lapply (All_nth ???? (does_not_occur_All … no_id_in_tl) ? nth_opt_n)
282    change with (eq_identifier ???) in match (instruction_matches_identifier ????);
283    >eq_identifier_refl * #H elim (H I) ] ]
284  #occ_once_tl
285  >(index_of_label_from_internal … occ_once_tl)
286  cases n [2,4: -n #n] whd in match (nth_opt ???);
287  [3,4:  #ABS destruct(ABS) elim Heq #ABS' elim (ABS' ?) %
288  |*: #H >(IH … H) [1,3: %] assumption
289  ]
290]
291qed.
Note: See TracBrowser for help on using the repository browser.