source: src/common/ExtraIdentifiers.ma @ 3367

Last change on this file since 3367 was 3259, checked in by piccolo, 7 years ago

changed ERTL semantics:
1) added manipulation of stack pointer directly in the semantics
2) added values of Callee Saved in frames

File size: 19.5 KB
Line 
1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "common/Identifiers.ma".
16
17lemma fold_insert_singleton : ∀A,B : Type[0].∀a :A.
18∀i : Pos.∀f,b.
19fold A B f (pm_set A i (Some ? a) (pm_leaf A)) b = f i a b.
20#A #B #a #i elim i -i normalize
21[//] #i #IH #f #b @IH
22qed.
23
24let rec pm_clean (A : Type[0]) (p : positive_map A) on p : positive_map A ≝
25match p with
26[ pm_leaf ⇒ pm_leaf A
27| pm_node a l r ⇒ let l' ≝ pm_clean A l in
28                  let r' ≝ pm_clean A r in
29                  if andb (is_none ? a)
30                      (andb (is_pm_leaf ? l') (is_pm_leaf ? r')) then
31                     pm_leaf A
32                  else
33                     pm_node ? a l' r'
34].
35 
36lemma lookup_pm_clean : ∀A : Type[0].∀p,p' : positive_map A.
37(∀i.lookup_opt A i p = lookup_opt A i p') →
38pm_clean A p = pm_clean A p'.
39#A #p elim p
40[ #p' elim p' [ #_ normalize %] * [2: #a] #l #r #IHl #IHr #H normalize
41  [ lapply(H one) normalize #EQ destruct]
42  <IHl [2,4: #i lapply(H (p0 i)) normalize //] normalize
43  <IHr [2,4: #i lapply(H (p1 i)) normalize //] %
44| #opt_a #l #r #IHl #IHr *
45  [ #H normalize lapply(H one) normalize #EQ destruct(EQ) normalize
46    >(IHl (pm_leaf ?)) [2: #i lapply(H (p0 i)) normalize //] normalize
47    >(IHr (pm_leaf ?)) [2: #i lapply(H (p1 i)) normalize //] %
48  | #opt_a' #l' #r' #H normalize lapply(H one) normalize #EQ destruct(EQ)
49    >(IHl l') [2: #i lapply(H (p0 i)) normalize //]
50    >(IHr r') [2: #i lapply(H (p1 i)) normalize //] %
51  ]
52]
53qed. 
54
55definition pm_find_all : ∀A : Type[0].positive_map A →
56(Pos → A → bool) → positive_map A ≝
57λA,p,P.fold ??
58 (λi,a,p'.if P i a then pm_set ? i (Some ? a) p' else p') p (pm_leaf A).
59 
60
61lemma pm_clean_idempotent : ∀A : Type[0].∀p : positive_map A.
62pm_clean ? p = pm_clean ? (pm_clean ? p).
63cases daemon
64qed.
65
66 
67lemma pm_find_all_canonic : ∀A : Type[0].∀p : positive_map A.∀P.
68pm_find_all A p P = pm_clean A (pm_find_all A p P).
69#A #p #P whd in match pm_find_all; normalize nodelta
70@pm_fold_ind
71[ %] #i #ps #a #b #H #H1 #H2 cases(P i a) normalize
72[2: assumption] lapply H2 lapply b elim i
73[ normalize * [ #_ %] #opt_a #l #r
74  normalize nodelta normalize cases opt_a
75  [2: #a1 normalize #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct >e0 in ⊢ (??%?);
76      >e1 in ⊢ (??%?); % ] normalize
77  cases(pm_clean ? l) normalize [2: #opt_a1 #l1 #r1
78  #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct >e0 in ⊢ (??%?); %]
79  cases(pm_clean ? r) normalize [#EQ destruct] #opt_a1 #l1 #r1
80  #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct %
81|*: #x #IH * normalize
82   [1,3: #_ <IH [2,4: % ]
83    inversion(pm_set A x ??) [2,4: #opt_a1 #l1 #r1 #_#_#_ %]
84    #ABS @⊥ cases x in ABS; [1,4: normalize #EQ destruct] #x1 normalize
85    #EQ destruct
86   |*: * [2,4: #a1] #l #r normalize
87       [1,2: #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct >e0 in ⊢ (??%?);
88             >e1 in ⊢ (??%?); <IH
89             [ @eq_f3 try % >e1 in ⊢ (???%); %
90             | assumption
91             | @eq_f3 try % @pm_clean_idempotent
92             | @pm_clean_idempotent
93             ]
94       |*: inversion(pm_clean A l) normalize
95           [ #H3 inversion(pm_clean A r) normalize [#_ #EQ destruct] #opt_a1 #l1 #r1
96             #_ #_ #H4 #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ  <(IH r)
97             [2: cut(r = pm_node A opt_a1 l1 r1) [ destruct %] #H5
98             >H5 in ⊢ (??%?); <H4 % ] inversion(pm_set A x ??)
99             [2: #opt_a2 #l2 #r2 #_ #_ #_ normalize destruct %]
100             #ABS @⊥ cases x in ABS; normalize cases r normalize
101             [| #z #w1 #w2| #x1 | #z #w1 #w2 #x1 | #x1 | #z #w1 #w2 #x1 ]
102             #EQ1 destruct
103           | #opt_a1 #l1 #r1 #_ #_ #H3 #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
104             <(IH r) [destruct %] destruct assumption
105           | #H3 cases(pm_clean A r) normalize [#EQ destruct] #opt_a1 #l1 #r1
106              #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ <(IH l) [2: >H3 destruct %]
107              inversion(pm_set A x ??)
108              [2: #opt_a2 #l2 #r2 #_ #_ #_ normalize destruct %]
109              #ABS @⊥ cases x in ABS; normalize cases l normalize
110              [| #z #w1 #w2| #x1 | #z #w1 #w2 #x1 | #x1 | #z #w1 #w2 #x1 ]
111              #EQ1 destruct
112           | #opt_a1 #l1 #r1 #_ #_ #H3 #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
113             <(IH l) [2: >H3 destruct %] inversion(pm_set A x ??)
114              [2: #opt_a2 #l2 #r2 #_ #_ #_ normalize destruct >e0 in ⊢ (??%?); %]
115              #ABS @⊥ cases x in ABS; normalize cases l normalize
116              [| #z #w1 #w2| #x1 | #z #w1 #w2 #x1 | #x1 | #z #w1 #w2 #x1 ]
117              #EQ1 destruct
118           ] 
119       ]   
120   ]
121]
122qed. 
123
124
125definition find_all : ∀tag,A. identifier_map tag A →
126(identifier tag → A → bool) → identifier_map tag A ≝
127λtag,A,m,P.match m with
128  [an_id_map p ⇒ an_id_map ?? (pm_find_all A p (λx,a.P (an_identifier tag x) a))].
129(*
130
131lemma find_all_lookup_predicate : ∀tag,A.∀m : identifier_map tag A.
132∀P : (identifier tag → A → bool).∀i,a.
133lookup tag A (find_all tag A m P) i = Some ? a →
134lookup tag A m i = Some ? a  ∧ (bool_to_Prop (P i a)).
135#tag #A * #m #P * #i #a whd in match find_all; normalize @pm_fold_ind
136[ normalize #EQ destruct
137| #k #ks #a1 #b * #H #H1 #H2 inversion(P (an_identifier tag i) a1)
138  [ cases(decidable_eq_pos i k)
139    [#EQ destruct #H3 >H3 in H2; normalize >looku
140
141
142  [#EQ destruct inversion(
143
144  [ #H3 normalize nodelta >H3 cases(decidable_eq_pos i k)
145    [ #EQ destruct >H3 in H2;
146 
147 
148    cut(bool_to_Prop (eq_identifier tag (an_identifier tag i) (an_identifierk) ∨
149     (bool_to_Prop (notb (eq_identifier tag i k))))
150    [@eq_identifier_elim #_ [ %%|%2 %]]
151    @eq_identifier_elim
152    [ #EQ destruct(EQ) #_ >lookup_add_hit #EQ destruct(EQ) %{H1} >H3 @I
153    | #H4 #_ >lookup_add_miss [2: assumption] @H2
154    ]
155  | #H3 normalize nodelta @H2
156  ]
157]
158qed.
159
160
161lemma find_find_all : ∀tag,A.∀m : identifier_map tag A.
162∀P : (identifier tag → A → bool).∀i,a. lookup tag A m i = Some ? a →
163P i a → lookup tag A (find_all tag A m P) i = Some ? a.
164#tag #A #m #P #i #a #H #H1 cut(present tag unit (domain_of_map … m) i)
165[ cases(domain_of_map_present tag A m i) #H2 #_ @H2 whd >H % #EQ destruct]
166whd in match find_all; normalize nodelta @foldi_ind
167[ whd in ⊢ (% → ?); * #H2 @⊥ @H2 %]
168#k #ks #a1 #b * #H2 #H3 #H4 #H5
169cut(bool_to_Prop (eq_identifier tag i k) ∨
170    (bool_to_Prop (notb (eq_identifier tag i k))))
171[ @eq_identifier_elim #_ [ % % | %2 %] ]
172@eq_identifier_elim
173[ #EQ destruct(EQ) #_ >H in H3; #EQ destruct(EQ) >H1 normalize nodelta @lookup_add_hit
174| #EQ #_ cases(P k a1) normalize nodelta
175  [>lookup_add_miss [2: assumption] ]
176  @H4 whd % #H6 elim H5 #H5 @H5 >lookup_add_miss //
177]
178qed.
179*)
180(*
181 whd in match (add ?????); whd in match (add ?????); normalize nodelta
182whd in match (domain_of_map ???); whd in match (domain_of_map ???); normalize nodelta @eq_f
183whd in match (domain_of_pm ??); whd in match (domain_of_pm ??) in ⊢ (???%); *)
184
185
186axiom add_find_all : ∀tag,A.∀m : identifier_map tag A.
187∀P : (identifier tag → A → bool).∀i,a.P i a →
188add tag A (find_all tag A m P) i a = find_all tag A (add tag A m i a) P.
189
190 
191(*Map for identifier_map *)
192definition map : ∀tag,A,B. identifier_map tag A → (A → B) → identifier_map tag B ≝
193λtag,A,B,m,f.match m with
194[an_id_map p ⇒ an_id_map … (map ?? f p)].
195
196lemma lookup_map : ∀A,B : Type[0].
197  ∀tag : identifierTag.
198  ∀m : identifier_map tag A.
199  ∀ f:A → B.
200  ∀ id.
201lookup tag B (map tag A B m f) id =
202! a ← lookup tag A m id; return f a.
203#A #B #tag * #m #f * #id normalize >lookup_opt_map %
204qed.
205
206
207lemma map_add : ∀tag : identifierTag.∀A,B : Type[0].∀ f: A → B.∀m,id,v.
208map tag A B (add tag A m id v) f = add tag B (map tag A B m f) id (f v).
209#tag #A #B #f * #m * #id #v normalize @eq_f lapply v -v lapply id -id elim m
210[ #id elim id [#v %] #x #IH #id normalize >IH normalize inversion(pm_set ? ? ? ?)
211  normalize // cases x normalize [2,3,5,6: #y] #EQ destruct
212| #opt_a #l #r #Hl #Hr * [2,3: #x| #v normalize cases opt_a normalize [2: #a %]
213  cases (map_opt ? ? ? l) normalize [2: //] cases (map_opt ? ? ? r) normalize
214  //] #v normalize cases opt_a [2,4: #a] normalize //
215  [ cases(map_opt ? ? ? l) normalize // >Hr cases(map_opt ? ? ? r) normalize
216    [2: #opt_b #lb #rb] inversion(pm_set B x ? ?) normalize // cases x [2,3,5,6: #y]
217    normalize #EQ destruct
218  | >Hl cases(map_opt ? ? ? l) normalize [2: #opt_b #lb #rb]
219    inversion (pm_set B x ? ?) normalize //
220    [1,2: cases x [2,3,5,6: #y] normalize #EQ destruct]
221    #opt_b' #lb' #rb' #_ normalize #_ #EQ cases(map_opt ? ? ? r)
222    normalize nodelta [%] #opt_b'' #lb'' #rb'' >EQ %
223]
224qed.
225
226lemma update_ok_to_lookup : ∀ A : Type[0].
227∀ tag : identifierTag.
228∀m,m' : identifier_map tag A. ∀id,a.
229update tag A m id a = return m' →
230(lookup tag A m' id = Some ? a) ∧ lookup tag A m id ≠ None ? ∧
231(∀ id'. id ≠ id' → (lookup tag A m id' = lookup tag A m' id')).
232#A #tag * #m * #m' * #id #a
233whd in ⊢ (??%% →  ?); inversion(update A ???) normalize nodelta [#_ #ABS destruct]
234    #m1 #m1_spec #EQ destruct % [%]
235    [  normalize @(update_lookup_opt_same … m1_spec)
236    |3: * #id' * #id_spec' normalize @(update_lookup_opt_other … m1_spec ??)
237        % #EQ @id_spec' >EQ %
238    | % normalize lapply m1_spec lapply id lapply m' -id -m' elim m
239      [#m' * [|*: #x] normalize #EQ destruct] #opt_a #l #r #Hl #Hr #m' * [|*: #x]
240      normalize [ cases opt_a [2:#a] normalize #EQ1 #EQ2 destruct]
241      inversion (update A x a ?) [1,3: #_ normalize #EQ destruct]
242      #pos_map #EQpos_map normalize #EQ destruct [@Hr|@Hl] assumption
243    ]
244qed.
245
246lemma update_def : ∀tag,A,m,i,v.
247  update tag A m i v =
248  match lookup tag A m i with
249  [ Some _ ⇒ OK ? (add tag A m i v)
250  | None ⇒ Error ? [MSG MissingId; CTX … i]
251  ].
252#tag #A #m #i #v inversion(update tag A m i v)
253[ #m' #EQm' cases(update_ok_to_lookup ?????? EQm') * #_
254 #H #_ elim H cases(lookup tag A m i) [#H @⊥ @H %]
255 #x #_ normalize <EQm' lapply EQm' cases i cases m cases m' -m -m' -i
256 normalize #m' #m #i inversion(update A i v m) normalize [#_ #ABS destruct]
257 #m'' #EQm'' #EQ destruct(EQ) @eq_f @eq_f lapply EQm'' -EQm'' lapply i -i
258 lapply m' -m' elim m [#m' * [2,3: #z] normalize #EQ destruct]
259 #opt_a #l #r #Hl #Hr #m' * [2,3: #z] normalize
260 [3: cases opt_a normalize [2: #y] #EQ destruct %
261 |*: inversion(update A z v ?) [2,4: #m'']  #EQm'' normalize #EQ destruct
262     [<(Hr … EQm'') | <(Hl … EQm'')] %
263 ]
264| #err cases m -m cases i -i #i #m normalize inversion(update A i v m) [2:#m']
265  #EQerr normalize #EQ destruct lapply EQerr lapply i elim m
266  [ normalize #x #_ %] #opt_a #l #r #Hl #Hr * [2,3:#z] normalize
267 [3: cases opt_a [2:#w] normalize #EQ destruct %
268 |*: inversion(update A z v ?) [2,4: #m'] #EQm' normalize #EQ destruct
269     [lapply(Hr … EQm') | lapply(Hl … EQm')] cases(lookup_opt A z ?) [2,4: #a]
270     normalize #EQ destruct %
271 ]
272]
273qed.
274
275lemma map_update_commute : ∀tag : identifierTag.∀A,B : Type[0].∀f : A → B. ∀m,id,v.
276update tag B (map tag A B m f) id (f v) =
277!m' ← update tag A m id v; return map tag A B m' f.
278#tag #A #B #f #m #id #v >update_def >update_def >lookup_map
279cases (lookup tag A m id) [%] #a >m_return_bind >m_return_bind normalize nodelta
280whd in ⊢ (???%); @eq_f @sym_eq @map_add
281qed.
282
283(*restriction for maps *)
284definition restrict : ∀tag.∀A,B.
285identifier_map tag A → identifier_map tag B → identifier_map tag A ≝
286λtag,A,B,m1,m2.an_id_map …
287           (merge A B A (λo,o'.match o' with [None ⇒ None ? | Some _ ⇒ o])
288                  (match m1 with [an_id_map p1 ⇒ p1])
289                  (match m2 with [an_id_map p2 ⇒ p2])).
290
291interpretation "identifier map restriction" 'intersects a b = (restrict ??? a b).
292
293unification hint 0 ≔ tag ; R ≟ identifier tag ⊢ list R ≡ list (identifier tag).
294 
295lemma lookup_restrict : ∀tag,A,B.∀a : identifier_map tag A.∀b : identifier_map tag B.
296∀i.lookup ?? (a ∩ b) i = if i ∈ b then lookup … a i else None ?.
297#tag #A #B * #a * #b * #i normalize >lookup_opt_merge [2: %] cases (lookup_opt B i b)
298[2: #b] normalize % qed.
299
300lemma update_fail_lookup : ∀tag,A,m,i,v,e.update tag A m i v = Error … e → 
301  e = [MSG MissingId; CTX … i] ∧ lookup … m i = None ?.
302#tag #A #m #i #v #errmsg >update_def cases(lookup tag A m i) [2: #a] normalize
303#EQ destruct % //
304qed.
305
306lemma lookup_miss_update : ∀tag,A,m,i,v.lookup tag A m i = None ? → 
307  update … m i v = Error … [MSG MissingId; CTX … i].
308#tag #A #m #i #v #EQ >update_def >EQ normalize %
309qed.
310
311lemma update_ok_old_lookup : ∀tag,A,m,i,v,m'.update tag A m i v = OK ? m' →
312  i ∈ m.
313#tag #A #m #i #v #m' >update_def inversion(lookup tag A m i) [2: #a] #EQ normalize
314#EQ destruct >EQ normalize @I
315qed.
316
317lemma lookup_update_ok : ∀tag,A,m,i,v,m',i'.update tag A m i v = OK ? m' →
318  lookup … m' i' = if eq_identifier ? i' i then Some ? v else lookup … m i'.
319#tag #A #m #i #v #m' #i' >update_def inversion(lookup tag A m i) [2: #a] #EQ
320normalize nodelta #EQ1 destruct @eq_identifier_elim
321[ #H normalize nodelta >H @lookup_add_hit
322| #H normalize nodelta @lookup_add_miss assumption
323]
324qed.
325
326include "utilities/extra_bool.ma".
327
328lemma mem_set_restrict : ∀tag,A,B.∀a : identifier_map tag A.∀b : identifier_map tag B.
329∀i.i ∈ a ∩ b = (i ∈ a ∧ i ∈ b).
330#tag #A #B * #a * #b  * #i normalize >lookup_opt_merge [2: %] cases(lookup_opt B i b)
331[2: #a1] normalize [2: @if_elim #_ %] cases(lookup_opt A i a) [2: #a2] normalize %
332qed.
333
334lemma lookup_set_minus : ∀tag,A,B. ∀a : identifier_map tag A. ∀b : identifier_map tag B.
335∀i. lookup ?? (a ∖ b) i = if i ∈ b then None ? else lookup … a i.
336#tag #A #B * #a * #b * #i normalize >lookup_opt_merge [2: %] cases(lookup_opt B i b)
337[2: #b] % qed.
338
339lemma lookup_hit_update : ∀tag,A,m,i,v.i ∈ m → 
340  ∃m'.update tag A m i v = OK ? m'.
341#tag #A #m #i #v #H % [2: >update_def lapply(in_map_domain … m i) >H * #v #EQ >EQ
342normalize %|]
343qed.
344
345lemma add_set_minus  : ∀tag,A,B.∀a : identifier_map tag A.∀b : identifier_map tag B.
346∀i,v.¬(i ∈ b) → add tag A (a ∖ b) i v = (add tag A a i v) ∖ b.
347#tag #A #B * #a * #b * #i #v @notb_elim @if_elim normalize [#_ *]
348@if_elim [2: #_ *] @if_elim [#_ *] inversion(lookup_opt B i b) normalize [2: #x #_ *]
349#H * * * * @eq_f lapply H -H lapply v -v lapply b -b lapply a -a elim i
350[  *
351  [ * [2: #opt_b #l #r] #v normalize in ⊢ (% → ?); #EQ destruct [2: %]
352  normalize in ⊢ (??%%); cases (map_opt ??? l) // normalize cases(map_opt ??? r)
353  normalize //
354  | * [2: #a] #l #r * [2,4: #opt_b #l1 #r1] #v normalize in ⊢ (% → ?); #EQ destruct
355    normalize [3: % |1,2: cases(merge ???? l l1) // cases(merge ???? r r1) //]
356    cases(map_opt ??? l) normalize // cases(map_opt ??? r) //
357  ]
358|2,3: #x #IH * [2,4: #opt_a #l #r] * [2,4,6,8: #opt_b #l1 #r1] #v
359      normalize in ⊢ (% → ?); #H whd in match (pm_set ????) in ⊢ (???%);
360      whd in match (merge ??????) in ⊢ (???%);
361      [1,2,3,4: <IH try assumption whd in match (pm_set ????) in ⊢ (??%?);
362                whd in match (merge ??????) in ⊢ (??%?); cases opt_b normalize
363                [2,4,6,8: #b] [5,6: cases opt_a normalize //]
364                [1,2,3,4: cases (merge ???? l l1) normalize [2,4,6,8: #opt_a2 #l2 #r2]
365                          // cases (merge ???? r r1) normalize
366                          [2,4,6,8,10,12: #opt_a3 #l3 #r3] inversion(pm_set ????)
367                          normalize // cases x
368                          [2,3,5,6,8,9,11,12,14,15,17,18,20,21,23,24 : #y]
369                          normalize #EQ destruct
370                |*: cases(map_opt ??? l1) normalize [2,4,6,8: #opt_a2 #l2 #r2] //
371                    cases(map_opt ??? r1) normalize [2,4,6,8,10,12: #opt_a3 #l3 #r3]
372                    inversion(pm_set ????) normalize // cases x
373                    [2,3,5,6,8,9,11,12,14,15,17,18,20,21,23,24 : #y]
374                    normalize #EQ destruct
375                ]
376     |*: whd in match (pm_set ????) in ⊢ (??%?);
377         whd in match (merge ??????) in ⊢ (??%?); [1,2: cases opt_a [2,4: #a]]
378         normalize
379         [1,2: @eq_f2 [1,4:%] | cases(map_opt ??? l) [2: #opt_a1 #l1 #r1] normalize
380         | cases(map_opt ??? r) [2: #opt_a1 #l1 #r1] normalize]       
381         [1,3,4: lapply(map_add tag A A (λx.x) (an_id_map … r) (an_identifier ? x) v)
382         |2,5,6: lapply(map_add tag A A (λx.x) (an_id_map … l) (an_identifier ? x) v)
383         |*: lapply(map_add tag A A (λx.x) (an_id_map … (pm_leaf ?)) (an_identifier ? x) v)
384         ] normalize #EQ destruct >e0 try % [4,5: cases x [2,3,5,6: #y] normalize %]
385           cases(map_opt ????) [2,4,6: #opt_a1 #l1 #r1] normalize
386           inversion(pm_set ????) normalize // cases x [2,3,5,6,8,9,11,12: #y]
387           normalize #EQ1 destruct
388     ]
389]
390qed.     
391
392lemma update_set_minus : ∀tag,A,B.∀a : identifier_map tag A.∀b : identifier_map tag B.
393∀i,v.¬(i ∈ b) → update ?? (a ∖ b) i v =
394  ! a' ← update ?? a i v ; return a' ∖ b.
395#tag #A #B #a #b #id #v #H >update_def >lookup_set_minus @if_elim
396[ #H1 @⊥ lapply H1 lapply H @notb_elim >H1 normalize *] #_ >update_def
397cases (lookup tag A a id) normalize [ %] #a @eq_f @add_set_minus assumption
398qed.
399
400
401lemma add_idempotent : ∀tag,A.∀m : identifier_map tag A. ∀i,a1,a2.
402add tag A (add tag A m i a1) i a2 = add tag A m i a2.
403#tag #A * #m * #i #a1 #a2 normalize @eq_f lapply a1 -a1 lapply a2 -a2 lapply m -m
404elim i
405[ * [ #a1 #a2 %] #opt_a #l #r #a1 #a2 %] #x #IH *
406[1,3: #a1 #a2 normalize @eq_f2 try % @IH] #opt_a #l1 #l2 #a1 #a2 normalize
407@eq_f2 try % @IH
408qed.
409
410
411lemma empty_set_minus : ∀tag,A,B.∀m : identifier_map tag B. empty_map tag A =
412empty_map tag A ∖ m.
413#tag #A #B * #m normalize @eq_f elim m [%] #opt_b #l #r #IHl #IHr normalize
414cases opt_b normalize [2: #b] <IHl <IHr %
415qed.
416
417lemma map_opt_none : ∀A,B.∀m : positive_map A.
418      map_opt A B (λx.None ?) m = pm_leaf B.
419#A #B #m elim m [%] #opt_a #l #r #EQ1 #EQ2 cases opt_a [2: #a] normalize
420>EQ1 >EQ2 %
421qed.
422
423lemma set_minus_add :∀tag,A,B.∀a:identifier_map tag A.∀b:identifier_map tag B.
424           ∀i,v.i∈b→ (add tag A a i v)∖b = a ∖ b.
425#tag #A #B * #a * #b * #i #v normalize inversion(lookup_opt B i b) [ #_ *]
426#v1 #EQv1 #_ @eq_f lapply EQv1 -EQv1 lapply v1 -v1 lapply v -v lapply b -b
427lapply i -i elim a
428[ #i elim i [ * [2: #opt_v #l #r] #v1 #v2 normalize #EQb destruct(EQb) %]
429#i1 #IH * [2,4: #opt_v #l #r] #v1 #v2 normalize [3,4: #ABS destruct(ABS)]
430cases opt_v [2,4: #v'] normalize nodelta #EQb >(IH … EQb) >map_opt_none %
431| #opt_v #l #r #IHl #IHr #i * [#v1 #v2 normalize #EQ destruct] #opt_v1 #l1 #r1
432  #c1 #c2 normalize cases i [2,3: #x] normalize [3: #EQ destruct] normalize nodelta
433[ %] #EQc2 cases opt_v [2,4: #c3] normalize cases opt_v1 [2,4,6,8: #c4] normalize
434[1,3,4,5,7: >(IHr … EQc2) inversion(merge A B A ? l l1) //
435            [2: #opt_v4 #l4 #r4 #_ #_] #EQ <EQ >(IHl … EQc2) //
436|*: >(IHl … EQc2) //
437]
438qed.
439           
440
Note: See TracBrowser for help on using the repository browser.