source: src/common/LabelledObjects.ma @ 1971

Last change on this file since 1971 was 1882, checked in by tranquil, 8 years ago

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

File size: 9.8 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
139let rec index_of_internal A (test : A → bool) (l : list A) acc on l : ℕ ≝
140  match l with
141  [ nil ⇒ ?
142  | cons x tl ⇒ if test x then acc else index_of_internal A test tl (S acc)
143  ].
144cases not_implemented
145qed.
146
147definition index_of ≝ λA,test,l.index_of_internal A test l 0.
148
149lemma index_of_internal_None: ∀tag,A,i,id,instr_list,n.
150 occurs_exactly_once ?? id (instr_list@[〈None …,i〉]) →
151   index_of_internal ? (instruction_matches_identifier tag A id) instr_list n =
152   index_of_internal ? (instruction_matches_identifier tag A id) (instr_list@[〈None …,i〉]) n.
153 #tag #A #i #id #instr_list >occurs_exactly_once_None
154  elim instr_list
155  [ #n *
156  | #hd #tl #IH #n whd in ⊢ (% → ??%%); whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ?);
157    cases (instruction_matches_identifier ????) normalize nodelta [ #_ % ]
158    #H @(IH ? H)
159  ]
160qed.
161
162lemma index_of_internal_Some_miss: ∀tag,A,i,id,id'.
163 eq_identifier ? id' id = false →
164 ∀instr_list,n.
165 occurs_exactly_once ?? id (instr_list@[〈Some ? id',i〉]) →
166  index_of_internal ? (instruction_matches_identifier tag A id) instr_list n =
167   index_of_internal ? (instruction_matches_identifier ?? id) (instr_list@[〈Some ? id',i〉]) n.
168 #tag #A #i #id #id' #EQ #instr_list #n
169 >occurs_exactly_once_Some_eq >EQ normalize nodelta
170 generalize in match n; -n elim instr_list
171  [ #n *
172  | #hd #tl #IH #n whd in ⊢ (?% → ??%%);
173    cases (instruction_matches_identifier ?? id hd)
174    normalize nodelta
175    [ // | #K @IH //]]
176qed.
177
178lemma index_of_internal_Some_hit: ∀tag,A,i,id.
179 ∀instr_list,n.
180  occurs_exactly_once tag A id (instr_list@[〈Some ? id,i〉]) →
181   index_of_internal ? (instruction_matches_identifier tag A id) (instr_list@[〈Some ? id,i〉]) n
182  = |instr_list| + n.
183 #tag #A #i #id #instr_list #n
184  >occurs_exactly_once_Some_eq >eq_identifier_refl normalize nodelta lapply n -n
185  elim instr_list
186  [ #n #_ whd in ⊢ (??%%); change with (if eq_identifier … id id then ? else ? = ?) >eq_identifier_refl %
187  | #hd #tl #IH #n whd in ⊢ (?% → ??%%);
188    cases (instruction_matches_identifier ?? id hd)
189    normalize nodelta
190    [ * | #H >plus_n_Sm <(IH (S n)) //]]
191qed.
192
193definition index_of_label : ∀tag,A.identifier tag →
194  list (labelled_obj tag A) → ℕ ≝
195  λtag,A,l.index_of ? (instruction_matches_identifier ?? l).
196 
197lemma index_of_label_from_internal : ∀tag,A,id,instrs,n.
198  occurs_exactly_once tag A id instrs →
199    index_of_internal ? (instruction_matches_identifier ?? id) instrs n =
200      n + index_of_label ?? id instrs.
201#tag #A #id #instrs elim instrs
202[ #n *
203| **[2: #lbl] #s #tl #IH #n
204  whd in match (occurs_exactly_once ????);
205  whd in match (index_of_label ????);
206  whd in match (index_of_internal ????);
207  [ change with (eq_identifier ???) in match (instruction_matches_identifier ????);
208    @eq_identifier_elim #Heq normalize nodelta
209    [ #_ @plus_n_O ] ]
210  #Htl >(IH ? Htl) >(IH ? Htl)
211  [ generalize in match (index_of_label ?? id tl);
212  | generalize in match (index_of_label ?? id tl);
213  ] /2 by plus_minus_m_m/
214]
215qed.
216 
217lemma index_of_label_nth_opt : ∀tag,A,id,instrs.
218  occurs_exactly_once tag A id instrs →
219    ∃s.nth_opt ? (index_of_label tag A id instrs) instrs = Some ? 〈Some ? id, s〉.
220#tag #A #id #instrs elim instrs
221[ *
222| * * [2: #lbl] #s #tl #IH
223  whd in match (occurs_exactly_once ????);
224  whd in match (index_of_label ????);
225  [ change with (eq_identifier ???) in match (instruction_matches_identifier ????);
226    @eq_identifier_elim #Heq normalize nodelta
227    [ #_ %{s} >Heq % ] ]
228  #occ_once_tl
229  >(index_of_label_from_internal … occ_once_tl)
230  whd in match (nth_opt ???);
231  @IH assumption
232]
233qed.
234
235lemma does_not_occur_All : ∀tag,A,id,instrs.does_not_occur tag A id instrs →
236  All ? (λls.¬(bool_to_Prop (instruction_matches_identifier tag A id ls))) instrs.
237#tag #A #id #instrs elim instrs
238[ * %
239| * * [2: #lbl] #s #tl #IH
240  whd in match (does_not_occur ????);
241  #H %
242  [1: lapply H -H
243    change with (eq_identifier ???) in match (instruction_matches_identifier ????);
244    @eq_identifier_elim #Heq normalize nodelta [1,3:* |*: #_ % *]
245  |3: % *
246  |*: @IH
247    [elim (¬(instruction_matches_identifier ????)) in H; normalize nodelta [ #H | *]]
248    assumption
249  ]
250]
251qed.
252
253lemma nth_opt_index_of_label : ∀tag,A,id,instrs,n,s.
254  occurs_exactly_once tag A id instrs →
255    nth_opt ? n instrs = Some ? 〈Some ? id, s〉 → index_of_label ?? id instrs = n.
256#tag #A #id #instrs elim instrs
257[ #n #s *
258| * * [2: #lbl] #s #tl #IH #n #s'
259  whd in match (occurs_exactly_once ????);
260  whd in match (index_of_label ????);
261  [ change with (eq_identifier ???) in match (instruction_matches_identifier ????);
262    @eq_identifier_elim #Heq normalize nodelta
263    [ #no_id_in_tl cases n [#_ %] -n #n whd in match (nth_opt ???); #nth_opt_n
264    lapply (All_nth ???? (does_not_occur_All … no_id_in_tl) ? nth_opt_n)
265    change with (eq_identifier ???) in match (instruction_matches_identifier ????);
266    >eq_identifier_refl * #H elim (H I) ] ]
267  #occ_once_tl
268  >(index_of_label_from_internal … occ_once_tl)
269  cases n [2,4: -n #n] whd in match (nth_opt ???);
270  [3,4:  #ABS destruct(ABS) elim Heq #ABS' elim (ABS' ?) %
271  |*: #H >(IH … H) [1,3: %] assumption
272  ]
273]
274qed.
Note: See TracBrowser for help on using the repository browser.