source: src/common/LabelledObjects.ma @ 2474

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